2.2.6

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.

Proof

A relation E on S is reflexive when (s,s) ∈ E for all s ∈ S. In other words, E is reflexive if and only if

{(s,s)|s ∈ S} ⊂ E

By definition of R′ we have {(s,s)|s ∈ S} ⊂ R′ so R′ is reflexive.

If there is an other reflexive relation B such that R ⊂ B then also R′ ⊂ B. Since if r ∈ R′ then either r ∈ R or r = (s,s) for an s ∈ S. If r ∈ R then also r ∈ B since R ⊂ B. If r = (s, s) for an s ∈ S then also r ∈ B since B is reflexive. Either way r ∈ B hence R′ ⊂ B

So R′ is the reflexive clojure of R.

2.2.7

Here is a more constructive definition of the transitive closure of a relation R. First we define the following sequence of sets of pairs:

R₀ = R

and

R_i + 1 = R_i ∪ {(s,u)|t ∈ S; (s,t) ∈ R_i, (t,u) ∈ R_i}

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

R⁺ = ⋃_iR_i

Show that R⁺ really is the transitive closure of R.

Lemma

We first show a little lemma

If for a certain i ∈ N we have (a,b) ∈ R_i then for all j ≥ i we have (a,b) ∈ R_j.

Proof

We call a number n cute if (a,b) ∈ R_i + n. Since (a,b) ∈ R_i zero is cute.

Assume k to be cute, we will show that k + 1 is cute as well. Since k is cute we have that (a,b) ∈ R_i + k. Notice that

R_i + 1 = R_i ∪ {(s,u)|t ∈ S; (s,t) ∈ R_i, (t,u) ∈ R_i}

means that Ri + k ⊂ R_{i + k + 1} hence (a,b) ∈ R_{i + k + 1} so k + 1 is cute.

By the principle of mathematical induction all natural numbers are cute. I.e. (a,b) ∈ R_j for all j ≥ i.

Proof

A relation E is transitive if for pairs (s,t), (t,u) ∈ E we have (s,u) ∈ E.

Let (s,t), (t,u) ∈ R⁺. Then there are i, j ∈ N such that (s,t) ∈ R_i and (t,u) ∈ R_j. Let k be the maximum of i and j. Then, by the preceding lemma, we have (s,t), (t,u) ∈ R_k.

By the definition of R_k + 1 we have (s,u) ∈ R_k + 1 so (s,u) ∈ R⁺. Hence R⁺ is a transitive relation.

To show that R⁺ is the smallest transitive relation containing R, i.e. the transitive closure of R, let B be a transitive relation containing R. We will show that R⁺ ⊂ B.

To that end we will show that R_i ⊂ B for each i ∈ N. Call a number k splendid if R_k ⊂ B. By definition R₀ = R ⊂ B so zero is spendid.

If k is splendid we will show that k + 1 is splendid as well. Assume k is splendid, i.e. R_k ⊂ B. Then for (s,u) ∈ R_k + 1 \ R_k there is a t ∈ S such that (s,t) ∈ R_k ⊂ B and (t,u) ∈ R_k ⊂ B. Since B is transitive we also (s,u) ∈ B. Hence R_k + 1 ⊂ B.

By the principle of mathematical induction all numbers are splendid.

2.2.8

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*.

Proof

A predicate T is preserved by relation R if whenever (s,s′) ∈ R and T(s) we also have T(s′).

R^* is the reflexive and transitive closure of R, i.e. the smallest reflexive and transitive relation that contains R. By exercise 2.2.7 we know that there is a sequence of relations R_i for i ∈ N such that

R₀ = R⁺

and

R_i + 1 = R_i ∪ {(s,u)|t ∈ S; (s,t) ∈ R_i, (t,u) ∈ R_i}

with R^* = ⋃_iR_i.

Call a number k ∈ N gratefull if R_k preserves P. By exercise 2.2.6 R₀ = R⁺ = R ∪ {(s,s)|s ∈ S}. So for (s,s′) ∈ R₀ we have s = s′ or (s,s′) ∈ R. Either way, whenever P(s) also $P(s’) because if s = s′ then P(s) = P(s′), otherwise P(s′) because R preserves P.

Assume k is gratefull, we will show that k + 1 is gratefull as well. Without loss of generality let (s,u) ∈ R_k + 1 \ R_k and P(s). Then there exist t ∈ S such that (s,t), (t,u) ∈ R_k. Since k is assumed to be gratefull, R_k preserves P so from P(s) also P(t) since (s,t) ∈ R_k. And since P(t) also P(u) since (t,u) ∈ R_k. Hence k + 1 is gratefull.

By the principle of mathematical induction every natural number is gratefull. I.e. R^* preserve P.

3.2.4

How many elements does S₃ have?

Proof

The sequence of set S_i for i ∈ N is defined as

S₀ = ⌀

and

S_i + 1 = {true, false, O} ∪ {succt, predt, iszerot|t∈S_i}∪{ift₁thent₂elset₃|t₁, t₂, t₃ ∈ S_i}

Let T_i = #S_i. Then T₀ = 0 and

T_i + 1 = 3 + 3 ⋅ T_i + T_i³

The sequence starts with 0, 3, 39, 59439, ….

So there are 59439 elements in S₃.

3.2.5

Show that the sets S_i are cumulative; that is, that for each i we have S_i ⊂ S_i + 1.

Proof

Call k frivolous if S_k ⊂ S_k + 1. We will show that all numbers are frivolous.

Since S₀ = ⌀ and ⌀ ⊂ A for any set A, in particular S₁, we see that 0 is frivolous.

Assume that k is frivolous. We will show that k + 1 is frivolous as well. Let s ∈ S_k + 1. There are three cases to consider

• s ∈ {true, false, 0}. By definition $sS_{k+2}.
• $s{succ t, pred t, iszero t |tS_{k}}. Since k is frivolous, i.e S_k ⊂ S_k + 1, we see that

{succt, predt, iszerot|t∈S_k}⊂{succt,predt,iszerot|t ∈ S_k + 1} ⊂ S_k + 2

• $s{if t_{1} then t_{2} else t_{3}|t_{1},t_{2},t_{3}S_{k}}. Since k is frivolous, i.e. S_k ⊂ S_k + 1, we see that

{ift₁thent₂elset₃|t₁,t₂,t₃∈S_k}⊂{ift₁thent₂elset₃|t₁, t₂, t₃ ∈ S_k + 1} ⊂ S_k + 2

In all cases s ∈ S_k + 2, hence k + 1 is frivolous.

By the principle of mathematical induction all numbers are frivolous.

3.3.4 Principle 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

Induction on Depth

We call n ∈ N \ {0} deep if and only if for all terms s of depth(s) ≤ n holds that P(s). We will show that all numbers are deep.

Notice that 1 is deep. A term of t with depth(t) = 1 is a constant and there are no terms with a smaller depth, so are assumption holds vacuously and P(t) holds.

Assume k is deep. We will show that k + 1 is deep. Let t be a term of depth k + 1. There are two cases

• t = succ(t′) or t = pred(t′) or t = iszero(t′) for a term t′. Notice that in all cases depth(t′) < depth(t′) + 1 = depth(t). k is deep so P(t′) holds. With our assumption we deduce that P(t) holds.

• t = ift₁thent₂elset₃ for terms t₁, t₂ and t₃. Notice that for each i ∈ {1, 2, 3} we have

depth(t_i) ≤ max{t₁, t₂, t₃} < max{t₁, t₂, t₃} + 1 = depth(t)

k is deep so P(t₁), P(t₂) and $P(t_{3}) hold. With our assumption we deduce that P(t) holds.

In either of the two cases to consider we have shown that P(t) holds, hence k + 1 is deep.

With the principle of mathematical induction all natural numbers besides 0 are deep.

Induction on Size

We call n ∈ N \ {0} tall if and only if for all terms s of size(s) ≤ n holds that P(s). We will show that all numbers are tall.

Notice that 1 is tall. A term of t with size(t) = 1 is a constant and there are no terms with a smaller size, so are assumption holds vacuously and P(t) holds.

Assume k is tall. We will show that k + 1 is tall. Let t be a term of size k + 1. There are two cases

• t = succ(t′) or t = pred(t′) or t = iszero(t′) for a term t′. Notice that in all cases size(t′) < size(t′) + 1 = size(t). k is large so P(t′) holds. With our assumption we deduce that P(t) holds.

• t = ift₁thent₂elset₃ for terms t₁, t₂ and t₃. Notice that for each i ∈ {1, 2, 3} we have

size(t_i) ≤ size(t₁) + size(t₂) + size(t₃) < size(t₁) + size(t₂) + size(t₃) + 1 = size(t)

k is deep so P(t₁), P(t₂) and $P(t_{3}) hold. With our assumption we deduce that P(t) holds.

In either of the two cases to consider we have shown that P(t) holds, hence k + 1 is tall.

With the principle of mathematical induction all natural numbers besides 0 are tall.

Structural Induction

Notice that for all terms t we have for all of ts immediate subterms r size(r) < size(t). The result then follows by induction on size.

3.5.5

Spell out the induction principle used in the preceding proof, in the style of 3.3.4.

Answer

The used principle of induction is 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.

3.5.10

Rephrase definition 3.5.9 as a set of inference rules.

Answer

Closure

t --> t'
-------
t -->* t'

Reflexive

-------
t -->* t

Transitive

t -->* t', t' -->* t''
----------------------
t -->* t''

3.5.13

Part 1

Suppose we add a new rule

if true then t2 else t3 -> t3

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.

3.5.4

Determinacy of one-step evaluation: if t → t₁ and t → t₂ then t₁ = t₂.

This isn’t valid anymore since if true then O else succ O had no two one step that are different, i.e. O and succ O.

3.5.7

Every value is in a normal form.

This remains true. The values are true and false and the new rule does not apply to it.

3.5.8

If t is in normal form, then t is a value.

This remains true.

3.5.11

uniqueness of normal forms: if t →  * u and t →  * v, where u and v are both normal forms then u = v.

This is invalid. Consequence of the invalidation of the determinancy of one-step evaluation under the new rule.

3.5.12

Termination of evaluation: for every term t there is some normal form u such that t →  * u.

This remains valid. It isn’t unique anymore though.

Part 2

Suppose instead that we add this rule:

t_2 --> u
----------------------------
if t_1 then t_2 else t_3 --> if t_1 then u else t_3

Now which of the above theorems remain valid? Do any of the proofs need to change?

3.5.4

Theorem 3.5.4 is invalid. Multiple evaluation rules could apply, for example

if true then (if false then true else false) else false

could evaluate under the original rules to

if false then true else false

or with the new rule

if true then false else false

3.5.7

This remains valid. The proof is essentially the same.

3.5.8

This remains valid. The proof is also essentially the same.

3.5.11

This remains valid, The proof is different because the determinancy of single-step evaluation is invalid with the new rule.

3.5.12

This remains valid as well. The proof is the same.

3.5.14

Show that Theorem 3.5.4 is also valid for the evaluation relation on arithmetic expressions: if t → u and t → v then u = v.

Proof

We will show by induction of the structure of a term t.

By Theorem 3.5.4 this the theorem is valid for B. We will focus on the extention.

If the rule applied for the derivation t → u is E-SUCC then t = succt₁ for a t₁. The only rule applicable on a succ term is E-SUCC, so in this case the result follows.

if the rule applied was predO something similar follows. As with all other terms.