Lambda Calculus

Untyped Lambda calculus

Syntax

Terms, notational conventions, Currying, static binding, free and bound variables, substitution, alpha-conversion.

Beta-reduction

Definition of beta-reduction. Definition of parallel reduction >. Proof that > has the diamond property. Because > ^* = → _β ^* this implies that β-reduction is confluent. (See confluence proof for orthogonal TRS)

Eta-reduction

Motivation, definition and basic properties: termination and (local) confluence. No proofs.

Reduction strategies

Without proof: contraction of leftmost β-redexes leads to a normal form if one exists.

Lambda calculus as a programming language

Booleans, pairs, Church numerals, fixed-point combinators.

Typed Lambda calculus

Simply typed lambda calculus

Simple types. Implicitly and explicitly typed terms. Type checking rules. Properties: 1. beta-reduction preserves types ("subject reduction") (w/o proof). 2. beta-reduction terminates on type-correct terms (w/o proof). Thus beta-equivalence is decidable for type-correct terms (but has non-elementary complexity). Corollary The simply-typed lambda-calculus can only represent total functions. Thm Every computable functions is representable as a closed type-correct lambda-term whose only contants are additional fixed-point combinators (proof only sketched).

Type inference

The rules. Type-correct terms no longer have a unique type but still a most general type. Proof by a concrete Prolog-like interpretation of the typing rules as backward computation rules.

Let-polymorphism

Universally quantified type schemas. Typing rules for "let" and for type schemas. Syntax-directed typing rules with built-in quantifier handling.

Curry-Howard isomorphism

Types = formulas, lambda-terms = proofs, beta-reduction = proof-reduction. Proof of the subterm property of proofs in normal form. Proof of decidability of intuitionistic propositional logic via proofs in normal form.