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
A
( 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
A
Π 1 : AxB -> A
A&B
B
Π 2 : AxB -> B
Matthias: note the correspondence between introduction and elimination rules. This was the inspiration for parts of HtDP.

Disjunction

logic lambda-calc
A
A|B
( inl B M A ) A+B
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?

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.