SIGNATURE SetFold[data,< :data ** data -> bool]

-- folding of sets

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

IMPORT  Set[data, <] ONLY set

FUN / : (data ** data -> data) ** set -> data
    -- folding of sets
    -- 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
    -- + / {e0, e1, ..., en} == e0 + (e1 + ( ... + en) ... )
    -- undefined for empty sets