MapByBSTReduce

Reducing the codomain of maps

Signature of MapByBSTReduce

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

SIGNATURE MapByBSTReduce[dom, <, codom, to]

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

IMPORT MapByBST[dom,<,codom] ONLY map

Parameter

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

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

Reducing Maps

(o, e) / m: reduce m by o on codom with value e as initial 2nd argument. Function f should be left-commutative: x o (y o z) = y o (x o z), since reduction order is implementation dependent and should not be relevant! Informally, (o, e)/({(d1->c1),(d2->c2),...,(dn->cn)) = c1 o (c2 o (...(cn o e)...))}

FUN / : (codom ** to -> to) ** to ** map[dom,<,codom] -> to             

(o, e) / m: reduce m by o on codom with value e as initial 2nd argument. Function f should be left-commutative: (d1,c1) o ((d2,c2) o z) = (d2,c2) o ((d1,c1) o z), since reduction order is implementation dependent and should not be relevant! Informally, (o, e)/({(d1->c1),(d2->c2),...,(dn->cn)) == (d1,c1) o ((d2,c2) o (...((dn,cn) o e)...))}

FUN / : (dom ** codom ** to -> to) ** to ** map[dom,<,codom] -> to

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