Curry-Howard Isomorphism

Presented by Carl Eastlund
Transcribed by Sam Tobin-H.

Curry-Feys 58

Uses combinators instead of explicit lambda terms

Combinators	Axioms of P(=>)
K = \x.\y.x	A=> (B => A)
S = \x.\y.\z.(xz)(yz)	(A=>(B=>C))=>(A=>B)=>A=>C
Application	Modus Ponens

Matthias: What's the correspondence here?

Dave: propositions and types

Matthias: these are the basic axioms of logic

Howard 69, published 80

Implication

logic

lambda-calc

A |- A

x ^A

G,A |- B

G |- A=>B

(λ x ^A . M ^B ) ^A->B

G |- A; G |- A=>B

G |- B

( M ^A->B N ^A ) ^B

Propositions

Types

Proofs

Terms

Matthias: Types are propositions about programs

Strongly normalizing

( (λ x ^A . M ^B ) ^A->B N ^A ) ^B
reduces to
M ^B [ N ^A / x ^A ] ^B

Cut elimination is equivalent to beta reduction

Why must our language be strongly normalizing?

Ω : A for ANY A, this leads to inconsitency

Matthias: All programs are proofs, but what are they proofs of?

Negation

logic

lambda-calc

false, ~A := A => false

∅ , A -> ∅

false

( abort ^{∅
->A} M ^∅ ) ^A

Felix: how do we get M?

Carl: in unreachable parts of the program

Conjunction

logic

lambda-calc

B; A

A&B

< M ^A , N ^B > ^AxB

A&B

Π ₁ : AxB -> A

A&B

Π ₂ : AxB -> B

Matthias: note the correspondence between introduction and elimination rules. This was the inspiration for parts of HtDP.

Disjunction

logic

lambda-calc

A|B

( inl ^B M ^A ) ^A+B

A|B

( inr ^A M ^B ) ^A+B

G,A |- C; G,B |- C; G |- A|B

G |- C

( case T ^A+B of
inl x ^A => M ^C
inr x ^B => N ^C ) ^C

What don't we have?

effects
A | ~A -- the excluded middle
~~A -- double negation
quantification

Constructivism

Truth = Proof = Direct evidence

Neither the excluded middle nor double negation provide a witness

Quantification

logic

lambda-calc

(a not in G); G,a in t |- A(a)

G |- forall x in t.A(x)

(λ a ^t . M ^A(a) ) ^{forall x in t.A(x)}

a in t; G|- forall x in t.A(x)

G |- A(a)

( M ^{forall x in t.A(x)} a ^t ) ^A(a)

A(a); a in t

exists x in t.A(x)

< a ^t M ^A(a) > ^{exists x in t.A(x)}

G, a in t, A(a) |- C; G |- exists x in t.A(x)

G |- C

( let ( x ^t , u ^A ) = M ^{exists x in t.A(x)} in N ^C ) ^C

Griffin 90

Control operators = Classical logic

The following are the rules for the control operators from Friedman, Felleisen
E[A(M)] → M
E[C(M)] → Mλ z.A(E[z])

This gives us the following types
C : ((α→ false)→ false)→α
which is isomorphic to ~~A => A
A : β→α
which is isomorphic to abort.

With this, we can recover all of classical logic.