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?

Notebook

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.

Dexterdexterity

This is a related question I asked in google groups: Say I have a function f. How do I show that this translates to a natural number 0? What other functions do I need in order to infer that my function f behaves like a 0? – Notebook

If you want to prove that a function f is zero under the usual encoding, you need to show that for all g (f g x) == x. You don't need to know anything beyond this. – Dexterdexterity

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

Histiocyte

It doesn't answer the question, it just repeats the encoding which the OP already clearly knows. He just doesn't understand HOW or WHY 0 ≡ λf.λx. x (and neither do I, which is why I am here lol) – Vernavernacular

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.

Featherbrain

Answer 4

In usual imperative programming languages we have similar notation of for loops

for(state = <start_state>; state!=<end_state>; state = inc(state)){
   foo(state);
}

where we apply function foo on the current state and by doing that, we modify the current state to the next state. (e.g. increment a variable)

You can think of numbers in church notation as for loops with its given initial state z and a function s applied to each state returned by previous calls. The lambda representing a number should then take these as arguments. e.g. (λsz.s z) for applying one for loop cycle on the initial state. Using this logic we can construct λsz.z for 0 because we know that the function is applied zero times on the initial state, therefore the number represents 0.

Clingfish