2009-04-07

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

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.

No comments: