SIGNATURE MapByOSReduce[dom, <, codom, to]

-- reducing the codomain of maps

-- Parameter
SORT dom codom to
FUN <   : dom ** dom -> bool
        -- total strict-order; in 
        --   ~(x < y) AND ~(y < x) => x = y
        -- should = represent semantic equality

IMPORT MapByOS[dom,<,codom] ONLY map

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: 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 / : (dom ** 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 o should be left-commutative: (d1,c1) o ((d2,c2) o z) 
        -- 					   = (d2,c2) o ((d1,c1) o z)
        -- 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)...))

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

-- (o, e) / m == (o/e)(m)