PFPL Errata

If typographic (or other) errors are found in the PFPL, post them here.

Chapter 1

• the X_s in "family of disjoint finite sets X_s" (p.5) is not italicized.
• the first sentences in the 1st and 3rd paragraphs of 1.1 (p.4) are basically the same, and similarly for the first sentences of the 1st and 4th paragraphs of 1.2.
• Delete the apostrophe in "it's fresh counterpart", p.8.

Chapter 2

• In the proof of Lemma 2.1, p. 17, P(a nat) should be P(a) (the formalism has changed since the 1st edition).

Chapter 5

• Inconsistent notation for the judgement of equality of natural numbers between the first table in chapter 2.1, the definition of is in chapter 2, and rule 5.4(a). Also, something else seems wrong since is expresses structural equality on naturals and the presence of + rules out the possibility of equality. Is n1 + n2 is n nat a different (3-place) judgement that hasn't been defined before?
• First paragraph of 5.3: add a comma after "The judgement e val".
• Second paragraph of 5.4: script X should be x-> (otherwise no fresh vars available?)

Chapter 8

• p. 68: 'eevaluation' ...

Chapter 9

• First line of 9.5: delete extra "Gödel".
• Add a '.' to the end of theorem 9.3.

Chapter 10

• Definition of e' in terms of iter (first equation in 10.3): concrete and abstract syntax are mixed.

Chapter 11

• Section 11.2: 'When I = {l_1, l_2, ..., l_n}' should be 'When I = {i_1, ..., i_n}'. 'the class l_i' should be 'the class i_j'.
• Section 11.3.3, last paragraph: "... all possible Unicode (...) of characters ... " -> "... all possible Unicode (...) characters ..."

Chapter 12

• Exercise 12.3: 'constructive propositional forms a Heyting algebra' is missing the word 'logic'.

Chapter 13

• Exercise 13.1 assumes the reader has already completed exercise 30.2! Also, 'inhabited your solution' should be 'inhabited in your solution'.

Chapter 32

• Page 291 fourth line: unbound sigma should be unbound mu
• Page 289: "variables is intolerable" => "variables are intolerable"
• Appendix A: psi(v) should be psi(u) in the function definition

Chapter 43

• Page 413 (section 43.5) line 4: c2 : k (pronounced "c2 has type kappa") should be c2 :: k (pronounced "c2 has kind kappa")