Hindley and Seldin "Introduction to Combinators and Lambda calculus": Question about the solution to exercise 3.5.

219 Views Asked by At

The question is concerning the solution to exercise 3.5. In the exercise, they ask us to prove that any finite set of simultaneous equations $x_iy_1...y_n=Z_i$, where $1\leq i\leq k$, can be solved for each $x_i$ in both $\lambda$ and CL.

The situation with just one equation I understand as it was presented in Corollary 3.3.1. There they say that a solution $X$ is a term such that $Xy_1...y_n=_{\beta,w}[X/x]Z$. And they give $X\equiv Y(\lambda xy_1...y_n.Z)$ as a solution. (where $Y$ is a fixed point combinator.) This makes sense to me.

However, in the solution given to the exercise in the book, they first define $X$ to be the solution to $xy_1...y_n=D^{(k)}Z_1...Z_k$, where $D^{(k)}$ is a k-tuple combinator, and then they say that $X_i\equiv\lambda y_1...y_k.D^{(k)}_i(Xy_1...y_k)$ are the solutions to the set of equations, where $D^{(k)}_i$ is the i-th projection of $D^{(k)}$.

First of all I suspect the subscript k's in $X_i$ should be n's, but even then this confuses me, for if I've understood correctly, what we get when we plug this into the equations over is that $X_iy_1...y_n=_{\beta,w}[X/x]Z_i$. To me this doesn't look like a solution to simultaneous equations. I would have thought that it would look more like $$X_iy_1...y_n=_{\beta,w}[X_1/x_1,...X_i/x_i,...,X_k/x_k]Z_i$$ for $1\leq i\leq k$.

One obvious problem to me is that the variable $x$ in the solution given in the book doesn't seem to have any relation to the $x_i$'s. Other than that I could accept the way they did it as a definition different from what I would intuitively think of. As long as I understood what the relation between $x$ and $x_i$ was, I'd be totally fine with this. But right after the exercise they prove the "Double fixed-point theorem" where they seem to use the definition of simultaneous solutions I proposed! This bugs me a lot, so if anyone has any insight to share on this it would be extremely much appreciated!