1. Given are functions with types as follows:
| a : A | b : B | f : A → A | g : A → B | h : A × B → A |
(Note that a and b are zero-argument functions, which is to say that they are constants.)
For each of the following expressions, indicate its type (i.e., the type of the value obtained by evaluating the expression) or else indicate that it is not "type correct". In the latter case, identify a smallest subexpression that is a source of the incorrectness.
| (a) f.a | (b) g.a | (c) g.b | (d) f(g.a) | (e) f(f.a) |
| (f) f(h(a,b)) | (g) g(h(a,b)) | (h) f(h(g.a,a)) | (i) h(f.a,g.a) | (j) h(h(f.a,g.a),g.a) |
Recall that G&S denote function application by a period (or "full stop", if you prefer), as in f.a, when the argument is atomic, but they use the more traditional notation when the function's argument is non-atomic (e.g., f(f.a)).
2. Making use of this definition, show (in step-by-step fashion) the result of carrying out the following textual substitutions. In each one, ★ is some arbitrary associative and symmetric operator on numbers.
(a) (★x | v ≤ x < n : x+v)[v := v+2]
(b) (★x | 0 ≤ x < n : x+v)[x := 8]
(c) (★x | 0 ≤ x < n : x+v)[n := 2x+1]
(d) (★x | 0 ≤ x ≤ r :
(★y | 0 ≤ y : y+r))[r := y]
(e) (★x | 0 ≤ x ≤ r :
(★y | 1 ≤ y ≤ n : x+y+n))[n := x-y]
3. Let s be the state
To clarify, b[0..4]:(5,0,-4,2,1] means that b is an array with index range [0..5) and that b[0] has value 5, b[1] has value 0, ..., b[4] has value 1.
Let E be the expression
Note: Even if you have not thought about it this way before (or seen it treated this way in a math book), the max operator is conveniently considered to be a binary infix operator, just like addition, multiplication, conjunction, and disjunction. And, like those operators, it is associative and symmetric and thus is suitable for use as a quantification operator. End of Note
(a)
Indicate, for each occurrence of a variable in E,
whether it is bound or free.
(b) Compute s.E (i.e., the value of E
in state s)
Show your work.
The remaining problems call for the use of the theorems in Chapter 8 of Gries & Schneider. In particular, Theorem (8.24) will be useful in several problems for the purpose of rewriting the range of a quantification.
Essentially, what (8.24) says is that if b≤c≤d, then we can split up the range [b..d) into two ranges: [b..c) and [c..d). In other words, if b≤c≤d, the expression b≤i<d is equivalent to b≤i<c ∨ c≤i<d.
In Problems 4 and 5, assume that ★ is an associative and symmetric binary operator having an identity element. In Problems 7 and 8, f is a function of type ℕ×ℕ→ℕ. In Problem 9, g is a function of type ℕ→ℕ.
4. Prove
(a)
(★i | 0≤i<11 : P) =
(★i | 0≤i<5 : P) ★ (★i | 5≤i<11 : P)
(b)
(★i | 0≤i<11 : P) =
(★i | 0≤i<5 : P) ★ P[i:=5] ★
(★i | 6≤i<11 : P)
5. Prove (★i | 1≤i<10 : P) ★ (★i | 1≤i<5 : Q) = (★i | 1≤i<5 : P★Q) ★ (★i | 5≤i<10 : P)
6. Prove (∨i | 1≤i<10 : P) = (∨i | 1≤i≤7 : P) ∨ (∨i | 4≤i<10 : P)
Hint: Make use of one of the properties of disjunction (i.e., ∨).
7. Prove (+i | 0≤i<n : (+j | 0≤j<m : f.i.j)) = (+k | 0≤k<m : (+i | 0≤i<n : f.i.k))
8. Prove (+i,j | 0≤i≤j<n : f.i.j) = (+i | 0≤i<n : (+j | i≤j<n : f.i.j))
Keep in mind that the expression a≤b≤c is an abbreviation for the conjunction a≤b ∧ b≤c and that, by transitivity of ≤, a≤c is a consequence of that conjunction, so that a≤b≤c is (by Theorem (3.60)) equivalent to a≤b ∧ b≤c ∧ a≤c.
9. Prove (∧i,j | 0≤i≤j≤m : g.i ≥ g.j) = (∧i,j | 0≤i<j≤m : g.i ≥ g.j)
Hint #1: Starting with the LHS, rewrite the range R as R1 ∨ R2, where R1 (respectively, R2) covers all (i,j)-pairs in R's "truth set" in which i<j (respectively, i=j). Then use Axiom (8.16).
Hint #2: Manipulate the quantification having R2 as its range so as to obtain one of the form (∀i | Q : (∀j | j=i : P)), to which (8.14) can be applied.
Hint #3: Recall that ≥ is reflexive, which is to say that x ≥ x is true for all x.
Hint #4: If the body of a universal quantification is true, the whole quantification is equivalent to true. (See Theorem (9.8).)