2
$\begingroup$

This is really a second part to my first question, but I felt that this was different enough from the first part that it merited its own question.

So, using Church numerals, we define

$3 = {\lambda} f. {\lambda}x.f(f(f(x)))$,

and

$4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$.

We can then add with an expression like

$3\ g\ (4\ g\ z)$

And this reduces to:

$(g (g (g (g (g (g (g\ z)))))))$.

But, of course, this is not how we would define $7$ in the scheme above. $7$ would be

${\lambda}g.{\lambda}z.(g (g (g (g (g (g (g\ z)))))))$.

Why is it still legitimate to call the application $3\ g\ (4\ g\ z)$ "7" when we can no longer perform functions with it?

$\endgroup$
  • $\begingroup$ This is not quite how you add two Church numerals; $g$ and $z$ should be quantified variables. $\endgroup$ – Yuval Filmus Jan 28 at 3:41
4
$\begingroup$

This is just a shorthand, leaving off some things that aren't really needed to understand the concepts. If you want your $7$ to be written as a function again, all you need are a couple more implicit lambdas. Here's how I'd write the Church addition with those lambdas in place:

$$3 + 4 = \lambda g . \lambda z . 3 g (4 g z) = \lambda g . \lambda z . 7 g z$$

But we also know that:

$$\lambda k . f k = f$$

Therefore:

$$\lambda g . \lambda z . 7 g z = 7$$

$\endgroup$

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.