4 ms·
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
by tromp 4y ago
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)
- daniel-cussen 4y agoWhat I don't get is when it decrements and checks if we're at the base case?
- tromp 4y agoThe 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))