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 = ( ) .
|