2009-04-08

SUCC1

Japanese version

Now we are ready to calculate SUCC 1.

SUCC 1
= (λ n f x. f (n f x))(λ f x. f x)

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

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

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

= λ f x. f (f x)

= 2

SUCC 1 is 2.

The red color characters are processed at each line.

In case if ((λ f x. f x) f x)) is not clear, we could change the
variable name more unique to distinguish.

((λ f x. f x) f x)) is the same to ((λ g h. g h) f x)).

((λ g h. g h) f x)) ... f is replaced with g.

((λ h. f h) x)) ... h is replaced with x.

(f x)

I hope this is not ambiguous anymore.

No comments: