Church digits: how to code zero in lambda calculus?

Question

I am studying lambda calculus, but I can not understand the encoding for the number 0.

like "a function that takes a function and a second value, and applies the time of the null function to the argument" zero "? Is there any other way to encode zero? Can someone here help me encode 0?

Answer 1

A ", which takes a function and a second value and applies the time of the argument's null function," is certainly not zero. This is encoding of zero. When you are dealing with simple lambda calculus, you must somehow encode numbers (as well as other primitive types), and there are several requirements for each of these types. For example, one requirement for natural numbers is to be able to add 1 to a specific number, and the other is to distinguish zero from large numbers (if you want to know more, find "Peano Arithmetic"). The popular encoding Dario quotes gives you these two things, and it also represents the integer N by a function that does something (encoded as an argument f ) N times - this is a kind of natural way to use naturals.

There are other encodings that are possible - for example, as soon as you can present lists, you can represent N as a list of N elements. These encodings have their pros and cons, but one of them is certainly the most popular.

Answer 2

See wikipedia :

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

Answer 3

If you study Lambda Calculus, you probably already know that λxy.y arg1 * arg2 * will decrease to arg2, since x is replaced with nothing, and the remainder (λy.y) is an identical function.

You can write zero in many other ways (i.e. come up with a different convention), but there are good reasons for using λxy.y. For example, you want zero to be the first positive integer, so if you apply the successor function to it, you get 1, 2, 3, etc. Using 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 the whole system of numbers.

In addition, you want zero to be a neutral element with respect to addition. With our successor function S: = λabc.b (abc), we can determine n + * m * for n S m, i.e., apply the successor function to m n times. Our zero λxy.y satisfies this, both 0 S m and m S 0 are reduced to m.