*Deadline*: 5.30pm, Thursday 29 January 2004.

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

PQ= new (x) . ( outx();0| inx();P| inx();Q)

1. Show the following:

PQ^{*}=_{gc}P

PQ^{*}=_{gc}Q

2. Let *P* =_{} *Q*
be an equivalence such that:

- If
*P*^{*}*Q*then*P*=_{}*Q*. - If
*P*=_{gc}*Q*then*P*=_{}*Q*. - If
*P*=_{}*Q*then*Q*=_{}*P*. - 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

outMN;P

inM(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 TrueM;PFAIL

out FalseM;PFAIL

in True (x);PFAIL

in False (x);PFAIL

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.