In general, unifying y with an expression involving y would require our being able to find a fixed point of the equation y $=$ $\textit{expression involving}$y. It is sometimes possible to syntactically form an expression that appears to be the solution. For example, y $=$ list("f", y) seems to have the fixed point list("f", list("f", list("f",))), which we can produce by beginning with the expression list("f", y) and repeatedly substituting list("f", y) for y. Unfortunately, not every such equation has a meaningful fixed point. The issues that arise here are similar to the issues of manipulating infinite series in mathematics. For example, we know that 2 is the solution to the equation $y = 1 + y/2$. Beginning with the expression $1 + y/2$ and repeatedly substituting $1 + y/2$ for $y$ gives $2 = y = 1 + y/2 = 1 + (1+y/2)/2 = 1 + 1/2 + y/4 =\cdots,$ which leads to $2 = 1 + 1/2 + 1/4 + 1/8 +\cdots.$ However, if we try the same manipulation beginning with the observation that $-1$ is the solution to the equation $y = 1 + 2y$, we obtain $-1 = y = 1 + 2y = 1 + 2(1 + 2y) = 1 + 2 + 4y = \cdots,$ which leads to $-1 = 1 + 2 + 4 + 8 +\cdots.$ Although the formal manipulations used in deriving these two equations are identical, the first result is a valid assertion about infinite series but the second is not. Similarly, for our unification results, reasoning with an arbitrary syntactically constructed expression may lead to errors.
4.4.4 Implementing the Query System