Filtering does not terminate on a small set of unifiers.

[UberPyro]

Using Maude 3.3.1 on Ubuntu 20.04 and an Intel processor, I'm loading Maude with a file containing the following:

fmod SUB-STACK is
  sorts Nat Stk .
  op 0 : -> Nat [ctor] .
  op s : Nat -> Nat [ctor] .

  subsort Nat < Stk .
  op emp : -> Stk .
  op mk : Nat -> Stk [ctor] .
  op _*_ : Stk Stk -> Stk [ctor assoc id: emp] .
  op _+_ : Stk Stk -> Stk [ctor assoc comm] .

  vars X Y : [Stk] .
  eq [sub] : (X * Y) + X = X [variant] .

endfm

Running variant unify in SUB-STACK : R:Stk =? S:Stk + T:Stk . provides a set of 5 unifiers as expected. However, adding the filtered keyword filtered variant unify in SUB-STACK : R:Stk =? S:Stk + T:Stk . does not terminate. I am wondering if this is a bug, or maybe because the rules I'm working with have poor properties.

Curiously, a slightly more complicated example filtered variant unify in SUB-STACK : R:Stk * mk(0) =? S:Stk + T:Stk . terminates quickly with 2 unifiers.

Thanks in advance.

[stevenmeker]

Sorry for the long delay in responding. Your example is quite subtle and I wanted a second opinion.

Santiago Escobar sescobar@upv.es provided me with the following analysis:

---

This theory is not AC-coherent, since the term “s(s(0)) + s(0) + (0 * s(0))” cannot be reduced to “s(s(0)) + s(0)”. Note that you should use “get variants” instead of “reduce”.

The problem is not the Y variable in the inner position but the outermost plus symbol. The theory should be extended with

eq [sub] : (X * Y) + X + Z = X + Z [variant] .

but then it does not have the finite variant property anymore. The variant unify command does not terminate. Probably, what happened is that the unification call "R:Stk =? S:Stk + T:Stk” reported in GitHub does not get into the coherence problem but the filtering does, since you create more general terms to be checked for variant-based matching. But, IMHO, the absence of the coherent version should not yield into a termination problem. So you may want to trace the variant-based pattern matching procedures.

However, there is a fix for the theory if you have a non-empty sort for Stk.

---

fmod SUB-STACK is sorts Nat Stk Emp NeStk . op 0 : -> Nat [ctor] . op s : Nat -> Nat [ctor] . subsort Nat < NeStk . subsorts Emp NeStk < Stk . op emp : -> Emp . op mk : Nat -> NeStk [ctor] . op * : Stk Stk -> Stk [ctor assoc id: emp] . op * : NeStk Stk -> NeStk [ctor ditto] . op * : Stk NeStk -> NeStk [ctor ditto] . op + : Stk Stk -> Stk [ctor assoc comm] . var Y : Stk . vars X Z : NeStk . eq [sub] : (X Y) + X = X [variant] . eq [sub-Coh] : (X Y) + X + Z = X + Z [variant] . endfm

---

Now all commands finish and the filtered version returns only one most general unifier.

---

So despite the lack of AC-coherence, your example should have terminated and exposes a rather subtle bug in the variant subsumption algorithm which never terminates. I plan to fix it in a future public alpha release. May I use your example in the Maude test suite?

Steven Eker

[UberPyro]

Thank you very much for the detailed response, this is quite interesting and I appreciate the time that you all took to look at my example. Feel free to use the example in your test suite.

[stevenmeker]

I've fixed the bug in Alpha152 and added your example to the test suite as tests/ResolvedBugs/filteredVariantUnifyJune2023.maude