2 ms·

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

• tromp 4y ago
  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))