6. Recursion and Fixpoints

Contents

Working System

This chapter uses untyped lambda recursion ideas (fixpoints) implemented in eager Python via Z and thunks.

6. Recursion and Fixpoints#

Goal. Express recursion in the untyped lambda calculus using fixpoint combinators, and run them in Python.

You will learn

  • What a fixpoint is and how the Y/Z combinators encode recursion

  • Why eager evaluation forces laziness for conditionals (IF_THUNK)

  • How to write primitive recursive definitions as functionals passed to Z

  • How to recognize divergence caused by evaluating the recursive branch too early

  • Practical limits (runtime and recursion depth) when running Church encodings in Python

Roadmap#

  1. Define fixpoints and explain why the naive Y combinator diverges in eager Python.

  2. Introduce Z as an eager-safe fixpoint combinator.

  3. Introduce IF_THUNK and show how it prevents eager evaluation of recursive branches.

  4. Implement recursive examples on integers and on Church numerals.

  5. Exercises.

Remark (Eager Evaluation in Python)

The pure lambda-calculus IF evaluates only the selected branch, but Python is eager. To avoid infinite recursion we wrap each branch in a thunk (a zero-argument function) and use IF_THUNK to force only the chosen branch.

Definition (Fixpoint)

A fixpoint of a function F is a value X such that F(X) = X.

The Y combinator produces a fixpoint in the pure lambda calculus. In a strict language like Python, we use an eager version called Z.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / 'church_core.py').exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

# Naive Y combinator (for pure lambda calculus)
Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))

# In eager Python, evaluating Y typically diverges immediately.
# We intentionally do not call it directly in a live cell.
print('Defined Y (not executed). We will use Z (imported) for eager-safe recursion.')

# Eager fixpoint combinator (works in Python)
from church_core import Z

Defined Y (not executed). We will use Z (imported) for eager-safe recursion.

Example (Factorial on Integers)

Use Z to define recursion without naming the recursive function.

fact = Z(lambda fact: (lambda n: 1 if n == 0 else n * fact(n - 1)))
print(fact(5))

120

Now we connect recursion to Church numerals.

from church_core import (
    TRUE,
    FALSE,
    IF,
    IF_THUNK,
    to_bool,
    church,
    to_int,
    succ,
    add,
    mul,
    pair,
    fst,
    snd,
    pred,
    is_zero,
    Z,
)

one = church(1)

FACT = Z(
    lambda f: (
        lambda n: IF_THUNK(is_zero(n))(
            lambda: one
        )(
            lambda: mul(n)(f(pred(n)))
        )
    )
)

print(to_int(FACT(church(5))))

120

Remark (Runtime Practicality)

Recursive Church-encoded computations can hit Python recursion limits and become expensive quickly. Use small examples, or raise the recursion limit carefully for experiments.

Exercise

  1. Define a recursive sum_to_n function using Z on Python integers.

  2. Using Church numerals, define a recursive pow via repeated multiplication.

  3. Define a recursive fib (Fibonacci) on Python integers using Z. Test it for n <= 10.

  4. Define factorial on Church numerals using Z and IF_THUNK, and check to_int(FACT(church(5))) = 120. See solution: Exercise 6 (Recursion and Fixpoints)

Summary#

  • Fixpoints turn self-reference into higher-order structure: recursion is achieved without naming.

  • In eager Python, conditionals must be lazy or recursion diverges even in base cases.

  • Z + IF_THUNK is the practical recipe for Church-style recursion in Python.

  • Operationally: when something diverges, look for eager evaluation of the recursive branch first.

  • Next: use these tools to build arithmetic (mod, divisibility) and simple number theory in Church style (Chapter 7).

Contents