Japanese version

Let's compute the SUCC function one by one. First time, I was confused and I tried to use `0' or `1' as a number. But here, a number is a Church number, then 0 is (λf x. x). You can see I am a totally amateur. Please keep the left-associative in mind,

SUCC 0 := (λn f x. f (n f x)) (λf x. x)

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

Because of left-associative `n' is (λf x. x). Here the underlined part,

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

Can you see that any `f' will vanish? For example, One argument function

(λf. 3)

means,

f(x) := 3.

Therefore, this function is always 3 for any `x.' Such variable `x' is called free variable (or the variable does not bound). It is like Marvin in the Heart of Gold. Anything does not matter for Marvin. Zaphod always forgets him. But this free variable is necessary as Marvin in Hitchhiker's guide to the Galaxy. The vending machine gensym3141 does not bound any variables until you put your credit card. Without credit card, all…

Let's compute the SUCC function one by one. First time, I was confused and I tried to use `0' or `1' as a number. But here, a number is a Church number, then 0 is (λf x. x). You can see I am a totally amateur. Please keep the left-associative in mind,

SUCC 0 := (λn f x. f (n f x)) (λf x. x)

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

Because of left-associative `n' is (λf x. x). Here the underlined part,

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

Can you see that any `f' will vanish? For example, One argument function

(λf. 3)

means,

f(x) := 3.

Therefore, this function is always 3 for any `x.' Such variable `x' is called free variable (or the variable does not bound). It is like Marvin in the Heart of Gold. Anything does not matter for Marvin. Zaphod always forgets him. But this free variable is necessary as Marvin in Hitchhiker's guide to the Galaxy. The vending machine gensym3141 does not bound any variables until you put your credit card. Without credit card, all…