Fixed‑Point Operators & Recursion in Lambda Calculus

This page explains how recursion is constructed in pure lambda calculus using fixed‑point operators such as Fix and the Y‑combinator. You may reuse this explanation on your own website.

1. Why Direct Recursion Is Not Allowed

In lambda calculus, a function cannot refer to its own name. So definitions like:

mult x y = cond (iszero x) 0 (add y (mult (pre x) y))

fact x = cond (iszero x) 1 (mult x (fact (pre x)))

These are intuitive, but illegal. Lambda calculus has no built‑in recursion.

2. Fixed‑Point Operators

A fixed‑point operator is a function Fix such that for any function A:

Fix A =β A (Fix A)

This equation gives a function a copy of itself — enabling recursion.

Example: Defining `mult` Using Fix

First, write a non‑recursive helper:

multfn ≡ λ z x y .
           cond (iszero x)
                0
                (add y (z (pre x) y))
    

Then define:

mult ≡ Fix multfn

Key β‑reduction:

Fix multfn =β multfn (Fix multfn)

mult = Fix multfn
     =β multfn (mult)
     =β λ x y . cond (iszero x) 0 (add y (mult (pre x) y))
      

This matches the recursive definition we wanted.

3. Factorial Using Fix

Intended behaviour:

fact x = cond (iszero x) 1 (mult x (fact (pre x)))

Rewrite into a helper:

factfn ≡ λ z x .
            cond (iszero x)
                 1
                 (mult x (z (pre x)))
    

Define factorial:

fact ≡ Fix factfn

β‑reduction:

Fix factfn =β factfn (Fix factfn)

fact = Fix factfn
     =β factfn (fact)
     =β λ x . cond (iszero x) 1 (mult x (fact (pre x)))
      

4. Fix Is Not Unique

There are many fixed‑point operators. One famous example is the Y‑combinator.

YCurry ≡ λ x . (λ y . x (y y)) (λ y . x (y y))

Proof that YCurry is a fixed‑point operator:

YCurry A
= (λ x . (λ y . x (y y)) (λ y . x (y y))) A
=β (λ y . A (y y)) (λ y . A (y y))
=β A ((λ y . A (y y)) (λ y . A (y y)))
=β A (YCurry A)
      

Copy Summary

This page explains how recursion is encoded in lambda calculus using fixed-point operators.
We start with intuitive recursive definitions, rewrite them into non-recursive helpers, and
use Fix to restore recursion. Fix is not unique; the Y-combinator (YCurry) is another
fixed-point operator satisfying YCurry A =β A (YCurry A).
    