Transcript Lambda-Calculus

Lambda Calculus
Introduction
Spring, 2011 –– Computational Thinking – Dennis Kafura – CS 2984
History
Gottfried Wilhelm Leibniz (1646 - 1716)
"It is unworthy of excellent men to lose
hours like slaves in the labour of
calculation which could safely be
regulated to anyone else if machines
were used."
Stepped Reckoner
Sought a formal language for a machine to
determine the truth of mathematical statements.
Spring, 2011 – Computational Thinking – Dennis Kafura – CS 2984
Entscheidungsproblem
The “decision problem” (1928):
Find an algorithm which takes as input
a description of a formal language
and a mathematical statement
expressed in that language and
outputs true or false depending on the
mathematical validity of the statement.
David Hilbert
William Ackermann
Spring, 2011 – Computational Thinking – Dennis Kafura – CS 2984
Alonzo Church


Church’s Theorem (1936)
Answered the decision problem in the
negative
Alonzo Church
1903-1995
Spring, 2011 – Computational Thinking – Dennis Kafura – CS 2984
Alonzo Church


Defined the Lambda (l)
Calculus - a language
foundation for computing
Led to family of functional
programming languages
Spring, 2011 – Computational Thinking – Dennis Kafura – CS 2984
Alan Turing





Independently answered the
decision problem in the negative
Defined the Turing Machine – a
machine foundation for computing
Led to Von Neumann computers
and family of imperative
programming languages
Work at Bletchley Park in WW2
Died by suicide (apple laced with cyanide)
Alan Turing
1912-1954
Spring, 2011 – Computational Thinking – Dennis Kafura – CS 2984
Bletchley Park
Turing designed the Bombe machine
to decrypt Enigma messages.
The Enigma Cryptographic Device
Spring, 2011 – Computational Thinking – Dennis Kafura – CS 2984
The l Calculus
<expression> := <name> |
<function> |
<application>
<function> := l <name> . <expression>
<application> := <expression> <expression>
Spring, 2011 – Computational Thinking – Dennis Kafura – CS 2984