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.