# Lambda Calculus

## General Notice

• Exam: The oral exam will be held on February 8, 2018.
• This course overlaps with the second half of the course Equational Logic and Lambda Calculus (IN2048). Only one of the two courses can be credited towards your degree.
• There will be weekly homework sheets, which will be graded. Students who achieve 50% of the homework points will receive a bonus mark of 0.3, provided that they also pass the final exam.

## Contents

### 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.