Abstracts.2021.STLCCC

Simply-Typed λ-Calculus and Cartesian Closed Categories

by Sandro Stucki and Andreas Abel

Three-part lecture series scheduled for Sep 16 and 23 and 30, 2021.

Part I: Simply-Typed λ-Calculus

Lecture given by Sandro Stucki.

• Recapitulation of simply-typed λ-calculus (STLC) with named bound variables, judgements Γ ⊢, ⊢ A, Γ ⊢ t : A, Γ ⊢ t = u : A, and function types A → B
• Internalization of substitutions as terms by adding judgements Δ ⊢ σ : Γ, Δ ⊢ σ = τ : Γ and explicit substitutions Δ ⊢ t ∘ σ : A
• Nameless representation of bound variables (de Bruijn style)
• Reduction of de Bruijn indices n to weakenings 0 ∘ pⁿ of the first de Bruijn index 0 by adding substitutions Γ, A ⊢ p : Γ
• Internalization of contexts as types by adding unit and product types 1 and A × B

Part II: Cartesian Closed Categories

Lecture given by Andreas Abel.

• Categories: Basic definition and structures of the algebra of functions
• Cartesian closed categories (CCCs) 𝒞 with a choice of
  • Terminal object 1 : 1 → 𝒞
  • Binary products -×- : 𝒞 × 𝒞 → 𝒞
  • Exponential/internal hom objects -A : 𝒞 → 𝒞 for each A : 𝒞

Part III: Exercises about the correspondence

In this part we plan to work out in groups (some) of the following topics:

• Prove the equivalence of the two definitions of Cartesian Closed Categories, CCC₁ with eval : BA × A → B and CCC₂ with apply(t : C → BA,u : C → A) : C → B (in Agda)
• Prove the equivalence of the two definitions of a CCC with a strong monad, ML₁ with bind : M(A) × M(B)A → M(B) and ML₂ with mu : M(M(A)) → M(A), M(t : A → B) : M(A) → M(B), tau : A × M(B) → M(A × B) (in Agda)
• Prove that the collection of substitutions for any name-free substitution calculus (with or without explicit weakening) form a category, this category has finite products, and this category is equivalent to the category of types if the calculus has finite products (in Agda)
• Do exercises from Andreas' ccc.pdf (with pen on paper)
• Read section 6.6 in Awodey's book (see literature below) and do exercise 14 (set-theoretic models of the theory of a reflexive domain) (with pen on paper or in Agda).

Slides, Notes, Exercises and Code

• Slides:

  • Part I

• Lecture notes and exercises:

  • Part II

• Code:

  • An Agda mechanization of the lectures
  • The agda-categories library contains Agda versions of most of the definitions, examples and exercises covered in the second lecture

Literature

Reading on this lecture:

• Wikipedia, Curry–Howard–Lambek-Correspondence
• Martín Abadi, Luca Cardelli, Pierre-Louis Curien and Jean-Jacques Lévy, Explicit Substitutions (aka the λσ-calculus)
• Andreas Abel, Lambda-Kalkül, Kapitel 7 (7.0, 7.3, 7.4) und 9 (9.0, 9.1, 9.3, 9.4) (in German)
• Jonathan Prieto-Cubides, The Simply Typed Lambda Calculus, slides: From named terms to de Bruijn terms; type-checking. Based on Agda code by gergoerdi
• Steve Awodey, Category theory, Section 6.6
• Joachim Lambek and Philip J. Scott, Introduction to higher order categorical logic

Further reading on categorical logic of typed λ-calculus:

• Simon Castellan and Pierre Clairambault and Peter Dybjer, Categories with Families: Unityped, Simply Typed, and Dependently Typed, see Section 4 for the simply-typed case
• nLab, Closed Cartesian multicategories

Further reading on λ-calculus:

• Peter Selinger, Lecture Notes on the Lambda Calculus
• Ralph Loader, Notes on Simply Typed Lambda Calculus
• Paul Blain Levy, Typed λ-calculus: course notes

Related talks:

• Andreas, Simply-typed lambda-calculus and cartesian closed categories
• Nachi, Categorical Combinators
• Andreas and Sandro, Simply-Typed λ-Calculus and Cartesian Closed Categories