MapByBST

This structure defines the data type of mappings from a domain to a codomain.

This implementation is based on balanced search trees, which gives good performance an single element operations such as def, undef and ! (select), but not on operations on whole maps, such as <+. Use this family of structures, if you absolutely want to rely on this implementation; otherwise you are advised to use the standard implementation of maps.

Signature of MapByBST

List of Import References :
See BOOL
See BSTree
See DENOTATION
See Nat
See Option
See Pair
See Seq
See SetByBST
See Tree

SIGNATURE MapByBST [dom:SORT,< : dom ** dom -> bool,codom: SORT]

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

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

Parameter

dom is the type of the domain, codom the type of the codomain. < is a total strict order: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold.

SORT dom codom
FUN <   : dom ** dom -> bool

The Type Itself

SORT map

Nonfree Constructors

The empty map.

FUN {}          : map   

(Re)define map at point.

FUN def         : dom ** codom ** map -> map

Constructing a Map From Datas

(Re)define resp. undefine map at point.

FUN def         : dom ** codom ** map -> map
    undef       : dom ** map -> map

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

FUN upd         : dom ** (codom -> codom) ** map -> map 

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

FUN extend      : map ** seq[dom] ** seq[codom]->map

Constructing a Map From a Function

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

FUN ..          : nat ** nat -> (nat -> dom) ** (dom -> codom) -> map

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        : dom ** (dom -> dom) ** (dom -> bool) -> (dom -> codom) -> map

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

FUN init        : set[dom, <] ** (dom -> codom) -> map

Combining Maps

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

FUN <+          : map ** map -> map                     

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

FUN <-          : map ** set[dom,<] -> map

Accessing Codom - Elements

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

FUN !           : map ** dom -> codom           

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

FUN !?          : map ** dom -> option[codom]

Information About a Map

test for empty map

FUN {}?         : map -> bool

test for definedness

FUN def?        : dom ** map -> bool

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

FUN dom         : map -> set[dom,<]     

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

FUN codom       : map -> seq[codom]

cardinality of dom(m)

FUN #           : map -> nat                    

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

FUN exist?      : (dom ** codom -> bool) ** map -> bool

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

FUN find?       : (dom ** codom -> bool) ** map -> option[pair]

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

FUN forall?     : (dom ** codom -> bool) ** map -> bool

not for user purpose

IMPORT Pair[dom, codom] ONLY pair
       SetByBST[pair[dom, codom], less] ONLY set

FUN less : pair ** pair -> bool
FUN abs: set[pair, less] -> map
FUN rep: map -> set[pair, less]

next node: MapByBSTConv,
prev node: Subsystem Maps By Binary Search Trees,
up to node: Subsystem Maps By Binary Search Trees