Tuples

Generics| Basics| Specifics


  1. Generics
  Introduces: component .   component = ž.
  open.
   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+) ; x0 = ( ) ; xsuccessor n:natural = (x, xn) .
   (2) component* = ( ) component | (component+, component+) (disjoint) .
closed except Generics .
   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 (t1:tuple, t2:tuple) = sum (count t1, count t2).
    (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 (t1:tuple, t2:tuple) = (reverse t2, reverse t1).
    (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 ; (c1:component, t1:tuple) is (c2:component, t2:tuple) = both (c1 is c2, t1 is t2) .
  • 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 = ( ) .




   
Data Notation Summary | Instant| Truth-Values | Numbers | Lists | Strings | Sets | Maps