Cheat Sheet

Setup (Imports That Match the Book)

The book keeps reusable code in book/ and book/advanced/. If you run code from book/notebooks/, add the parent book/ directory to sys.path once:

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "lc_core.py").exists():
    # Likely running from book/notebooks/
    book_root = book_root.parent

if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

import lc_core as lc
import lc_interactive as lci
import church_core as ch
import stlc_core as st

from advanced import stlc_nbe as nbe
from advanced import dependent_codes as dep
from advanced import sequent_imp as sq
from advanced import classical_control as cc
from advanced import systemf_core as sf

Lambda Terms (AST Form)

Terms are Var, Lam, and App.

t = lc.Lam("x", lc.App(lc.Var("x"), lc.Var("y")))
print(lc.show(t))

Free vs Bound Variables

Free variables drive capture-avoidance.

t = lc.Lam("x", lc.App(lc.Var("x"), lc.Var("y")))
print("FV =", lc.free_vars(t))   # {'y'}
print("all =", lc.all_vars(t))   # {'x','y'}

Alpha-Renaming (Capture-Avoiding)

Rename a binder, but avoid capturing free variables.

capture_sensitive = lc.Lam("x", lc.App(lc.Var("x"), lc.Var("y")))
print(lc.show(lc.alpha_rename(capture_sensitive, "y")))  # freshens to y0, y1, ...

Substitution (Capture-Avoiding)

Substitute [x := r]t while avoiding capture by renaming binders when needed.

t = lc.Lam("y", lc.Var("x"))
out = lc.subst(t, "x", lc.Var("y"))
print(lc.show(out))  # (lambda y0. y)

Beta Reduction: Normal vs Applicative Order

Normal order can terminate where applicative order gets stuck reducing an argument.

omega = lc.App(
    lc.Lam("x", lc.App(lc.Var("x"), lc.Var("x"))),
    lc.Lam("x", lc.App(lc.Var("x"), lc.Var("x"))),
)
term = lc.App(lc.Lam("x", lc.Var("y")), omega)  # (λx. y) Ω

print("normal:", lc.show(lc.normalize(lc.beta_step_normal, term, limit=12)))
print("applicative (12 steps):", lc.show(lc.normalize(lc.beta_step_applicative, term, limit=12)))

Definitional Equality (Beta + Eta + Alpha)

lc.defeq(a,b) compares normal forms up to alpha-renaming and eta.

a = lc.Lam("x", lc.App(lc.Var("f"), lc.Var("x")))
b = lc.Var("f")
print(lc.defeq(a, b))  # True (eta)

Interactive Reduction Player (HTML)

In a notebook, render an interactive step-by-step beta trace.

from IPython.display import HTML, display

expr = r"(lambda x. x) (lambda y. y)"
display(HTML(lci.format_reduction_player(expr, max_steps=8, title="β-trace")))

Church Booleans (and Lazy IF in Python)

Church booleans are functions. In eager Python, use IF_THUNK so only one branch is evaluated.

print(ch.to_bool(ch.AND(ch.TRUE)(ch.FALSE)))     # False
print(ch.to_bool(ch.OR(ch.FALSE)(ch.TRUE)))      # True
print(ch.to_bool(ch.NOT(ch.FALSE)))              # True

x = ch.IF_THUNK(ch.TRUE)(lambda: "then")(lambda: 1 / 0)
print(x)  # "then"

Church Numerals (Conversions + Arithmetic)

Numerals are iterators. Convert with from_int/to_int.

n = ch.from_int(3)
m = ch.from_int(4)

print(ch.to_int(ch.add(n)(m)))   # 7
print(ch.to_int(ch.mul(n)(m)))   # 12
print(ch.to_int(ch.pred(n)))     # 2
print(ch.to_bool(ch.eq_church(n)(m)))  # False

Recursion (Fixpoints) in Eager Python

Use the strict fixpoint Z plus IF_THUNK.

one = ch.from_int(1)

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

print(ch.to_int(FACT(ch.from_int(5))))  # 120

Curry-Howard (STLC Proof Terms)

Types are propositions; terms are proofs. Use st.check_goal to validate.

A = st.TyVar("A")
B = st.TyVar("B")

idA = st.Lam("x", A, st.Var("x"))
st.check_goal("id", idA, st.Arrow(A, A))

# Or-commutativity: (A ∨ B) -> (B ∨ A)
or_comm = st.Lam(
    "p",
    st.Or(A, B),
    st.Case(
        st.Var("p"),
        "a",
        st.Inr(st.Var("a"), B),  # A -> Or(B,A)
        "b",
        st.Inl(st.Var("b"), A),  # B -> Or(B,A)
    ),
)
st.check_goal("or_comm", or_comm, st.Arrow(st.Or(A, B), st.Or(B, A)))

Sequent Calculus (Search + Extraction + Proof Trees)

Prove a goal, extract a natural-deduction term, and render the sequent proof tree.

from IPython.display import HTML, display

A = sq.Atom("A")
B = sq.Atom("B")
goal = sq.Imp(A, sq.Imp(B, A))  # A -> (B -> A)

pf, term = sq.prove_and_extract(goal, depth=14)
print("term:", sq.show_t(term))
display(HTML(sq.render_proof_tree(pf)))

Denotational Semantics: Least Fixed Point via Kleene Chain

Approximate lfp(F) = sup_n F^n(⊥) by iterating F from the bottom function.

BOTTOM = None

def kleene_chain(F, steps=6):
    f = lambda n: BOTTOM
    out = [f]
    for _ in range(steps):
        f = F(f)
        out.append(f)
    return out

def FactF(f):
    def g(n):
        if n < 0:
            return BOTTOM
        if n == 0:
            return 1
        prev = f(n - 1)
        return BOTTOM if prev is BOTTOM else n * prev
    return g

for k, fk in enumerate(kleene_chain(FactF, steps=6)):
    print(k, [fk(n) for n in range(7)])

NbE (Normalization by Evaluation) for STLC

Compare naive beta-rewriting traces to NbE normalization.

ex = nbe.build_basic_examples()
id_tm = ex["id_tm"]
id_ty = ex["id_ty"]

print("NbE:", nbe.show_tm(nbe.nbe(id_tm, id_ty)))

trace = nbe.beta_trace(id_tm, max_steps=4)
print("beta steps:", [nbe.show_tm(t) for t in trace])

Dependent-Type Codes (Executable Model)

PiCode is a dependent function type; SigmaCode is a dependent pair type.

Nat = dep.NatCode()
Bool = dep.BoolCode()

VecBool = lambda n: dep.VecCode(Bool, n)
exists_vec = dep.SigmaCode(Nat, lambda n: VecBool(n))

print(dep.is_in((0, []), exists_vec, depth=6))
print(dep.is_in((3, [True, False, True]), exists_vec, depth=6))

# head : Π n. Vec(Bool,n+1) -> Bool
head_ty = dep.PiCode(Nat, lambda n: dep.implies_code(VecBool(n + 1), Bool))
head = lambda n: (lambda xs: xs[0])
print(dep.is_in(head, head_ty, depth=5))

Classical Control (callcc) Patterns

Use callcc as an escape continuation (early exit, backtracking witnesses).

print(cc.first_satisfying([1, 3, 8, 9], lambda x: x % 2 == 0, default=None))
print(cc.subset_sum_first([3, 5, 6, 7, 9], 14))  # witness subset summing to 14 (or None)

System F (Explicit Polymorphism)

Type abstraction is TyLam; type application is TyApp. Full inference is not automatic, so instantiate explicitly.

id_term = sf.TyLam("a", sf.Lam("x", sf.TVar("a"), sf.Var("x")))
print("id:", sf.show_tm(id_term))
print("type:", sf.show_ty(sf.infer(id_term, {}, set())))

use = sf.App(sf.TyApp(id_term, sf.TInt()), sf.IntLit(7))
print("use:", sf.show_tm(use))
print("type:", sf.show_ty(sf.infer(use, {}, set())))