Church Numerals: how to encode zero in lambda calculus?

Question

I am learning lambda calculus but I cant seem to understand the encoding for the number 0.

how is "function that takes in a function and a second value and applies the function zero times on the argument" a zero? Is there any other way to encode zero? Could anyone here help me encode 0?

Answer 1

A "function that takes in a function and a second value and applies the function zero times on the argument" is, of course, not zero. It's an encoding of zero. When you deal with plain lambda calculus, you have to encode numbers (as well as other primitive types) in some way, and there are a few requirements dictated for each of these types. For example, one requirement for natural numbers is to be able to add 1 to a given number, and another is to be able to distinguish zero from bigger numbers (if you want to know more, look for "Peano Arithmetic"). The popular encoding that Dario quoted gives you these two things, and it is also representing an integer N by a function that does something (encoded as the f argument) N times -- which is a kind of a natural way to use naturals.

There are other encodings that are possible -- for example, once you can represent lists, you can represent N as a list of N items. These encodings have their pros and cons, but the one above is by far the most popular one.

Answer 2

See wikipedia:

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x

Answer 3

If you learn Lambda Calculus, you probably already know that λxy.y arg1 *arg2* will reduce to arg2, since the x is replaced by nothing, and the remainder (λy.y) is the identity function.

You could write zero in many other ways (i.e. come up with a different convention), but there are good reasons for using λxy.y. For instance, you want zero to be the first natural number, so that if you apply the successor function to it, you get 1, 2, 3 etc. With the function λabc.b(abc), you get λxy.x(y), λxy.x(x(y)), λxy.x(x(x(y))) etc., in other words, you get a whole number system.

Furthermore, you want zero to be the neutral element with respect to addition. With our successor function S := λabc.b(abc), we can define n+*m* as n S m, i.e., n times the application of the successor function to m. Our zero λxy.y satisfies this, both 0 S m and m S 0 reduce to m.