[Maude-help] Priorities between rules
eker at csl.sri.com
Wed Sep 27 17:08:39 CDT 2006
Rewriting with priorities is a tricky issue due to confluence. Maude's owise
feature is explained by a somewhat cumbersome theory transformation to a TRS
Rules on the other hand represent change of state and need not be terminating
or confluent. However the rewrite command does not support priorities and you
should not rely on it using any particular ordering on the rules. What you
really want is a strategy for applying rules. At the moment this must be done
by the user from the metalevel but in the next release (around the end of
this year) there will be a built-in strategy language and you will be able to
write commands like:
srew t using (r1 or-else r2 or-else r3)* .
Your example problem might be fixed by a hack using the sort test operator:
subsort U < T < S .
crl [NameS] : Name s => "sort-s" if not(s :: T) .
crl [NameT] : Name t = > "sort-t" if not (t :: U) .
crl [NameU] : Name u = > "sort-u" .
Of course this becomes tricky if your sort structure is non-linear.
On Wednesday 13 September 2006 01:55, Marc Boyer wrote:
> Dear all,
> I would like to have priorities between rules.
> The motivation is some calculation of upper bound,
> with some basic rules and some better one.
> A minimal running example is the following:
> mod RULE-PREC is
> protecting STRING .
> sorts S T .
> subsort T < S .
> var s : S .
> var t : T .
> op Name _ : S -> String .
> op doS : -> S .
> op doT : -> T .
> *** Equational version
> *** eq [NameS] : Name s = "sort-s" .
> *** eq [NameT] : Name t = "sort-t" .
> *** Rule version
> rl [NameS] : Name s => "sort-s" .
> rl [NameT] : Name t => "sort-t" .
> rew Name doS .
> rew Name doT .
> I would like 'Name doS' to become "sort-s" and 'name doT'
> to become "sort-t". But the code, as given there,
> rewrite 'Name doT' in "sort-s", which is true, but not
> the more accurate.
> I have found two hacks, but I was wondering if there i a better way.
> a) Changing rule orders
> If I change the order of rule [NameS] and [NameT] in the source
> file, it works. But, in my real problem, S and T are in different
> b) Using equations and the [owise] attribute
> I can use equations instead of rules, and set the [owise]
> attribute to equation [NameS]. It works (that is what I am using),
> but it is not scalable: with a sort U, subsort of T, it fails.
> Is there any other (and better) way ?
> Marc Boyer
More information about the Maude-help