Foundational calculi
Lambda-calculus
Equivalence
Derived forms
What is a foundational calculus?
What are some examples of foundational calculi?
Why are they interesting?
Most foundational calculi come with:
1) Syntax of core language.
2) Dynamic semantics of core language.
3) Derived forms.
What are these?
Many problems in computing are safety properties.
What is a safety property?
What are example safety properties?
What are example properties which are not safety properties?
How can we give a formal definition of a safety properties?
What are the goals of the lambda-calculus?
History: Schönfinkel (1920's), Church (1930's), McCarthy (1950's), Landin (1960's), Scheme / Standard ML / Haskell / CAML / ... (1970's-now).
Assume a collection of variables x, y, z... Core syntax:
L, M, N ::=
x
M N
x.M
What are these?
Note: no booleans, integers, while loops, etc. Is this worrying?
Also note: no threads, concurrency controls, etc. Is this worrying?
Examples:
Which of these `are the same program'? What does that mean?
Two notions of `are the same program':
Which of the examples are alpha-equivalent? Which are beta-equivalent?
Formalize alpha-equivalence...
Define [M/x]N as `replace M for x in N'. Examples:
Alpha-equivalence is generated by:
(x . M ) = (
y . [y/x]M ) when y is fresh
Which of these are alpha-equivalent?
Formalize function application (jargon: beta-reduction) generated by:
(x . M ) N
( [N/x]M )
Examples:
Beta-equivalence:
M =N whenever
L . M
* L and N
* L
Sanity checks:
M
=
M?
If M
=
N
then N
=
M?
If L
=
M
and M
=
N
then L
=
N?
Booleans:
True = (x .
y . x )
False = (x .
y . y )
if L { M } else { N } = ( L M N )
Verify:
if True { M } else { N } =M
if False { M } else { N } =N
Pairs:
( M, N ) = (x . x M N )
Fst =z . z (
x .
y . x )
Snd =z . z (
x .
y . y )
Verify:
Fst ( M, N ) =M
Snd ( M, N ) =N
Similar codings for integers, lists, etc.
Recursion:
fix M = (x . M ( x x ) ) (
x . M ( x x ) )
Verify:
fix M =M ( fix M )
Example:
factorial = fix fact
fact = (f .
x . if (x < 2) { 1 } else { x * f (x - 1) } )
Verify:
factorial 3 =6
Homework sheet 2.
Calculi for protocols: pi- and spi-calculus.