程序代写代做代考 Last time

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