Maude-help mailing list

[Francisco Durán <narudocap AT gmail.com>]

Hi Ozan,

There is no way to enforce such a form of rewriting in Maude. 

Perhaps you can look on how to directly restrict it programmatically. By your 
"maximum depth" I understand on operators whose arguments are constructor 
terms. If so, I suppose that if your spec is sufficiently complete, you can 
either go to the metalevel (to look for ctor attributes, although paying a 
high price in efficiency) or add checking ops. Perhaps something like...

mod FOO is 
  sort Foo .
  op a : -> Foo [ctor] .
  ops f g : Foo -> Foo .
  op ctor : Foo ~> Bool .
  eq ctor(a) = true .
  var X : Foo .
  crl f(X) => g(X) if ctor(X) .
endm

search f(f(f(a))) =>+ X .

output:

Solution 1 (state 1)
states: 2  rewrites: 2 in 0ms cpu (0ms real) (80000 rewrites/second)
X --> f(f(g(a)))

No more solutions.
states: 2  rewrites: 2 in 0ms cpu (0ms real) (40000 rewrites/second)

Best,

Francisco


> On 3 Jan 2021, at 16:39, Ozan Kahramanogullari 
> <ozan.kah AT gmail.com>
>  wrote:
> 
> Hi,
> 
> I was wondering if there is a way to control the depth of the rewrites in a 
> term in a system module. 
> 
> For example, if I want the rewrites to happen only at the maximum depth and 
> nowhere else. Let's say that I have a rule  
> 
> f(x) -> g(x)
>  
> and I rewrite f(f(f(a))) and I want to allow only f(f(g(a))) as a solution 
> so there will be no solution of the form f(g(f(a))) or g(f(f(a))). 
> 
> Is this possible in a system module with a search query?
> 
> Thanks,
> Ozan