How can I express the following function by a lambda term?
f(n) = T if n != 0. F if n = 0.
n stands for a Church numeral.
I know that 0 := λf.λx.x where λx.x is the identity function and all other natural numbers can be expressed by n := λf.λx.f (f ... (f x)) which contains f n times more than the 0-term. E.g. 3 := λf.λx.f (f (f x)).
But how can I derive a valid λ-term for the function above? I think I need a y too for getting the T/F. Therefore I can express the number n by λf.(λxy.fxy), right? But what about the F and T? Is the following a right λ-term for the function above? λf.(λxy.fxy(yFT)) where T=λxy.x and F=λxy.y?
No, you're given the term for n. It is a function that expects two arguments, an f and a z:
isZero n = n ( ;; f, a function, expecting x
;; or the result of (f (f ... (f x) ...))
λx.
;; but we know what we want it to return, always: it is:
F ;; false, for n is _not_ 0
)
( ;; the initial x, in case n is ......... 0!
;; so we know what we want it to be, in case n is 0:
T ;; true, for n _is_ 0
)
and thus
isZero = λn.n(λx.F)T
If n was 0, isZero n will return T; and otherwise, F:
{0}(λx.F)T = T
{1}(λx.F)T = (λx.F)T = F
{2}(λx.F)T = (λx.F)((λx.F)T) = F
{3}(λx.F)T = (λx.F)((λx.F)((λx.F)T)) = F
....