MapCompose

Composing Maps

Signature of MapCompose

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

SIGNATURE MapCompose[dom, < : dom ** dom -> bool, 

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

                     interdom, < : interdom ** interdom -> bool, 
                     codom]

IMPORT Map[dom, <, interdom] ONLY map
       Map[interdom, <, codom] ONLY map
       Map[dom, <, codom] ONLY map

Parameter

The first map maps elements from dom to interdom, the second maps from interdom to codom. The resulting map finally maps elements from dom to codom.

The < are total strict orders: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold.

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

Composing Maps

M1 o M2 = {(d -> r) | EX m. M1!d = m and M2!m = r}

FUN o : map[dom, <, interdom] ** map[interdom, <, codom] -> 
                    map[dom, <, codom]

next node: MapInvert,
prev node: MapReduce,
up to node: Subsystem Maps Proper