This is a follow up to the question here about acyclic terms. I am now interested in cyclic terms, and it seems their unification is not anymore linear in the Wielemaker-Demoen unification. The test case is basically:
?- X = f(f(X)), Y = f(f(f(Y))), X = Y.
X = Y, Y = f(f(f(Y))).
But we use larger number of function symbol iteration, and we also use arity 2 of the function symbol, and not only arity 1. For n=10,30,50,70 I get this quadratic behaviour, series 1 is the measured time of (=)/2 and series 2 is n*(n+1)/2:
Is there some impossibility theorem that would say unification for cyclic terms cannot be linear. Or otherwise might unification for cyclic terms also fall under the Patterson-Wegman unification, and therefore could be made linear?
Open source:
Linear or Exponential III?
https://gist.github.com/jburse/279b6280ab4311de456e458a7386c1da#file-bart-pl