Types, Expressions, States, Quantified Predicates

HW 2: Classes 3 - 4
Types, Expressions, States, Quantified Predicates
CS 536: Science of Programming
2022-09-12 Group policy, Problems #6d, #9; 09-13 #8, #9
A. Formatting and Submitting Your Work
• Remember to use a word processor to write out your answers. Quantified variables range over ℤ
unless otherwise specified.
• New Policy: For the group work, you can work in groups of 2 or 3 (preferably 3). You can work by
yourself in a group of 1 but there's a 5% penalty (3 points out of 60). [no penalty for HW 2]
• [2022-09-13] To speed up grading, be sure to include your group number and a list of the group
members' userids and A# numbers. Use *.pdfs, not *.doc files.
B. Problems [60 points total]
Class 3: Types, Expressions, and Arrays
1. (6 = 3 * 2 points) For each of the following, is the expression legal or illegal according to the
syntax we're using. If illegal, why? If legal, what is the type of the resulting expression? Below,
assume b1, and b2 are one-dimensional and b3 is two-dimensional.
a. ( x < y ? T : y ) // Note < works on integers, not booleans
b. match(b1, b2, n) // Are the first n elements of b1 and b2 equal (component-wise)?
// I.e., b1[0] = b2[0], b1[1] = b2[1], ....
c. b3[0] + b3[2][3]
2. (6 = 3 * 2 points) For each set below, is it a well-formed state? If not, why? *
a. {x = (4), y = 5} // Is the value of x an integer or a short array?
b. {u = (3, 4), v = 0, w = u[1] }
c. {r = one, s = four, t = r + s}
3. (4 = 2 * 2 points) Let σ = {x = 2, b = β} where β = (7, 12, 3, 0).
a. Rewrite σ giving the value of b as a set of ordered pairs.
b. Rewrite σ giving the value of b as separate bindings for b[0], b[1], etc.
4. (6 = 3 * 2 points) Let φ ≡ x = y*z ∧ y = 4*z ∧ z = b[0] + b[2] ∧ 2 < b[1] < b[2] < 5. Complete the
definition of σ = {x = ____, y = ____, z = 5, b = __________ } so that σ ⊨ φ. If some value is
unconstrained, give it a greek letter name (δ, ζ, η, .... your choice).
 For this assignment, a lot of semantic values are underlined for emphasis (but not necessarily all of them). *
CS 536: Science of Programming – 1 – © James Sasaki, 2022
Illinois Institute of Technology Tue 2022-09-13, 1713 HW 2: Classes 3 - 4
5. (8 = 4 * 2 points) Take the expression 0 * b[b[k]]. For each state below, is it well-formed and
proper for the expression? And if so, does the expression terminate correctly (and with what
result)? If not, why?
a. {k = 0, b = (3, 6, 1, 4), c = (2)}
b. ∅
c. {k = 0, b = 3}
d. {b = (3), k = 0}
Class 4: State Updates, Satisfaction of Quantified Predicates
6. (9 points) Let σ₀ = {x = 2, y = 4, b = (-1, 4, 3, 9, 10)}.
a. [2 points] Is there a difference between σ₀[z ↦ 1] and σ₀ ∪ {(z, 1)} ? Very briefly justify your
answer. (A sentence should be fine.)
b. [2 points] Repeat, on σ₀[x ↦ 4] and σ₀ ∪ {(x, 4)}.
c. [2 points] Let σ₁ = {x = β+3, y = 2 β, b = (β, 0, 2 β, β)} where β = 2. What is σ₁[ b[0] ↦ σ₁(b[2]) ]?
d [3 points] Now let τ = σ₁[ b[0] ↦ σ₁(b[2]) ]. What is τ[ b[1] ↦ σ₁(b[1]) + 8 ]? [2022-09-12]
7. (6 = 3 * 2 points) For each of the following, say whether the state satisfies the quantified
predicate (and if not, briefly why). Give a witness value (for satisfied existentials) or a
counterexample (for unsatisfied universals).
a. Does {x = 4, y = 7, b = (5, 4, 8)} ⊨ (∃ x. ∃ m. b[m] < x < y) ? If not, why?
b. Does {x = 1, b = (2, 8, 9)} ⊨ ( ∀x. ∀k. 0 < k < 3 → x < b[k] ) ? If not, why?
c. Does {x = 0, b = (5, 3, 6)} ⊨( ∀x. ∀k. 0 < k < 3 ∧ x < b[k] ) ? If not, why?
8. (9 = 3 * 3 points) In English, explain briefly when each of the following holds.
a. ⊭ (∀ x ∈ V . (∃ y ∈ U . P(x, y)) ∧ (∀ z ∈ U . Q(x, z)))
b. ⊭ ∀ y ∈ V . ((∃ x ∈ W. P(x, y)) → (∃ y ∈ U . Q(y, y))) [2022-09-13]
c. σ ⊭ (∃ x ∈ W . (∀ y ∈ U . P(x, y)))
9. (6 points) Write a definition for a predicate function Subset(b1, b2, x, y) ≡ … such that {b1[0],
b1[1], …, b1[x]} ⊆ {b2[0], b2[1], …, b2[y]}. For example, say we have a state where b1 = (0, 3, 7,
2, 1, 4) and b2= (0, 2, 7, 3, 3, 5) [2022-09-13], then [See class 2 for discussion of predicate
functions]
• Subset(b1, b2, 3, 5) is true because {0, 3, 7, 2} ⊆ {0, 2, 7, 3, 3, 5}.
• Subset(b2, b1, 5, 3) is false because {0, 2, 7, 3, 3, 5} ⊈ {0, 3, 7, 2}.
• Subset(b1, b2, 2, 2) is false because {0, 3, 7} ⊈ {0, 2, 7}. [2022-09-13]
• Subset(b2, b1, 2, 3) is true because {0, 2, 7} ⊆ {0, 3, 7, 2}. [2022-09-13]
CS 536: Science of Programming – 2 – © James Sasaki, 2022
Illinois Institute of Technology Tue 2022-09-13, 1713 HW 2: Classes 3 - 4
If x or y are illegal as indexes for b1 or b2 respectively, have P return false. (You can add this as
an explicit test or have it work implicitly -- either way is fine.) Feel free to write helper predicate
functions if it makes your life easier.
CS 536: Science of Programming – 3 – © James Sasaki, 2022