NatMap

This structure defines the specialization of the general data type of mappings from a domain to a codomain for the fixed domain of natural numbers.

Signature of NatMap

List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Pair
See Seq
See Set

SIGNATURE NatMap[codom: SORT]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

IMPORT Nat              ONLY nat <
       Option[codom]    ONLY option
       Set[nat,<]       ONLY set
       Seq[nat]         ONLY seq
       Seq[codom]       ONLY seq
       Pair[nat, codom] ONLY pair
       Option[pair]     ONLY option

Parameter

nat is the type of the domain, codom the type of the codomain.

SORT codom

The Type Itself

SORT natMap

Nonfree Constructors

The empty natMap.

FUN {}          : natMap   

(Re)define natMap at point.

FUN def         : nat ** codom ** natMap -> natMap

Constructing a Map From Datas

(Re)define resp. undefine natMap at point.

FUN def         : nat ** codom ** natMap -> natMap
    undef       : nat ** natMap -> natMap

In upd (d, f, m), redefine m at d by f(m!d)

FUN upd         : nat ** (codom -> codom) ** natMap -> natMap 

Best explained informally: extend (M, <d1, ..., dn>, <c1, ..., cn>) results def(...def(M,d1,c1)...,dn,cn).

FUN extend      : natMap ** seq[nat] ** seq[codom]->natMap

Constructing a Map From a Function

(n1 .. n2)(g) == {n1 -> g(n1), ... , n2 -> gn(2)}

FUN ..          : nat ** nat -> (nat -> codom) -> natMap

Generate elements of the domain from start upto (excluding) the first element, for which P(it^x(start)) does not hold. The function f assigns to each element of the domain the associated codom element.

FUN iter        : nat ** (nat -> nat) ** (nat -> bool) -> (nat -> codom) -> natMap

Add for every element d of the set the maplet d -> f(d) to the natMap

FUN init        : set[nat, <] ** (nat -> codom) -> natMap

Combining Maps

Lifting of def to natMaps. Informally, M <+ {d1->c1,...,dn -> cn = def(...def(M,d1,c1)...,dn,cn)}

FUN <+          : natMap ** natMap -> natMap                     

Lifting of undef to sets. Informally, M <- {d1,...,dn = undef(...undef(M,d1)...,dn)}.

FUN <-          : natMap ** set[nat,<] -> natMap

Accessing Codom - Elements

m!d: give associated value to d in m which must exist

FUN !           : natMap ** nat -> codom           

m ?! d: give associated value to d in m, if it exists, else nil

FUN !?          : natMap ** nat -> option[codom]

Information About a Map

test for empty natMap

FUN {}?         : natMap -> bool

test for definedness

FUN def?        : nat ** natMap -> bool

domain of the natMap. Informally, dom ( {d1->c1,...,dn -> cn ) = {d1, ..., dn}}

FUN dom         : natMap -> set[nat,<]   

Codomain of the natMap. Note that this is a sequence and not a set!

FUN codom       : natMap -> seq[codom]

return some nat not element of the domain

FUN new         : natMap -> nat

cardinality of dom(m)

FUN #           : natMap -> nat                    

exist?(P, M): is there d in dom(M) with P(d, M!d) ?

FUN exist?      : (nat ** codom -> bool) ** natMap -> bool

find?(P, M): return avail(c, d) for some c->d in M for which P holds

FUN find?       : (nat ** codom -> bool) ** natMap -> option[pair]

forall?(P, M): does P hold for every (d, r) in M ?

FUN forall?     : (nat ** codom -> bool) ** natMap -> bool

not for user purpose

see structure NatMapNotForUSerPurpose

next node: NatMapNotForUserPurpose,
prev node: Subsystem Mapping Natural Numbers,
up to node: Subsystem Mapping Natural Numbers