Fixed-point Combinator - How IT Works

How It Works

Ignoring for now the question whether fixed-point combinators even exist (to be addressed in the next section), we illustrate how a function satisfying the fixed-point combinator equation works. To trace the computation steps, we choose untyped lambda calculus as our programming language. The (computational) equality from the equation that defines a fixed-point combinator corresponds to beta reduction in lambda calculus.

As a concrete example of a fixed-point combinator applied to a function, we use the standard recursive mathematical equation that defines the factorial function

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 the lambda abstraction

F = λf. λn. IFTHENELSE (ISZERO n) 1 (MULT n (f (PRED n)))

using the usual encoding for booleans, and Church encoding for numerals. The functions in CAPITALS above can all be defined as lambda abstractions with their intuitive meaning; see lambda calculus for their precise definitions. Intuitively, f in F is a place-holder argument for the factorial function itself.

We now investigate what happens when a fixed-point combinator FIX is applied to F and the resulting abstraction, which we hope would be the factorial function, is in turn applied to a (Church-encoded) numeral.

(FIX F) n = (F (FIX F)) n --- expanded the defining equation of FIX = (λx. IFTHENELSE (ISZERO x) 1 (MULT x ((FIX F) (PRED x)))) n --- expanded the first F = IFTHENELSE (ISZERO n) 1 (MULT n ((FIX F) (PRED n))) --- applied abstraction to n.

If we now abbreviate FIX F as FACT, we recognize that any application of the abstraction FACT to a Church numeral calculates its factorial

FACT n = IFTHENELSE (ISZERO n) 1 (MULT n (FACT (PRED n))).

Recall that in lambda calculus all abstractions are anonymous, and that the names we give to some of them are only syntactic sugar. Therefore, it's meaningless in this context to contrast FACT as a recursive function with F as somehow being "not recursive". What fixed point operators really buy us here is the ability to solve recursive equations. That is, we can ask the question in reverse: does there exist a lambda abstraction that satisfies the equation of FACT? The answer is yes, and we have a "mechanical" procedure for producing such an abstraction: simply define F as above, and then use any fixed point combinator FIX to obtain FACT as FIX F.

In the practice of programming, substituting FACT at a call site by the expression FIX F is sometimes called anonymous recursion. In the lambda abstraction F, FACT is represented by the bound variable f, which corresponds to an argument in a programming language, therefore F need not be bound to an identifier. F however is a higher-order function because the argument f is itself called as a function, so the programming language must allow passing functions as arguments. It must also allow function literals because FIX F is an expression rather than an identifier. In practice, there are further limitations imposed on FIX, depending on the evaluation strategy employed by the programming environment and the type checker. These are described in the implementation section.