Suppose that function k is defined in λ-calculus by k = λf.λx.if (isZero(x)) (1) (times (2) (f (pred x))).

If function g is defined by g = fix k, then which of the following is true of g?

  1. g(0) = 0, g(1) = 1, g(2) = 2.
  2. g(0) = 1, g(1) = 2, g(2) = 4.
  3. g(0) = 1, g(1) = 1, g(2) = 1.
  4. g(x) has no normal form for every Church-numeral x.

(b). If g is a fixed-point of k, then it must satisfy equation

  g(x) = if (isZero(x)) (1) (times (2) (g(pred x))).

Written in more common notation,

  g(x) = if x = 0 then 1 else 2*g(x − 1).