succ -- Apply numbers (Cont.)

Japanese version

I could not update the blog for a while, since I was in Muenchen for a week.

(λf x. x) f x


f x. x) f x
... remove f since f is not bound.

x. x) x
... Input x, output x.


(λx. x) x




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


(λ 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.

No comments: