| P1: | B ∨ C |
| P2: | B ⟹ (D ∨ E) |
| P3: | D ⟹ (F ∧ A) |
| P4: | (A ∧ ¬E) ⟹ ¬ F | P5: | ¬E |
the conclusion C follows. (Note that none of the parentheses are needed, due to both conjunction and disjunction having higher precedence than implication. They were included to reduce the likelihood that a student would make an incorrect interpretation.)
2. Repeat the previous problem, but this time show a proof that conforms to the style of Gries & Schneider. Here it will be very useful to rewrite premise P1 as ¬B ⟹ C and to rewrite premises P2 and P3 by applying Contrapositive (3.61). Expect to make use of Theorem (4.3), with the roles of p and q being played by the antecedant and consequent, respectively, of one of the premises.
3. Given are functions with types (i.e., signatures) as follows:
| x : A | y : B | f : A → A | g : A → B | h : B × A → A |
(Note that x and y 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) g.x | (b) f(g.x) | (c) g(f.x) | (d) f(h(g.x,x)) | (e) h(y,g.x) | (f) h(g.x, h(g.x,f.x)) |
Recall that Gries & Schneider denote function application by a period (or "full stop", if you prefer), as in f.x, when the argument is atomic, but they use the more traditional notation when the function's argument is non-atomic (e.g., f(f.x)).
4. Let s be the state
To clarify, b[0..7):(5,2,-4,3,-1,0,9) means that b is an array with index range [0..7) and that b[0] has value 5, b[1] has value 2, ..., b[6] has value 9.
Each problem presents an expression E. You are to
(a) Indicate, for each occurrence of a variable in E,
whether it is bound or free, and
(b) Evaluate E in state s. (Show your work.)
(i) (i-j) + (+i | j≤i≤k : b[i])
(ii) (∀j | i≤j<k : (∃m | 0≤m<j : b[m] > b[j]))
(iii) (d ∨ i≠j) ≡ ((MAX j | 1<j≤k : b[i+j]) > k)
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
5. Making use of this definition, show (in step-by-step fashion) the result of carrying out the following textual substitutions:
(a) (★x | 0 ≤ x < n-v : x+v)[v := w+1]
(b) (★x | 0 ≤ x < n+r : x+v)[x := 3]
(c) (★x | 0 ≤ x < n+r : x+v)[n := n-x]
(d) (★x | 0 ≤ x < r :
(★y | 0 ≤ y ≤ x : x+y+n))[r := y+1]
(e) (★x | 0 ≤ x < r :
(★y | 1 ≤ y < x: x+y+n))[n := x+y]
The remaining problems call for the use of the theorems in Chapter 8 of Gries and 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 ℕ→ℕ.
6. Prove
(a)
(★i | 0≤i<10 : P) =
(★i | 0≤i<4 : P) ★ (★i | 4≤i<10 : P)
(b)
(★i | 0≤i<10 : P) =
(★i | 0≤i<4 : P) ★ P[i:=4] ★
(★i | 5≤i<10 : P)
7. Prove (★i | 0≤i<10 : P) ★ (★i | 0≤i<6 : Q) = (★i | 0≤i<6 : P★Q) ★ (★i | 6≤i<10 : P)
8. Prove (∧i | 0≤i<10 : P) = (∧i | 4≤i<10 : P) ∧ (∧i | 0≤i≤6 : P)
Hint: Make use of one of the properties of conjunction.