Church numerals: How should I interpret the numbers from expressions?

Question

Can someone explain to me using substitutions how we get a number "zero" or the rest of natural numbers?

For example the value: "zero"

λf.λx.x

if I apply this expression on an another expression:

"(λf.(λx.x)) a"

then using substitution:

:=[a/f](λx.x)
:=(λx.x)

what am I missing? How should I interpret these number expressions?

Answer 1

The church numeral n is a function that takes another function f and returns a function that applies f to its argument n times. So 0 a (where 0 is, as you said, λf.λx.x ) returns λx.x because that applies a to x 0 times.

1 a gives you λx. a x, 2 a gives you λx. a (a x) and so on.

Answer 2

Below is the explanation based on paper by Erhan Bagdemir in the comment to answer by sepp2k.

Essential points to grasp:

• all Church numerals are functions of two parameters;
• for Church numerals, it is implied that:
  • f — is the 'successor' function (i.e. function which accepts a Church numeral and return church numeral next one, it's basically and increment);
  • x — is a (Church numeral) value representing 'zero' (the count starting point).

Keeping that in mind:

λf . λx . x

will be equal to zero, if we will pass the appropriate f (in this particular case it doesn't matter what function will be passed as f, since it never applied) and x:

λf . λx . ZERO

following:

λf . λx .  fx

will be evaluated to 1:

λf . λx . INCREMENT ZERO

and this:

λf . λx . f f x

will be qual to 2:

λf . λx . INCREMENT(INCREMENT ZERO)

and so on, for all the successive numbers.

See my (broader) answer to another (but closely related) question.

Answer 3

A church numeral n, (say 2,) represents the "action" of applying any given function n times (here,two times) on any given parameter.

A church numeral, by definition, is a function that takes two parameters, namely
1) a function
2) a parameter or expression or value on which the supplied function is applied.

When the supplied function is the successor function, and the supplied second parameter is Zero , you get the numeral. (2, in the above example)

Church numeral 2 is by definition,

λf . λx . f( f( x)) 

,Which is obviously a function that takes two parameters.

On passing the successor function, i.e f(x)=x+1 as first parameter and zero as second parameter to the function, we get...

f(f(0))  
=f(1) 
=2

This explanation is kinda simplified as definition of successor function and zero aren't as shown, in lambda calculus..

Refer :http://www.cse.unt.edu/~tarau/teaching/GPL/docs/Church%20encoding.pdf An excellent explanation on church encodings