Tag
lambda-calculus
- Aug 6, 2026 Abstract Machines: The CEK, the Krivine Machine, and Closure Conversion How an evaluator becomes an explicit state machine with a control string, an environment, and a continuation, and what each of the three registers costs. computation theory
- Apr 30, 2026 Böhm Trees, Separability, and What Normal Forms Cannot Distinguish Why beta-eta equivalence fails to identify terms that agree on every argument, how Böhm trees record the observable behaviour of a term, and where the separability theorem stops. computation theory
- Apr 22, 2026 Alpha-Equivalence and de Bruijn Indices in the Lambda Calculus Why the names of bound variables carry no information, how alpha-equivalence is defined, and how nameless indices turn it into structural equality with a shift operation. computation theory
- May 27, 2025 Bracket Abstraction: Compiling Lambda Terms into Combinators How the lambda-free basis S and K can express every abstraction, the translation that removes binders one at a time, and why the naive translation explodes in size. computation theory
- Mar 30, 2025 Fixed-Point Combinators and How Recursion Enters a Nameless Calculus Why a finite lambda term cannot refer to itself, how the Y and Turing combinators manufacture self-reference through duplication, and what the Z variant fixes about call-by-value. computation theory
- Jan 28, 2025 Capture-Avoiding Substitution and the Substitution Lemma Why naive textual replacement of a variable silently changes the meaning of a term, how renaming repairs it, and what the substitution lemma guarantees about the interaction with reduction. computation theory
- Dec 4, 2024 Eta Conversion, Extensionality, and When Two Functions Are the Same What the eta rule asserts about functions that differ only in an unused argument, why it is unsound under call-by-value, and how eta-expansion survives in compilers as an arity fix. computation theory
- Nov 21, 2024 Proof Terms: Reading a Derivation as a Program The correspondence between natural-deduction proofs and typed lambda terms, why normalisation is evaluation, and which logical principles correspond to which programming constructs. computation theory
- Jan 28, 2024 Church Encodings and the Cost of Representing Data as Functions How numerals, booleans, and pairs are built from nothing but abstractions, why predecessor is the hard case, and what unary representation costs in reduction steps. computation theory
- Nov 7, 2023 Beta Reduction and the Consequences of Evaluation Order How the single rewrite rule of the lambda calculus produces drastically different programs depending on where it is applied, and why normal order finds a value whenever one exists. computation theory
- Jun 15, 2022 Confluence and the Church-Rosser Theorem for Beta Reduction Why the order of beta reductions cannot change the final answer, how the diamond property is proved by parallel reduction, and what the standardisation theorem adds. computation theory