SIGNATURE BagReduce [from,<,to]

-- reductions of bags

IMPORT Bag[from,<] ONLY bag
       Nat         ONLY nat

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 ** bag -> to
        -- (o , e) / b
        -- reduce b by o with value e as initial 2nd argument
        -- function o 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,a,b,...,y,z}) == a o (a o (b o (...(y o (z o e))...)))

FUN / : (from ** nat ** to -> to) ** to ** bag -> to    
        -- (o, e) / b
        -- reduce b by o under consideration of occurences
        -- with value e as initial 2nd argument
        -- function o 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,a,b,...,z,z,z}) == (a,2) o ((b,1) o (...((z,3) o e)...))

-- old fashioned
FUN / : (from ** to -> to) ** to -> bag -> to           
FUN / : (from ** nat ** to -> to) ** to -> bag -> to    

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