Lists

Flat | Nested
    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
Generics| Basics| Specifics

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 .



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