在Pattern Unification的概念中，有一類等式依賴non-linear spine，會沒有general solution，例如 ?0 x x=?x?0\ x\ x \overset{?}{=} x?0 x x=?x 這裡至少有兩組答案： λx.λy.x\lambda x. \lambda y. xλx.λy.x 跟 λx.λy.y\lambda x. \lambda y. yλx.λy.y