Comment by tromp | Hacker News Reader

Comment by tromp | Hacker News Reader

The author skips the (standard) construction of numbers in lambda calculus, the so-called Church numerals C0,C1,C2,... which iterate a given function a certain number of times on a given argument. So

    C0 f x => x
    C1 f x => f x
    C2 f x => f (f x)

Curiously, for these numbers, you can define the factorial function without any use of recursion, instead using their built-in iterative behaviour. Written in the standard notation for lambda calculus, it is

    factorial = λn.λf.n(λf.λn.n(f(λf.λx.n f(f x))))(λx.f)(λx.x)

What I don't get is when it decrements and checks if we're at the base case?

The definition of factorial (fac for short) can be broken down as

    succ = \n\f\x. n f (f x) -- the successor function for Church numerals
    F   = \c\n. n (c (succ n))
    fac = \n\f. n F (\x.f) id

As you can see there is no use of a decrement function. Instead, numbers 1..n are recreated by the iterated successor function.

We can follow the reduction of fac 3 as

    0 = \f\x. x
    1 = \f\x. f x
    2 = \f\x. f(f x)
    3 = \f\x. f(f(f x))
    fac 3 = \f. F (F (F (\x.f))) 1
          = \f. 1 (F (F (\x.f))  2)
          = \f. 1 (2 (F (\x.f)   3))
          = \f. 1 (2 (3 ((\x.f)  4)))
          = \f. 1 (2 (3 f))

Reply on news.ycombinator.com