Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Substitution in the lambda Calculus and the role of the Curry School

Fairouz Kamareddine

TL;DR

This work surveys how the Curry school approached substitution in the lambda calculus, focusing on the interplay between $α$-congruence and substitution and tracing the path from grafting to ordered-variable replacement and beyond. It develops two coherent routes to define syntactic equivalence modulo bound-variable names, $=_{α}$ and $=_{α'}$, and introduces two beta-reduction families, $β'$ and $β''$, that preserve the Church-Rosser property when paired with their respective equivalences. The discussion then moves to the de Bruijn index formulation and finally to explicit substitutions, showing how these formalisms support implementation while preserving semantic integrity. Overall, the paper highlights how historical insights from Hindley and Seldin illuminate a practical, implementation-friendly theory of substitution in the lambda calculus with a clear bridge from syntax to execution.

Abstract

Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the lambda calculus, we cannot define alpha congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of alpha congruence (e.g., when we take lambda terms modulo bound variables). Students on a lambda calculus course usually find this confusing. The elegant writings and research of the Curry school have settled this problem very well. This article is an ode to the contributions of the Curry school (especially the excellent book of Hindley and Seldin) on the subject of alpha congruence and substitution.

Substitution in the lambda Calculus and the role of the Curry School

TL;DR

This work surveys how the Curry school approached substitution in the lambda calculus, focusing on the interplay between -congruence and substitution and tracing the path from grafting to ordered-variable replacement and beyond. It develops two coherent routes to define syntactic equivalence modulo bound-variable names, and , and introduces two beta-reduction families, and , that preserve the Church-Rosser property when paired with their respective equivalences. The discussion then moves to the de Bruijn index formulation and finally to explicit substitutions, showing how these formalisms support implementation while preserving semantic integrity. Overall, the paper highlights how historical insights from Hindley and Seldin illuminate a practical, implementation-friendly theory of substitution in the lambda calculus with a clear bridge from syntax to execution.

Abstract

Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the lambda calculus, we cannot define alpha congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of alpha congruence (e.g., when we take lambda terms modulo bound variables). Students on a lambda calculus course usually find this confusing. The elegant writings and research of the Curry school have settled this problem very well. This article is an ode to the contributions of the Curry school (especially the excellent book of Hindley and Seldin) on the subject of alpha congruence and substitution.
Paper Structure (17 sections, 11 theorems, 19 equations, 2 figures, 1 table)

This paper contains 17 sections, 11 theorems, 19 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. The Syntax and Denotational Semantics of the $\lambda$-calculus
  3. Computing $\lambda$-terms
  4. Defining ${A}_{v:=B}$ as Grafting $A\{v:=B\}$ does not work
  5. Free and bound occurrences of variables
  6. Defining ${A}_{v:=B}$ as Replacement $A\langle\langle v:=B\rangle\rangle$ Using Ordered Variables
  7. Syntactic identity revised, Searching for $\equiv$
  8. Defining $=_\alpha$ using the replacement based on ordered variables
  9. Defining $=_{\alpha'}$
  10. Beta Reduction
  11. Computation ${\beta'}$-reduction based on $=_\alpha$
  12. ${\beta"}$-reduction based on clean terms and $=_{\alpha'}$
  13. Equating terms modulo $\equiv$
  14. The $\lambda$-calculus with de Bruijn indices, towards Explicit Substitutions
  15. The classical $\lambda$-calculus with de Bruijn indices
  16. ...and 2 more sections

Key Result

Lemma 1

Figures (2)

  • Figure 1: The $\lambda s$-rules
  • Figure 2: The new rules of the $\lambda s_e$-calculus

Theorems & Definitions (48)

  • Definition 2: $\lambda$-terms in ${\cal M}$
  • Definition 3: Compatibility
  • Definition 4: Strict Equality $=_{\cal M}$
  • Definition 5: $\texttt{ENV}$, Changing Environments
  • Definition 6: Denotational meaning of terms
  • Definition 7: Grafting $A\{v:=B\}$
  • Definition 8: Term Occurrence
  • Definition 9: Scope, Free/Bound Occurrences, Combinator
  • Definition 10: Replacement $A \langle \langle v:=B\rangle\rangle$ using ordered variables
  • Lemma 1
  • ...and 38 more