## Errata for  "The pi-calculus: a Theory of Mobile Processes"

Page 19, Definition 1.2.3 of structural congruence
The following text should be added at the end of the sentence:
"and the following equational rules for summations:
CONG-sum1    M_1 = M_2 implies M_1 + M_3 = M_2 + M_3
CONG-sum2    M_1 = M_2 implies M_3 + M_1 = M_3 + M_2    "
Accordingly, at the end of the paragraph following the definition we should add
"and the two rules above for summations".
[Thanks to Feng Guo and Hongqi Wang]

Page 27, line 22 (second last line of the proof of Lemma 1.2.18), using "\nu" for the restriction operator:
"\nu P" should be "\nu z P", and "\nu Q'" should be "\nu z Q'"      [Thanks to Henk Goeman]

Page 51, Harmony Lemma:

-- In the 2nd line of the proof "main" should be removed.
-- The 9th line should be "The assertion in (1) is precisely Fact 1.4.16, written in a less concise way." instead of "The assertion follows from Fact 1.4.16."

Page 67, Exercise 2.2.6, second line:
"strong bisimulations it not" should be "strong bisimulations is not"
[Thanks to Prashanth Mundkur]

Page 68, third line of proof:
"C[P\sigma] ~ C[Q\sigma]" should be "C[P]\sigma   ~   C[Q]\sigma"
[Thanks to Prashanth Mundkur]

Page 70, Claim 2.2.12:
The first 2 lines of the assertion of the claim should be:
"Let S be an infinite set of names, with its complement (the remaining names) also infinite. Suppose that n>=0 , and P\not\sim_n Q with fn(P,Q) not in S. Then there is a summation M such that for any z~, with z~ not in S, and any s \in S, with s \not\in fn (M), "
The following adjustments are then needed in the proof of the claim:
-- At the beginning of the proof, add "In this proof we say that a name is fresh to mean that it is taken from S and does not appear in the processes or actions of the statement. In the assertion of the claim, the complement of S is also required to be infinite so to make sure that alpha conversion of names remains possible."
-- 6th line of the proof. Replace "~w \subseteq fn(P',Q_i)" with "~w \cap S = \emptyset"
-- 1st line page 71. Replace "~z \subseteq fn(P,Q)" with "~z \cap S = \emptyset"
Also, the use of the claim at page 72 is modified thus. In the 3rd line page 72, replace "Then let M be as given by Claim 2.2.12, let s be fresh" with "Given some infinite set of fresh names S, let M be as given by Claim 2.2.12, let s \in S be fresh for M"
[Thanks to Benjamin Pierce and Steve Zdancewic]

Page 85, 2nd line after Exercise 2.3.15:
The definition of F^0(R) should be F(R) (rather than simply R as it was stated)       [Thanks to Luke Simon]

Page 87, Lemma 2.3.19:
The equality should be an inclusion, and moreover on the right hand side the identity function should be added (thus the assertion is: F_ni is included in (F_ni1)* union identity)
This lemma was only used in the following Lemma 2.3.21. Lemma 2.3.21 is correct but requires a slightly longer proof (with the same structure). It is also possible to maintain the same proof at the price of obtaining a slightly weaker result, which is anyhow sufficient for all uses of the lemma in the book. To help the reader, all the section, beginning with the line preceding Lemma 2.3.19 until the end of the section, has been rewritten and can be found here (postscript file; see here for a pdf). This includes the alternative to Lemma 2.3.21 mentioned above (appended at the end of the section as the new subsection 2.3.4)
Elsewhere in the book: the only consequences of the modifications above are the updates to the proofs of Lemmas 2.4.52 and 2.4.55 and to page 112 indicated below.
[Thanks to Luke Simon and Kazushige Terui]

Page 96, Lemma 2.4.11, first line:
The first symbol, before "is the largest symmetic relation...", should have been that of bisimilarity (\approx), instead of that for barbed bisimilarity.
[Thanks to Prashanth Mundkur]

Page 112, 8th line before Lemma 2.4.51:
Replace in the strong case, it suffices to work with (single-hole) contexts in the proof of Lemma 2.3.21.'' with in the strong case, an alternative to Lemma 2.3.21 exists where it is sufficient to work with (single-hole) contexts.''

Page 113-116, Lemma 2.4.52, Lemma 2.4.55, and Exercise 2.4.67:
In the assertions of Lemmas 2.4.52 and 2.4.55, we also need to use structural congruence in order to obtain the safety of the functions considered (F_ni and F_C). It is then useful to recall this addition in Exercise 2.4.67.
To help the reader, the complete corrected text of the two lemmas and of the exercise can be found here (postscript file; see here for a pdf).
[Thanks to Damien Pous]

Page 113, first line proof of Lemma 2.4.52:
remove but more complex because we have to use multihole contexts''
Note: another correction to this lemma is mentioned below, and the full corrected text is given.

Page 114, proof Lemma 2.4.55:
remove but again more complex because we have to use multihole contexts''
Note: another correction to this lemma is mentioned below, and the full corrected text is given.

Page 118, line 17, and page 565, line 33:
"Engelfreit" should be "Engelfriet"       [Thanks to Henk Goeman]

Page 169, second and last lines before Definition 4.6.5:
E_M and E_M' should be swapped (that is, it should be "E_M' \subseteq E_M", and it should say "E_M' is a finer relation than E_M")       [Thanks to Frederic Peschanski]

Page 185, Section 4.8.4 :
The congruence rule for parallel composition
P = Q implies P|R = Q|R
is missing       [Thanks to Massimo Merro]

Note on Page 197, Theorem 5.3.11 (3):
It should be stressed that the reverse implication holds too       [Thanks to Robin Milner]

Page 347, proof of Theorem 10.5.1(2):
The definition of H should include two copies of P. Hence we have:
-- 3rd line: the definition of H should be "Q | P {a=(x).R} | P {a=(x).R}"
-- 9th line: replace "(P | !P)" with "(P | P | !P)"
-- 12th line: the definition of P*_2 should be "Q | P {a=(x).R} | P {a=(x).R} | (!P) {a=(x).R}"
[Thanks to Benjamin Pierce and Steve Zdancewic]

Page 435, line 11 (second line of the definition of the CPS version of f):
"u + n" should be "v + w"      [Thanks to Bob Harper]