Types and Programming Languages Exercises

Preface

2 Mathematical Preliminaries

2.2 Ordered Sets

2.2.6

Exercise [★★ ↛]: Suppose we are given a relation R on a set S. Define the relation R′ as follows:

R′ = R ∪ {(s, s) | s ∈ S}.

That is, R′ contains all the pairs in R plus all pairs of the form (s, s). Show that R′ is the reflexive closure of R.

We need to show that:

• R′ is reflexive:
  • For every element s in S, we have (s, s) ∈ {(s, s) | s ∈ S} ⊆ (R ∪ {(s, s) | s ∈ S}) = R′, so R′ is reflexive.
• R ⊆ R′:
  • R ⊆ (R ∪ {(s, s) | s ∈ S}) = R′, so R ⊆ R′.
• R′ is smallest:
  • All elements in R′ is either an element in R or an element in {(s, s) | s ∈ S}, remove any element will cause R′ no longer containing either R or {(s, s) | s ∈ S}, which breaks the reflexive closure definition, so we can’t remove any element from R′, R′ must be smallest.

2.2.7

Exercise [★★, ↛]: Here is a more constructive definition of the transitive closure of a relation R. First, we define the following sequence of sets of pairs:

$$\begin{array}{ccc}{R}_0& =& R\\ R_{i+1}& =& R_i\cup \{(s,u)\mid \text{for some }t\text{, }(s,t)\in R_i\text{ and }(t,u)\in R_i\}\end{array}$$

That is, we construct each R_{i + 1} by adding to R_i all the pairs that can be obtained by “one step of transitivity” from pairs already in R_i. Finally, define the relation R⁺ as the union of all the R_i:

$$R^{+}=\bigcup _i{R}_i$$

Show that this R⁺ is really the transitive closure of $R$—i.e., that it satisfies the conditions given in Definition 2.2.5.

We need to show that:

• R⁺ is transitive:
  • If (s, t) ∈ R⁺ and (t, u) ∈ R⁺, then there must exist an i such that (s, t) ∈ R_i and (t, u) ∈ R_i. By definition, (s, u) will be added to R⁺ at some i + n step. So R⁺ is transitive.
• R ⊆ R⁺:
  • R = R₀ ⊆ $\bigcup _i{R}_i$ = R⁺, so R ⊆ R′.
• R⁺ is smallest:
  • All elements in R⁺ is either originally contained in R, or added to R⁺ at some later step. If we remove an element from R⁺ that is originally contained in R, R⁺ will no longer contain R, which breaks the transitive closure condition. Similarly, we also can’t remove an element that is added at some later step. If (s, u) is added at some later step, is must due to the set also containing some t, so that both (s, t) and (t, u) are in the set. If we remove (s, u), the condition that (s, t) ∈ R⁺ and (t, u) ∈ R⁺ implies (s, u) ∈ R⁺ will be broken. So we can’t remove any element from R⁺, R⁺ must be smallest.

2.2.8

Exercise [★★, ↛]: Suppose R is a binary relation on a set S and P is a predicate on S that is preserved by R. Show that P is also preserved by R^∗.

We need to show that: For any s ∈ S and t ∈ S: (s, t) ∈ R^∗ and s ∈ P implies t ∈ P.

Since P is preserved by R, we have: For any s ∈ S and t ∈ S: (s, t) ∈ R and s ∈ P implies t ∈ P.

First, we prove that for all i, P is preserved by R_i that is defined in exercise 2.2.7. This can be done by induction:

• Base case: If i = 0, we have R_i = R₀ = R, which preserves P by definition.

• Inductive cases: Assume P is preserved by R_i, (s, t) ∈ R_i, (t, u) ∈ R_i, and the pair we add to R_i to get R_{i + 1} is (s, u):

  • If s ∈ P, since P is preserved by R_i, we have t ∈ P and u ∈ P. Since both s ∈ P and u ∈ P, adding (s, u) to R_i doesn’t break the preserving property.
  • If s ∉ P, trivially, adding (s, u) to R_i doesn’t break the preserving property.

  So we have P is also preserved by R_{i + 1}.

Since R^∗ is the union of all R_i, P is also preserved by R^∗.

3 Untyped Arithmetic Expressions

3.2 Syntax

3.2.4

Exercise [★★]: How many elements does S₃ have?

By definition:

• If i = 0, |S_i| = 0.
• If i > 0, |S_i| = 3 + |S_{i - 1}| × 3 + |S_{i - 1}|³.

So we have:

• |S₀| = 0.
• |S₁| = 3 + |S₀| × 3 + |S₀|³ = 3 + 0 × 3 + 0³ = 3.
• |S₂| = 3 + |S₁| × 3 + |S₁|³ = 3 + 3 × 3 + 3³ = 39.
• |S₃| = 3 + |S₂| × 3 + |S₂|³ = 3 + 39 × 3 + 39³ = 59439.

3.2.5

Exercise [★★]: Show that the sets S_i are cumulative—that is, that for each i we have S_i ⊆ S_{i + 1}.

Proof by induction:

• Base case: if i = 0, S_i = S₀ = ∅, so S_i ⊆ S_{i + 1}.
• Inductive cases: assume S_i ⊆ S_{i + 1}, we can prove that any t ∈ S_{i + 1}, t ∈ S_{i + 2}:
  • If t ∈ {true, false, 0}, by definition, t ∈ S_{i + 2}.
  • If t ∈ {succ t₁, pred t₁, iszero t₁ | t₁ ∈ S_i}, by induction, since S_i ⊆ S_{i + 1}, t ∈ {succ t₁, pred t₁, iszero t₁ | t₁ ∈ S_{i + 1}}, so t ∈ S_{i + 2}.
  • If t ∈ {if t₁ then t₂ else t₃ | t₁, t₂, t₃ ∈ S_i}, this is similar to the previous case.

3.3 Induction on Terms

3.3.4

Theorem [Principles of induction on terms]: Suppose P is a predicate on terms.

• Induction on depth:
  • If, for each term s,
    • given P(r) for all r such that depth(r) < depth(s)
      we can show P(s),
  • then P(s) holds for all s.
• Induction on size:
  • If, for each term s,
    • given P(r) for all r such that size(r) < size(s)
      we can show P(s),
  • then P(s) holds for all s.
• Structural induction:
  • If, for each term s,
    • given P(r) for all immediate subterms r of s
      we can show P(s),
  • then P(s) holds for all s.

Proof: Exercise (★★).

• Induction on depth:
  • If the following reasoning holds:
    • If, for each term s,
      • given P(r) for all r such that depth(r) < depth(s)
        we can show P(s),
  • Let Q(i) = “P(r) holds for all r such that depth(r) = i”, we have:
    • If, for each natural number n,
      • given Q(i) for all i < n
        we can show Q(n).
  • By principle of complete induction on natural numbers, we have:
    • Q(n) holds for all n, that is:
      • P(r) holds for all r such that depth(r) = n for all n,
    • which means:
      • P(s) holds for all s.
• Induction on size:
  • If the following reasoning holds:
    • If, for each term s,
      • given P(r) for all r such that size(r) < size(s)
        we can show P(s),
  • Let Q(i) = “P(r) holds for all r such that size(r) = i”, we have:
    • If, for each natural number n,
      • given Q(i) for all i < n
        we can show Q(n).
  • By principle of complete induction on natural numbers, we have:
    • Q(n) holds for all n, that is:
      • P(r) holds for all r such that size(r) = n for all n,
    • which means:
      • P(s) holds for all s.
• Structural induction:
  • If the following reasoning holds:
    • If, for each term s,
      • given P(r) for all immediate subterms r of s
        we can show P(s),
  • Let Q(i) = “P(r) holds for all r such that depth(r) = i”, we have:
    • If, for each natural number n,
      • given Q(i) for all i < n
        we can show Q(n).
  • By principle of complete induction on natural numbers, we have:
    • Q(n) holds for all n, that is:
      • P(r) holds for all r such that depth(r) = n for all n,
    • which means:
      • P(s) holds for all s.

3.5 Evaluation

3.5.5

Exercise [★]: Spell out the induction principle used in the preceding proof, in the style of Theorem 3.3.4.

• If, for each derivation D,
  • given P(C) for all immediate subderivations C of D
    we can show P(D),
• then P(D) holds for all D.

3.5.10

Exercise [★]: Rephrase Definition 3.5.9 as a set of inference rules.

$$\frac{\text{<code>t</code>}\to \text{<code>t</code>}\prime }{\text{<code>t</code>}{\to }^{\ast }\text{<code>t</code>}\prime }$$

$$\frac{}{\text{<code>t</code>}{\to }^{\ast }\text{<code>t</code>}}$$

$$\frac{\text{<code>t</code>}{\to }^{\ast }\text{<code>t</code>}\prime \text{<code>t</code>}\prime {\to }^{\ast }\text{<code>t</code>}″}{\text{<code>t</code>}{\to }^{\ast }\text{<code>t</code>}″}$$

3.5.13

Exercise [Recommended, ★★]:

1. Suppose we add a new rule
   $$\text{<code>if</code>}\text{<code>true</code>}\text{<code>then</code>}{\text{<code>t</code>}}_2\text{<code>else</code>}{\text{<code>t</code>}}_3\to {\text{<code>t</code>}}_3$$ (E-Funny1)
   to the ones in Figure 3-1. Which of the above theorems (3.5.4, 3.5.7, 3.5.8, 3.5.11, and 3.5.12) remain valid?
2. Suppose instead that we add this rule:
   $$\frac{{\text{<code>t</code>}}_2\to {\text{<code>t</code>}}_2\prime }{\text{<code>if</code>}{\text{<code>t</code>}}_1\text{<code>then</code>}{\text{<code>t</code>}}_2\text{<code>else</code>}{\text{<code>t</code>}}_3\to \text{<code>if</code>}{\text{<code>t</code>}}_1\text{<code>then</code>}{\text{<code>t</code>}}_2\prime \text{<code>else</code>}{\text{<code>t</code>}}_3}$$ (E-Funny2)
   Now which of the above theorems remain valid? Do any of the proofs need to change?

1. • 3.5.4: If t → t′ and t → t″, then t′ = t″.
     • Invalid.
   • 3.5.7: Every value is in normal form.
     • Valid.
   • 3.5.8: If t is in normal form, then t is a value.
     • Valid.
   • 3.5.11: If t →^∗ u and t →^∗ u′, where u and u′ are both normal forms, then u = u′.
     • Invalid.
   • 3.5.12: For every term t there is some normal form t′ such that t →^∗ t′.
     • Valid.
2. • 3.5.4: If t → t′ and t → t″, then t′ = t″.
     • Invalid.
   • 3.5.7: Every value is in normal form.
     • Valid.
   • 3.5.8: If t is in normal form, then t is a value.
     • Valid.
   • 3.5.11: If t →^∗ u and t →^∗ u′, where u and u′ are both normal forms, then u = u′.
     • Valid.
   • 3.5.12: For every term t there is some normal form t′ such that t →^∗ t′.
     • Valid.

List of common unicode characters:

Code Point	Name	Alias	Character
U+2032	PRIME	minutes, feet	′
U+2033	DOUBLE PRIME	seconds, inches	″
U+219B	RIGHTWARDS ARROW WITH STROKE		↛
U+2205	EMPTY SET	null set	∅
U+2208	ELEMENT OF		∈
U+2209	NOT AN ELEMENT OF		∉
U+2217	ASTERISK OPERATOR		∗
U+2223	DIVIDES	such that, APL stile	∣
U+222A	UNION	cup	∪
U+2286	SUBSET OF OR EQUAL TO		⊆
U+22C3	N-ARY UNION	z notation generalised union	⋃
U+2605	BLACK STAR		★