Introduction to the (un)typed lambda calculus

Included in this repository is a paper I wrote for the Applied Logic course (at the University of Antwerp) titled "Introduction into the (un)typed Lambda calculus".

Abstract

This paper serves as an introduction into the lambda calculus. It begins with an overview of the untyped lambda calculus. The different notations, operations, and encodings, such as abstraction, application, alpha conversion, beta reductions, Church numerals, arithmetic, etc. will be explained. Next, the paper will give an introduction into the simply typed lambda calculus. At each stage it will also pay attention to what one can and cannot do with the lambda calculus in its different forms. The concepts of Turing-completeness, decidability and the equivalence to other models of computability will be explored where appropriate.

Table of contents

• Untyped λ-calculus
  • Syntactic constructs
  • Abstraction and application
  • The substitution mechanism
  • Alpha
  • Beta
  • Eta
  • Encodings
    • Booleans
    • Pairs
    • Natural numbers
    • Arithmetic operations
  • Recursion
  • Normalisation, termination, and Turing completeness
• Simply Typed λ-calculus
  • Introduction into typing
  • Overview of typing systems
  • Contexts and inference
  • Typed reduction and termination