Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Errata for TYPES AND PROGRAMMING LANGUAGES (3rd printing) ========================================================== Last modified: July, 2004 The first section of this file lists all the errors that I'm aware of in the third printing of TAPL (errata for earlier printings are below). If you find one that's not listed here, please let me know! in the source code for the checkers: In the TmTimesFloat case of the "pr" function in syntax.ml in most of the checkers, the first occurrence of "printtm_ATerm false ctx t2" should be "printtm_ATerm false ctx t1". p 41, definition 3.5.15 the word "closed" is not needed here. p 57, definition of call-by-value "a term that is finished computing..." should be "a CLOSED term that is finished computing..." p 63, exercise 5.2.8 fold_left should be fold_right p 67, figure 5-2 the reduction from times c3 (fct (prd c3)) to times c3 (fct c2') is not valid in call-by-value semantics -- the application of times to c3 should be reduced first. p. 76, exercise 6.1.1 the combinator called "plus" does not implement the addition function (the solution in the back is correct, though) p 78, second line of 6.2 "To to" -> "To do" p 79, exercise 6.2.3 The statement to be shown is not quite true for d < 0. To be true for n>=0 and any integral d, it should be "Show that, if t is an n-term and, if d < 0, the free variables of t are all at least |d|, then is a (max(n+d,0))-term." p 106, proof of 9.3.8 "By induction on a derivation" should be "By induction on the depth of a derivation" p 107, Preservation theorem (and other preservation theorems throughout the text) The theorem is correct as stated, but we don't really need this powerful a version of it for present purposes. Since (a) we have chosen only to be interested in evaluating closed terms and (b) the evaluation strategy is call-by-value (so evaluating a closed term only involved evaluating closed sub-terms), there is no reason for Gamma ever to be non-empty. p 110, part 2 of Theorem 9.5.2 the first "typed" should be "untyped" p 120, Theorem 11.3.1 The first part of the Theorem doesn't hold, for a couple of reasons. First, the statement in the "if" direction should read: if e(t) -> u, then there is a lambda-E term t' such that u = e(t') and t -> t' Second, the E-SeqNext rule should be changed to read v1; t2 -> t2 (with v1 in place of unit), to match the semantics of E-AppAbs. p 130, second paragraph, second sentence "affect" should be "effect" p 136, figure 11-11: the value syntax for variants is missing. It should read: v ::= ... as T p 137, paragraph 3 "finite mappings" should be "partial mappings" p 144, line 4 T should be T1 p 146 Lists are not implemented in the fullsimple checker. p 152, line 1 The first heavy open paren should be dropped. p 152, line 3 The first close paren should be in typewriter (heavy) font. p 152, Exercise 12.1.7 "Figure 3-1" should be "Figure 8-1" p 162, 166 The notation for extending stores with new mappings is a little inconsistent ("[l |-> v2]\mu" in some places and "\mu, l |-> v1" in others). p 163 The last l_1 on the pge should be l_2 p 166 In the syntax of stores, = should be --> p 184 In "most variants of Abadi and Cardelli's object calculus omit width subtyping", "width" should be replaced by "depth." p 190, Lemma 15.3.6, part 2 {k_j=v_j ^ {a \in 1..m}} should be {k_a=v_a ^ {a \in 1..m}} p 204, second equation in definition of [[ - ]] \x:T1 should be \x:T1.t2 p 206, first sentence of third para In "The inhabitants of the intersection type T_1 /\ T_2 are terms belonging to both S and T", S and T should be T_1 and T_2. p 232, line -3 "C++ and ," should be "C++ and Java," p 243, line 3 Ref InstrCounter <: Ref SetCounter should be Source InstrCounter <: Source SetCounter p 273, first paragraph the erasure of the fix combinator defined here is not quite the same as the fix defined on p. 65: this one is missing the abstractions on y (which are needed to make it work in the call-by-value setting). p 342, near bottom In addition to We continue the convention (5.3.4) that the names of (term or type) variables should be chosen so as to be different from all the names already bound by $\Gamma$, ... we should add the restriction that a context of the form $\Gamma, x : T$ is well-formed only if every type variable free in $T$ is bound by $\Gamma$. p 354, second para "A term M" should be "A term m" p 371, line 1 ATD should be ADT p 402: Proof of 26.4.8 In the case for S-TVar, if Y=X, then [X -> P]S = P (not Q), which requires G |- P <: Q (from the premise) to reach the desired result. p 404, proof of 26.4.13 In the second subcase of the argument for T-TApp, the reference to 26.4.6 should instead be to 26.4.9. p 405, proof of 26.4.14 (near the end) The -> in \forall X<:T_1 -> S_2 should be a dot. p 411-416 (chapter 27) The whole of chapter 27 is not very convincing. The purpose in using Fsub is supposedly to enable us to create the method table just once per class, rather than once per object. The code indeed manages to have it create something just once for each class, but that something is a *function* that creates the method table *at every open self recursive call*! (See the "(!self r)" calls that happen during a method invocation.) In other words, the final efficiency is worse than what we ended up at the end of Chapter 18. Many thanks to John Tang Boyland for pointing this out! John also proposes a different case study, using f-omega-sub in the style of chapter 32 to implement objects in an imperative style. A sketch of the main constructions can be found here: http://www.cis.upenn.edu/~bcpierce/tapl/boyland-object-encoding.txt Some code implementing the idea is here: http://www.cs.uwm.edu/classes/cs790/types-f2003/Chapter27-replacement.txt http://www.cs.uwm.edu/classes/cs790/types-f2003/fullfomsubref.tar.gz p 412, footnote The description of method lookup in real-world OO languages is misleadingly simplistic: real implementations do things that are much fancier and more efficient than this. p 423, definition 28.3.4 The weight of a subtyping statement should be defined as the *sum* (not the max) of the weights of S and T. Also, it would help to note explicitly that the weight function is well defined because the total size of all the types in Gamma plus the size of the type whose weight is being defined always decreases. p 461 The type operator "Class" is not actually used in Chapter 32. p 462, para 2 "abstraction \x:T.t_2 is a family of terms [x <- s]t_1" should end "[x <- s]t_2" p 469: exericse 31.2.1 The exercise is correct as stated, but it would have been more interesting if instead of (or in addition to) "FB <: FB" it had asked whether "FA <: FB" holds. Also, in the second and third parts from the bottom, it would have been clearer to use G instead of F. p 494, solution to exercise 3.5.13 the diamond lemma as stated is false: In the case where r->s by E-IfFalse and r->t by E-Funny2, we have t->s, rather than s->u and t->u for any u. It should be restated as follows: LEMMA: If r->s and r->t, then either s->t or t->s or there is some u such that s->u and t->u. The argument in the diagram chase below must now be slightly refined to take the modified lemma into account. p 496, solution to 3.5.16 To fully capture the informal claim that "the original and new semantics agree," Proposition A.2 should be augmented with another (almost obvious) property: PROPOSITION: g --o-->* v iff g --w-->* v, for all original terms g. p 499, end of A.8 both occurrences (in cases E-IfTrue and E-IfFalse) of "then t2 else t2" should be "then t2 else t3" p 501, solution to 5.2.11 in the second to last line of the solution, sumlist should be sumlist' p 503, solution to 6.1.5 the subscripts in the third clauses should be just "Gamma", not "Gamma,x" p 507, solution to 9.3.10 The term given doesn't actually reduce under the call-by-value rules. A better example would be: (\x:Bool->Bool. \y:Bool. y) (\z:Bool. true true) p. 508, solution to 11.4.1 The third "x" on the second line should be deleted. p. 510, top of page The "\in" in the conclusion of rule P-Rcd' should be ":" p. 519, top two displays the derivations should say "\Gamma |- t : S" and "\Gamma |- t : U" rather than "\Gamma |- t \in S" and "\Gamma |- t \in U" p 526, solution to 16.4.1 The 'if' typing rule (+ alternative) uses normal turnstiles; it should use algorithmic turnstiles. p 539, solution to 21.3.4 "the set pairs R = {(T(pi),T(pi)) | pi in {1,2}*}" should be "the set of pairs R = {(Q,Q) | Q a subtree of T}" It is not quite true that (mu S) only relates finite types: every type (even an infinite one) is a subtype of Top. A more complex argument is needed here. In the second paragraph, "follow" should be "can" and "byu induction on the size T" should be "by induction on the sum of the sizes of S and T." p 542, solution to 22.3.9 The end of the proposed lemma should read "... do not appear in F'." p 546, solution to 23.4.6 false and true should be fls and tru p 562, solution to 30.5.1 FloatList should be just List ########################################################################### ########################################################################### ########################################################################### Errata for TYPES AND PROGRAMMING LANGUAGES (2nd printing) ========================================================== This section lists all the errors that I'm aware of in the second printing of TAPL (not counting the errors listed above). They should be corrected in the third printing. SUBSTANTIVE ERRORS ------------------ p 96, second line of proof of 8.3.2 T-IsZero should be T-Zero This error does *not* appear in the first printing. :-( p 280: The citations for early papers on syntactic properties of recursive types (without subtyping) should also mention an paper by Claude Pair, published in Algol Bulletin n. 31, March 1970, which contains what appears to be the first proof of the decidability of equality for equi-recursive types. A scanned copy of the paper has kindly been made available by Pierre Lescanne, at the following URL: http://www.ens-lyon.fr/~plescann/PUBLICATIONS/RecursiveTypes/ p 354, Theorem 23.6.2 The cited articles by Boehm (85 and 89) actually prove a slight variant of the stated result. Other variants (closer to the stated one) can be found in Pfenning (1993a). Surprisingly, though, the decidability of precisely this partial type inference problem appears still to be open. p 502, solution to 5.3.6 In the full beta-reduction rules, one is missing: t1 -> t1' --------------- (E-Abs) \x.t1 -> \x.t1' Also, na1' in rule E-App1 should be renamed t1'. ########################################################################### ########################################################################### ########################################################################### Errata for TYPES AND PROGRAMMING LANGUAGES (1st printing) ========================================================== The following errors appear only in the first printing -- they should all be corrected in the second printing (Summer, 2002). The errors listed above are also present in the first printing. SUBSTANTIVE ERRORS ------------------ p xxi Erik Hilsdale's name is spelled with a k Fermin Reig's name should be typeset Ferm\'{\i}n p 71, last line of display near top of page There should be a close-paren after the second t1. p 96, second to last line of T-If case in proof of 8.3.2 T-If should be E-If p 97, T-If case in proof of 8.3.3 E-True and E-False should be E-IfTrue and E-IfFalse p 107, end of first para The annotation on y should be T2, not T1 p 146 footnote 9 is redundant with Exercise 11.12.2. p 168, para 3, line 5 \mu should be \Sigma in "or else it is exactly ..." also, in line 7 of the paragraph below Thm 13.5.3 (\mu, l \mapsto v_1) should be [l \mapsto v_1]\mu p 208, chapter quote Mannasse should be Manasse p 226, footnote 1: "Other languages, such as and , ...". The words "Java" and "C++" are missing p 268, picture the braces in "{nil: , cons: }" should look like "" p 320, Example 22.2.2 The last solution is wrong. Correct alternatives include: ( [ X |-> Nat -> Nat -> Nat, Y |-> Nat ], Nat -> Nat ) or ( [ X |-> Nat -> Nat, Y |-> Nat ], Nat ) p 321, para 1, 3rd to last line t_1 should be T_1 p 324, line 3 "Is a solution for (Gamma, t2, S2, C)" should be "Is a solution for ((Gamma,x:T1), t2, S2, C)" p 325, lines 3 and 4 T2 should be S2 in the third line and T1 should be S1 in the fourth line. p 394 In the rule S-All, the premise "Gamma |- U1 :: K1" should be omitted. p 425, lemma 28.4.1, case 1: ``Suppose that $\Gamma$ is a'' should be ``Suppose that $\Delta$ is a'' p 497, subcase g1 = succ g1 The argument for this subcase should conclude "From this derivation, w we construct a derivation of g -->* if wrong then g2 else g3, which w after a final instance of E-If-Wrong yields g -->* wrong p 499, Lemma A.8, E-IfTrue and E-IfFalse cases the second t_2 should be t_3 p 499, 4.2.1 the constructor 'Some' was incorrectly typeset (twice) as \exists p 503, solution 5.3.8 t' should be called v p 505 to 507 exercise 9.4.1 is misfiled (it can be found between 9.2.3 and 9.3.2) p 506 solution to 9.3.2 ".... But this means that size(T1) is strictly greater than size(T1 -> T2), ..." should read "... size(T1) is equal to size(T1 -> T2) ..." [It is impossible because all types in this system have finite size.] Also, there is no formal definition of the "size" of a type. This can be taken to be the number of nodes in its tree representation. p 507, solution to 11.3.2 The conclusion in T-Wildcard should read Gamma |- \_:T1.t2 : T1->T2 not Gamma |- \_.t2 : T2 p 538, lines 1 and 8 $X \subseteq P$ implies $F(X) \subseteq P$ should be $F(P) \subseteq P$ p 541, proof sketch of Lemma A.17 The first sentence should read "By induction on k = mu-height(S)." ======================================================================== GRAMMATICAL / TYPOGRAPHICAL / COSMETIC ERRORS --------------------------------------------- p 15 The font used for (the set) T in 2.1.1 and 2.1.5 is inconsistent with the rest of the chapter. Ditto U in 2.1.5. p 19 "P(0)" should be slanted in 2.4.1 p 25 "in under" --> "under" "is does not" --> "does not" The paragraph beginning "for brevity" would make more sense if it were moved just before the example higher on the page. p 27 concete --> concrete p 56 the middle item in the first sample reduction sequence has an extra pair of parens p 57 all occurrences of "call by X" should be hyphenated (except, arguably, the first use of "call by need") p 71, last line the RHS should (arguably) be parenthesized to match the corresponding line at the top of the page p 142 top line is garbled (some latex markup for index entries got into the text instead) p 155, first line missing "of" between "result" and "the" p 220, exercise 16.3.4 15-5 should be 15.5 p 301 'An sample' -> 'A sample' p 303, line -8 "we claim that R={...}" -> "we claim that R={...} is such a set" p 334, para 1, line 1 "One caveat is here that" should be "One caveat here is that" p 338, para 4, 2nd to last line "e.g. using by" should be "e.g. by using" p 439, para 3, line 2 "type constructorstype operators" should be just "type constructors" p 444, footnote wrong font for ' p 488, first sentence of 32.10 it introduced => it was introduced p 500, solution 5.2.4 the names of the arguments m and n should be exchanged