---
title: "The Calculi of Lambda-Conversion"
authors:
  - "Alonzo Church"
year: 1941
venue: "Annals of Mathematics Studies, Princeton University Press"
arxiv: null
doi: null
source: "https://press.princeton.edu/books/paperback/9780691083940/the-calculi-of-lambda-conversion"
topics:
  - lambda-calculus
  - church
  - conversion
seed_rank: 511
seed_batch: "foundations-greats-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 10
lineage: foundations-of-computing
cites:
  - title: "An Unsolvable Problem of Elementary Number Theory"
    url: "https://doi.org/10.2307/2371045"
    year: 1936
    arxiv: null
    doi: "10.2307/2371045"
  - title: "A Formulation of the Simple Theory of Types"
    url: "https://doi.org/10.2307/2266170"
    year: 1940
    arxiv: null
    doi: "10.2307/2266170"
  - title: "Computability and λ-Definability"
    url: "https://doi.org/10.2307/2268280"
    year: 1937
    arxiv: null
    doi: "10.2307/2268280"
  - title: "The Mechanical Evaluation of Expressions"
    url: "https://doi.org/10.1093/comjnl/6.4.308"
    year: 1964
    arxiv: null
    doi: "10.1093/comjnl/6.4.308"
  - title: "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I"
    url: "https://doi.org/10.1145/367177.367199"
    year: 1960
    arxiv: null
    doi: "10.1145/367177.367199"
  - title: "Computational lambda-calculus and monads"
    url: "https://doi.org/10.1109/LICS.1989.39155"
    year: 1989
    arxiv: null
    doi: "10.1109/LICS.1989.39155"
see:
  - "507-an-unsolvable-problem-of-elementary-number-theory"
  - "510-a-formulation-of-the-simple-theory-of-types"
  - "517-computability-and-lambda-definability"
  - "617-the-mechanical-evaluation-of-expressions"
  - "575-recursive-functions-of-symbolic-expressions-and-their-comput"
  - "037-computational-lambda-calculus-and-monads"
---

# The Calculi of Lambda-Conversion

## One-sentence takeaway

Church's 1941 monograph is the systematic book on λ-conversion: substitution, λI versus λK, normal forms, and the link to effective calculability.

## Why it matters here

Every later λ / monad / effects card in the corpus sits on this notation. Ano still writes abstraction and application the way this book standardized them; Landin, McCarthy, and Moggi are commentary.

## Key ideas

- Distinguishes the λI-calculus (abstraction only when the variable occurs free) from the λK-calculus (unrestricted abstraction, including constant functions).
- Develops conversion, α-renaming, substitution with capture-avoidance, and the Church–Rosser property as the discipline of equality.
- Treats λ-definable functions of natural numbers as the official notion of effective calculability inherited from the 1936 papers.
- Princeton Annals of Mathematics Study that fixed the modern syntax of λ.

## Caveats

## Links

- Princeton: https://press.princeton.edu/books/paperback/9780691083940/the-calculi-of-lambda-conversion