[Maude-help] Priorities between rules

[Steven Eker]

Hi Marc,

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 
without owise.

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.

Regards,
Steven Eker

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" .
> endm
>
> 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
> modules.
>
> 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