NatMapReduce

Reducing the codomain of natmaps

Signature of NatMapReduce

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

SIGNATURE NatMapReduce[codom, to]

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

IMPORT NatMap[codom] ONLY natMap
       Nat ONLY nat

Parameter

codom the type of the codomain; to is the result type of the reduce.

SORT codom to

Reducing NatMaps

(o, e) / nm: reduce nm 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 ** natMap[codom] -> to                

(o, e) / nm: reduce nm 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 / : (nat ** codom ** to -> to) ** to ** natMap[codom] -> to

next node: NatMaps,
prev node: NatMapMap,
up to node: Subsystem Mapping Natural Numbers