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?


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)$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.