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]