prolog - Wielemaker-Demoen统一的非线性

Question

这是对这里关于非循环项的问题的后续。我现在对循环术语感兴趣，而且似乎它们的统一在 Wielemaker-Demoen 统一中不再是线性的。测试用例基本上是：

?- X = f(f(X)), Y = f(f(f(Y))), X = Y.
X = Y, Y = f(f(f(Y))).

但是我们使用更大数量的函数符号迭代，并且我们还使用函数符号的 arity 2，而不仅仅是 arity 1。对于 n=10,30,50,70 我得到了这个二次行为，系列 1 是测量的时间(=)/2 并且系列 2 是 n*(n+1)/2：

是否有一些不可能定理说循环项的统一不能是线性的。或者，循环项的统一也可能属于帕特森-韦格曼统一，因此可以成为线性的？

开源：

线性还是指数 III？
https://gist.github.com/jburse/279b6280ab4311de456e458a7386c1da#file-bart-pl

标签： prologswi-prologunification