SE547: Lecture 2

Overview

Foundational calculi

Lambda-calculus

Equivalence

Derived forms

Foundational calculi

What is a foundational calculus?

What are some examples of foundational calculi?

Why are they interesting?

Foundational calculi

Most foundational calculi come with:

1) Syntax of core language.

2) Dynamic semantics of core language.

3) Derived forms.

What are these?

Foundational calculi

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?

Lambda-calculus

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).

Lambda-calculus

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?

Lambda-calculus

Examples:

1. x . x
2. y . y
3. y . x
4. x . y . x
5. x . y . y
6. y . x . y
7. ( x . x )( y . y )
8. ( x . x ( y . y ) )
9. ( x . x ( y . y ) ) ( z . z )
10. ( x . x x ) ( x . x x )

Which of these `are the same program'? What does that mean?

Equivalence

Two notions of `are the same program':

1. alpha-equivalence: `allowed to rename bound variables'.
2. beta-equivalence: alpha + `allowed to apply functions'.

Which of the examples are alpha-equivalent? Which are beta-equivalent?

Equivalence

Formalize alpha-equivalence...

Define [M/x]N as `replace M for x in N'. Examples:

1. [ y . y / x ]( x )
2. [ z . z / x ] ( x ( y . y ) )
3. [ x . x x / x ] ( x x )

Alpha-equivalence is generated by:

( x . M ) = ( y . [y/x]M )       when y is fresh

Which of these are alpha-equivalent?

1. x . y . x
2. x . y . y
3. y . x . y

Equivalence

Formalize function application (jargon: beta-reduction) generated by:

( x . M ) N ( [N/x]M )

Examples:

1. ( x . x )( y . y )
2. ( x . x ( y . y ) )
3. ( x . x ( y . y ) ) ( z . z )
4. ( x . x x ) ( x . x x )

Equivalence

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?

Derived forms

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

Derived forms

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.

Derived forms

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

Next week

Homework sheet 2.

Calculi for protocols: pi- and spi-calculus.