SIGNATURE SetReduce [from,<,to]

-- reductions of sets 

IMPORT Set[from,<] ONLY set

SORT from to

FUN < : from ** from -> bool
        -- total strict-order; in 
        --   ~(x < y) AND ~(y < x) => x = y
        -- should = represent semantic equality

FUN / : (from ** to -> to) ** to ** set[from,<] -> to
        -- (o, e)/ s
        -- reduce s by o 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)({a,b,...,y,z}) == a o (b o (...(y o (z o e))...))

-- old fashioned
FUN / : (from ** to -> to) ** to -> set[from,<] -> to
        --  (o / e)(s) === (o, e) / s