Simply Typed $𝜆$ -calculus

Simply typed $𝜆$ -calculus, also known as STLC, is the most basic type system on can equip $𝜆$ -calculus with.

On the logical side, STLC corresponds to propositional logic. On the semantic side, STLC corresponds to cartesian-closed categories.

Definition

Syntax

For this section, assume we have a (possibly infinite) set $𝒯︀$ of atomic types. A type $𝜏$ is defined by the following grammar:

\begin{aligned} 𝜏 ≔ & 𝑇 \in 𝒯︀ \\ | & 𝜏 \to 𝜏 \end{aligned}

We equip the previewλ-calculus with the following type system.

𝑥 : 𝜏 \in Γ

Γ ⊢ 𝑥 : 𝜏

Γ, 𝑥 : 𝜏 ⊢ 𝑡 : 𝜏^{'}

Γ ⊢ 𝜆 𝑥 . 𝑡 : 𝜏 \to 𝜏^{'}

Γ ⊢ 𝑢 : 𝜏 \to 𝜏^{'}

Γ ⊢ 𝑣 : 𝜏

Γ ⊢ 𝑢 𝑣 : 𝜏^{'}

Semantics

Let $𝒞︀$ be a previewcartesian closed category, and a function $𝜌 : 𝒯︀ \to 𝒞︀$ that maps atomic types to objects of $𝒞︀$ . We can define an interpretation $⟦ - ⟧$ going from types to objects of $𝒞︀$ , as well as, for any open term $𝑡$ such that $Γ ⊢ 𝑡 : 𝜏$ , we have

⟦ 𝑡 ⟧ : ⟦ Γ ⟧ \to ⟦ 𝜏 ⟧

defined by induction on the typing derivation, where

⟦ 𝑥_{1} : 𝜏_{1}, \dots, 𝑥_{𝑛} : 𝜏_{𝑛} ⟧ = ⟦ 𝜏_{1} ⟧ \times \dots \times ⟦ 𝜏_{𝑛} ⟧

Axiom: by definition of a product, there exists a projection $⟦ Γ ⟧ \to ⟦ 𝜏 ⟧$ if $𝑥 : 𝜏 \in Γ$
Abstraction: by induction hypothesis, we have constructed a morphism $⟦ 𝑡 ⟧ : ⟦ Γ ⟧ \times ⟦ 𝜏 ⟧ ⟶ ⟦ 𝜏^{'} ⟧$ . By adjunction, this corresponds exactly to a morphism $⟦ 𝜆 𝑥 . 𝑡 ⟧ = 𝜆 (⟦ 𝑡 ⟧) : ⟦ Γ ⟧ ⟶ ⟦ 𝜏 ⟧ \Rightarrow ⟦ 𝜏^{'} ⟧$ .
Application: by induction hypothesis, we have $⟦ 𝑢 ⟧ : ⟦ Γ ⟧ ⟶ ⟦ 𝜏 ⟧ \Rightarrow ⟦ 𝜏^{'} ⟧$ and $⟦ 𝑣 ⟧ : ⟦ Γ ⟧ ⟶ ⟦ 𝜏 ⟧$ . By adjunction, the former morphism corresponds exactly to a $app (⟦ 𝑢 ⟧) : ⟦ Γ ⟧ \times ⟦ 𝜏 ⟧ ⟶ ⟦ 𝜏^{'} ⟧$ . Therefore, we have

Meta-theory

Strong normalization

Theorem Strong normalization Soit $𝑡$ un terme (potentiellement ouvert), tel qu’il existe un type $𝜏$ et un environnement $Γ$ tels que

Γ ⊢ 𝑡 : 𝜏

$𝑡$ est fortement normalisant.

In order prove this highly non-trivial result, we need to define an interpretation of types $⟦ 𝜏 ⟧$ , by induction on $𝜏$ 11 Note that, while it might be more intuitive would be to enforce that, if $𝑢 \in ⟦ 𝜏 ⟧$ , then $𝑢 : 𝜏$ . This would work, but it turns out this assumption is never used in the rest of the proof, and would add unnecessary complexity.:

$⟦ 𝑇 ⟧ ≔ {𝑢 : Term | 𝑢 is strongly normalizing}$
$⟦ 𝜏 \to 𝜏^{'} ⟧ ≔ {𝑢 : Term | \forall 𝑣 \in ⟦ 𝜏 ⟧, 𝑢 𝑣 \in ⟦ 𝜏^{'} ⟧}$

Simply Typed 𝜆-calculus