MPRI Concurrency (Cours 23) Final exam, 20052006 22 Feb 2006, 16.15–19.15 James.Leifer@inria.fr Question annotations:∗= easy;∗∗= medium;∗∗∗= hard 1. Considerthe termP=νy.(x(x).x(x).xy)|νy.(xy.νx.(yx.x(x))) withx6=y. (a)∗What is the set of free names ofP? Solution:{x}. ′ (b)∗Define a processPthat isαequivalent toPand has all bound names distinct from each other and from all free names. ′ Solution:P=νy1.(x(x1).x1(x2).x2 1)|νy2.(x2.νx3.(2x3.x3(x4))).
′ (c)∗What is the set of free names ofP? Solution:{x}, sinceαconversion doesn’t change the free names. ′ (d)∗∗Show the sequence of three reduction steps (−→) starting atP, taking care to make explicit any scope extrusions you need (i.e. use of(strex)in≡). Solution: ′ P ≡νy1, y2.(x(x1).x1(x2).x2y1|xy2.νx3.(y2x3.x3(x4))) extrusionofy2 −→νy1, y2.(y2(x2).x2y1|νx3.(y2x3.x3(x4))) communicationonx ≡νy1, y2, x3.(y2(x2).x2y1|y2x3.x3(x4)) extrusionofx3 −→νy1, y2, x3.(x3y1|x3(x4)) communicationony2 −→νy1, y2, x3.(0|0on) communicationx3
2. This question explores the relationship between name hiding and bisimulation in the coreπ calculus (i.e. the calculus on slide 3 with no extra features).
(a)∗∗∗Prove that strong bisimilarity is closed by new binding, i.e.P∼Qimpliesνx.P∼ νx.Q. Youmay only use the basic definitions of bisimulation and labelled transition (no “up to” techniques). Hint: startwith a relationR={(νx.P,νx.Q)/ P∼Q}and try to show thatRis a strong bisimulation. Youmay have to add some more pairs toR. ′ ′ Solution:TakeR=R ∪(∼aim to show that). WeRTo dois a bisimulation. α ′ ′ RandP−→Pwit that we need to consider (P0, Q0)∈0 0hbn(α)∩fn(Q0) =∅. We distinguish two cases. α ′ ′ CaseP∼Q:By definition of∼, there existsQsuc−→Q 0 00h thatQ0 0and ′ ′′ ′′ P∼Q, hence (QP ,)∈ R, as desired. 0 00 0 Case(P0, Q0)∈ R:Then there existsPandQsuch thatP∼QandP0=νx.P andQ0=νx.Qconsider the two possible ways that the labelled transition. We α ′ Pould derived. P0−→0c havebeen α ′ ′′ ′ Case(labnew):Then there existsPsuch thatP−→PandP=νx.P 0 andx /∈bn(αhypothesis, we also have). Bybn(α)∩fn(Q0) =∅, hence bn(α)∩fn(Q) =∅, thus it is safe to apply the definition of bisimulation to α ′ ′′ ′ the hypothesisP∼Q; hence there existsQsuch thatQ−→QandP∼Q. α ′ ′′ ′′ ′ LetQ=νx.Qby. Then(labnew),Q0−→Q. Finally,(P ,Q)∈ R ⊆ R, 0 00 0 as desired.