Japanese version
I could not update the blog for a while, since I was in Muenchen for a week.
(λf x. x) f x
is
(λf x. x) f x
... remove f since f is not bound.
(λ x. x) x
... Input x, output x.
This
(λx. x) x
is
x,
Therefore,
(λ f x. f ((λf x. x) f x))
is
(λ f x. f (x)).
Although parentheses '()' represent priority of the expression, there is not so much meaning in this case. Then lazy mathematicians will write it as
(λ f x. f x)
Almost, but not yet. We can remove the outmost parentheses also.
λ f x. f x
Now, this is Church number 1. Therefore, SUCC 0 is 1.
Finally, it was a long way, but we compute the SUCC 0 in the lambda expression way. Let's move on to SUCC 1.
I could not update the blog for a while, since I was in Muenchen for a week.
(λf x. x) f x
is
(λf x. x) f x
... remove f since f is not bound.
(λ x. x) x
... Input x, output x.
This
(λx. x) x
is
x,
Therefore,
(λ f x. f ((λf x. x) f x))
is
(λ f x. f (x)).
Although parentheses '()' represent priority of the expression, there is not so much meaning in this case. Then lazy mathematicians will write it as
(λ f x. f x)
Almost, but not yet. We can remove the outmost parentheses also.
λ f x. f x
Now, this is Church number 1. Therefore, SUCC 0 is 1.
Finally, it was a long way, but we compute the SUCC 0 in the lambda expression way. Let's move on to SUCC 1.
Comments