[Math] lambda calculus: predecessor function

lambda-calculus

Apparently this expression can be used to calculate the predecessor of a given church numeral:

$\renewcommand{\l}{\lambda}$
$\l n.(n\ \l p . (p.2,\ s p.2)\ (\overline{0},\ \overline{0})).1$

$<tuple>.n$ being the projection onto the $n$th element.

Now, applying this to some number, let's say $3$ I get:

$\l n.(n\ \l p . (p.2,\ s\ p.2)\ (\overline{0},\ \overline{0})).1\ \overline{3}$

$\rightarrow (\overline{3}\ ((\overline{0},\ \overline{0}).2,\ s\ (\overline{0},\ \overline{0}).2)).1$

$\rightarrow (\overline{3}\ (\overline{0},\ \overline{1})).1$

I assume I made some mistake here, because this makes no sense, because the expression is not a tuple, so there can be no projection being applied to it. Well, maybe I just need to unfold the expression further…

$\rightarrow ((\l f. \l x. f(f(f\ x)))\ (\overline{0},\ \overline{1})).1$

$\rightarrow ((\l x. (\overline{0},\ \overline{1})((\overline{0},\ \overline{1})((\overline{0},\ \overline{1})\ x)))\ ).1$

No.. this does not look any better… I can't apply $x$ the the right most/ inner most tuple, no any of the tuples to any other tuple… so… what am I missing here?

Best Answer

The error is where you go from

$$ \l n.(n\ \l p . (p.2,\ s\ p.2)\ (\overline{0},\ \overline{0})).1\ \overline{3} $$

to

$$ (\overline{3}\ ((\overline{0},\ \overline{0}).2,\ s\ (\overline{0},\ \overline{0}).2)).1\;. $$

In lambda calculus, function application is by convention left-associative, so

$$ \l n.(n\ \l p . (p.2,\ s\ p.2)\ (\overline{0},\ \overline{0})).1\ \overline{3} $$

is

$$ ((\overline3\ \l p . (p.2,\ s\ p.2))\ (\overline{0},\ \overline{0})).1 $$