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