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.
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.
Comments