Formal Foundations of Computer Science 1 (Errata)
Formal Foundations of Computer Science 1 (Errata) |
|
Wolfgang Schreiner
Replace
forall x0, ..., xn-1, y: f(x0, ..., xn-1) = y <=> (<x0, ..., xn-1> in A /\ y = T).by
forall x0, ..., xn-1: <x0, ..., xn-1> in A => f(x0, ..., xn-1) = T.
Drop
(usually x is free in A).
Add
(usually x is free in A).
Replace
by
forall S, R: R is equivalence class on R => x in [x]R.
forall S, R: R is equivalence relation on S => forall x in S: x in [x]R.
Replace
for every formula F: (F(0) /\ forall x in N: F(x) => F(x+1)) => forall x in N: F(x).
by
where the quantified variable F denotes a unary relation.
forall F: (F(0) /\ forall x in N: F(x) => F(x+1)) => forall x in N: F(x).
Replace
A number greater than 1 is prime (prim) if its only divisors are are 1 and itself:
by
A number greater than 1 is prime (prim) if its only divisors are 1 and itself:
Replace
x * y := ((x0 *R y0) -R (x1 *R y1)) + ((x0 * R y1) + (x1 *R y0))i;
by
x * y := ((x0 *R y0) -R (x1 *R y1)) + ((x0 * R y1) +R (x1 *R y0))i;
Replace
(x+(-y))+y = (associativity of+)
by
(x+(-y))+y = (associativity of +)
Replace "for some x" by "for every x".
Replace
s is a finite sequence over S : <=>by
exists n in N: s is a sequence of length n over S.
s is a finite sequence over S : <=>
exists n in N: s is a sequence of length n over S.
Replace
A0 = 0, A1 =0, A2 = 3; A3=1; A4=2.
by
A0 = 0, A1 =0, A2 = 3; A3=1; A4=1.
Replace
x <= a /\ x < b
by
a <= x /\ x < b
Replace
is used to denote (sum0 <= i <= a T).
by
is used to denote (suma <= i <= b T).
Replace
(prodx, F T) = T[x <- y] + (prodx, F /\ x != y T)).
by
(prodx, F T) = T[x <- y] * (prodx, F /\ x != y T)).
Replace
(n k) = (prodn-k+1 <= i <= n i)/(prod1 <= i <= n i).
by
(n k) = (prodn-k+1 <= i <= n i)/(prod1 <= i <= k i).
Replace
[ ]: Poly x R -> R p[a] := (sum0 <= i <= deg(p) pi*ai).
by
[ ]: Poly x R -> R p[a] := (sum0 <= i <= deg(p) pi *R ai).
Replace
cPoly[a] = cPoly, x[a] = aPoly, (p+q)[a] = p[a] + q[a], (p*q)[a] = p[a] * q[a].
by
cPoly[a] = c, x[a] = a, (p+q)[a] = p[a] +R q[a], (p*q)[a] = p[a] *R q[a].
Replace
(x+1)[2] = 2+1 (= 3Poly) (x*x)[2] = 2*2 (= 4Poly) (x*x+2*x+1)[3] = 3*3+2*3+1 (= 16Poly)
by
(x+1)[2] = 2+1 = 3 (x*x)[2] = 2*2 = 4 (x*x+2*x+1)[3] = 3*3+2*3+1 = 16
Replace
a in A /\ c in C
by
a in domain(R) /\ c in range(S)
Replace
Proposition
by
Definition
Replace
is the base formula in which f does not occur and where every application of f in the recursion formula
by
is the base formula in which p does not occur and where every application of p in the recursion formula
Replace
The number of permutations of length n is 2n:forall n in N: |{f: f is permutation of length n}| = 2n.
by
The number of permutations of length n is n!:forall n in N: |{f: f is permutation of length n}| = n!.
Replace
Assume |{f: f is permutation of length n}| = 2n.
by
Assume |{f: f is permutation of length n}| = n!.
Replace
Thus we can define a "polar" variant of CC' := R x [0,2pi[assuming that angles are uniquely expressed in "radians" (i.e., pi = 180 o ).
by
Thus we can define a "polar" variant of CC' := (R> 0 x [0,2pi[) union {<0,3 pi /2>}where we assume that angles are uniquely expressed in "radians" (i.e., pi = 180 o ) and assign to the zero point the unique (but arbitrary) angle 3 pi /2 (see the definition of "polar" given below).
Replace
Every set is smaller than the set of all functions into it:
forall A, B: B is smaller than A -> B.
by
Every set is smaller than the set of all functions from an infinite domain into it:
forall A, B: A is infinite => B is smaller than A -> B.
Replace
(4) n+1 < 2n+1 <= 2n+2n = 2*2n = 2n+1
by
(4) n+1 < 2n+1 <= 2n+2n = 2*2n = 2n+1
Replace
for some constructors "empty" and "tree".
by
for some constructors "empty" and "node".
Replace
An element of "Formula" is "forall(X, and(T, or(T, F)))" (assuming X in "Variable").
by
An element of "Formula" is "forall(X, and(T, and(T, T)))" (assuming X in "Variable").
Replace
value: Term -> N value(0) := 0N value(1) := 1N value(-x) := -Nvalue(x) value(x+y) := value(x)+Nvalue(y) value(x*y) := value(x)*Nvalue(y)
by
value: Term -> Z value(0) := 0Z value(1) := 1Z value(-x) := -Zvalue(x) value(x+y) := value(x)+Zvalue(y) value(x*y) := value(x)*Zvalue(y)
Replace
(exists x: A) /\ (exists x: B) (exists x: A /\ B)
by
(exists x: A /\ B) (exists x: A) /\ (exists x: B)
Change the example to
Let s := [(-1)i*1/i]i. We show that s converges to 0. Take arbitrary epsilon > 0. We have to find some n in N such thatforall i >= n: |(-1)i*1/i - 0| < epsilonwhich can be simplified toforall i >= n: 1/i < epsilon .Take n := such n in N: 1/ epsilon < n. Because epsilon > 0, we know 1/ epsilon in R>0. Because N is unbounded (i.e., forall r in R: exists n in N: r < n), we know 1/ epsilon < n and thus n > 0.Take arbitrary i >= n. We then know i > 0 and
1/i <= 1/n < 1/1/ epsilon = epsilon .
Replace
f is surjective (surjektiv) (also called onto) if it
by
f is surjective (surjektiv) (also called onto) if
Replace
f is monotonically decreasing (monoton wachsend)
by
f is monotonically decreasing (monoton fallend)
Replace
f is strictly monotonically decreasing (streng monoton wachsend)
by
f is strictly monotonically decreasing (streng monoton fallend)
Replace
f has a lower bound (untere Schranke) L, if every element of f is lower than or equal L:L is lower bound of f : <=> f: N -> R /\ forall i in N: fi <= L.
by
f has a lower bound (untere Schranke) L, if every element of f is greater than or equal L:L is lower bound of f : <=> f: N -> R /\ forall i in N: fi >= L.
Replace
(f+g)(x) := f(x) - g(x);
by
(f-g)(x) := f(x) - g(x);
Replace
if we shift it up one unit, it lies completely above the floor function
by
if we shift it up one unit, it lies completely above the ceiling function
Replace
If we have to show G0 <=> G1 <=> G2, i.e., (G0 <=> G1) /\ (G1 <=> G0),
by
If we have to show G0 <=> G1 <=> G2, i.e., (G0 <=> G1) /\ (G1 <=> G2),
Replace
~~>
K G0 /\ G1 ~~>
K union {~G0 \/ ~G1} F(alse)
K union ~G0 F(alse)
K union ~G1 F(alse)
by
~~>
K G0 /\ G1 ~~>
K union {~G0 \/ ~G1} F(alse)
K union {~G0} F(alse)
K union {~G1} F(alse)
Replace
~~>
K G0 \/ G1
K union ~G0 G1
by
~~>
K G0 \/ G1
K union {~G0} G1
Replace
For proving the goal F[x <- G(a0, ..., an-1)] where f is a function explicitly defined asG(x0, ..., xn-1) := T,it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]] (for some terms T, a0, ..., an-1):
~~>
K union {forall x0, ..., xn-1: G(x0, ..., xn-1) = T} G[x <- G(a0, ..., an-1)]
K union {forall x0, ..., xn-1: G(x0, ..., xn-1) = T} G[x <- T[x0 <- a0, ..., xn-1 <- an-1]]
by
For proving the goal G[x <- F(a0, ..., an-1)] where F is a function explicitly defined asF(x0, ..., xn-1) := T,it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]] (for some terms T, a0, ..., an-1):
~~>
K union {forall x0, ..., xn-1: F(x0, ..., xn-1) = T} G[x <- F(a0, ..., an-1)]
K union {forall x0, ..., xn-1: F(x0, ..., xn-1) = T} G[x <- T[x0 <- a0, ..., xn-1 <- an-1]]
After the definition: replace
We have to prove F[x <- G(a0, ..., an-1)]. By definition of G, it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]].
by
We have to prove G[x <- F(a0, ..., an-1)]. By definition of F, it suffices to prove G[x <- T[x0 <- a0, ..., xn-1 <- an-1]].
Replace
~~>
K G (F holds in every domain in which K holds).
K union F G
by
~~>
K G (F holds in every domain in which K holds).
K union {F} G
Replace
If A is of size n, then A has 2n subsets:
forall A, n in N: |A| = n => |{S in P(S): T}| = 2n.
by
If A is of size n, then A has 2n subsets:
forall A, n in N: |A| = n => |P(A)| = 2n.
Replace
t is sorted with respect to <= : <=> forall 0 <= i < length(t): ti <= ti+1.
by
t is sorted with respect to <= : <=> forall 0 <= i < length(t)-1: ti <= ti+1.
Replace
(x + y)[a] = x(a) +R y(a) (x - y)[a] = x(a) -R y(a) (-x)[a] = -Rx(a) (x * y)[a] = x(a) *R y(a)
by
(x + y)[a] = x[a] +R y[a] (x - y)[a] = x[a] -R y[a] (-x)[a] = -Rx[a] (x * y)[a] = x[a] *R y[a]
Replace
cartesian: C ->iso(*C, *C') C' polar: C' ->iso(*C', *C) C
by
polar: C ->iso(*C, *C') C' cartesian: C' ->iso(*C', *C) C
Replace the picture by
Replace
Again, since we don't know the truth of G for sure, we generally we have two possibilities:
by
Again, since we don't know the truth of G for sure, we generally have two possibilities:
Replace
[i3]i has no upper bound and no lower bound.
by
[i3*(-1)i]i has no upper bound and no lower bound.
Replace picture by
Replace
Thus our definition of Z meets one of the two requirements stated at the begin of this section.
by
Thus our definition of Z meets one of the two requirements stated at the beginning of this section.
Also on page 117, after proof: replace
Our definition of Q meets one of the two requirements stated at the begin of this section.
by
Our definition of Q meets one of the two requirements stated at the beginning of this section.
Also on page 121, after example: replace
Then we have the following result which implies that the problem stated at the begin of this section can be solved.
by
Then we have the following result which implies that the problem stated at the beginning of this section can be solved.
Also on page 124, after Definition 152: replace
This imaginary constant is the "missing value" that solves the equation stated at the begin of this section.
by
This imaginary constant is the "missing value" that solves the equation stated at the beginning of this section.
Replace
Thenp o q = [1,2,0,4,3],e.g., (p o q)(2) = q(p(2)) = q(4) = 0. We also havee.g., p-1(2) = 1 because p(1)=2, and thus
p-1 = [2,0,1,4,3]
p o p-1 = p-1 o p = [0,1,2,3,4].
by
Thenr := p o q = [1,2,0,4,3],e.g., r(2) = (p o q)(2) = q(p(2)) = q(4) = 0. We also havee.g., r-1(2) = 1 because r(1)=2, and thus
r-1 = [2,0,1,4,3]
r o r-1 = r-1 o r = [0,1,2,3,4].
Replace
Let r(x, y) : <=> x0+y0 = x1+y1. Then r is an equivalence relation on R x R.
by
Let r(x, y) : <=> x0+y1 = x1+y0. Then r is an equivalence relation on R x R.
Replace
Take k:=ka+kb and f(i):=if i < ka then fa(i) else fb(i).
by
Take k:=ka+kb and f(i):=if i < ka then fa(i) else fb(i-ka).
Replace
i(0Z') = 0Z, i(x+Z'y) = x+Zy, i(-Z' x) = -Z x, i(x-Z'y) = x-Zy, i(x*Z'y) = i(x)*Zi(y), x <= Z' y <=> i(x) <= Z i(y).
by
i(0Z') = 0Z, i(x+Z'y) = i(x)+Zi(y), i(-Z' x) = -Z i(x), i(x-Z'y) = i(x)-Zi(y), i(x*Z'y) = i(x)*Zi(y), x <= Z' y <=> i(x) <= Z i(y).
Replace the proof by
Take arbitrary x in Z' and y in Z'. We proveWe know
i(x+Z'y) = i(x)+Zi(y).
i(x+Z'y) = i(I(x0 +N y0, x1 +N y1)).
- Case x0 +N y0 >= x1 +N y1:
- We have
i(I(x0 +N y0, x1 +N y1)) = i(<(x0 +N y0) - (x1 +N y1)>) = [<(x0 +N y0) - (x1 +N y1)>] = (definition ~ Z) [<x0 +N y0, x1 +N y1>] = (congruence properties) [x] +Z [y] = i(x) +Z i(y). - Case x0 +N y0 < x1 +N y1:
- Proceeds analogously.
Replace
i(0Q') = 0Q, i(x+Q'y) = x+Qy, i(-Q' x) = -Q x, i(x-Q'y) = x-Qy, i(x*Q'y) = x*Qy, i(x-1) = x-1, i(x/Q'y) = x/Qy, x <= Q' y <=> i(x) <= Q i(y).
by
i(0Q') = 0Q, i(x+Q'y) = i(x)+Qi(y), i(-Q' x) = -Q i(x), i(x-Q'y) = i(x)-Qi(y), i(x*Q'y) = i(x)*Qi(y), i(x-1) = i(x)-1, i(x/Q'y) = i(x)/Qi(y), x <= Q' y <=> i(x) <= Q i(y).
Replace
B := {x in N: x is odd /\ x is not prime}.
by
C := {x in N: x is odd /\ x is not prime}.
Replace
Let r subset R x R such that r(x, y) <=> x0+x1 = y0+y1.
by
Let r subset (R x R) x (R x R) such that r(x, y) <=> x0+x1 = y0+y1.
Replace definition by
A binary relation on S is a quasi order (Quasi-Ordnung), if it is irreflexive and transitive:
R is quasi order on S : <=> R subset S x S /\ R is irreflexive on S /\ R is transitive on S.
Replace
Please note that an lower (respectively upper bound) of a set S need not be an element of S:
by
Please note that a lower (respectively upper) bound of a set S need not be an element of S:
Replace
A path from x to y has initial node x and terminal node y : <=>
by
A path from x to y has initial node x and terminal node y:
Replace
reflexiveN5(E) = {<0, 0>, <1, 1>, <2, 2>, <3, 3>, <4, 4>}.
by
reflexiveN5(E) = E union {<0, 0>, <1, 1>, <2, 2>, <3, 3>, <4, 4>}.
Replace
forall S, R: R subset S x S => reflexiveS(R) = R union (S x S).
by
forall S, R: R subset S x S => reflexiveS(R) = R union {<x, x>: x in S}.
Replace
If x is an element of S such that no element of S is smaller than S, then x is called a minimal element (minimales Element) of S.
...
Correspondingly, if x is an element of S such that no element of S is greater than S, then x is called a maximal element (maximales Element) of S.
by
If x is an element of S such that no element of S is smaller than x, then x is called a minimal element (minimales Element) of S.
...
Correspondingly, if x is an element of S such that no element of S is greater than x, then x is called a maximal element (maximales Element) of S.
Replace
A directed graph (gerichteter Graph) is a pair <V, E> of a set V of vertices (Knoten) or nodes and a set of E of edges (Kanten) or arcs where E is a binary relation on S:
by
A directed graph (gerichteter Graph) is a pair <V, E> of a set V of vertices (Knoten) or nodes and a set of E of edges (Kanten) or arcs where E is a binary relation on V:
Replace
Both nodes are then adjazent.
by
Both nodes are then adjacent.
Replace
w := such u in W_n-1: forall i in N_n-1: u_i = w_i+1
by
w := such u: exists n in N: w in W_n /\ u in W_n-1 /\ forall i in N_n-1: u_i = w_i+1
Replace
w <= _n u : <=> n = 0 \/ w_0 < u_0 \/ (w_0 = u_0 /\ w <= _n-1 u)
by
w <= _n u : <=> n = 0 \/ w_0 < u_0 \/ (w_0 = u_0 /\ w <= _n-1 u)
Replace
length(p) := such n in N: p: Nn+1 -> V.
by
length(p) := such n in N: exists V: p: Nn+1 -> V.
Replace
p is elementary : <=> forall i in Nn, j in Nn: pi = pj => i = j where n = length(p).
by
p is elementary : <=> forall i in Nn, j in Nn: pi = pj => i = j where n = 1+length(p).
Replace
Let Q' denote the old construction of the integers and Q denote the new one.
by
Let Q' denote the old construction of the rationals and Q denote the new one.
Drop the
return C;
Replace
(see the example on page 105)
by
(see the example on page 265)
Replace
In other words, the transitive closure of R is the union of all members of the sequence
by
In other words, we can compute the transitive closure of R by the sequence
Replace
if we are given some knowledge, we must able to check it (i.e., its proof).
by
if we are given some knowledge, we must be able to check it (i.e., its proof).
Replace
the skeleton provided by the proof rules help us
the skeleton provided by the proof rules helps us
Replace
and the proof that the square root of 2 is not rational on page 4.4
by
and the proof that the square root of 2 is not rational on page 118
Replace
if F holds in every domain in which (some of) the formulas in K holds.
by
if F holds in every domain in which (some of) the formulas in K hold.
