Definitions Index

Definitions Index#

This page lists the canonical definitions used throughout the book and where they appear.

Reading Guide

Some concepts appear in two forms:

  • Symbolic AST form (Var, Lam, App) for proof traces.

  • Executable Church/Python form for computation experiments.

Core Lambda Syntax (AST)#

  • Introduced in: notebooks/01_lambda_basics

  • Canonical implementation: lc_core.py

  • Names:

    • Var, Lam, App

    • variable analysis: free_vars, all_vars

    • alpha-renaming: alpha_rename

    • capture-avoiding substitution: subst

Reduction Engines#

  • Canonical implementation: lc_core.py

  • Names:

    • beta-step reducers: beta_step_normal, beta_step_applicative

    • normalization: normalize, nf, trace_reduce

    • eta: eta_step, eta_nf

  • Interactive traces + diffs: lc_interactive.py

Church Booleans and Logic#

  • Introduced in: notebooks/03_church_booleans_logic

  • Canonical implementation: church_core.py

  • Names:

    • TRUE, FALSE, IF, IF_THUNK

    • AND, OR, NOT, IMPLIES

    • helpers: to_bool

Church Numerals and Arithmetic#

  • Introduced in: notebooks/05_church_numerals

  • Canonical implementation: church_core.py

  • Names:

    • numerals and conversions: church, to_int, from_int

    • arithmetic: succ, add, mul, pred, sub

    • predicates: is_zero, leq_church, eq_church

    • pairs: pair, fst, snd

Fixpoints and Recursion#

  • Introduced in: notebooks/06_recursion_fixpoints

  • Canonical implementation:

    • Z is exported by church_core.py (used across Chapters 6-9)

    • Y appears only as a reference (not executed in eager Python)

  • Recursive Church examples (FACT, POW): notebooks/06_recursion_fixpoints

Logic as Types (STLC)#

  • Introduced in: notebooks/04_propositional_logic

  • Canonical implementation: stlc_core.py

  • Names:

    • type constructors: Arrow, And, Or, Unit, Void

    • typing: type_of

Induction Proof Objects#

  • Chapter 8 symbolic proof scripts (beta/eta/alpha-aware equality): notebooks/08_induction

  • Chapter 9 witness objects and theorem iterators:

    • theorem1_forall, theorem2_forall, theorem3_forall, theorem4_forall, theorem5_forall

    • notebooks/09_induction_arithmetic

Fast Verification Layer (Chapter 9)#

  • Decoded equality/order helpers (eq, leq, lt): notebooks/09_induction_arithmetic

  • Fast modulo helper mod (with mod 0 undefined): notebooks/09_induction_arithmetic

Advanced Modules (Chapters 12-16)#

Chapters 12-16 rely on small prototype modules under advanced/:

  • NbE prototype: advanced/stlc_nbe.py

  • Dependent-types toy code: advanced/dependent_codes.py

  • Sequent calculus search/extraction: advanced/sequent_imp.py

  • Control operators: advanced/classical_control.py

  • System F core: advanced/systemf_core.py

Scope Note

Chapter 4 is intuitionistic propositional logic (Curry-Howard in STLC). Chapters 1-3 and 5-9 primarily use untyped lambda encodings and meta-level proof tooling.

Contents