Japanese version
These series of the examples might be not so fun if you don't try to apply them by yourself. If you do not follow them step by step, these are just a bunch of equations. Therefore, I recommend to try it.
We will define the subtraction using PRED function.
SUB := λ m n. n PRED m
SUB 3 2 = (λ m n. n PRED m) (λ f x. f (f (f x))) (λ f x. f (f x))
= (λ n. n PRED (λ f x. f (f (f x)))) (λ f x. f (f x))
= (λ f x. f (f x)) PRED (λ f x. f (f (f x)))
= (λ x. PRED (PRED x)) (λ f x. f (f (f x)))
You see that the PRED is duplicated as the second argument (= 2). This is the trick. If the second argument (subtrahend) is ten, then PRED is repeated ten times.
= PRED (PRED (λ f x. f (f (f x))))
This is PRED (PRED 3).
= PRED 2
= 1
Therefore, 3 - 2 = 1. We can do subtraction.
These series of the examples might be not so fun if you don't try to apply them by yourself. If you do not follow them step by step, these are just a bunch of equations. Therefore, I recommend to try it.
We will define the subtraction using PRED function.
SUB := λ m n. n PRED m
SUB 3 2 = (λ m n. n PRED m) (λ f x. f (f (f x))) (λ f x. f (f x))
= (λ n. n PRED (λ f x. f (f (f x)))) (λ f x. f (f x))
= (λ f x. f (f x)) PRED (λ f x. f (f (f x)))
= (λ x. PRED (PRED x)) (λ f x. f (f (f x)))
You see that the PRED is duplicated as the second argument (= 2). This is the trick. If the second argument (subtrahend) is ten, then PRED is repeated ten times.
= PRED (PRED (λ f x. f (f (f x))))
This is PRED (PRED 3).
= PRED 2
= 1
Therefore, 3 - 2 = 1. We can do subtraction.
Comments