I was recently reading "Lambda calculus and combinators" by J.R. Hindley and J.P Seldin.
In the book at some point we encounter the following reductions :
- $(\lambda x.x)v$
- $(\lambda x.xxy)(\lambda x.xxy)$
Now in the first case we get :
- $(\lambda x.x)v \equiv_{\beta} v$
Clearly we can substitute the bounded x for v obtaining the $\beta \text{ normal form} $ of the expression.
Yet in the second example we have :
- $(\lambda x.xxy)(\lambda x.xxy) \equiv_{\beta} (\lambda x.xxy)(\lambda x.xxy)y$
The book says we can not find a $\beta \text{ normal form}$ for the original expression, stating we would go on and on like this :
$ L \equiv (\lambda x.xxy)(\lambda x.xxy) \implies L\,\,\triangleright_{\beta}\,\,Ly\,\,\triangleright_{\beta}\,\,Lyy \,\,\triangleright_{\beta}\,\,… $
Now I'd think, since the syntax is the same we could do the following :
$(\lambda x.xxy)(\lambda x.xxy) \equiv_{\beta} (\lambda x.xxy)(\lambda x.xxy)y \equiv_{\beta} (\lambda x.xxy)(yyy) \equiv_{\beta} (yyyyyyy)$
How come I can not make such a substitution?
Best Answer
The mistake is thinking that application is right-associative, when in fact it is left-associative.
The term $(\lambda x. x x y)(\lambda x. x x y) y$ must be interpreted as $\color{red}((\lambda x. x x y)(\lambda x. x x y)\color{red})y$, from which you see that you can't replace $x$ with $y$ in the second $\lambda x. x x y$.
In general, $L M N$ means $(L M) N$, and not $L (M N)$.