3

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?

MFranc
  • 213

1 Answers1

4

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

Luca Bressan
  • 6,845