For convenience, we will refer to each change using the number of the page on which it appears. Detailed explanations are given below.
VAR x, y.
VAR j.
We have decided to delimit lambda expressions using parentheses, to match the format of mu expressions. So the function expression
\lambda n : \nat \spot n + n + nwill now appear as
(\lambda n : \nat \spot n + n + n)This change has been made throughout the book.
We have decided to delimit lambda expressions using parentheses: see the update for Page 102.
In the definition of bag count - the sharp symbol - the lowercase x in the declaration part ought to be an uppercase X - it is an instance of the generic parameter.
The proof tree on this page should include the additional
constraints |t1 \in Tree| and |t1 \in Tree|
on its top line (part of Assumption 1).
We have decided to delimit lambda expressions using parentheses: see the update for Page 102.
In the sequence displayed at the bottom of the page, there should be an additional comma after the second item.
The declaration of contents in the proof uses a maplet symbol, when it should be using a partial function symbol.
The two schemas File and System are missing from the
declaration part of the displayed schema that follows `applying the
definition of Promote to yield'. Also, it would be more
sensible to write \{ File \spot \theta File \}.
The instance of Local half-way down the page should read File instead: this is the name for the local data type in this application of promotion.
We have decided to model resources as natural numbers, so the two instances of the set Resource should be replaced with the set of natural numbers.
The predicate part of the schema Store has been transposed to match the predicate part of Read; this should make it more obvious that the two preconditions are complementary.
The two instances of CSystems' should both read CSystem'.
The phrase The temperature can always be incremented, provided that the value does not go below the maximum should read The temperature can always be incremented, provided that the value does not go above the maximum.
using to the laws of the relational calculus should read using the laws of the relational calculus.
The example of local block introduction declares x and
y but omits the range. The declaration should read
VAR x, y : T
The local block introduction at the bottom of the page declares a
variable j but omits the range. The declaration should
read
VAR j : 1 .. n+1
The phrase we have that shown should read we have shown that.
| text | slides | exercises | solutions | cards | contents |