Home Forums Blogs Articles Photos Videos Contact FAQ

Fixed point combinator - Example

Fixed point combinator - Example: Encyclopedia II - Fixed point combinator - Example

Consider the factorial function (under Church encoding). The usual recursive mathematical equation is fact(n) = if n=0 then 1 else n * fact(n-1) We can express a "single step" of this recursion in lambda calculus as F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))), where "f" is a place-holder argument for the factorial function to be passed to itself. The function F performs a single step in the evaluation of the recursive formula. A ...

Fixed point combinator: Encyclopedia II - Fixed point combinator - Example

Fixed point combinator - Example

Consider the factorial function (under Church encoding). The usual recursive mathematical equation is

fact(n) = if n=0 then 1 else n * fact(n-1)

We can express a "single step" of this recursion in lambda calculus as

F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))),

where "f" is a place-holder argument for the factorial function to be passed to itself. The function F performs a single step in the evaluation of the recursive formula. Applying the fix operator gives

fix(F)(n) = F(fix(F))(n) fix(F)(n) = λx. (ISZERO x) 1 (MULT x (fix(F) (PRED x)))(n) fix(F)(n) = (ISZERO n) 1 (MULT n (fix(F) (PRED n)))

We can abbreviate fix(F) as fact, and we have

fact(n) = (ISZERO n) 1 (MULT n (fact(PRED n)))

So we see that a fixed-point operator really does turn our non-recursive "factorial step" function into a recursive function satisfying the intended equation.