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