Tuples

Generics | Basics | Specifics

introduces:	component .
component = ž.
open.

 Back to the beginning.

2. Basics

includes:	tuple , ( ) , ( _ , _ ), _^? , _^* , _⁺ , _^- .

The symbol `( _ , _ )' may be used as an infix `_ , _', omitting the parentheses, when this does not cause ambiguity. In particular, `(x, y, z)' is a legal way of writing `((x, y), z)'.

tuple >= component .
( ) : tuple .
( _ , _ ) :: (tuple, tuple -> tuple (total, associative, unit is ( )) .
_^?  ::  tuple -> tuple .
_^*  :: tuple -> tuple .
_⁺  :: tuple -> tuple .
_^-  :: tuple, natural -> tuple .
(1) x^? = ( ) | x ; 
       x^* = ( ) | x⁺ ; 
       x⁺ = x | (x⁺, x⁺) ; 
       x⁰ = ( ) ; x^{successor n:natural} = (x, xⁿ) .
(2) component^* = ( )  
        component | (component⁺, component⁺) (disjoint) .

closed except Generics .

 Back to the beginning.

3. Specifics

introduces: 	count _ , first _ , rest _ , reverse _ , rotate _ _ , shuffle _ ,
			component#_ _ , components from #_ _ , components from #_ to #_ _ ,
			equal _ , distinct _ , strictly-increasing _ , strictly-decreasing _ . 

includes:	Instant/Distinction ( tuple for s, _ is _ ) .

includes:	Instant/Partial Order ( component for s , _ is _ , _ is less than _ ) .
count _ 	:: tuple -> natural (total) . 
first _ 	:: tuple -> component (partial) .
rest _ 		:: tuple -> tuple (partial) .
reverse _ 	:: tuple -> tuple (total, injective) .
rotate _ _ 	:: natural, tuple -> tuple (total) .
shuffle _ 	:: tuple -> tuple (strict, linear) .

rotate n t shifts the tuple t left n times, putting the first component at the end each time. shuffle t is the sort union of all the individual permutations of the tuple t.

(1) count ( ) = 0 ; count (c:component) = 1 ;
        count (t₁:tuple, t₂:tuple) = sum (count t₁, count t₂) .
(2) first ( ) = nothing ; first (c:component, t:tuple) = c .
(3) rest ( ) = nothing ; rest (c:component, t:tuple) = t .
(4) reverse ( ) = ( ) ; reverse c:component = c ; 
        reverse (t₁:tuple, t₂:tuple) = (reverse t₂, reverse t₁) .
(5) rotate 0 (t:tuple) = t ; rotate (n:natural) ( ) = ( ) ; 
        rotate (n:natural) (c:component) = c ;
        rotate (successor (n:natural)) (c:component, t:tuple) = rotate n (t, c) .
(6) shuffle ( ) = ( ) ; shuffle c:component = c ;
        shuffle (c:component, t:tuple) = 
		rotate (natural [max count t]) (c, shuffle t) .
equal _	:: (component⁺, component⁺) -> truth-value (partial, commutative) . 
distinct _ 	:: (component⁺, component⁺) -> truth-value (partial, commutative) . 
strictly-increasing _ :: (component⁺, component⁺) -> truth-value (partial) . 
strictly-decreasing _ :: (component⁺, component⁺) -> truth-value (partial) . 
_ is _ 	:: tuple, tuple -> truth-value (partial) .
(7) equal (x:component, y:component) = x is y ;
        equal (x:component⁺, y:component, z:component⁺) = 
		both (equal (x, y), equal (y, z)) .
(8) distinct (x:component, y:component) = not (x is y) ;
        distinct (x:component⁺, y:component, z:component⁺) = 
		all (distinct (x, y), distinct (x, z), distinct (y, z)) .
(9) strictly-increasing (x:component, y:component) = x is less than y;
(10)strictly-increasing (x:component⁺, y:component, z:component⁺) =
           	both (strictly-increasing (x, y), strictly-increasing (y, z)) .
(11)strictly-decreasing (x:component, y:component) = x is greater than y ;
        strictly-decreasing (x:component⁺, y:component, z:component⁺) =
	   	both (strictly-decreasing (x, y), strictly-decreasing (y, z)) .
(12)( ) is t:component⁺ = false ;
        (c₁:component, t₁:tuple) is (c₂:component, t₂:tuple) = 
	   	both (c₁ is c₂, t₁ is t₂) .
component#_ _ :: positive-integer, tuple -> component (partial) .
components from #_ _ :: positive-integer, tuple -> tuple (partial) .
components from #_ to #_ _ :: positive-integer, positive-integer, tuple -> tuple (partial) .
(13)component#i:positive-integer ( ) = nothing ;
        component#1 (c:component, t:tuple) = c ;
        component#successor i:positive-integer (c:component, t:tuple) = 
	   	component#i t .
(14)components from #i:positive-integer ( ) = nothing ;
        components from #1 t:tuple = t ;
        components from #successor i:positive-integer (c:component, t:tuple) = 
	   	components from #i t .
(15)  components from #i:positive-integer to #j:positive-integer ( ) = nothing ;
        components from #1 to #1 t:tuple = component#1 t ;
        components from #1 to #successor j:positive-integer (c:component, t:tuple) =
		(c, components from #1 to #j t) ;
        components from #successor i:positive-integer to #successor j:positive-integer 
           	(c:component, t:tuple) = components from #i to #j t ;
        components from #successor i:positive-integer to #1 t = ( ) .  

 Back to the beginning.