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 the variables are free variable for gensym3141. λ function has such a function.
In (λf x. x) f x, first, f is applied to f, however, this is a free variable. Then this f is vanished. (This λ expression has only `x' after the `.'.) If you are confused two fs in this λ expression, we can rewrite it to (λg x. x) f x. This is the same. When the function apples to f, g does not bound, then f will vanish.
Then, this will be
(λf x. x) f x
(λx. x) x.
The last line, λ expression applys to x, then it becomes x. Again, there are three xs here. To make this clear, we could change the variable name to y.
(λy. y) x
This is totally same as (λx. x) x. If we write this in conventional way,
f(x) := x
f(y) := y.
These two are substantially the same.
Marvin is ``マービン'' in Japanese. It is "Marvin" in English. But Marvin itself does never change according to which language do you use. Please note that the variable name can be changed does not mean (λx.x) can be (λx.y). The corresponding what to what must be kept. This is the line and if you over that, anyone can treat Vogon correctly.
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 the variables are free variable for gensym3141. λ function has such a function.
In (λf x. x) f x, first, f is applied to f, however, this is a free variable. Then this f is vanished. (This λ expression has only `x' after the `.'.) If you are confused two fs in this λ expression, we can rewrite it to (λg x. x) f x. This is the same. When the function apples to f, g does not bound, then f will vanish.
Then, this will be
(λf x. x) f x
(λx. x) x.
The last line, λ expression applys to x, then it becomes x. Again, there are three xs here. To make this clear, we could change the variable name to y.
(λy. y) x
This is totally same as (λx. x) x. If we write this in conventional way,
f(x) := x
f(y) := y.
These two are substantially the same.
Marvin is ``マービン'' in Japanese. It is "Marvin" in English. But Marvin itself does never change according to which language do you use. Please note that the variable name can be changed does not mean (λx.x) can be (λx.y). The corresponding what to what must be kept. This is the line and if you over that, anyone can treat Vogon correctly.
Comments