Theoretical computer science is unnatural ... Page 5 ... but is it unnatural like Ikebana ... Alonzo Church (1932) â L
The Unreasonable Effectiveness of Logic Philip Wadler University of Edinburgh
[email protected]
Is computing a deep subject?
Theoretical computer science is unnatural ...
... but is it unnatural like Ikebana?
... or is it unnatural like Judo?
More than a coincidence? second-order logic
polymorphism
Java
Milner modal logic
monads
XML
Moggi,Buneman classical logic
continuations Plotkin
Links
Part I
A remarkable coincidence
Gerhard Gentzen (1909–1945)
Gerhard Gentzen (1935) — Natural Deduction
Gerhard Gentzen (1935) — Natural Deduction [A]x · · · B A⊃B
A
B
A&B
&-I
A⊃B B
⊃-Ix
A&B A
&-E0
A
⊃-E
A&B B
&-E1
Simplifying a proof [B & A]z A
&-E1
[B & A]z B
A&B (B & A) ⊃ (A & B)
&-E0
&-I
⊃-Iz
A&B
[B]y
[A]x
B&A
&-I
⊃-E
Simplifying a proof [B & A]z A
[B & A]z
&-E1
B
A&B (B & A) ⊃ (A & B)
&-E0
&-I
[B]y
⊃-Iz
B&A
A&B ⇓ [B]y
[A]x
B&A A
&-I
&-E1 A&B
[A]x
[B]y
[A]x
B&A B
&-I
&-E0
&-I
&-I
⊃-E
Simplifying a proof [B & A]z A
[B & A]z
&-E1
B
A&B (B & A) ⊃ (A & B)
&-E0
&-I
[B]y
⊃-Iz
B&A
A&B ⇓ [B]y
[A]x
B&A A
&-I
[B]y
&-E1 A&B ⇓ [A]x [B]y A&B
[A]x
[A]x
B&A B
&-I
&-I
&-E0
&-I
&-I
⊃-E
Alonzo Church (1903–1995)
Alonzo Church (1932) — Lambda calculus
Alonzo Church (1940) — Typed λ-calculus [x : A]x · · · u:B λx. u : A ⊃ B
t:A
u:B
ht, ui : A & B
&-I
s:A⊃B st : B
⊃-Ix
s:A&B s0 : A
&-E0
t:A
⊃-E
s:A&B s1 : B
&-E1
Simplifying a program [z : B & A]z z1 : A
&-E1
[z : B & A]z
hz1 , z0 i : A & B
z0 : B
&-E0
&-I
λz. hz1 , z0 i : (B & A) ⊃ (A & B)
⊃-Iz
(λz. hz1 , z0 i) hy, xi : A & B
[y : B]y
[x : A]x
hy, xi : B & A
&-I
⊃-E
Simplifying a program [z : B & A]z z1 : A
&-E1
[z : B & A]z
hz1 , z0 i : A & B
z0 : B
&-E0
&-I
λz. hz1 , z0 i : (B & A) ⊃ (A & B)
⊃-Iz
[y : B]y
[x : A]x
hy, xi : B & A
(λz. hz1 , z0 i) hy, xi : A & B ⇓ [y : B]y [x : A]x [y : B]y [x : A]x &-I &-I hy, xi : B & A hy, xi : B & A &-E1 &-E0 hy, xi1 : A hy, xi0 : B &-I hhy, xi1 , hy, xi0 i : A & B
&-I
⊃-E
Simplifying a program [z : B & A]z z1 : A
&-E1
[z : B & A]z
hz1 , z0 i : A & B
z0 : B
&-E0
&-I
λz. hz1 , z0 i : (B & A) ⊃ (A & B)
⊃-Iz
[y : B]y
[x : A]x
hy, xi : B & A
(λz. hz1 , z0 i) hy, xi : A & B ⇓ [y : B]y [x : A]x [y : B]y [x : A]x &-I &-I hy, xi : B & A hy, xi : B & A &-E1 &-E0 hy, xi1 : A hy, xi0 : B &-I hhy, xi1 , hy, xi0 i : A & B ⇓ [x : A]x [y : B]y &-I hx, yi : A & B
&-I
⊃-E
William Howard (1980) — Curry-Howard Isomorphism
More than a coincidence? second-order logic
polymorphism
Java
Milner modal logic
monads
XML
Moggi,Buneman classical logic
continuations Plotkin
Links
Part II
Second-order logic, Polymorphism, and Java
Gottlob Frege (1879) — Quantifiers (∀)
Gottlob Frege (1879) — Quantifiers (∀)
John Reynolds (1974) — Polymorphism
Jean-Yves Girard (1972) — Polymorphism
Robin Milner (1975) — Polymorphism
Gosling, Joy, Steele (1996) — Java
Odersky and Wadler (1997) — Pizza
Igarashi, Pierce, and Wadler (1999) — Featherweight Java
Igarashi, Pierce, and Wadler (1999) — Featherweight Generic Java
Gosling, Joy, Steele, Bracha (2004) — Java 5
Part III
Modality, monads, and XML
Clarence Lewis (1918) — Modal Logic
Eugenio Moggi (1988) — Monads
Philip Wadler (1990) — Comprehensions
Peter Buneman et al (1991) — Comprehensions
XQuery (2004) — FLWOR
XQuery (2004) — FLWOR
XQuery (2004) — Formal Semantics
Part IV
Classical logic, continuations, and the Web
Andrei Kolmogorov (1925)
Gordon Plotkin (1975)
Philip Wadler (2000)
Philip Wadler (2000)
Orbitz: Two flights
Graunke, Findler, Krishnamurthi, Felleisen (ESOP 2003)
Orbitz: Clone and submit first
Orbitz: Submit second
Orbitz: Select first – problem!
Burstall, MacQueen, and Sannella (1980) — Hope
Burstall, MacQueen, and Sannella (1980) — Hope
Wadler and Yallop (2005) — Links
main() -> todo([]). todo(items) -> Items to do
{ for item in items return | {item} | |
}
.
Part V
Conclusions
Kinds of coincidence Historical confluence of great minds — Hume, Hutton, Smith
Geographical shape of continents
Astronomical size of sun and moon from earth
More than a coincidence? second-order logic
polymorphism
Java
Milner modal logic
monads
XML
Moggi,Buneman classical logic
continuations Plotkin
Links
More than a coincidence? second-order logic
polymorphism
Java
Milner modal logic
monads
XML
Moggi,Buneman classical logic
continuations Plotkin
Links
Invitation Scottish Programming Language Seminar Invited speakers: John Reynolds, David Watt 10.00–16.00, 7 December 2004, University of Glasgow Simon Gay,
[email protected]
Special thanks to My colleagues for their ideas Martina Sharp, Avaya Labs, and Diana Sisu, Informatics, for scanning Adam and Leora for their books
Catherine for the tie You for listening
