The λ-calculus

Se basa en

Requisitos previos obligatorios, hasta el fondo: 15

Aprenderás a

• Reduce λ-terms and encode booleans, pairs and natural numbers (Church numerals).
• Use a fixed-point combinator to define recursive functions, and explain why untyped terms need not terminate.
• State the Church–Rosser theorem and explain why every simply typed term has a normal form.

Definición

• λ-terms are built from variables by application (M N) and abstraction (λx. M).
• β-reduction rewrites (λx. M) N to M[N/x], using capture-avoiding substitution.
• A term is in normal form if no β-reduction applies to it.

Teorema

• Church–Rosser: β-reduction is confluent, so a term has at most one normal form.
• The untyped λ-calculus computes exactly the partial recursive functions.
• Every simply typed λ-term has a normal form; in fact the simply typed λ-calculus is strongly normalising.

Errores frecuentes

• Substituting without renaming bound variables (variable capture).
• Thinking every λ-term has a normal form; (λx. x x)(λx. x x) does not.

Conduce a

Descubrimientos opcionales

• Categorical logic The simply typed λ-calculus with products is an internal language for cartesian closed categories (Lambek).
• ← Products, coproducts, initial and terminal objects
• ← Adjunctions
• ← Computability

Itinerarios de aprendizaje

• Computer science and formal methods

Lecturas complementarias

• H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics (1981)
• J. Roger Hindley and Jonathan P. Seldin, Lambda-Calculus and Combinators: An Introduction (2008)
• Benjamin C. Pierce, Types and Programming Languages (2002)