Last time
Γ ⊢ M : ?
1/ 18
This time
Γ ⊢ A
2/ 18
A suggestive notation
A → B
∀α.A
∃α.A
Curry-Howard
3/ 18
A suggestive notation
A → B
∀α.A
∃α.A
A× B
A+ B
Curry-Howard
3/ 18
A suggestive notation
A → B
∀α.A
∃α.A
A ∧ B
A ∨ B
Curry-Howard
3/ 18
A suggestive notation
A → B
∀α.A
∃α.A
A ∧ B
A ∨ B
Types correspond to propositions
Curry-Howard
3/ 18
A suggestive notation
A → B
∀α.A
∃α.A
A ∧ B
A ∨ B
Types correspond to propositions
(Part 1 of the Curry-Howard correspondendence)
3/ 18
What logic?
λ→
B A → B A ∧ B A ∨ B
What about first-order logic?
4/ 18
What logic?
λ→ corresponds to propositional logic
B A → B A ∧ B A ∨ B
What about first-order logic?
4/ 18
What logic?
λ→ corresponds to propositional logic
B A → B A ∧ B A ∨ B
System F
∀α.A ∃α.A
What about first-order logic?
4/ 18
What logic?
λ→ corresponds to propositional logic
B A → B A ∧ B A ∨ B
System F corresponds to second-order propositional logic
∀α.A ∃α.A
What about first-order logic?
4/ 18
What logic?
λ→ corresponds to propositional logic
B A → B A ∧ B A ∨ B
System F corresponds to second-order propositional logic
∀α.A ∃α.A
System Fω
λα.A A B
What about first-order logic?
4/ 18
What logic?
λ→ corresponds to propositional logic
B A → B A ∧ B A ∨ B
System F corresponds to second-order propositional logic
∀α.A ∃α.A
System Fω corresponds to higher-order propositional logic
λα.A A B
What about first-order logic?
4/ 18
What logic?
λ→ corresponds to propositional logic
B A → B A ∧ B A ∨ B
System F corresponds to second-order propositional logic
∀α.A ∃α.A
System Fω corresponds to higher-order propositional logic
λα.A A B
What about first-order logic?
4/ 18
Propositional vs predicate
Propositional logic
P → Q
(∀P.P → P) → (∃Q.Q → Q)
Predicate logic (FOPL)
P(x)
∀x ∈ A.P(x)
5/ 18
Lambda and logic cubes
Fω // λC
F
??�������
// λP2
??�������
λω //
OO
λPω
OO
λ→ //
??������
OO
λP
??������
OO
6/ 18
Lambda and logic cubes
Fω // λC
F
??�������
// λP2
??�������
λω //
OO
λPω
OO
λ→ //
??������
OO
λP
??������
OO
propω // predω
prop2
??�������
// pred2
??�������
propω //
OO
predω
OO
prop //
??������
OO
pred
??������
OO
6/ 18
More suggestive notation
Γ ⊢ M : A → B Γ ⊢ N : A
Γ ⊢ M N : B
Γ ⊢ A → B Γ ⊢ A
Γ ⊢ B
Terms correspond to proofs
Curry-Howard
7/ 18
More suggestive notation
Γ ⊢ M : A → B Γ ⊢ N : A
Γ ⊢ M N : B
Γ ⊢ A → B Γ ⊢ A
Γ ⊢ B
Terms correspond to proofs
Curry-Howard
7/ 18
More suggestive notation
Γ ⊢ M : A → B Γ ⊢ N : A
Γ ⊢ M N : B
Γ ⊢ A → B Γ ⊢ A
Γ ⊢ B
Terms correspond to proofs
Curry-Howard
7/ 18
More suggestive notation
Γ ⊢ M : A → B Γ ⊢ N : A
Γ ⊢ M N : B
Γ ⊢ A → B Γ ⊢ A
Γ ⊢ B
Terms correspond to proofs
(Part 2 of the Curry-Howard correspondendence)
7/ 18
Inference rules for →
x : A ∈ Γ
tvar
Γ ⊢ x : A
A ∈ Γ
Γ ⊢ A
Γ, x : A ⊢ M : B
→-intro
Γ ⊢ λx:A.M : A → B Γ, A ⊢ B
Γ ⊢ A → B
Γ ⊢ M : A → B
Γ ⊢ N : A →-elim
Γ ⊢ M N : B
Γ ⊢ A → B
Γ ⊢ A
Γ ⊢ B
8/ 18
Inference rules for ×
Γ ⊢ M : A Γ ⊢ N : B ×-intro
Γ ⊢ ⟨M, N⟩ : A× B
Γ ⊢ A Γ ⊢ B ∧-intro
Γ ⊢ A ∧ B
Γ ⊢ M : A× B ×-elim-1
Γ ⊢ fst M : A
Γ ⊢ M : A× B ×-elim-2
Γ ⊢ snd M : B
Γ ⊢ A ∧ B ∧-elim-1
Γ ⊢ A
Γ ⊢ A ∧ B ∧-elim-2
Γ ⊢ B
9/ 18
Classical vs intuitionistic logic
Classical logic
Emphasis on truth
Truth values: ⊤, ⊥
A ∨ ¬A always holds
Intuitionistic logic
Emphasis on proof
Proofs inhabit propositions
A ∨ ¬A doesn’t hold in general
10/ 18
Brouwer-Heyting-Kolmogorov (BHK) interpretation
A proof of A → B:
a function that builds a proof of B from a proof of A.
A proof of A ∧ B:
a pair of a proof of A and a proof of B.
¬A
means A → ⊥
⊥
has no proof
11/ 18
Continuing the correspondence
Types correspond to propositions
Programs correspond to proofs
Curry-Howard
12/ 18
Continuing the correspondence
Types correspond to propositions
Programs correspond to proofs
Evaluation corresponds to proof simplification
Curry-Howard
12/ 18
Continuing the correspondence
Types correspond to propositions
Programs correspond to proofs
Evaluation corresponds to proof simplification
(The three-part Curry-Howard correspondendence)
12/ 18
Who should care?
Language designers
e.g. linear logic : restrictions on structural rules
corresponds to a language with resource management guarantees
Logicians
since results about programming languages transfer “for free”
e.g. strong normalization implies consistency
Authors (and users) of proof assistants
e.g. Coq and other tools based on type theory
Programmers?
13/ 18
Logical equivalences
∀β.(∀α.(Pα → β)) → β ↔ ∃α.Pα
∀β.(P → β) ∧ (Q → β) → β ↔ P ∨ Q
Proof: we must show
∀β.(∀α.(Pα → β)) → β ⊢ ∃α.Pα
∃α.Pα ⊢ ∀β.(∀α.(Pα → β)) → β
etc .
14/ 18
A proof
Let Γ = ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
15/ 18
A program from a proof
Let Γ = ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
15/ 18
A program from a proof
Let Γ = ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
∃-intro
Γ, α, v : Pα ⊢ pack α, v as ∃α.Pα : ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
15/ 18
A program from a proof
Let Γ = ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
∃-intro
Γ, α, v : Pα ⊢ pack α, v as ∃α.Pα : ∃α.Pα
→-intro
Γ, α ⊢ λv : Pα.pack α, v as ∃α.Pα : Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
15/ 18
A program from a proof
Let Γ = ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
∃-intro
Γ, α, v : Pα ⊢ pack α, v as ∃α.Pα : ∃α.Pα
→-intro
Γ, α ⊢ λv : Pα.pack α, v as ∃α.Pα : Pα → ∃α.Pα
∀-intro
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
15/ 18
A program from a proof
Let Γ = ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
∃-intro
Γ, α, v : Pα ⊢ pack α, v as ∃α.Pα : ∃α.Pα
→-intro
Γ, α ⊢ λv : Pα.pack α, v as ∃α.Pα : Pα → ∃α.Pα
∀-intro
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
Left subtree:
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
15/ 18
A program from a proof
Let Γ = H : ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
∃-intro
Γ, α, v : Pα ⊢ pack α, v as ∃α.Pα : ∃α.Pα
→-intro
Γ, α ⊢ λv : Pα.pack α, v as ∃α.Pα : Pα → ∃α.Pα
∀-intro
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
Left subtree:
Γ ⊢ H : ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
15/ 18
A program from a proof
Let Γ = H : ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
∃-intro
Γ, α, v : Pα ⊢ pack α, v as ∃α.Pα : ∃α.Pα
→-intro
Γ, α ⊢ λv : Pα.pack α, v as ∃α.Pα : Pα → ∃α.Pα
∀-intro
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
Left subtree:
Γ ⊢ H : ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ H [∃α.Pα] : (∀α.Pα → ∃α.Pα) → ∃α.Pα
15/ 18
A program from a proof
Let Γ = H : ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
. . . ∀-intro
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
Left subtree:
. . . ∀-elim
Γ ⊢ H [∃α.Pα] : (∀α.Pα → ∃α.Pα) → ∃α.Pα
Finally:
Γ ⊢ H [∃α.Vα] : (∀α.Pα → ∃α.Pα) → ∃α.Pα
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
15/ 18
A program from a proof
Let Γ = H : ∀β.(∀α.Pα → β) → β. Then
Γ ⊢ ∀β.(∀α.Pα → β) → β
∀-elim
Γ ⊢ (∀α.Pα → ∃α.Pα) → ∃α.Pα
∃-intro
Γ, α, Pα ⊢ ∃α.Pα
→-intro
Γ, α ⊢ Pα → ∃α.Pα
∀-intro
Γ ⊢ ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ ∃α.Pα
Right subtree:
. . . ∀-intro
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
Left subtree:
. . . ∀-elim
Γ ⊢ H [∃α.Pα] : (∀α.Pα → ∃α.Pα) → ∃α.Pα
Finally:
Γ ⊢ H [∃α.Vα] : (∀α.Pα → ∃α.Pα) → ∃α.Pα
Γ ⊢ Λα.λv : Pα.pack α, v as ∃α.Pα : ∀α.Pα → ∃α.Pα
→-elim
Γ ⊢ H [∃α.Vα] (Λα.λv : Pα.pack α, v as ∃α.Pα) : ∃α.Pα
15/ 18
Is it useful?
∀β.(P → β) ∧ (Q → β) → β ↔ P ∨ Q
These type equivalences can be useful in constructing programs.
The data type encodings we saw last week can be derived this way.
16/ 18
Closing thoughts
The correspondence suggests a way of thinking about programming
— and a way of systematically constructing (some) programs
However, propositional logic is quite weak
(and our types are often uninformative)
We’ll have richer types available later (GADTs, monads),
at which point we’ll revisit the question of usefulness
17/ 18
Next time
Abstraction
18/ 18