Recursive Functions

Using Y

To define a recursive function in lambda calculus:

1. Write a step function that takes an extra parameter f
2. In the body, use f wherever you would make a recursive call
3. Apply Y to the step function: MYFUNC = Y step

Y finds the fixed point of the step function, which means step MYFUNC = MYFUNC. The step function "becomes" recursive because Y arranges for f to be MYFUNC itself.

No self-reference, no names in the language -- just Y doing the wiring.

The Factorial Step Function

The factorial step function is:

λf.λn. IF (ISZERO n) ONE (MUL n (f (PRED n)))

Read it as: "Given a function f and a number n, if n is zero return ONE; otherwise multiply n by f applied to n - 1."

The parameter f stands for the recursive call. The step function does not know what f is -- it just uses f wherever factorial would call itself. Y will later supply the actual recursive function as f.

Factorial via Y

With the factorial step function in hand:

step = λf.λn. IF (ISZERO n) ONE (MUL n (f (PRED n)))

We define factorial as:

FACT = Y step

Because Y finds the fixed point, we know step FACT = FACT. This means FACT behaves exactly like the step function with f replaced by FACT itself -- which is exactly the recursive definition of factorial.

We never executed anything. We never expanded Y. We just observed that Y's fixed-point property guarantees FACT calls itself through f.

The Fibonacci Step Function

Fibonacci requires two recursive calls: fib(n-1) and fib(n-2). The step function handles this naturally:

λf.λn. IF (ISZERO n) ZERO (IF (ISZERO (PRED n)) ONE (ADD (f (PRED n)) (f (PRED (PRED n)))))

The parameter f appears twice -- once for each recursive call. This is fine. The step function does not care how many times it uses f. Y supplies the fixed point the same way as before:

FIB = Y step

The pattern is identical to factorial. Only the step function's body changes.

The Pattern

The pattern for defining recursive functions in lambda calculus is always the same:

1. Write a step function λf.λ... body using f for recursive calls
2. Apply Y: MYFUNC = Y step

This works for factorial, Fibonacci, and any other recursive function. Y is a universal recursion tool -- it does not know or care what the step function computes. You provide the logic; Y provides the self-reference.

Turing Complete

With the Y combinator, lambda calculus can define factorial, Fibonacci, and every other recursive function -- not through special syntax, but through the fixed-point property of a pure lambda term.

This is a remarkable result. Lambda calculus has no loops, no variables that change, no built-in recursion. Yet with Church encodings for data and Y for recursion, it can compute anything a Turing machine can compute. This equivalence is the Church-Turing thesis, which we will explore in the metatheory topic.