Maude-help mailing list

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

Thanks for your help with this. Going back to the first question, on how to 
get all the one-step reducts of a given term, I've found the machinery I need 
(metaSearch), but there isn't enough documentation on how to use it. I can 
use search correctly to get what I want - depth bound 1, solution number 
unbounded, by
search [,1] in CESK : [some-ambiguous-term] =>+ s:State .

I get the two reducts I expect in my example (elided).

But using metaSearch, the result sort doesn't allow for more than one reduct, 
so I'm really confused. I run

rewrite in CESK : metaSearch(upModule('CESK, false),
           upTerm([some-ambiguous-term]),
           'ς1:State, nil, '+, 1, 0) .

and expect to see the two reducts I get from normal search, but I only get 
the first one in a ResultTriple. The final "solution number" argument doesn't 
make a lot of sense to me. 0 and 1 work to give me the one solution, but 2 
leads to a failure and unbounded doesn't even reduce.

After I cross that hurdle, I still need to figure out how to consume a search 
result to get a set of states in the non-meta world. I assume I'll need to 
perform the substitution and use downTerm on something, but it's just not 
that clear from the docs how to use them here. In grepping through the 
manual, there only looks to be one function that might even consume a 
substitution metaSearch would produce, and that's metaXapply, but I don't 
want to perform a reduction rule on the result; I just want to get the 
resulting term.

Thanks,
-Ian
----- Original Message -----
From: "Steven Eker" 
<eker AT csl.sri.com>
To: 
maude-help AT cs.uiuc.edu
Sent: Friday, May 31, 2013 2:53:38 PM GMT -05:00 US/Canada Eastern
Subject: Re: [Maude-help] Step all states in a set as a function.

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

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help