Maude-help mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

I'm trying to make a widened version of a reduction relation I have that does 
several reductions as one step.
1) I don't see any way in the syntax to capture all the states that something 
could reduce to.
2) What is the proper way to iterate over a finite set? Order doesn't matter, 
but I want to commit to a single order to avoid an explosion.

The gist is I have a nondeterministic semantics in CESK machine style < c, e, 
s, k > that gets injected into a deterministic semantics that has a set of 
seen states, a set of states to do (without an s component) and a shared s 
component. A single step in this machine will associate the s component with 
every state in the todo set, use the CESK semantics to step them all (to all 
their possibilities), get the least upper bound of all their s components 
(s'), add the resulting states with s' to the seen set, and make the new todo 
set the states that weren't already seen.

I can write the LUB and other functions just fine, but the "all 
possibilities" part along with a chosen order to recur over a set are eluding 
me in this language. Is this possible?

-Ian