Maude-help mailing list

[Robert Colvin <r.colvin AT uq.edu.au>]

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