SE547: Homework 3

Deadline: 5.30pm, Thursday 29 January 2004.

Homework

Consider the following coding of nondeterminism in the pi-calculus:

P Q = new (x) . ( out x (); 0 | in x (); P | in x (); Q )

1. Show the following:

P Q * =gc P
P Q * =gc Q

2. Let P = Q be an equivalence such that:

  1. If P * Q then P = Q.
  2. If P =gc Q then P = Q.
  3. If P = Q then Q = P.
  4. If P = Q and Q = R then P = R.

Show that for any processes P and Q we have that P = Q (and therefore that beta-equivalence is not much use for concurrent languages).

Hint: use P Q.

3. Extra credit:

Consider the following pi-calculus with booleans:

M, N ::=
    c
    True
    False
P, Q, R ::=
    0
    out M N; P
    in M (y); P
    P | Q
    !P
    new (x); P
    if ( M ) { P } else { Q }
    FAIL

whose dynamic semantics is given by the rules for the pi-calculus together with:

if ( True ) { P } else { Q } P
if ( False ) { P } else { Q } Q
if ( c ) { P } else { Q } FAIL
out True M; P FAIL
out False M; P FAIL
in True (x); P FAIL
in False (x); P FAIL

Give a type system in the style of Pitts for this language, ensuring that any program containing FAIL does not typecheck.

Hint: Use types given by the grammar:

, ::=
    bool
    chan ()

Submit your answer (either as a plain text file, a PDF file, an HTML file, or scanned handwriting) using Courses On Line.