Semantics Engineering with PLT Redex, by
Matthias Felleisen,
Robby Findler, and
Matthew Flatt.
Page 18, in the first subcase of the first inductive case of the proof for Lemma 2.4, the if statements are reversed. This is the correct case:
Pages 26 and 46, the substitution functions should have had the condition X3 != X2 in the second lambda case. These are the corrected figures:
Page 40, Lemma 3.4 should have -->>n instead of -->>r in the statement of Church-Rosser.
Page 57, in the first case of the proof of Lemma 4.7, the second N should be N'. Thanks to Stephen Chang.
Page 67, Lemma 5.1 is incorrectly referred to as "Theorem 5.1".
Page 69, "reductions steps" should be "reduction steps".
Page 72, the proof of Lemma 5.5 uses Lemma 5.6 incorrectly. The second (bullet) case should state that M |-->>_v K, not just in single-step mode. Thanks to Tony Garnock-Jones and the 2010 class of John Clements (CalPoly).
Page 73, the statement of the first full case of Lemma 5.5 on this page should use N'i instead of Ni:
Page 73, the statement of the third case of Lemma 5.6. should use J instead of L (to avoid confusion with the term L in the statement of the lemma). Furthermore, the result of applying the induction hypothesis yields a reduction sequence that ends in L (not N):
Page 75, the calculation introduced with "Putting it all together, we get" should be as follows
Page 75, the statement of the first full case of Lemma 5.6 on this page should use N'i instead of Ni. Thanks to Stephen Chang.
Page 76, the undefined variables s denotes the size of the constructed term. Thanks to Stephen Chang.
Page 77, third subcase and the last case should use capitalized "Y" not lower-case "y." Thanks to Stephen Chang.
Page 79, the statement of the first full case of Lemma 5.8 on this page should use N'i instead of Ni. Thanks to Stephen Chang.
Page 79, the proof of Lemma 5.2 should refer to theorem 5.4, not 5.5. Thanks to Stephen Chang.
Page 82, Proof for Lemma 5.10 refers to "theorem" 5.1. This should be a reference "lemma" 5.1. Thanks to Stephen Chang.
Page 84, Proof for Lemma 5.11 mentions the "assumption that C[Ω] is undefined." This should say "assumption that evalv(C[Ω]) is undefined." Thanks to Stephen Chang.
Page 86, line 2: "(case 3)" should be "(case 2)". Thanks to Stephen Chang.
Pages 141 through 143, section 8.4 (part I) contains a major flaw. The notions of reductions on page 142 do not satisfy the Church-Rosser lemma and therefore theorem 8.17 is false as stated. Here is a counter-example:
and
catch (+ (throw 0) 1) with (λxy.yx) = catch (throw 0) with (λxy.yx) by throw = (λxy.yx) 0 (λy.y) by cntrl = (λy.y) 0 by βv = 0 by βv
catch (+ (throw 0) 1) with (λxy.x) = (λxy.x) 0 (λy.(+ y 1)) by cntrl = (λy.(+ y 1)) 0 by βv = (+ 0 1) by βv = 1 by δ
We can fix this problem with the elimination of throw from the first box on page 142. This change induces changes to the definitions of the evaluation functions on page 142 and 143 as well as the definitions of the standard reduction function. To avoid any confusion, here is the revised pages 141 through 143.
Thanks to Ryan Culpepper for discovering this major problem.
Page 170, the side-condition on the [ceskgc] rule is incorrect. It should be this:
Thanks to David Van Horn.
Page 172, "<M,Ebar>" on the right hand side of the [ceksgc1] rule should be "c".
Page 208, "conjunction" should be "disjunction". Thanks to Matt Might.
Page 213, true and false should be swapped in the definition of bool-red. This is the correct definition:
