Errata in the 7’th Edition (December 9, 2003)

Exercise 1.4.1: The dot below capital a is a misprint. Page 106, 2nd line below the 1st table: ’variable, then..’.

Read: ’variable or number, then..’. Section 1.20, line 12: ’..constructs that form statements as directives’.

Read: ’..constructs that may form statements without values as directives’.

Reason: Statements may be true, false or without a value.

In the latter case they contain at least one directive and are no terms. Page 133, line 12: ’[A ≡ ⊥]^{·} if..’. Read:’If [A ≡ ⊥]^{·} then..’.

Reason: If some information about A is revealed during the infinite

computation then A is not equal to ⊥. Page 145, lines 6 and 12: ’= (9.81+ 0̸.311)@3’. Read:’= (9.81+0.311)@3’. Section 3.8, line 4: ’≡ 0.333F ]^{o}’. Read:’≡ 0̸.333F ]^{o}’ Section 3.9, line 15: ’..integer division with round to [−∞]^{·}.’

Read: ’..division with rounding to [−∞]^{·}.’ Page 148, last line, and Page 609, last line before the type table:

’(d) [x = 10]^{·}..’. Read: ’(d) [x ≡ 10]^{·}..’.

Reason: Otherwise, (d) and (c) will make contradictory statements about terms like 10.0F^{2}. Section 4.11, line 6: ’..a definition of for..’. Read: ’..a definition of form..’. Section 4.12, line 8: ’..term reduction of the root of a syntax tree..’.

Read: ’..term reduction of the root of a parse tree..’.

Reason: As long as term (or macro) reductions are possible, the tree is no syntax tree. Exercise 5.3.1: ’..parse trees..’. Read: ’..syntax trees..’.

Reason: The macro definition (x) ¨= x is to be used for reducing the parse trees. Page 182, line 5 from below, and page 183, line 1: ’..(x + y)..’ Read: ’..(x :: y)..’. Page 188, The line before Mac rule HeadPair: ’The syntax tree of’.

Read: ’The parse tree of’. Reason: The tree contains directives and macros. Page 189, last line: (same misprint as on page 188). Page 190, line 3: ’ Lem ’. Read: ’ Lemma ’. Page 190, last line: ’..merelly’. Read: ’..merely..’. Page 192, line 4: ’..tail :: y..’. Read: ’..tail ≡ y..’. Page 192, line 6: ’..the third line..’. Read: ’..the second line..’. Page 192, line 14: ’is a replacement..’. Read: ’..is a reverse replacement..’. Page 192, 5th line from below: ’v::(x::y) tail ≡ v::(x::y) tail’. Read: ’v::(x::y) tail’. Page 194, 2nd and 3rd line from below: ’..lemmas and proofs..’.

Read: ’..the terms in lemmas and proofs..’. Mac lemma L6.14.4, p.198: Remove the dot in the lemma. Page 213 lines 14 and 16, Page 220 line 17, Page 530 last line in the ’Mac rules’ section,

Page 315 the last line, the first two lines in Section 8.16, Page 316 line 1, Page 354 line 8 from below, and Page 355 line 13: ’..bound variables..’. Read: ’..binding (and corresponding bound) variables..’.

Page 217, line 11: ’..be replacing all free..’. Read: ’..by replacing all free..’. Page 220, line 16: ’..substitutuions..’. Read: ’..substitutions..’. Page 307, line 10: ’..a variables..’. Read: ’..a variable..’.

Pages 313&522, Mac rule SubLambdaXYFreeFor: ’..freefor(λx.A,y,S)..’ Read: ’..freefor(λy.A,x,S)..’.

Section 10.9, line 1: ’..set of lists’. Read: ’..set of finite lists’. Page 353, line 7: ’(2 :: 1) tail ▷..’. Read: ’(2 :: 1) tail ≡ 1 ▷..’. (Continued)

Page 354, line 4 in Section 11.7: ’.. how-’. Read: ’.. How-’. Exercise 11.8.1 (b): ’..case(x,b,c)..’. Read: ’..case(x,b,d)..’. Section 11.9: The word ’formula’ appears several places in chapters 11 and 12.

It is synonymous with the word ’equation’. Page 358, the type table: The entries corresponding to one variable in Z^{+}

and the other in N should be Z^{+} instead of N (cf. the table in A.80). Page 363, lines 2 and 3 from below: ’..nlist(1+1)..’. Read: ’..nlist(1-1)..’. Page 363, line 1 in Section 11.20: ’..defintions..’. Read: ’..definitions..’. Exercise 11.23.2 and page 388 line L07: ’..f(¬x)..’. Read: ’..f_{9}(¬x)..’. Page 366, line 5: ’..Axioms..’. Read: ’..(Derivation) Rules..’. Page 366, The Table: Add the constructs [x ≡ y]^{·}, [x rule y:z]^{·}, [x ⊢ y]^{·} and [(x)]^{·}. Page 389, Mac proof of L13.5.3: ’L4: TailPair..’. Read: ’L4: Replace ▷ TailPair..’.

Reason: Contrary to the rule in line L5, TailPair is only used to reduce a part of the expression. Mac lemma L14.1.1: The expression x∨¬x∈T occurs 4 times in the lemma and its proof. The expression

should read (x∨¬x) ∈T. Due to the relatively high priority of ∈ these expressions are not equivalent.

Page 395, line 9 from below: ’L07: Reverse’▷ L1 ▷ L6..’. Read: ’L07: Reverse’▷ L6 ▷ L1..’.

Page 408, line 9: ’..which I present later.’.

Read: ’which I, however, do not show in this edition of the lecture notes.’. Page 410, line 10: ’..≡ y..≡ y..’. Read: ’..≡ x..≡ x..’. Page 410, lines 12 to 24: 0.1F should read 0̸.1F. Page 410, line 13: ’x + y - y ≡ 1F’ should read ’x + y - y ≡ 0F’. Page 410, lines 18 to 20: ’= 1’ should read ’= 0F’.

Answer 16.1.5: The three lemmas should be marked (b), (a) and (c) (in that order!)

Answer 16.3.2: ’(b) [x ≡ 0]^{·}’ should read ’(b) [n ≡ 0]^{·}’. Exercise 17.14.3, line 2: ’f_{10} ¨=..’ should read ’f_{10}(x) ¨=..’

Page 432, line 9: ’L2: MonotonicityHead..’. Read: ’L2: MonotonicityTail..’.

Page 433, the proofs of L17.16.4 and L17.16.5: ’L14: TUnequalF ▷ ..’.

Read: ’L14: TUnequalF ▷ L13 ▷ ..’. Section 18.3, line 2: ’..then [A]^{·} is true..’ should read ’..then [< A |x:=B >]^{·} is true..’.

Page 438, the two proofs of L18.5.1: In the lines L05 ’x·y’ should be read as ’x·x’.

Mac proof of L18.8.1, line L07: ’TypeZ+Z’ should be read as ’TypeZ·Z’ Mac proof of L18.8.1, line L10: ’..2·(x + 1 = z) ;’ should read ’..2·(x + 1) = z ;’

Mac proof of L18.2.2, line L5: ’TypeD_{∞}^{·}+D_{∞}^{·} ▷ ..’. Read: ’TypeD_{∞}^{·}+D_{∞}^{·} ▷ L3 ▷ L4 ▷ ..’.
Mac proof of L18.3.3, line L07: ’TypeZ+Z ▷ ..’. Read: ’TypeZ+Z ▷ L5 ▷ L6 ▷ ..’.

A.3, page 503, and E.1, page 679: The last ’)’ in ’(x ▷ y) ▷ z )’ should be deleted. A.4 (p.504), A.7 (p.507) and A.12 (p.512): The last A in the rules EqualAll,

EqualChoice and EqualExists should read B.

A.22, page 524: The last D_{∞}^{−∞} in the last row of the type tables should read D_{∞}^{∞}.
A.28, page 530: The first two occurences of < A|x := B > should read < x|y := z >.

A.47, in the Description: ’..the function..’. Read: ’..the term..’. A.61, page 582: In the type table ’x!’ should read ’x?’. A.86, page 616, the line after the heading Sort: ’[Mac rule x:y]^{·} is...’.Read: ’[x rule y:z]^{·} is...’. A.91, in the Description: ’..the first element..’. Read: ’..the last element..’. Type table, page 626: The two ’x tail’s should read ’x^{+}’. E.2, last line: Add ’ ˘> x ˘=y ˘> x ˘>y’ just before ’]’.