Transcript proofs-programs

Proofs are Programs:
19th Century Logic
and
21st Century Computing
CS 510: Programming Languages
(a talk adapted from Philip Wadler)
How to Talk to Aliens
Basic natural phenomena
• Some mathematical phenomena seem so
unavoidable that we must view them as
“discovered” rather than “invented”
– natural numbers
• 0 appears first in India (700 CE)
– mathematical constants
• pi, e
– geometry
• basic shapes (circle, triangle)
• geometric laws (triangle inequality, area and volume)
Computer Science
• Invented or discovered?
• Are there fundamental, unavoidable
computational phenomena?
– laws or concepts with the same unavoidable feeling
as Newton’s laws of gravity?
• How would we know?
– these concepts would appear across time and culture
– but computer science is only 50 years old! Or is it?
The History of Logic
• George Boole
– 1815-1864
– inventor (discoverer?) of
Boolean algebra
– conjectured the existence of
fundamental Laws of Thought
The History of Logic
• George Boole (Laws of Thought, 1854)
History of Logic
• Gotlob Frege (1848-1925)
– the first hints of modern logic
– formal diagrams to depict
mathematical inferences
History of Logic
• Frege’s inferences (1879)
• Look vaguely familiar?
History of Logic
• Frege continued (1879)
History of Logic
• Frege in modern notation
History of Logic
• Gerhard Gentzen (1934)
– Natural Deduction
– The definition of logical
connectives exclusively in
terms of introduction of the
connective and elimination of
the connective
– Prior work specified logic via
axioms that related one
connective to another
History of Logic
• Gentzen (1934)
History of Logic
• Gentzen (1934)
History of Logic
• Gentzen (1934)
– in modern notation:
History of Logic
• Gentzen (1934)
– proof simplification rules:
History of Logic
• Proof simplification
History of Logic
• Proof simplification
History of Logic
• Alonzo Church
– invented (discovered?) the
lambda calculus
– the first programming
language researcher
History of Logic
• Alonzo Church (1903-1995)
– invented (discovered?) the
lambda calculus
– the first programming
language researcher
– he didn’t know it at the time
(we were still lacking the
computers)
History of Logic
• Church (1932)
– the introduction of free and bound variables
History of Logic
• Church (1932)
– the logic is defined entirely and abstractly by a
system of inference rules
– symbols do not have pre-conceived meanings
– pure logic uninfluenced by culture
History of Logic
• Church (1932)
– in case you missed the last line
– I’ll say.
History of Logic
• Church (1932)
– proof terms, bound variables and the notion of
well-formed objects
History of Logic
• Computing with Church’s lambda calculus
• General evaluation rules:
History of Logic
• Sample evaluation
History of Logic
• Church’s typed lambda calculus
History of Logic
• Simplifying programs
History of Logic
• Simplifying programs
History of Logic
• Curry-Howard Isomorphism
Haskell Curry (1900-1982)
William Howard
History of Logic
• Curry-Howard Isomorphism
– First noticed by Curry in 1960
– First published by Howard in 1980
• Fundamental ideas:
–
–
–
–
–
Proofs are programs
Formulas are types
Proof rules are type checking rules
Proof simplification is operational semantics
Ideas and observations about logic are ideas
and observations about programming languages
History of Logic
• Curry-Howard (intuitionistic logic)
2nd-order intuitionistic logic
Polymorphic Lambda Calculus
(PolyMinML - recursion)
(formula variable) a
(implication)
A => B
(conjunction)
AB
(disjunction)
AB
(truth)
True
(falsehood)
False
(universal quant) a.A
(existential quant) a.A
(type variable)
(function type)
(pair type)
(sum type)
(unit)
(void)
(universal poly)
(existential poly)
a
AB
A*B
A+B
unit
void
a.A
a.A
History of Logic
• Curry-Howard (intuitionistic logic)
2nd-order intuitionistic logic
G, A |- B
-------------------------- (=> I)
G |- A => B
G |- A => B
G |- A
------------------------------- (=>E)
G |- B
Polymorphic Lambda Calculus
G, x:A |- e : B
--------------------------(Fun)
G |- x:A.e : A => B
G |- e1 : A => B G |- e2 : A
---------------------------------- (App)
G |- e1 e2 : B
• Note: You don’t have to omit proof terms from logical rules
History of Logic
• Curry-Howard (intuitionistic logic)
2nd-order intuitionistic logic
G |- A G |- B
------------------- ( I)
G |- A  B
G |- A  B
------------- (E1)
G |- A
G |- A  B
------------- (E2)
G |- B
Polymorphic Lambda Calculus
G |- e1 : A G |- e2 : B
------------------------------(Pair)
G |- <e1,e2> : A * B
G |- e : A  B
G |- e : A  B
----------------- (E1) ----------------- (E2)
G |- e.1 : A
G |- e.2 B
History of Logic
• Other Examples
– Hindley/Milner: formula reconstruction/type inference
– Girard/Reynolds:
• System F/Polymorphic lambda calculus
• Linear Logic/Syntactic control of interference, linear types
–
–
–
–
Murthy: classical logic/callcc
Abramsky: multiplicative vs additive/strict vs lazy
Pfenning and Davies: modal logic/RTCG
Phil Wadler: and dual to or/CBV dual to CBN
History of Logic
• The Curry-Howard isomorphism
– Coincidence? Or are aliens trying to tell us something?
– Identical concepts arise across time and culture
– Certain logical/computational definitions seem
unavoidable
– Are they inventions or discoveries?
• Is this talk about the history of logic or the history
of computer programming?
• Was this course about logic or computer science?