Maude-help mailing list

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

There is no such execution mechanism at the object level. If you want to write your own execution mechanism at the metalevel you can give rules the nonexec attribute; then Maude will not try to execute them, or complain about variables being used before they are bound; it will be your responsibility to pass a suitable binding via the Substitution argument to the metaApply() or metaXapply() descent functions.

Steven

On 4/9/13 11:36 PM, Robert Colvin wrote: Hi,

Is there some way of defining rewrite rules with free variables that do
not appear in the LHS of the rule?  Having read the META* modules, and
the parts on unification and narrowing, it seems to me this may be
possible, but if so I can't figure out how to do it.  I would like to
leave a variable uninstantiated in a rule with the intention that
another rule may instantiate it appropriately, similarly to unification
in logic programming.

Following Verdejo and Mart-Oliet's guidelines for giving SOS rules in
Maude, I would like rules such as:

    rl [var] : X => {X = V} V .

    crl [state] : state(X == V, E) => {tau} state(X == V, E')
        if E => {X = V} E' .

The intention is to generate evaluations like
    rew state(y == 1, y)   =   {tau} state(y == 1, 1)
but other evaluation with values other than 1 replacing y are
implicitly prevented in rule state by the matching of V in state(..) on
the LHS with V in the label on the RHS.

Unfortunately rule var is not accepted since V is not ground in the LHS
of the rule.  ["..variable V is used before it is bound in rule:..."]

Is there some way of flagging V in the first rule to be a meta-variable
which is (potentially) instantiated later (implicitly by the second
rule)?  Or some other abstract technique?

I am currently working around the problem using a ground placeholder
instead of V in rule var and doing term replacement in rule state, but
this approach is somewhat limited and obviously places a gap between the
written semantics and its implementation in Maude.

I can provide more context and the code if required.

Thanks,
Rob

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