Logic and
Computation
“Dr. Ghica”
Dan R. Ghica dan@ghica.net
“Dan”
“Dr. Dan”
“Ghica”
1
Antikythera 100 BCE
Aristotle 384 – 322 BCE
Engineering
2
Logic
Engineering
1945-1952
2017-
346 Gflops (692,000x) 100 Gb (833,000x) 174 g (155,000x) 1-10W (15,000 x)
cat videos
speed: memory: weight: power: purpose:
500 flops 120b
27t 150kW
atomic weapons
3
Programming the computer
1940 : Binary 1945 : Assembly 1957 : FORTRAN 1960 : ALGOL
•
•
•
•
• 1972 : C •
• •
Progress?
1983 : C++ 1995 : JAVA …
4
Programming as a
mathematical-logical
activity. 5
Barbara
All men are mortal. Aristotle is a man. Aristotle is mortal.
vs. All wabes are slithy.
The mome is a wabe. The mome is slithy.
the conclusion is formal and can be computed: mechanical application of rules
Forward 1,000 years
7
also invented “algebra” (al-jabr = cancellation)
“algorithm”
Abu Abdullah Muhammad bin Musa al-Khwarizmi
780-850 AD 8
Forward 1,000 years
9
set theory
= formalisation of all of mathematics
Georg Cantor 1845 – 1918
10
“a grave disease infecting the discipline of
•
mathematics” — Poincare
• •
“a scientific charlatan” — Kronecker “utter nonsense” — Wittgenstein
11
No one shall expel us from the paradise that Cantor has created.
David Hilbert 1862 – 1943
12
There is a little problem.
Gottlob Frege 1848 – 1925
Bertrand Russell 1872 – 1970
13
A paradox of self-reference
{x ∣ x∉x} ∉ {x ∣ x∉x} 14
A good formal system
a bunch of rules
• • •
sound (true ≠ false) complete (true or false) computable (by machines)
15
either sound or complete (not both)
Kurt Gödel 1906 – 1978
16
not computable
not computable
Alonzo Church 1903 – 1995
17
Alan Turing 1912 – 1954
Computer science
is born out of the ashes of
Hilbert’s great dream.
18
It’s all over!
John von Neumann 1903 – 1957
19
Turing machine (1936) to
EDVAC (1945)
⇒ lambda calculus (1936) ⇒ FORTRAN (1957)
⇒ ISWIM (1966)
⇒ ML (1973)
⇒ Haskell (1990) ⇒ Scala (2004)
Backus 1924-2007
Landin 1930-2009
Milner
Peyton- Odersky
1934-2010 Jones 20
• • • • •
Week 7: Computer Proof Checking. Week 8: Curry-Howard Correspondence. Week 9: Lambda calculus.
Week 10: Inductive types.
Week 11: Reasoning about code.
•
•
Admin stuff All module material:
https://git.cs.bham.ac.uk/drg/logic-and-computation-2019/
Weekly equal-weight assignments
•
22