Japanese version
We have addition and multiplication. Next I would like to subtraction. But, we do not have minus numbers of Church numbers. Because we construct the numbers by number of f-s. For simplicity, we do not think about minus numbers here. If you want to know more, you can look up Wikipedia.
We prepare PRED before we go to subtraction. The PRED (predecessor) function generates one Church number before the input number. Here we will not think about before the number 0.
The definition of PRED is
PRED := λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u).
Let's compute PRED 2.
PRED 2 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. f (f x))
= (λ f x. (λ f x. f (f x)) (λ g h. h (g f)) (λ u. x) (λ u. u))
= (λ f x. (λ x. (λ g h. h (g f)) ((λ g h. h (g f)) x)) (λ u. x) (λ u. u))
= (λ f x. (λ x. (λ g h. h (g f)) (λ h. h (x f))) (λ u. x) (λ u. u))
= (λ f x. (λ g h. h (g f)) (λ h. h ( (λ u. x) f)) (λ u. u))
= (λ f x. (λ h. h ((λ h. h ( (λ u. x) f)) f)) (λ u. u))
Notice, one 'f' is vanished here. Number of 'f's represent Church number, therefore, remove one 'f' is minus 1.
= (λ f x. (λ h. h ((λ h. h x) f)) (λ u. u))
= (λ f x. (λ h. h ((f x))) (λ u. u))
= (λ f x. ((λ u. u) ((f x))) )
= (λ f x. (f x))
= (λ f x. f x)
= 1
It is curious to compute PRED 0. What is the predecessor of 0?
PRED 0 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. x)
= (λ f x. (λ f x. x) (λ g h. h (g f)) (λ u. x) (λ u. u))
= (λ f x. (λ x. x) (λ u. x) (λ u. u))
= (λ f x. (λ u. x) (λ u. u))
= (λ f x. x)
It returns 0. This is a nice property of this PRED definition. PRED returns 0 if the input is 0, otherwise it returns one predecessor number.
I am fascinated that Church number itself is part of program. The number is a program here. Of course Church number is a function. Therefore, it is natural in a sense.
If we apply λ n . n (λ g h. h (g f)) to 0,
(λ n . n (λ g h. h (g f))) (λ f x . x)
= (λ f x . x) (λ g h. h (g f))
= (λ x . x)
This is part of PRED function. The output is 0. In PRED function has more terms, so I would like to stop here. The basic mechanism here is that when this part of the function apples to 0, then the first team is ignored. Since Church number 0 (λ x . x) does not have binding to 'f'.
We have addition and multiplication. Next I would like to subtraction. But, we do not have minus numbers of Church numbers. Because we construct the numbers by number of f-s. For simplicity, we do not think about minus numbers here. If you want to know more, you can look up Wikipedia.
We prepare PRED before we go to subtraction. The PRED (predecessor) function generates one Church number before the input number. Here we will not think about before the number 0.
The definition of PRED is
PRED := λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u).
Let's compute PRED 2.
PRED 2 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. f (f x))
= (λ f x. (λ f x. f (f x)) (λ g h. h (g f)) (λ u. x) (λ u. u))
= (λ f x. (λ x. (λ g h. h (g f)) ((λ g h. h (g f)) x)) (λ u. x) (λ u. u))
= (λ f x. (λ x. (λ g h. h (g f)) (λ h. h (x f))) (λ u. x) (λ u. u))
= (λ f x. (λ g h. h (g f)) (λ h. h ( (λ u. x) f)) (λ u. u))
= (λ f x. (λ h. h ((λ h. h ( (λ u. x) f)) f)) (λ u. u))
Notice, one 'f' is vanished here. Number of 'f's represent Church number, therefore, remove one 'f' is minus 1.
= (λ f x. (λ h. h ((λ h. h x) f)) (λ u. u))
= (λ f x. (λ h. h ((f x))) (λ u. u))
= (λ f x. ((λ u. u) ((f x))) )
= (λ f x. (f x))
= (λ f x. f x)
= 1
It is curious to compute PRED 0. What is the predecessor of 0?
PRED 0 := (λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)) (λ f x. x)
= (λ f x. (λ f x. x) (λ g h. h (g f)) (λ u. x) (λ u. u))
= (λ f x. (λ x. x) (λ u. x) (λ u. u))
= (λ f x. (λ u. x) (λ u. u))
= (λ f x. x)
It returns 0. This is a nice property of this PRED definition. PRED returns 0 if the input is 0, otherwise it returns one predecessor number.
I am fascinated that Church number itself is part of program. The number is a program here. Of course Church number is a function. Therefore, it is natural in a sense.
If we apply λ n . n (λ g h. h (g f)) to 0,
(λ n . n (λ g h. h (g f))) (λ f x . x)
= (λ f x . x) (λ g h. h (g f))
= (λ x . x)
This is part of PRED function. The output is 0. In PRED function has more terms, so I would like to stop here. The basic mechanism here is that when this part of the function apples to 0, then the first team is ignored. Since Church number 0 (λ x . x) does not have binding to 'f'.
Comments