The Curry-Howard Correspondence

Simply Typed Lambda Calculus (STLC) Definition

• Core typed functional language

• Variables, abstraction λ(x:τ).e, and application e u

• Types: base types ι or function types τ → σ

• Terminating and deterministic

STLC Type Rules

• Variables: (x:τ)∈Γ implies Γ ⊢ x:τ

• Abstraction: Γ,x:τ ⊢ e:σ implies Γ ⊢ λ(x:τ).e : τ→σ

• Application: Γ ⊢ e:τ→σ and Γ ⊢ u:τ implies Γ ⊢ e u : σ

STLC Termination Property

• STLC is terminating
• No expression reduces indefinitely
• Not Turing complete, unlike untyped λ-calculus

Recursion via fix Operator

• Fix operator adds recursion
• fix (λx.e) reduces to e[x := fix (λx.e)]
• Type rule: Γ ⊢ e : τ → τ implies Γ ⊢ fix e : τ

isEven via fix

• f = λ(isEven:ℕ→𝔹).λ(x:ℕ)
• if (isZero x) then true
• else if (isZero (x-1)) then false
• else isEven (x-2)
• fix f gives recursive isEven

Natural Deduction Rules

• For intuitionistic logic: axioms, ⊤-I, ⊥-E, ⇒-I, ⇒-E, ∧-I, ∧-E, ∨-I, ∨-E
• Propositions from atomic p, implication ⇒, conjunction ∧, disjunction ∨, truth ⊤, falsity ⊥

Curry-Howard Correspondence Core Insight

• Proofs in intuitionistic natural deduction correspond to programs in STLC
• Types correspond to logical propositions, terms correspond to proofs

Implication and Function Correspondence

• Γ,x:τ ⊢ x:τ corresponds to Δ,A ⊢ A (axiom)
• Γ,x:τ ⊢ e:σ implies Γ ⊢ λ(x:τ).e:τ→σ corresponds to Δ,A ⊢ B implies Δ ⊢ A⇒B (⇒-I)
• Γ ⊢ e:τ→σ and Γ ⊢ u:τ implies Γ ⊢ e u:σ corresponds to Δ ⊢ A⇒B and Δ ⊢ A implies Δ ⊢ B (⇒-E)

Curry-Howard Theorem Statement

• A proposition A₁,…,Aₙ ⊢ A derivable in intuitionistic logic
• there exists a term t such that x₁:τ₁,…,xₙ:τₙ ⊢ t:τ
• each proposition corresponds to a type

Composition as Logical Tautology

• λ(f:σ→δ).λ(g:τ→σ).λ(x:τ).f(g x)
• corresponds to logical tautology (B⇒C) ⇒ (A⇒B) ⇒ A ⇒ C

Conjunction and Product Correspondence

• Γ ⊢ t:τ and Γ ⊢ s:σ implies Γ ⊢ (t,s):τ×σ
• corresponds to Δ ⊢ A and Δ ⊢ B implies Δ ⊢ A∧B (∧-I)
• Pairs correspond to conjunction introduction

Disjunction and Sum Correspondence

• Γ ⊢ t:τᵢ implies Γ ⊢ inl/inr t : τ₁+τ₂
• corresponds to Δ ⊢ Aᵢ implies Δ ⊢ A₁∨A₂ (∨-I)
• Sum types correspond to disjunction introduction

Truth and Unit Correspondence

• Γ ⊢ () : Unit corresponds to Δ ⊢ ⊤ (⊤-I)
• Unit type with exactly one value corresponds to logical truth

Falsity and Void Correspondence

• Γ ⊢ e : Void implies Γ ⊢ magic e : τ
• corresponds to Δ ⊢ ⊥ implies Δ ⊢ A (⊥-E)
• Empty type corresponds to logical falsity, with ex falso quodlibet

Beyond Intuitionistic Logic

• Intuitionistic logic rejects the law of excluded middle (A ⇒ A)
• Corresponds to control operators like call/cc with type ((a→b)→a)→a