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.