1.
Flat
Generics|
Basics|
Specifics
1.1.
Generics
Introduces: item .
open.
1.2. Basics
Introduces: flat-list, list of _ .
Needs: Tuples/Basics. item <= component .
- flat-list = list of item* .
- list of _ ::item* -> flat-list (total, injective) .
(1) item & flat-list = nothing .
closed except Generics .
1.3. Specifics
Introduces: _[ _ ] , items_ , head_ , tail_ , empty-list , concatenation_ .
Includes: Instant/Distinction ( list for s , _is_ ) .
Needs: Tuples . flat-list <= component .
- _[ _ ] :: flat-list, item -> flat-list .
- items_ :: flat-list -> item* (total, injective) .
- head_ :: flat-list -> item (partial) .
- tail_:: flat-list -> flat-list (partial) .
- empty-list : flat-list .
- concatenation_
:: flat-list* ->
flat-list (total, associative, unit
is empty-list).
Needs: Numbers/Naturals .
(1) (l <= flat-list) [i <= item ] = l & list of i* .
(2) l = list of i => items l:flat-list = i .
(3) head of l:flat-list = component#1 items l .
(4) tail of l:flat-list = list of components from #2 items l .
(5) empty-list = list of ( ) .
(6) concatenation (l1:flat-list, l2:flat-list) = list of (items
l1, items l2).
(7) l1:flat-list is l2:flat-list = items
l1 is items l2 .
2. Nested
2.1. Generics
Introduces: leaf .
open.
2.2. Basics
Introduces: list ,tree .
Needs: Tuples/Basics . tree <= component .
- list = list of tree* .
- tree = leaf | list (disjoint) .
- list of_ :: tree* -> list (total, injective) .
closed except Generics.
2.3. Specifics
Introduces: _ [ _ ], branches_, leaves_, head _, tail _ , empty-list, concatenation_ .
Includes: Instant/Distinction (
tree for s , _is_ ) .
Needs: Tuples .
- _ [ _ ] :: list, tree -> list .
- branches_ :: list -> tree* (total, injective) .
- leaves_ :: tree* -> leaf* (total) .
- head_ :: list -> tree (partial) .
- tail_ :: list -> list (partial) .
- empty-list : list .
- concatenation_ :: list* -> list (total, associative, unit is empty-list) .
Needs: Numbers/Naturals .
(1) (l <= list) [ t <= tree ] = l&list of t* .
(2) branches list of t:tree* = t .
(3) leaves l:leaf = l ; leaves list of t:tree* = leaves
t .
leaves ( ) = ( ) ; leaves (t1:tree*,
t2:tree*) =
(leaves t1, leaves t2) .
(4) head l:list = component#1 branches l .
(5) tail l:list = list of components from #2 branches l .
(6) empty-list = list of ( ) .
(7) concatenation (l1:list, l2:list) = list of (branches
l1, branches l2) .
(8) l1:list is l2:list = branches l1 is branches
l2 ; x:leaf is l:list = false .
|