How to define a function with Church numerals in lambda-terms?

Question

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?

Answer 1

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