Maps

Generics|Basics|Specifics
1. Generics
Introduces: nonmap-range .
open.
2. Basics
Introduces: map , range , map of _ to _ , empty-map , disjoint-union _ , mapped-set _ .
Needs: Tuples/Basics . map <= component .
  • map = disjoint-union (map of element to range)* .
  • range = nonmap-range | map (disjoint) .
  • map of _ to _ :: element, range -> map (total, injective) .
  • empty-map : map .
  • disjoint-union _ :: map* -> map (partial, associative, commutative, unit is empty-map) .
  • mapped-set _ :: map -> set (total) .
(1) disjoint-union ( ) = empty-map ; disjoint-union (map of e:element to r:range) = map of e:element to r:range . intersection (mapped-set m1, mapped-set m2) is empty-set = true => disjoint-union (m1:map, m2:map) : map . intersection (mapped-set m1, mapped-set m2) is empty-set = false => disjoint-union (m1:map, m2:map) = nothing .
(2) mapped-set empty-map = empty-set ; mapped-set map of e:element to r:range = set of e ; mapped-set disjoint-union (m1:map, m2:map) = disjoint-union (mapped-set m1, mapped-set m2) .
closed except Generics.

3. Specifics
Introduces: _ [ _to_ ] , _at_ , overlay_ , _restricted to_ , _omitting_ .
Includes: Instant/Distinction ( map for s , _ is _ ) . Needs: Tuples/Basics .
  • _ [ _to_ ] :: map, element, range -> map .
  • _at_ :: map, element -> range (partial) .
  • overlay _ :: map* -> map (total, associative, idempotent, unit is empty-map).
  • _restricted to_ :: map, set -> map (total).
  • _omitting_ :: map, set -> map (total) .
(1) (m <= map) [e <= element to r <= range] = m & disjoint-union (map of e to r)*.
(2) empty-map at e:element = nothing ; map of e':element to r:range at e:element = when e is e' then r disjoint-union (m:map, m':map) at e:element = when there is disjoint-union (m, m') then ((m at e)|(m' at e)) .
(3) overlay (m:map, m':map) = disjoint-union (m, m' omitting mapped-set m) .
(4) empty-map restricted to s:set = empty-map ; map of e:element to r:range restricted to s:set = if e is in s then map of e to r else empty-map ; disjoint-union (m:map, m':map) restricted to s:set = when there is disjoint-union (m, m') then disjoint-union (m restricted to s, m' restricted to s) .
(5) empty-map omitting s:set = empty-map ; map of e:element to r:range omitting s:set = if e is in s then empty-map else map of e to r ; disjoint-union (m:map, m':map) omitting s:set = when there is disjoint-union (m, m') then disjoint-union (m omitting s, m' omitting s) .
(6) empty-map is m:disjoint-union (map of element to range)+ = false ; map of e1:element to r1
:range is map of e2:element to r2:range = if e1 is e2 then r1 is r2 else false ; disjoint-union (map of e:element to r:range, m:map) is m':map = when not (e is in mapped-set m) then if not (e is in mapped set m') then false else both ((r is (m' at e)), (m is (m' omitting set of e))) .

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