Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

If you want a guaranteed traversal order when pulling elements out of a 
container, you need to use a LIST (or LIST* for Lisp-style nestable 
lists) and pull elements from one end.

fmod TEST is
  pr LIST{Nat} .

  var N : Nat .
  var L : List{Nat} .

  op squares : List{Nat} -> List{Nat} .
  eq squares(N L) = (N * N) squares(L) .
  eq squares(nil) = nil .
endfm

red squares(9 1 8 2 7 3 6 4 5) .

Steven


On 5/31/13 8:40 AM, J. Ian Johnson wrote:
> 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
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help