Solutions to Selected Exercises

Foundations for Programming Languages John C. Mitchell Book copyright MIT Press, 1996. Thanks to teaching assistants My Hoang, Brian Howard and Ramesh Viswanathan for their assistance with these solutions.

Chapter 1

Exercise 1.2.2. The fully parenthesized expression is

(((λx: nat.(λy: nat.(x + y))) 3) 2).

Since the function λx: nat.(λy: nat.(x + y)) adds its two arguments, the value of this expression should be 3 + 2, or 5. There is no other way to insert additional parentheses into the original expression and still have a well-formed term. For example, you cannot group (3 2), because 3 is not a function. If you remove the parentheses that were given in the problem statement, then you can get the expression

((λx: nat.((λy: nat.(x + y)) 3)) 2),

which coincidentally also has value 5 (why?).

Exercise 1.3.1.

(λf: nat → nat. f 5)(λx: nat. x + x) →^{β} (λx: nat. x + x) 5
→^{β} 5 + 5.

Exercise 1.3.2. Let us write f^{n}x for the expression f(f(⋯ (f x) ⋯)) with n occurrences of f. Let N be the term λg: a → a. λy: a. g^{2}y. For any natural number n, the term

(λf: (a → a) →(a → a). λx: a → a. f^{n}x) N,

which has the form requested, has length 20 + 3n, counting parentheses. Beginning with this term, we have the following β -reductions:

\begin{matrix}→ & λx: a → a. N^{n}x \\ → & λx: a → a. N^{n−1}(λy: a. x^{2}y) \\ → & λx: a → a. N^{n−2}(λy: a.(λy: a. x^{2}y)^{2}y) \\ → & λx: a → a. N^{n−2}(λy: a.(λy: a. x^{2}y)(x^{2}y)) \\ → & λx: a → a. N^{n−2}(λy: a. x^{4}y) \\ → & … \\ → & λx: a → a. λy: a. x^{2^{n}}y. \end{matrix}

The final term has length 5 + 3 · 2^{n}, which is more than double 20 + 3n for any n ≥ 5. In fact, it is much more than double, which will be useful in Exercise 1.3.3 below.

Exercise 1.3.3. First define a sequence α_{0}, α_{1}, … of types by setting α_{0} = a and α_{n+1} = α_{n} → α_{n}. Then, for k, n ≥ 0, define terms F_{k} and G_{k,n} by:

\begin{aligned}F_{k} & = & λx: α_{k} → α_{k}. λy: α_{k}. x^{2}y \\ G_{k,n} & = & λx: α_{k} → α_{k}. λy: α_{k}. x^{n}y. \end{aligned}

The term used in the Exercise 1.3.2 was G_{1,6}F_{0} , which reduced to G_{0,64} . A similar sequence of reductions will show that the term G_{k+1,n}F_{k} reduces to the term G_{k,2^{n}}. Now consider the term H_{n} = G_{n,n}F_{n−1}F_{n−2} ⋯ F_{0} . This will reduce to G_{n−1,2^{n}}F_{n−2} ⋯ F_{0} , and hence will continue to reduce to G_{0,f(n)} = λx: a → a. λy: a. x^{f(n)}y, where f(n) = 2^{2^{...2^{n}}} (with n 2’s in the column), as given. Since we do not count types in the length of a term, the length of H_{n} is O(n) and it reduces to a term of length greater than f(n), as desired.

Exercise 1.7.1. The parse tree for the derivation given in the section is

[figure: e; n; n; d; 2; d; 5]

There are other derivations which differ in the order in which the non-terminals are expanded, such as the following one:

e → n → nd → n5 → d5 → 25

However, there are no other parse trees for it.

Exercise 1.7.3.

(a) An abstract syntax does not require that the grammar is unambiguous or that operators have a precedence or associative preference; however, the abstract syntax should at least describe the possible expressions in the concrete syntax. Obtaining a unique parsing is the goal of the concrete syntax. The abstract syntax of

e : : = 0 | 1 | e + e | e − e | e ∗ e

appropriately captures the possible expressions of interest. It is not a good concrete syntax since the grammar is ambiguous. For example, the expression 1 + 1 + 1 has two parse trees according to the above grammar, as follows:

[figure: e; e; e; 1; +; e; 1; +; e; 1; e; e; 1; +; e; e; +; e; 1; 1]

(b)

[figure: e; e; 1; −; e; e; ∗; e; 1; 1]

(c)

[figure: e; e; e; 1; −; e; 1; +; e; 1]

(d)

[figure: e; e; −; e; e; 1; −; e; e; 1; +; e; 1; e; +; e; 1; 1]

Exercise 1.8.8. We prove the property

P (e) =^{def} the value of e is an even integer

by induction on the structure of expressions. The base cases are to establish the property for 0 and 2 which is trivially seen. The induction step follows from the fact that the sum and product of two even integers are even integers.

Exercise 1.8.9. Let us first define the height of trees and the size (i.e., the number of nodes) of trees by induction on the structure of trees.

h(nil) = 0  size(nil) = 0
h(leaf ) = 1  size(leaf ) = 1
h(node(t_{1}, t_{2})) = max(h(t_{1}), h(t_{2})) + 1 size(node(t_{1}, t_{2})) = size(t_{1}) + size(t_{2}) + 1

We are required to prove that for all trees t, size(t) ≤ 2^{h(t)} . However, this property is not provable by induction on the structure of trees (the induction step does not go through). We will instead prove the property

P (t) =^{def} size(t) ≤ 2^{h(t)} − 1

by induction on the structure of trees.

Base Cases: We need to prove that P (nil) and P (tree) which can be easily verified using the definition of size, h on nil and tree .

Induction step: Suppose that P (t_{1}) and P (t_{2}). We can prove that P (node(t_{1}, t_{2})) as follows:

size(node(t_{1}, t_{2})) = size(t_{1}) + size(t_{2}) + 1  (definition of size)
≤ (2^{h(t_{1})} − 1) + (2^{h(t_{2})} − 1) + 1  (induction hypothesis)
= (2^{h(t_{1})} + 2^{h(t_{2})}) − 1
≤ (2^{max(h(t_{1}),h(t_{2}))} + 2^{max(h(t_{1}),h(t_{2}))}) − 1 (h(t_{1}), h(t_{2}) ≤ max(h(t_{1}), h(t_{2})))
= 2^{max(h(t_{1}),h(t_{2}))+1} − 1
= 2^{h(node(t_{1},t_{2}))} − 1  (definition of h)

Since P (t) implies that size(t) ≤ 2^{h(t)} , we obtain the property stated in the question.

Chapter 2

Exercise 2.2.2. Boolean functions and, ∧, and or, ∨, are defined implicitly by the following expressions:

x ∧ y ≡ if x then y else false,

x ∨ y ≡ if x then true else y.

There are many other possibilities. For example, we may replace an occurrence of x in either expression by (if x then true else false), because on replacing x by either true or false this conditional expression simplifies to the constant substituted for x.

Exercise 2.2.3. For any basic natural number expression M with numeric variables x and y, we define a polynomial p_{M}(x, y) in x and y by induction on the structure of M:

p_{⌈n⌉}(x, y) = n, for n ∈ N
p_{x}(x, y) = x
p_{y}(x, y) = y
p_{M+N}(x, y) = p_{M}(x, y) + p_{N}(x, y)
p_{(if P then M else N)}(x, y) = p_{M}(x, y) + p_{N}(x, y).

By induction on the structure of M, it is easy to prove that for any natural numbers n, m, if [⌈n⌉/x]([⌈m⌉/y]M) → → ⌈r⌉ then r ≤ p_{M}(n, m). We can also prove by induction on the structure of M that p_{M}(x, y) = ax + by + c, for some constants a, b, and c that depend on M. Since x^{y} grows more quickly than any linear polynomial, no basic natural number expression can define exponentiation implicitly.

Exercise 2.2.4.

λf: nat → nat. λx: nat. (fx) + (fx)

Exercise 2.2.5. The first step in substitution is to rename bound variables to avoid capture. For the term given, simply inserting x in place of (y + 3) will allow the inserted occurrences of y to be bound by λy. If we rename bound occurrences of y to z, then the result of (correct) substitution is

(λf: nat → nat. λz: nat. f((y + 3) + z))(λx: nat. x + y).

Exercise 2.2.8.

Uncurry = λf: nat →(nat → nat). λp: nat × nat. f(Proj_{1}p)(Proj_{2}p)

If g is a function of type nat × nat → nat , then we have the following:

Uncurry(Curry g) = Uncurry(λx: nat. λy: nat. g⟨x, y⟩)
= λp: nat × nat. (λx: nat. λy: nat. g⟨x, y⟩)(Proj_{1}p)(Proj_{2}p)
= λp: nat × nat. g⟨Proj_{1}p, Proj_{2}p⟩
= λp: nat × nat. gp
= g.

And, if g is a function of type nat →(nat → nat), then we have the following:

Curry(Uncurry g) = Curry(λp: nat × nat. g(Proj_{1}p)(Proj_{2}p))
= (λx: nat. λy: nat. (λp: nat × nat. g(Proj_{1}p)(Proj_{2}p))⟨x, y⟩)
= λx: nat. λy: nat. g(Proj_{1}⟨x, y⟩)(Proj_{2}⟨x, y⟩)
= λx: nat. λy: nat. gxy
= λx: nat. gx
= g.

Exercise 2.2.12.

(a) λ⟨x: σ, y: τ⟩. M =^{def} Uncurry(λx: σ. λy: τ. M)

(b) let f⟨x: σ, y: τ⟩: ρ = M in N =^{def} let f: (σ × τ) → ρ = λ⟨x: σ, y: τ⟩.M in N

Exercise 2.2.13.

(a) Let M be the given expression. Then using the derived rule for reducing let expressions, we

have

M
→ let f(y: nat): nat = 3 + y in let x: nat = 4 in f 5
=^{def} let f: nat → nat = λy: nat. 3 + y in let x: nat = 4 in f 5
→ let x: nat = 4 in (λy: nat. 3 + y) 5
→ (λy: nat. 3 + y) 5
→ 3 + 5
→ 8

(b) Suppose we begin by substituting λy: nat. x + y for f in the inner expression let x: nat = 4 in f 5. By rules for substitution, since x is free in the term that we are substituting for f, the bound variable x in let x: nat = 4 in f 5 would be first renamed to a new variable z and all occurrences of x in the scope of this declaration, namely f 5 would be renamed to z before substituting λy: nat. x + y for f. Thus the term after the substitution is performed would be

let x: nat = 3 in let z: nat = 4 in (λy: nat. x + y) 5

which successfully resolves the occurrence of x in the body of f to be bound by the outermost declaration to 3.

(c) If we do not rename bound variables then we have the following sequence of reductions:

M
→ let x: nat = 3 in let x: nat = 4 in (λy: nat. x + y) 5
→ let x: nat = 3 in (λy: nat. 4 + y) 5
→ (λy: nat. 4 + y) 5
→ 4 + 5
→ 9

(d) By α-conversion, we may rename the variable x in the inner declaration of x to a new variable, say z and obtain 8 as a result as follows:

M

=^{α} let x: nat = 3 in

let f(y: nat): nat = x + y in let z: nat = 4 in f 5

→ let x: nat = 3 in let z: nat = 4 in (λy: nat. x + y) 5
→ let x: nat = 3 in (λy: nat. x + y) 5
→ (λy: nat. 3 + y) 5
→ 8

(e) Consider the expression M defined in (a) of the exercise. The reduction sequence given in (a) is a reduction in dynamically-scoped PCF as well and gives us the result 8. On the other hand the reduction sequence from M given in (c) reduces M to 9 which shows that confluence fails.

Exercise 2.2.14.

letrec fib(x: nat): nat = if Eq? x 0 then 1

                                         else if Eq? x 1 then 1

else fib(x − 1) + fib(x − 2)

in fib(4)

Make the following abbreviation :

F =^{def} λfib: nat → nat. λx: nat. if Eq? x 0 then 1 else if Eq? x 1 then 1

else fib(x − 1) + fib(x − 2)

Then, we have the following reduction sequence :

(fix F) n
→ → F (fix F) n
→ → if Eq? n 0 then 1 else if Eq? n 1 then 1 else (fix F)(n − 1) + (fix F)(n − 2)

When n = 0 or n = 1, the expression on the last line simplifies to 1, i.e. the zero-th and first Fibonacci number, respectively. Otherwise, we can simplify the conditional to obtain (fix F)(n − 1) + (fix F)(n − 2). Thus, by induction on n, we can prove the meta-theorem that (fix F) n may be reduced to the numeral for the n-th Fibonacci number. Now, the letrec expression we started with, after eliminating syntactic sugar, β -reduces to (fix F) 4; which, by our above argument may be reduced to the 4th Fibonacci number, namely 5.

Exercise 2.2.15. Let

M =^{def} fix_{σ × τ} (λ⟨f: σ, g: τ⟩. ⟨F f g, G f g⟩)

Then, we need to show that

Proj_{1}M = F (Proj_{1}M) (Proj_{2}M)  (11.1)
Proj_{2}M = G (Proj_{1}M) (Proj_{2}M)  (11.2)

We only show Equation 11.1, since Equation 11.2 is shown in an exactly similar manner.

Proj_{1}M = Proj_{1}((λ⟨f: σ, g: τ⟩. ⟨F f g, G f g⟩)M)
= Proj_{1}⟨F (Proj_{1}M) (Proj_{2}M), G (Proj_{1}M) (Proj_{2}M)⟩
= F (Proj_{1}M) (Proj_{2}M).

Exercise 2.2.16.

(a) We may define a fixed-point operator from letrec as follows:

FIX =^{def} λf: σ → σ. letrec x: σ = f x in x.

Expanding the letrec gives

λf: σ → σ.(λx: σ. x)(fix_{σ} λx: σ. f x),

which β -reduces to

λf: σ → σ. fix_{σ} λx: σ. f x.

If we apply η-reduction twice, we get fix_{σ}, as desired.

(b) A reasonable reduction rule for letrec is

letrec f: σ = M in N → [ [(letrec f: σ = M in f)/f]M /f]N.

The innermost term, letrec f: σ = M in f, is provably equal to FIX (λf: σ. M), by two applications of (β), and (α) to rename f to x. Therefore, the term produced by letrec reduction is provably equal to

[[FIX (λf: σ. M)/f]M/f]N,

as desired.

(c) Apply one β -reduction to FIX M to get letrec x: σ = M x in x, which is called F in the problem statement. One application of the letrec reduction rule given in part (b) yields

[ [(letrec x: σ = M in x)/x](Mx) /x]x = M (letrec x: σ = M in x).

This term is MF, as required.

Exercise 2.3.1. First let us adopt some abbreviations. Let C[ ] be the context (term with a “hole,” indicated by the square brackets)

C[ ] =^{def} λx: nat. if Eq? x 0 then 1 else [ ]

and let F be the term λf: nat → nat. C[f(x−1)]. With letrec expanded out to lambda abstraction, fix, and application, the first term becomes

(λf: nat → nat. M)(fix_{nat → nat} F),

while the second term is (α-equivalent to)

(λf: nat → nat. M) C[(λg: nat → nat. g(x − 1))(fix_{nat → nat} F)].

Using first the (fix) axiom and then (β), we may use congruence rules to prove that the first term is equal to

(λf: nat → nat. M)(F (fix_{nat → nat} F)).

Considering the form of F, we may use (β) again to get

(λf: nat → nat. M) C[(fix_{nat → nat} F)(x − 1)].

Finally, one more use (β) gives us the second term. Thus, by (fix), (β), congruence rules and transitivity, we have shown that the two terms are equal.

Exercise 2.3.2. If we could prove true = false in PCF then, since provable equality is a congruence, we could also prove

                 if true then M else N = if false then M else N,

for any well-formed expressions M and N of the same type. From this, it is easy to prove M = N, giving us an inconsistency. If instead we could prove m = n for distinct numerals m and n, then by similar reasoning we could prove Eq? m m = Eq? m n, which leads by the axioms for Eq? to true = false , hence we again reach an inconsistency.

It is interesting to note that the problem is solvable for a weakened version of PCF with a conditional expression if b then M else N allowed only when M and N both have type nat or type bool . The proof of inconsistency uses induction on types in this case. We use the argument above to show that any equation M = N is provable for terms of type nat or bool . For the induction steps, we assume M = N provable whenever these terms have type σ or τ. We will show that all equations between terms of type σ → τ and σ × τ are provable. In the first case, suppose two terms M and N of type σ → τ are not provably equal. Then, using the (η) rule, λx: σ. Mx and λx: σ. Nx must also be unequal. By the congruence of our proof system, this means that Mx and Nx cannot be equal; but they are both terms of type τ, which is a contradiction, so M = N. In the second case, let M and N be of type σ × τ. If M and N are not equal, then by the surjective pairing rule we must have that ⟨Proj_{1}M, Proj_{2}M⟩ and ⟨Proj_{1}N, Proj_{2}N⟩ are unequal, hence by congruence we can’t have both Proj_{1}M = Proj_{1}N and Proj_{2}M = Proj_{2}N. But these terms are of type σ and τ, respectively, so both equations must be provable, hence M = N. This completes the induction step, so M = N for any well-formed terms of the same type.

Exercise 2.3.3.

(b) Consider the terms

\begin{aligned}P & ≡ & fix_{(σ → σ) → σ}(λf: (σ → σ) → σ. λg: σ → σ. g(fg)) \\ M & ≡ & P x \end{aligned}

where x is a variable of type σ → σ. Then, using (fix) and (β) reduction steps we get that M → → x M. Using the rule (fix ind), we get that M = fix_{σ} x, i.e., P x = fix_{σ} x. Apply the congruence rules for functions to get λx: σ → σ. P x = λx: σ → σ. fix_{σ} x and then (η) to get the desired equation.

Exercise 2.3.4. First, suppose that programs M and N are operationally equivalent; then by the definition of operational equivalence, we have that eval(C[M]) ≃ eval(C[N]), for every program context C[ ]. In particular, since M and N are already programs, we may take C[ ] to be the empty context [ ]; hence we have that eval(M) ≃ eval(N).

For the converse, suppose that eval(M) ≃ eval(N), where M and N are programs and eval(M) is the unique normal form of M, if it exists, and is undefined otherwise. By assumption, if M and N have no normal forms, they are operationally equivalent; so suppose one of them has a normal form P — by the properties of eval and ≃, the other must also have normal form P. Now, take any program context C[ ]. Since reduction is confluent, we have that eval(C[M]) ≃ eval(C[P]), i.e., we may reduce the subterm M all the way to normal form P before reducing any of the context; similarly eval(C[N]) ≃ eval(C[P]). Kleene equality (≃) is obviously transitive and symmetric, so since C[ ] was chosen arbitrarily, we have that M and N are operationally equivalent.

Exercise 2.3.5. Let us denote by =_{op}^{S} the operational equivalence relation with S the set of observable types. A useful way to reformulate the definition of operational equivalence is that M ≠_{op}^{S} N iff there is a distinguishing context C[ ] such that C[M], C[N] are closed and of type σ ∈ S with eval(C[M]) ≠ eval(C[N]). Clearly, if S ⊆ T then M ≠_{op}^{S} N ⇒ M ≠_{op}^{T} N.

(a) We prove that for any terms M, N of the same type

M =_{op}^{{nat}} N iff M =_{op}^{{nat,bool}} N

By earlier remarks, it suffices to show that if M ≠_{op}^{{nat,bool}} N then M ≠_{op}^{{nat}} N. Suppose that M ≠_{op}^{{nat,bool}} N as evidenced by a distinguishing context C[ ]. If C[M] is of type nat , then the same context shows that M ≠_{op}^{{nat}} N. If C[N] is of type bool , then for the context

C′[ ] =^{def} if C[ ] then 0 else 1

we have that C′[M], C′[N]: nat and eval(C′[M]) ≠ eval(C′[N]).

(b) The set of observable types S is generated by the following grammar

τ : : = nat | bool | τ × τ

Since {nat, bool} ⊆ S, it suffices to show that if M ≠_{op}^{S} N then M ≠_{op}^{{nat,bool}} N. Suppose that M ≠_{op}^{S} N via a distinguishing context C[ ] of type τ ∈ S. We prove by induction on the structure of τ ∈ S that M ≠_{op}^{{nat,bool}} N. The base cases are when τ is nat or bool in which case the same context C[ ] shows that M ≠_{op}^{{nat,bool}} N. For the induction step suppose that τ ≡ τ_{1} × τ_{2} and eval(C[M]) ≠ eval(C[N]). Then at least one of C[M] and C[N] evaluates to a normal form. Without loss of generality assume that eval(C[M]) = P with P a normal form of type τ_{1} × τ_{2} . The only normal forms of type τ_{1} × τ_{2} are pairs, so P ≡ ⟨P_{1}, P_{2}⟩. Define context C_{i}[ ] = Proj_{i} C[ ] for i = 1, 2. Then C_{i}[M] is of type τ_{i} and for at least one of i = 1 or 2 we have that eval(C_{i}[M]) ≠ eval(C_{i}[N]). By induction hypothesis applied to τ_{1} or τ_{2} , we have that M ≠_{op}^{{nat,bool}} N.

Exercise 2.4.7. The expression letrec f: σ = M in N is syntactic sugar for (λf: σ. N)(fixF), where F is λf: σ. M. The subterm fixF may be “reduced” to F (fixF). Since fixF is still a subterm, this may be repeated indefinitely. Part (b) of Exercise 2.4.8 shows that a recursive function can terminate when it is possible to use reductions other than (fix) to eventually eliminate all occurrences of fixF.

Exercise 2.4.8.

(a) comp(λx: nat. x + 1)(λx: nat. x + 1)5

≡ (λf: nat → nat. λg: nat → nat. λx: nat. f(gx))(λx: nat. x + 1)(λx: nat. x + 1)5
→ → (λx: nat. x + 1)((λx: nat. x + 1)5)
→ (λx: nat. x + 1)(5 + 1)
→ (5 + 1) + 1
→ → 7.

(b) Make the following abbreviations:

N ≡ λx: bool. if x then false else true
F ≡ λf: nat → nat. λx: bool. if x then true else f(not x)
F′ ≡ [N/not]F.

Then we have this reduction sequence:

let not: bool → bool = λx: bool. if x then false else true in letrec f: bool → bool = λx: bool. if x then true else f(not x) in f false

≡ (λnot: bool → bool. (λf: bool → bool. f false)(fixF))N
→ (λf: bool → bool. f false)(fixF′)
→ (fixF′)false
→ F′(fixF′)false
→ → if false then true else (fixF′)(N false)
→ → (fixF′)(if false then false else true)
→ (fixF′)true
→ → if true then true else (fixF′)(N true)
→ true.

Exercise 2.4.9. Use the two terms obtained by applying (η) and (fix)_{alt} to λf: σ → σ. fix f, i.e., take M = λf: σ → σ. fix_{σ} f, N = fix_{σ}, and P = λf: σ → σ. f (fix_{σ} f).

Exercise ??. By the confluence of the reduction system, we know that x = ⟨Proj_{1}x, Proj_{2}x⟩ is provable in the related equational system only if x and ⟨Proj_{1}x, Proj_{2}x⟩ reduce to a common term. But no subterm of either of these matches the left-hand side of a reduction rule, so they must be distinct normal forms; therefore the equation cannot be proved.

Another solution which may help convince people who think the above is some kind of slightof-hand is to consider a model of the projection axioms that doesn’t satisfy the equation. (This solution is due to William Graham; a similar argument was given by Michael Greenwald, who considered implementations of pairs in LISP, where EQ tests equality of pointers rather than of the structures pointed to) Let the representation of the pair ⟨M, N⟩ be 2^{m}3^{n}, where m and n are the representations of M and N; we assume that there is some coding of the base types into natural numbers as well. Then the representation of the first projection function, Proj_{1} , is the natural number function which returns the exponent of 2 in the prime factorization of its argument, and the representation of Proj_{2} does the same for 3. Now let x be represented by 30 = 2^{1}3^{1}5^{1} ; then Proj_{1}x will be 1, as will Proj_{2}x; forming ⟨Proj_{1}x, Proj_{2}x⟩ from these two projections gives 2^{1}3^{1} = 6, which shows that the equation is false in this model. The key is that there may be extra information in an object of pair type than just its components, such as the factor of 5 in this example, and this information will not necessarily be preserved under the operations. The “surjective pairing” axiom is needed to insure that a pair is no more than “the sum of its parts.”

Exercise 2.4.17. First, the program given in Example 2.4.6 is equivalent to

(λf: nat → nat.(λg: nat → nat. f (g 5)) (fix G)) (λx: nat. 3)

where G : : = λg: nat → nat. λx: nat. g(x + 1). The left-most reduction is

(λf: nat → nat.(λg: nat → nat. f (g 5)) (fix G)) (λx: nat. 3)
→^{left} (λg: nat → nat.(λx: nat. 3) (g 5)) (fix G)
→^{left} (λx: nat. 3) ((fix G) 5)
→^{left} 3

Exercise 2.4.18. We may avoid reasoning about all possible reduction paths by using the standard deterministic interpreter. More specifically, if lazy reduction never terminates, then no reduction path will terminate. In detail, we apply left-most reduction to the term and show that it always contains fix as a subterm; since the (fix) reduction always applies, the reduction sequence must never reach a normal form. First, the expression letrec f(x: nat): nat = f(x + 1) in f 1 is equivalent to (λf: nat → nat. f 1)(fix F), where F ≡ λf: nat → nat. λx: nat. f(x + 1). The leftmost reduction is

(λf: nat → nat. f 1)(fix F) →^{left} (fix F)1
→^{left} ((λf: (nat → nat) →(nat → nat). f(fix f))F)1
→^{left} F (fix F)1
→^{left} (λx: nat.(fix F)(x + 1))1
→^{left} (fix F)(1 + 1)
→ →^{left} (fix F)((1 + 1) + 1)
→ →^{left} …,

which will obviously never terminate, hence the original expression has no normal form.

Exercise 2.4.19.

(a) For the forward direction, we first show that if M ⇒ N, then M → → N; from that it is easy to prove by induction on the length of a reduction that it also holds for the reflexive-transitive closure of ⇒. Now, we have two inference rules defining ⇒. For the first rule,

\frac{M → N}{M ⇒ N} ,

it is obvious that M → → N. For the second rule,

\frac{M_{1} ⇒ N_{1}, …, M_{k} ⇒ N_{k}}{C[M_{1}, …, M_{k}] ⇒ C[N_{1}, …, N_{k}]} ,

assume that we have already shown that M_{i} ⇒ N_{i} implies M_{i} → → N_{i}, for each of the (smaller) terms M_{1}, …, M_{k}; then since

C[M_{1}, …, M_{k}] → → C[M_{1}, …, M_{k−1}, N_{k}] → → ⋯ → → C[N_{1}, …, N_{k}],

we are done.

For the reverse direction, note that M → N directly implies M ⇒ N by the first inference rule, hence M → → N implies M ⇒ ⇒ N.

(b) By part (a), if M ⇒ ⇒ P, then M → → P; if also M → → N and N is a normal form, then confluence implies that P → → N. Finally, the other direction of part (a) establishes that P ⇒ ⇒ N.

(c) The counterexample does not rely on particular properties of parallel reduction. Take the set of terms {a, b, c} and the reduction rules a → b and a → c. Then assign M ≡ a, N ≡ b, and P ≡ c; thus M → → N, N is a normal form, and M ⇒ ⇒ P, as required, but P ⇏ ⇒ N.

Exercise 2.5.5.

half =^{def} λn: nat. search λx: nat. if Eq? (x + x) n then true else Eq? (x + x + 1) n.

Exercise 2.5.2.

(a) Using the ordering A, B, C for the record labels, we obtain the following desugared expression.

let r: int ×(bool ×(int → int)) = ⟨5, ⟨false, λx: int. x⟩⟩
in if Proj_{1}(Proj_{2} r) then Proj_{1} r else (Proj_{2}(Proj_{2} r)) (Proj_{1} r)

Exercise 2.5.6. Here is one solution (there are several ways to arrange the function calls):

comp =^{def} λn: nat. λf: nat → nat. λx: nat.
letrec g: nat → nat → nat = λy: nat. λm: nat.

if Eq? m n then y else g(f y)(m + 1) in g x 0

mult =^{def} λp: nat × nat. comp(Proj_{1}p) (λz: nat. z + Proj_{2}p) 0.

Exercise 2.5.7.

(a)

prim =^{def} λg: σ. λh: σ × nat → σ.

letrec f(x: nat): σ = if Eq? 0 x then g else h ⟨f(pred x), pred x⟩

                in f.

(b) We define predecessor, addition, and equality test using successor, test for zero, and a primitive recursion operator prim as follows:

pred =^{def} prim 0 (λ⟨m: nat, n: nat⟩. n)
add =^{def} λx: nat. prim x (λ⟨m: nat, n: nat⟩. succ m)
Eq? =^{def} prim zero? (λ⟨f: nat → bool, n: nat⟩. λx: nat. if zero? x then false

else f(pred x)).

Note that the addition and equality test functions are defined as their curried versions.

Exercise 2.5.10. We’ll start by defining a subtraction function minus ; since there are no negative numbers in PCF, we’ll set minus m n = 0 whenever m < n (this is known as the modified difference function).

minus =^{def} letrec f(m: nat)(n: nat): nat = if Eq? n 0 then m

else f(pred m)(pred n)

                 in f.

Now, if we represent the state of the variables with the pair ⟨q, r⟩, then the desired functions are

init =^{def} ⟨0, m⟩

next =^{def} λ⟨q: nat, r: nat⟩.⟨q + 1, minus r n⟩

done =^{def} λ⟨q: nat, r: nat⟩. if Eq? r n then false else Eq?(minus r n) 0.

To show that the PCF expression loop init next done performs essentially the same arithmetic operations as the given imperative program, first notice that each application of next corresponds to executing the body S of the while loop, while each use of done computes the test B, where ¬B ≡ (r ≥ n). Now, expanding the definition of loop gives the expression (fix F) init , where

F =^{def} λf: nat × nat → nat × nat. λx: nat × nat. if done x then x else f(next x).

Thus, one unfolding of the recursion corresponds to one application of the reduction rule for the

loop while ¬B do S end:

if done init then init else (fix F)(next init) ≈

                  if B then skip else (S; while ¬B do S end).

If the loop body is executed n times, i.e., the test in the conditional evaluates to false in each of n unfoldings, then we have

if done(next^{n} init) then (next^{n} init) else (fix F)(next^{n+1} init) ≈

                S^{n}; if B then skip else (S; while ¬B do S end).

If now the test evaluates to true , then the PCF expression evaluates to next^{n} init and the imperative program reduces to S^{n}; as mentioned above, each next does essentially the same computation as the statements in S, so we are done.

Exercise 2.5.11. We’ll start by defining a subtraction function minus , and a test for less-than function less; since there are no negative numbers in PCF, we’ll set minus m n = 0 whenever m < n (this is known as the modified difference function).

minus =^{def} letrec f(m: nat)(n: nat): nat = if Eq? n 0 then m

else f(pred m)(pred n)

                 in f.

less =^{def} λ⟨x: nat, y: nat⟩. if Eq? x y then false

else Eq?(minus x y) 0.

For the outer loop, we can represent the state by the pair ⟨m, n⟩, and the required functions are

init =^{def} ⟨m, n⟩

next =^{def} λ⟨m: nat, n: nat⟩.⟨n, InnerLoop⟩

done =^{def} λ⟨m: nat, n: nat⟩. Eq? n 0

For the inner loop, the required result InnerLoop can then be written as

InnerLoop =^{def} loop m (λr: nat. minus r n) (λr: nat. less r n)

Now, we can translate the program, expecting m and n as input, and producing m as output, as follows :

Gcd =^{def} λ⟨m: nat, n: nat⟩. Proj_{1}(loop init next done).

Exercise 2.5.13.

(a) Let us first define the function sumup which maps n to the sum of the first n natural

numbers.

sumup =^{def} λn: nat. half (mult ⟨n, (n + 1)⟩)

where half was defined in Exercise 2.5.5, and mult was defined in Exercise 2.5.6.

Then, the required pairing function is

pr =^{def} λ⟨n: nat, m: nat⟩. sumup (n + m) + m

To define the projection functions, let us first define a function which finds the sum of the two natural numbers, the code for whose pair is the input.

diag =^{def} λp: nat. search (λd: nat. less p (sumup(d + 1)))

where less was defined in Exercise 2.5.11.

Then, the required projection functions are

p_{1} =^{def} λp: nat. minus p (sumup (diag p))
p_{2} =^{def} λp: nat. minus(diag p) (p_{1} p)

where minus was also defined in Exercise 2.5.11.

(b) The required functions are

Car =^{def} λs: nat. p_{1} (p_{2} s)

Cons =^{def} λn: nat. λs: nat. pr ⟨(p_{1} s) + 1, pr ⟨n, s⟩⟩ Cdr =^{def} λs: nat. p_{2} (p_{2} s)

Null =^{def} 0

Empty? =^{def} λs: nat. Eq? s 0 Length =^{def} λs: nat. p_{1} s

The last four terms have not been asked in the question, but will be useful in the solution to other parts.

Let us also write a function concatRev which takes two sequences, reverses the first, and appends them together; and a function nthEntry , which gives the j th element of a sequence.

concatRev =^{def} letrec
conc(⟨s_{1}: nat, s_{2}: nat⟩): nat = if Empty? s_{1}

                                            then s_{2}

else conc ⟨Cdr s_{1}, Cons (Car s_{1}) s_{2}⟩

in conc

nthEntry =^{def} letrec
find(⟨j: nat, s: nat⟩): nat  = if Eq? j 1

                                            then Car s

else find ⟨pred j, Cdr s⟩

in find

(c) Let M be a single-tape Turing machine over the alphabet {0, 1}. As stated in the problem, we will represent the blank symbol b/ by the number 2 in our PCF-simulation. Suppose q_{f} is the natural number representing the halt state of M. Then, associated with the description of M, is the transition function δ_{M}, which is assumed to be a total function from ({1, …, q_{M}}− {q_{f}})×{0, 1, b/} to {1, …, q_{M}}×{0, 1, b/}×{L, R}, giving the new state, symbol to be written on the tape, and direction to move the head. In our PCF-simulation we will use the number 0 to represent the “hung” state of the Turing machine, when the tape head is moved off the left edge of the tape. The number n_{ℓ} will code the sequence of tape symbols to the left of the tape head, starting with the symbol immediately to the left of the tape head. The number n_{r} will code a finite sequence of tape symbols to the right of the tape head such that all the tape symbols on the tape to the right of this finite sequence are all blanks.

Given the Turing machine M, we can then construct a PCF function to compute the next state as follows :

newState_{M} =^{def} λ⟨q: nat, n_{ℓ}: nat, n_{r}: nat⟩.

if Eq? q 1

then                  if Eq? (Car n_{r}) 0 then Q_{1,0}
else if Eq? (Car n_{r}) 1 then Q_{1,1}
else Q_{1,b /}

⋮

                    else if Eq? q i

then                  if Eq? (Car n_{r}) 0 then Q_{i,0}
else if Eq? (Car n_{r}) 1 then Q_{i,1}
else Q_{i,b /}

⋮

                    else q

where we have a clause Q_{i,j} for each i ≤ q_{M}, i ≠ q_{f} and j ∈ {0, 1, b/} returning the next state if the current state is i, and the symbol being read is j. The number of such clauses is clearly finite in number, since the number of states is finite — hence, the above PCF expression can be constructed. The final else clause corresponds to the case q = 0 or q = q_{f}, i.e., if the current state is either the “hung” state or the final state we continue to remain in the same state. Each clause Q_{i,j} is constructed as follows :

δ(i, j) = (i′, j′, L) ⇒ Q_{i,j} =^{def} if (Empty? n_{ℓ}) then 0 else i′
δ(i, j) = (i′, j′, R) ⇒ Q_{i,j} =^{def} i′

The function which computes the next n_{ℓ} also looks like newState_{M} and is as follows :

newLeft_{M} =^{def} λ⟨q: nat, n_{ℓ}: nat, n_{r}: nat⟩.

if Eq? q 1

then                  if Eq? (Car n_{r}) 0 then L_{1,0}
else if Eq? (Car n_{r}) 1 then L_{1,1}
else L_{1,b /}

⋮

                    else if Eq? q i

then                  if Eq? (Car n_{r}) 0 then L_{i,0}
else if Eq? (Car n_{r}) 1 then L_{i,1}
else L_{i,b /}

⋮

                    else n_{ℓ}

where,

δ(i, j) = (i′, j′, L) ⇒ L_{i,j} =^{def} Cdr n_{ℓ}
δ(i, j) = (i′, j′, R) ⇒ L_{i,j} =^{def} Cons ⌈j′⌉ n_{ℓ}

and, ⌈j′⌉ denotes the natural number code for the symbol j′. Finally, the PCF-function to compute the next n_{r} is:

newRight_{M} =^{def} λ⟨q: nat, n_{ℓ}: nat, n_{r}: nat⟩.

if Eq? q 1

then                  if Eq? (Car n_{r}) 0 then R_{1,0}
else if Eq? (Car n_{r}) 1 then R_{1,1}
else R_{1,b /}

⋮

                    else if Eq? q i

then                  if Eq? (Car n_{r}) 0 then R_{i,0}
else if Eq? (Car n_{r}) 1 then R_{i,1}
else R_{i,b /}

⋮

                    else n_{r}

where,

δ(i, j) = (i′, j′, L) ⇒ R_{i,j} =^{def} Cons (Car n_{ℓ}) (Cons ⌈j′⌉ (Cdr n_{r}))
δ(i, j) = (i′, j′, R) ⇒ R_{i,j} =^{def} if Empty? (Cdr n_{r}) then Cons ⌈b/⌉ Null else Cdr n_{r}

(d) Let us first use the functions we wrote in (c), to write a function Run_{M} which gives us the configuration of the Turing Machine after running the machine for n steps.

Run_{M} =^{def} letrec run ⟨n: nat, q: nat, n_{ℓ}: nat, n_{r}: nat⟩: nat × nat × nat =

if Eq? n 0 then ⟨q, n_{ℓ}, n_{r}⟩

else run ⟨pred n, newState_{M} ⟨q, n_{ℓ}, n_{r}⟩, newLeft_{M} ⟨q, n_{ℓ}, n_{r}⟩, newRight_{M} ⟨q, n_{ℓ}, n_{r}⟩⟩

            in

run

Now, the required function f_{M} can be written as:

f_{M} =^{def} λ⟨j: nat, s: nat, n: nat⟩.

let finconfig: nat × nat × nat = Run_{M} ⟨n, q_{0}, Null, s⟩

                 in

let fintape: nat = concatRev ⟨Proj_{2} finconfig, Proj_{3} finconfig⟩

                 in

if less (Length fintape) j

                 then ⌈b/⌉

else nthEntry ⟨j, fintape⟩

where, q_{0} is the start state of the Turing machine M, and the head is initially assumed to be at the left end of the tape.

(e) The partial function f: N → N computed by the Turing machine M could be defined as follows. For any number n start the machine with the binary representation of n on the tape and the head at the left end. If the machine halts, then f(n) is the number whose binary representation is given by the initial sequence of non-blank symbols on the tape finally. f(n) is undefined if the machine “hangs” during the course of the computation, or never halts.

Then, given a Turing machine M, we could write a PCF-expression F_{M} which represents the same function as that computed by M as follows:

F_{M} =^{def} λx: nat.

           let

numSteps: nat = search (λn: nat. Eq? (Proj_{1} Run_{M} ⟨n, q_{0}, Null, nToB x⟩) q_{f} )

           in

let finconfig: nat × nat × nat = Run_{M} ⟨numSteps, q_{0}, Null, nToB x⟩ in bToN (concatRev ⟨Proj_{2} finconfig, Proj_{3} finconfig⟩)

Note that the search function ensures that we reach a normal form for an argument, only if the Turing Machine halts on the binary representation of that argument.

The conversion functions nToB , and bToN can be easily written as follows :

nToB =^{def} letrec aux (⟨x: nat, ans: nat⟩): nat =

if Eq? x 1 then ans

else aux ⟨half x, Cons (mod x 2) ans⟩

                    in

λx: nat. if Eq? x 0 then Cons 0 Null else aux ⟨x, Null⟩

bToN =^{def} letrec conv (b: nat): nat =

if Empty? b then 0

else if Eq? (Car b) ⌈b/⌉ then 0 else mult ⟨2, conv (Cdr b)⟩ + (Car b)

in conv

Exercise 2.5.18.

(a) We can define the term G as follows:

G =^{def} λx: bool. if (H_{bool} x) then fix (λy: bool. y) else true

If M does not have a normal form, then H_{bool} M → →^{left} true and hence G M → →^{left} fix (λy: bool. y) whose reduction proceeds infinitely under left-most reduction; hence, G M does not have a normal form. If M has a normal form, then H_{bool} M → → false and G M has normal form true .

(b) If fix G does not have a normal form, then by the properties of G, G (fix G) has a normal form, say R. Hence, G → → G (fix G) → → R, i.e., G also has a normal form, a contradiction. On the other hand, if fix G has a normal form, say Q, then fix G → → G (fix G) and hence, by confluence, G (fix G) also has normal form Q. This contradicts the property of G, for then, M ≡ fixG is a term that has a normal form, yet G M also has a normal form.

The contradiction in either case shows that there cannot exist such a term G. Hence, there is no term H_{bool} defining the halting function.

Exercise 2.5.26. Suppose there is a PCF expression PIF_{nat} with the properties stated in the question. Consider the context C[·, ·, ·] =^{def} PIF_{nat} [ ]_{1} [ ]_{2} [ ]_{3} . By Lemma 2.5.24, there are two possibilites for the lazy reduction of C[true, 1, 2] to 1. The first implies that C[M_{1}, M_{2}, M_{3}] → → 1 for all closed M_{1}: bool, M_{2}, M_{3}: nat . But this contradicts C[false, 1, 2] → → 2. Therefore, there is an integer i ∈ {1, 2, 3} such that for all closed M_{1}: bool, M_{2}, M_{3}: nat , there is an evaluation context ev[ ] with C[M_{1}, M_{2}, M_{3}] → →^{lazy} ev[M_{i}]. We show that each of the possiblities for i results in a contradiction.

Case i = 1. Then, for M_{1} ≡ fix_{bool}(λx: bool. x), M_{2} ≡ 1, M_{3} ≡ 1, PIF_{nat} M_{1}M_{2}M_{3} → →^{lazy} ev[M_{1}] which, by Lemma 2.5.21, would have no normal form, since M_{1} does not. This contradicts PIF_{nat} M_{1} M_{2} M_{3} → → 1.

Case i = 2. Then, for M_{1} ≡ false, M_{2} ≡ fix_{nat}(λx: nat. x), M_{3} ≡ 1, we will get that PIF_{nat} M_{1}M_{2}M_{3} has no normal form, while it is supposed to reduce to 1.

Case i = 3. Then, for M_{1} ≡ true, M_{2} ≡ 1, M_{3} ≡ fix_{nat}(λx: nat. x), we get a contradiction as in the case for i = 2.

Exercise 2.5.27. Let M and N be closed terms of type nat or bool having no normal form. Consider any context C[ ] such that C[M] and C[N] are programs. Suppose eval(C[M]) is defined and equal to P. Then C[M] has normal form P. By Lemma 2.5.24, there are two possiblities for the reduction of C[M]. The second possibility cannot be true, for then C[M] → →^{lazy} ev[M] which, by Lemma 2.5.21, cannot be reduced to normal form P. By the first possiblity, C[N] also has normal form P. A symmetric argument shows that if eval(C[N]) is defined and is equal to P, then eval(C[M] = P. Thus, we have shown that

eval(C[M]) = P iff eval(C[N]) = P

from which we get that

eval(C[M]) ≃ eval(C[N])

It follows that M =_{op} N.

Exercise 2.6.3.

(b) Apply f to both sides of g x = Case x (g ∘Inleft) (g ∘Inright) and combine with (f ∘g) x = Case x (f ∘ g ∘ Inleft) (f ∘ g ∘ Inright).

(d) By the extensionality axiom, we have M z = Case z (M ∘Inleft) (M ∘Inright). By assumption, M ∘ Inleft = λx: σ. M(Inleftx) = N and M ∘ Inright = λy: τ. M(Inrighty) = P. Therefore M z = Case z N P and by lambda abstraction and (η) we may prove M = λz: σ + τ. Case z N P.

Exercise 2.6.7. (c)

fix_{σ} =^{def} λf: σ → σ.(λx: σ′. f((dn x)x))(⌊ ⌋(λx: σ′. f((dn x)x)))

Chapter 3

Exercise 3.3.9. (a)

[[(x + 1) ∗ y]]η = ∗^{N} ([[(x + 1)]]η, [[y]]η)
= ∗^{N} (+^{N} ([[x]]η, [[1]]η), η(y))
= ∗^{N} (+^{N} (η(x), 1^{N}), 2^{N})
= ∗^{N} (+^{N} (1^{N} , 1^{N}), 2^{N})
= ∗^{N} (2^{N} , 2^{N})
= 4

(b) Let η(x) = k_{1} , η(y) = k_{2} , η(z) = k_{3} where k_{1}, k_{2}, k_{3} ∈ N.

Then,

[[(x + y) ∗ z]]η = ∗^{N} ([[(x + y)]]η, [[z]]η)
= ∗^{N} (+^{N} ([[x]]η, [[y]]η), [[z]]η)
= ∗^{N} (+^{N} (k_{1}, k_{2}), k_{3})
= (k_{1} + k_{2}) ∗ k_{3}

where the last expression denotes a natural number with + and ∗ the functions on N.

Similarly,

[[(x ∗ y) + (y ∗ z)]]η = (k_{1} ∗ k_{3}) + (k_{2} ∗ k_{3})

By properties of addition and multiplication over N (namely distributivity) we have that

(k_{1} + k_{2}) ∗ k_{3} = (k_{1} ∗ k_{3}) + (k_{2} ∗ k_{3})

which gives us the desired identity.

Exercise 3.3.10. (a)

[[push x (pop s)]]η = push^{A}([[x]]η, pop^{A}([[s]]η))
= push^{A}(3, pop^{A}(⟨2, 1⟩))
= push^{A}(3, ⟨1⟩)
= ⟨3, 1⟩

(b) Consider any environment η mapping s: stack to a nonempty sequence, say n: : t, where n ∈ N , t ∈ N^{∗}. Then,

[[push (top s) (pop s)]]η = push^{A}(top^{A}([[s]]η), pop^{A}([[s]]η))
= push^{A}(top^{A}(n: : t), pop^{A}(n: : t))
= push^{A}(n, t)
= n: : t
= [[s]]η

If η(s) = ϵ, then [[push (top s) (pop s)]]η = ⟨0⟩, but [[s]]η = ϵ.

Exercise 3.3.4. We prove by induction on the structure of M that, for any sort s, if M ∈ Terms^{s}(Σ, Γ) then M ∈ Terms^{s}(Σ, Γ′).

Base Case: M is a variable, say x. But then, x: s ∈ Γ. Since Γ ⊆ Γ′, we thus have x: s ∈ Γ′, and hence M ∈ Terms^{s}(Σ, Γ′).

Induction Step: M ≡ fM_{1} … M_{k}. Then M_{i} ∈ Terms^{s_{i}}(Σ, Γ). Hence, by the induction hypothesis M_{i} ∈ Terms^{s_{i}}(Σ, Γ′), and since f : s_{1} × … × s_{k} → s ∈ Σ, we therefore have

M ∈ Terms^{s}(Σ, Γ′).

Exercise 3.3.12. Suppose [[M]]η′ = [[N]]η′ for every environment η′ satisfying Γ, x: s. and P ∈ Terms^{s}(Σ, Γ) is a well-formed term. Let η be any environment satisfying Γ and let a = [[P]]η. Since P ∈ Terms^{s}(Σ, Γ), a will be in A^{s} and the environment η[a/x] will satisfy Γ, x: s. Therefore, [[M]]η[a/x] = [[N]]η[a/x]. By the Substitution Lemma, we have [[M]]η[a/x] = [[[P/x]M]]η, and similarly for N. Thus [[[P/x]M]]η = [[[P/x]N]]η. Since η was chosen arbitrary, this holds for every environment η satisfying Γ.

Exercise 3.4.2. If A^{s} = ∅, there is no environment η respecting the sort assignment {x: s} and thus we trivially have that for every environment η respecting the sort assignment,

A, η ⊧ x = x [{x: s}].

Otherwise, [[x]]η = η(x) = [[x]]η, and we have the required result.

Exercise 3.4.4. (a) The crucial observation to be made is that the function

f(x) = K^{A} ·^{A} x

is an injective function from A into A. This can be seen as follows :

f(a_{1}) = f(a_{2})
⇒ f(a_{1}) ·^{A} a_{1} = f(a_{2}) ·^{A} a_{1}
⇒ (K^{A} ·^{A} a_{1}) ·^{A} a_{1} = (K^{A} ·^{A} a_{2}) ·^{A} a_{1}
⇒ a_{1} = a_{2}.

We will now solve the problem by showing that if A has a finite number of elements, then it can only have one element. Suppose A is finite. Then f: A → A being injective, would be surjective — hence there is some a ∈ A with f(a) = K^{A} i.e. K^{A} ·^{A} a = K^{A}. Now consider any element x of A. We then have

f(x) = K^{A} ·^{A} x
= (K^{A} ·^{A} a) ·^{A} x
= a.

Hence, if x and y are elements of A, then f(x) = a = f(y). Since f is injective, this gives us x = y, for any x, y ∈ A; which implies that all elements of A must be equal to each other, i.e. A has only one element.

(b) We will solve the problem by showing that if · is associative, the carrier of the algebra can only have one element. If · is associative, then any pair of terms obtained by rearranging parentheses must be equal. But we get two very different equations by parenthesizing K ·K ·x·y ·z as follows.

\begin{matrix}A ⊧ ((K · K) · (x · (y · z))) = K \\ A ⊧ ((K · ((K · x) · y)) · z) = x. \end{matrix}

If · is associative, then these two must be equal. But this gives us

A ⊧ K = x,

which implies that every element of A is equal to K^{A}.

Exercise 3.4.8. For the ‘if’ direction, we must show that [[M]]η = [[N]]η for every environment η satisfying Γ; but this is trivially true since M and N are syntactically identical.

For the ‘only if’ direction, assume that Terms(Σ, Γ) ⊧ M = N [Γ]. Hence [[M]]η = [[N]]η for every environment η for Terms(Σ, Γ) that satisfies Γ; in particular, it holds for the environment which maps each variable x: s in Γ to the term x in Terms^{s}(Σ, Γ). Now, by Lemma 3.4.6, we know that [[M]]η = ηM and similarly [[N]]η = ηN; for the “identity” environment described above, ηM = M and ηN = N, so we find that M and N must be identical.

Exercise 3.4.9.

(a) Take M = 1, N = x, and P = y; then [M, N/x, y]P = x, while [M/x]([N/y]P) = 1 ≠ x.

(b) First obtain variables x′_{i} for 1 ≤ i ≤ k, different from x_{1}, …, x_{k}, such that x′_{i} does not occur in P or in M_{i+1}, …, M_{k}.

Now the sequence of single-variable substitutions

[M_{1}/x′_{1}], …, [M_{k}/x′_{k}], [x′_{1}/x_{1}], …, [x′_{k}/x_{k}]

will do the job, since there is no variable in M_{j} that could be captured by a later substitution, as x′_{i} does not occur in M_{j} for i < j.

Exercise 3.4.19. Let us first observe the following derived rule, which we will use repeatedly in our solution.

(aux)  \frac{M = N [Γ]}{[P/x]M = [P/x]N [(Γ − \{x: s\}) ∪ Γ′]} x: s ∈ Γ, P ∈ Terms^{s}(Σ, Γ′), Γ ∩ Γ′ = ϕ

Now, (aux) is a derived rule as follows. From the hypothesis, we may use (add var) repeatedly to derive the equation

M = N [Γ ∪ Γ′]

By (ref ), we also have the equation

P = P [(Γ − {x: s}) ∪ Γ′]

We may now use (subst) to give us the consequent of (aux).

Now, we show that the rule given in the question is a derived rule, as follows. Suppose

Γ = {x_{1}: s_{1}, …, x_{n}: s_{n}}

Then, if we take fresh variables x′_{1}, …, x′_{n} not occurring in Γ or Γ′, we know by Exercise 3.4.9 that

SM ≡ [Sx_{1}/x′_{1}](…, ([Sx_{n}/x′_{n}]([x′_{1}/x_{1}](…, ([x′_{n}/x_{n}]M) …))) …)

Applying (aux) to the hypothesis with Γ for Γ, x_{n} for x, {x′_{1}, …, x′_{n}} for Γ′ and x′_{n} for P, we will get the equation

[x′_{n}/x_{n}]M = [x′_{n}/x_{n}]N [Γ − {x_{n}}, x′_{1}, …, x′_{n}]

Applying (aux) n−1 more times, with appropriate x_{i} for x, and x′_{i} for P, we will get the equation

[x′_{1}/x_{1}](…, ([x′_{n}/x_{n}]M) …) = [x′_{1}/x_{1}](…, ([x′_{n}/x_{n}]N) …) [x′_{1}, …, x′_{n}]

Now apply (aux) with {x′_{1}, …, x′_{n}} for Γ, x′_{n} for x, Γ′ for Γ′ and Sx_{n} for P to obtain the equation

[Sx_{n}/x′_{n}]([x′_{1}/x_{1}](…, ([x′_{n}/x_{n}]M) …)) = [Sx_{n}/x′_{n}]([x′_{1}/x_{1}](…, ([x′_{n}/x_{n}]N) …)) [Γ′, x′_{1}, …, x′_{n−1}]

Applying (aux) n − 1 more times, with x′_{i} for x, and Sx_{i} for P we will get the equation

[Sx_{1}/x′_{1}](… [Sx_{n}/x′_{n}]([x′_{1}/x_{1}](… [x′_{n}/x_{n}]M …)) …) = [Sx_{1}/x′_{1}](… [Sx_{n}/x′_{n}]([x′_{1}/x_{1}](… [x′_{n}/x_{n}]N …)) …)[Γ′]

which, by Exercise 3.4.9 is the desired consequent.

Exercise 3.4.20.

(a) Let us first establish the following fact, which would be useful in solving (a) and (b). Suppose Γ is a sort assignment, and we have a term M ∈ Terms^{mset}(Σ, Γ) i.e. M is a term of sort mset. Then, if a and b are different numerals, we can prove the equation

count(a, (insert(b, M))) = count(a, M) [Γ]

from the specification, using the following proof (P1 ). We have as axiom

count(x, (insert(y, m))) = cond_{m}(Eq?(x, y), count(x, m)+1, count(x, m)) [x: nat, y: nat, m: mset] Applying Exercise 3.4.19 with S = [a, b, M/x, y, m], we get

count(a, (insert(b, M))) = cond_{m}(Eq?(a, b), count(a, M) + 1, count(a, M)) [Γ] (11.3)

Since, a and b are different numerals, we have as an axiom that

Eq?(a, b) = false [ ]

Thus, using (add var), (cong) and (ref ), we would get cond_{m}(Eq?(a, b), count(a, M)+1, count(a, M)) = cond_{m}(false, count(a, M)+1, count(a, M)) [Γ] Now, using the axiom

cond_{m}(false, u, v) = v [u: mset, v: mset]

and applying Exercise 3.4.19, we get

cond_{m}(false, count(a, M) + 1, count(a, M)) = count(a, M) [Γ]

Thus, using (trans), we get

cond_{m}(Eq?(a, b), count(a, M) + 1, count(a, M)) = count(a, M) [Γ]

Finally combining this with equation 11.3 using (trans), we get the desired equation. In an exactly similar fashion, if Γ is a sort assignment, and we have a term M ∈ Terms^{mset}(Σ, Γ) i.e. M is a term of sort mset, and a is a numeral, we can prove the equation

count(a, (insert(a, M))) = count(a, M) + 1 [Γ]

from the specification using a proof (P2 ). Now, we can prove the required equation as follows : Using proof (P1 ), with M as insert(3, empty), we can get the equation

count(3, insert(5, insert(3, empty))) = count(3, insert(3, empty)) [ ]

Now, using proof (P2 ), with M as empty, we get the equation

count(3, insert(3, empty)) = count(3, empty) + 1 [ ]

Thus, using (trans), we get

count(3, insert(5, insert(3, empty))) = count(3, empty) + 1  (11.4)

Now, we have as axiom

count(x, empty) = 0 [x: nat]

Thus, using (subst), we get

count(3, empty) = 0 [ ]

Now, using (ref ), (cong) and (trans) with one of the axioms for addition, we get that

count(3, empty) + 1 = 1 [ ]

Thus, using (trans) with Equation 11.4, we derive the required equation.

(b) Let a,b and c be any numerals. Then, there are four possible cases, and we prove the required equation from the specification, in each of the four cases. Case I a = b,a = c. Then, we have the required equation by (ref ). Case II a ≠ b, a = c. First, using the proof (P1 ), with M as insert(c, m), we get

count(a, insert(b, insert(c, m))) = count(a, insert(c, m)) [m: mset]

And, then, using the proof (P2 ), with M as m, we get

count(a, insert(c, m)) = count(a, m) + 1 [m: mset]

Thus, using (trans) we get

count(a, insert(b, insert(c, m))) = count(a, m) + 1 [m: mset]  (11.5)

Now, using the proof (P2 ), with M as insert(b, m), we get

count(a, insert(c, insert(b, m))) = count(a, insert(b, m)) + 1 [m: mset]

Using the proof(P1 ), with M as m, we get

count(a, insert(b, m)) = count(a, m) [m: mset]

Hence, using (ref ) and (cong), we get

count(a, insert(b, m)) + 1 = count(a, m) + 1 [m: mset]

Thus, using (trans), we get

count(a, insert(c, insert(b, m))) = count(a, m) + 1 [m: mset]

Now, using (sym), and (trans) with Equation 11.5, we can derive the required equation. Case III a ≠ c, a = b. Using Case II above, we know that we can derive the equation

count(a, insert(c, insert(b, m))) = count(a, insert(b, insert(c, m))) [m: mset] Now, using (sym), we can derive the required equation.

Case IV a ≠ b, a ≠ c. First, using the proof (P1 ), with M as insert(c, m), we get

count(a, insert(b, insert(c, m))) = count(a, insert(c, m)) [m: mset]

Then, using the proof (P1 ) with M as m, we get

count(a, insert(c, m)) = count(a, m) [m: mset]

Thus, using (trans), we get

count(a, insert(b, insert(c, m))) = count(a, m) [m: mset]

In an exactly similar fashion, we can derive

count(a, insert(c, insert(b, m))) = count(a, m) [m: mset]

Now, using (sym) and (trans), we can derive the required equation.

(c) Consider an algebra A in which we interpret the natural numbers and booleans in the usual way, and interprets multi-sets as sequences of numbers. To describe the functions on multisets, let us write n: : s for the result of adding natural number n onto the front of sequence s ∈ N^{∗}. Using this notation, we have A = ⟨N^{∗}, N , B, 0^{A}, 1^{A}, …, +^{A}, Eq?^{A}, true^{A}, false^{A}, empty^{A}, insert^{A}, count^{A}, cond_{n}^{A}, cond_{b}^{A}, cond_{m}^{A}⟩ with multi-set functions determined as follows

empty^{A}  = ϵ, the empty sequence
insert^{A}(n, s) = n: : s
count^{A}(n, s) = no. of times n appears in s

It is easy to see that A satisfies all the equations in the specification. However, A does not satisfy the equation

insert(x, insert(y, m)) = insert(y, insert(x, m)) [x: nat, y: nat, m: mset]

because if we take the environment η mapping x ↦ 0 , y ↦ 1 and m ↦ ϵ, then

A[[insert(x, insert(y, m))]]η = ⟨0, 1⟩
A[[insert(y, insert(x, m))]]η = ⟨1, 0⟩

and hence, A does not satisfy the given equation. The equation is also not satisfied by the initial algebra, because the ground instance of the equation with the ground substitution S = [0, 1, empty/x, y, m] is not satisfied by the algebra A and is hence not provable from the specification.

Exercise 3.4.21.

(a) We have as axiom the equation

lsub(node t t′) = t [t, t′ : tree, …]

Thus, using Exercise 3.4.19 with S = [rsub(node(leaf a) (leaf b)), (leaf c)/t, t′], we get

lsub(node(rsub(node(leaf a) (leaf b)) (leaf c))) = rsub(node(leaf a) (leaf b)) [ ] Similarly, applying Exercise 3.4.19 to the axiom

rsub(node t t′) = t′

we get

rsub(node(leaf a) (leaf b)) = leaf b [ ]

Now, using (trans), we get the desired equation.

(b) Applying Exercise 3.4.19 to the axiom for lsub , we get

lsub M = leaf a [ ]

Now, applying the derived rule (cong), we get

label(lsub M) = label(leaf a) [ ]

Similarly, using the axiom for rsub , Exercise 3.4.19 and (cong), we will get

label(rsub M) = label(leaf a) [ ]

Applying (sym) and (trans), we now get the desired equation.

(c) Case I: M ≡ leaf N. Then, using Exercise 3.4.19 and the axiom

is leaf ?(leaf x) = true

we will get

is leaf ? M = true  (11.6)

Now, using (cong) and (ref ), we will get

cond_{t} (is leaf ? M) (leaf a) M = cond_{t} true (leaf a) M [ ]

Now, using Exercise 3.4.19 and the axiom

cond_{t}(true, t, t′) = t

and (trans), we’ll get

cond_{t} (is leaf ? M) (leaf a) M = leaf a [ ]

Now, using (cong), we get

is leaf ?(cond_{t} (is leaf ? M) (leaf a) M) = is leaf ?(leaf a) [ ]

In the same way that we derived 11.6, we can get

is leaf ?(leaf a) = true [ ]

Thus, using (trans), we get

is leaf ?(cond_{t} (is leaf ? M) (leaf a)) = true  (11.7)

Now, applying (sym) and using (trans) with 11.6, we get the desired equation. Case II: M ≡ node N N′. Then, using Exercise 3.4.19 and the axiom

is leaf ?(node t t′) = false

we will get

is leaf ? M = false [ ]

Now, using (cong) and (ref ), we will get

cond_{t} (is leaf ? M) (leaf a) M = cond_{t} false (leaf a) M [ ]

Now, using Exercise 3.4.19 and the axiom

cond_{t}(false, t, t′) = t

and (trans), we’ll get

cond_{t} (is leaf ? M) (leaf a) M = M [ ]

Now, using (cong), we get

is leaf ?(cond_{t} (is leaf ? M) (leaf a) M) = is leaf ? M [ ]

Applying (sym), we get the desired equation in this case as well.

(d) Define the set T to contain exactly the following elements:

(1) If n ∈ N, then n ∈ T

(2) If t_{1}, t_{2} ∈ T , then ⟨t_{1}, t_{2}⟩ ∈ T .

Consider the algebra A in which we interpret atoms as natural numbers, booleans in the standard way, and take the set T to be the carrier for the sort tree , with interpretation for the tree functions defined as:

a^{A} = 0, b^{A} = 1, …

leaf^{A}(n) = n, for any n ∈ N

node^{A}(t_{1}, t_{2}) = ⟨t_{1}, t_{2}⟩

label^{A}(t) = \{ \begin{matrix}t & if t ∈ N \\ n & if t = ⟨n, t′⟩, n ∈ N \\ 0 & otherwise \end{matrix}

is leaf ?^{A}(t) = \{ \begin{matrix}true & if t ∈ N \\ false & if t = ⟨t_{1}, t_{2}⟩ \end{matrix}

lsub^{A}(t) = \{ \begin{matrix}t & if t ∈ N \\ t_{1} & if t = ⟨t_{1}, t_{2}⟩ \end{matrix}

rsub^{A}(t) = \{ \begin{matrix}t & if t ∈ N \\ t_{2} & if t = ⟨t_{1}, t_{2}⟩ \end{matrix}

It is easy to see that with the above interpretation, the algebra A satisfies all the equations in the specification. However, A does not satisfy the equation

label(node t t′) = label(node t′ t)

because if we take the environment η mapping t ↦ 1, t′ ↦ ⟨2, 3⟩, then

A[[label(node t t′)]]η = 1
A[[label(node t′ t)]]η = 0

and hence A does not satisfy the equation.

(e) We begin by defining a function ht: T → N as:

• ht(n) = 0, for n ∈ N,

• ht(⟨t_{1}, t_{2}⟩) = min(ht(t_{1}), ht(t_{2})) + 1.

We can now show that if M is a term of sort tree containing only atom variables x_{1}, …, x_{i}, boolean variables y_{1}, …, y_{j}, and tree variables z_{1}, …, z_{k} and not containing leaf , then for any number l, there is a minimum number m such that as long as environment η sends each stack variable z_{p} to a tree t_{p} with ht(t_{p}) ≥ m, ht(A[[M]]η) ≥ l. We use induction on the structure of M. If M is a tree variable z_{p}, then clearly we can choose m to be l. If M is node M_{1} M_{2} , then we can choose m = max(m_{1}, m_{2}) where m_{1} and m_{2} are the numbers for M_{1} and M_{2} to achieve heights l − 1. If M is lsub M_{1} or rsub M_{1} , then we can choose m = m_{1} where m_{1} is the number for M_{1} to achieve height l + 1. finally, if M is cond_{t} P M_{1} M_{2} , we can choose m = max(m_{1}, m_{2}) where m_{1} and m_{2} are the numbers for M_{1} and M_{2} to achieve height l. By examining the function symbols with range sort tree , we see that there are no other possiblities for M.

Now, consider the equation lsub(leaf x) = M [Γ, x: atom]

for any term M: tree not containing the function leaf . Consider an environment η such that ht(A[[M]]η) ≥ 1, which exists by the proof in the previous paragraph. Since

ht(A[[lsub(leaf x)]]η) = ht(η(x)) = 0

it follows that A[[M]]η ≠ A[[lsub(leaf x)]]η, and since A satisfies the specification, it follows by soundness that the equation is not provable.

Exercise 3.4.25.

(a) To show that ≡_{n} is a congruence relation we must first show that it is an equivalence relation.

Reflexive: since n divides |i − i| = 0 for every n and i, we have that i ≡_{n} i.

Symmetric: since |i − j| = |j − i|, we find that i ≡_{n} j implies j ≡_{n} i.

Transitive: an equivalent statement to “n divides |i−j|” is that i−j = cn for some integer c. Thus if i ≡_{n} j and j ≡_{n} k, then i − j = cn and j − k = dn for some c and d; hence

i − k = (i − j) + (j − k) = (c + d)n, so i ≡_{n} k.

Now we must show that ≡_{n} respects all the functions in Σ. The two “zero-ary” functions are easy: 0 ≡_{n} 0 and 1 ≡_{n} 1 since ≡_{n} is reflexive. For addition, we assume i ≡_{n} j and k ≡_{n} l, which means that i − j = cn and k − l = dn for some integers c and d. Thus (i + k) − (j + l) = (c + d)n, and so (i + k) ≡_{n} (j + l). This shows that ≡_{n} is a congruence relation.

(b) The carrier A^{nat}/ ≡_{n} consists of the equivalence classes of natural numbers modulo n. Since any i ≥ n is congruent modulo n to some j with 0 ≤ j ≤ n − 1, the set A^{nat}/ ≡_{n} has n elements, {[0], [1], …, [n − 1]}.

(c) Assume that i ≡_{n} j and k ≡_{n} l, which means that i−j = cn and k−l = dn for some integers c and d. Now, ik − jl = (i − j)(k − l) + (i − j)l + (k − l)j, and so ik − jl = (cl + dj + cdn)n which gives us that ik ≡_{n} jl. Hence, ≡_{n} is a congruence relation on A even if we have a multiplication symbol interpreted in the usual way.

Since ≡_{n} is not a congruence with respect to the property of primality, we would not expect ≡_{n} to be a congruence with the new symbol p. For example, take n to be 5. Then 2 ≡_{5} 7, but p(2) = 3, p(7) = 11 and 3 ≢_{5} 11.

Exercise 3.4.16. To show that Th(A) is a semantic theory, we need to show that it is closed under semantic implication, i.e., that if Th(A) ⊧ M = N [Γ], then M = N [Γ] ∈ Th(A). By the definition of ⊧, we know that if Th(A) ⊧ M = N [Γ], then for every algebra A′ such that A′ ⊧ Th(A), we must also have that A′ ⊧ M = N [Γ]. But by the definition of Th(A) we know that A is itself such an algebra, so A ⊧ M = N [Γ], hence M = N [Γ] ∈ Th(A).

Exercise 3.4.3. If A is trivial, then A ⊧ x = y [x: s, y: s] for each sort s and any variables x and y. If the carrier A^{s} of sort s in A has two or more elements, then choose two of them, a_{1} and a_{2} , and consider the environment η = {x := a_{1}, y := a_{2}}; then the above equation is not satisfied at η, which is a contradiction, so A^{s} must have at most one element.

In the other direction, if each carrier of A has at most one element, then consider an equation M = N [Γ]. If the sort assignment Γ contains a variable of a sort whose carrier is empty, then the equation is trivially satisfied; otherwise, let η be the unique environment for Γ, which maps each variable in Γ to the single element of the carrier for the corresponding sort. Now we have that A[[M]]η ∈ A^{s} and A[[M]]η ∈ A^{s}; since A^{s} has only one element, the meanings of M and N must be equal, hence the equation is satisfied. Since we have shown that every equation M = N [Γ] is satisfied by A, the algebra is trivial.

Exercise 3.5.6.

(a) We need to show that if we have a surjective homomorphism h from A to B, then every equation that holds in A also holds in B. Assume that M = N holds in A, i.e., that A[[M]]η = A[[N]]η for every appropriate environment η. Now, take an arbitrary environment η′ for B satisfying the sort assignment; since h is surjective, we can find an environment η for A such that η′ = η^{h} — simply choose η(x) to be some a ∈ A^{s} such that h(a) = η′(x). Then by Lemma 2.4.3, B[[M]]η′ = h(A[[M]]η), and similarly for N; thus B[[M]]η′ = B[[N]]η′, and, since η′ was arbitrary, M = N holds in B.

(b) If A and B are isomorphic, then we have surjective homomorphisms in each direction. Thus, by part (a), we know that Th(A) ⊆ Th(B) and Th(B) ⊆ Th(A), hence Th(A) = Th(B).

(c) Consider the trivial signature with one sort and no function symbols. Then two algebras for this signature are A = ⟨{a}⟩ and B = ⟨{a, b}⟩. There is a homomorphism h from A to B which maps a to a; it is not surjective, since nothing maps to b. Now, we have that A ⊧ x = y, but B |̸= x = y; hence the theory of A is not a subset of the theory of B.

Exercise 3.4.27. We first define the partial quotient structure A/ ∼ by defining the carrier and function interpretations as follows :

\begin{aligned}(A/∼)^{s} & = & \{ [a]_{∼} | a ∈ A, a ∼_{s} a \} \\ f^{A/∼}([a_{1}], …, [a_{k}]) & = & [f^{A}(a_{1}, …, a_{k})] \end{aligned}

To show that A/ ∼ is indeed an algebra, we need to show that each f^{A/∼} is a well-defined function. This involves showing that the right hand side in the above definition exists and is an element of (A/∼)^{s}; and that the value on the right is independent of the choice of the representatives a_{1}, …, a_{k}. Since, for each i, [a_{i}] ∈ (A/∼)^{s_{i}}, we have a_{1} ∼ a_{1}, …, a_{k} ∼ a_{k}, and hence f^{A}(a_{1}, …, a_{k}) ∼ f^{A}(a_{1}, …, a_{k}) — thus, [f^{A}(a_{1}, …, a_{k})] ∈ (A/∼)^{s}. To show the other aspect of the well-definedness, assume that [a_{1}] = [b_{1}], …, [a_{k}] = [b_{k}]. Then, a_{1} ∼ b_{1}, …, a_{k} ∼ b_{k} and hence f^{A}(a_{1}, …, a_{k}) = f^{A}(b_{1}, …, b_{k}) and thus, f^{A/∼}([a_{1}], …, [a_{k}]) = f^{A/∼}([b_{1}], …, [b_{k}]).

Next, we show by induction on the structure of M, that if η is an environment for A with η(x) ∼ η(x) for each x in M, then

(A/∼)[[M]]η_{∼} = [ A[[M]]η]_{∼}.

The inductive proof given for Lemma 3.4.22 goes through, for this, without any change.

Exercise 3.5.5. Let h: A → B and k: B → C be homomorphisms of Σ-algebras. Then, we have to show that the composition k ∘ h: A → C satisfies the definition of a homomorphism. But, this can be easily seen as follows: For any function symbol f: s_{1} × … × s_{k} → s of Σ,

(k ∘ h)^{s}(f^{A}(a_{1}, …, a_{k})) = k^{s}(h^{s}(f^{A}(a_{1}, …, a_{k})))
= k^{s}(f^{B}(h^{s_{1}}a_{1}, …, h^{s_{k}}a_{k})
= f^{C}(k^{s_{1}}(h^{s_{1}}a_{1}), …, k^{s_{k}}(h^{s_{k}}a_{k}))
= f^{C}((k ∘ h)^{s_{1}}a_{1}, …, (k ∘ h)^{s_{k}}a_{k}).

The first equation is just the definition of the composition k ∘ h, and after that we use the fact that h is a homomorphism, and then that k is a homomorphism.

Exercise 3.5.7. Assume that there is a surjective homomorphism h from A to B. Then define the relation ∼ on A as a_{1} ∼ a_{2} iff h(a_{1}) = h(a_{2}). We first show that ∼ is a congruence. The relation ∼ is an equivalence by the corresponding properties of equality. Moreover, suppose we have f: s_{1} × … × s_{k} → s, and elements a_{1}, …, a_{k}, b_{1}, …, b_{k} such that a_{i} ∼ b_{i}. Then,

h(f^{A}(a_{1}, …, a_{k})) = f^{B}(h(a_{1}), …, h(a_{k}))
= f^{B}(h(b_{1}), …, h(b_{k}))
= h(f^{A}(b_{1}, …, b_{k}))

where in the above, the first equation just follows from the fact that h is a homomorphism, and the second equation follows from the fact that a_{i} ∼ b_{i} implies that h(a_{i}) = h(b_{i}). Hence, from the above equation we have that f^{A}(a_{1}, …, a_{k}) ∼ f^{A}(b_{1}, …, b_{k}). With this ∼, which we have shown to be a congruence, define a map i: A/∼ → B by i([a]_{∼}) = h(a). Note that i is well-defined, since if [a] = [b], then by the definition of ∼, h(a) = h(b). Also i is a homomorphism, since for any function symbol f: s_{1} × … × s_{k} → s of Σ, we have that

i(f^{A/∼}([a_{1}]_{∼}, …, [a_{k}]_{∼})) = i([f^{A}(a_{1}, …, a_{k})]_{∼})
= h(f^{A}(a_{1}, …, a_{k}))
= f^{B}(h(a_{1}), …, h(a_{k}))
= f^{B}(i([a_{1}]_{∼}), …, i([a_{k}]_{∼}))

The first equation in the above is just the definition of the algebra A/∼. After that, we use the definition of i, and then the fact that h is a homomorphism. Now, i is surjective, since h is surjective. And, i is injective, because if i([a]_{∼}) = i([b]_{∼}), then h(a) = h(b), i.e. a ∼ b, or in other words, [a]_{∼} = [b]_{∼}. Hence i is a bijective homomorphism from A/∼ to B. Therefore, with this relation ∼, A/∼ is isomorphic to B.

For the other way, assume that for some congruence relation ∼, A/∼ is isomorphic to B. Let i be the bijective homomorphism from A/∼ to B. Now, define the map h: A → B by h(a) = i([a]_{∼}). Then, h is a homomorphism, since for any function symbol f: s_{1} × … × s_{k} → s of Σ, we have that

h(f^{A}(a_{1}, …, a_{k})) = i([f^{A}(a_{1}, …, a_{k})]_{∼})
= i(f^{A/∼}([a_{1}]_{∼}, …, [a_{k}]_{∼}))
= f^{B}(i([a_{1}]_{∼}), …, i([a_{k}]_{∼}))
= f^{B}(h(a_{1}), …, h(a_{k}))

The first equation in the above is just the definition of h. After that, we use the definition of the algebra A/∼, and then, the fact that i is a homomorphism, and finally the definition of h again. Thus, h is a homomorphism. Moreover, because i is surjective, h is surjective as well. Thus, there exists a surjective homomorphism from A to B.

Finally, we note that any algebra is isomorphic to itself and hence A/∼ is isomorphic to A/∼, for any congruence ∼ on A. Hence, taking B to be A/∼ in the result we have just shown, we have that there is a surjective homomorphism from A to A/∼. Therefore, from Exercise 3.5.6, Th(A) ⊆ Th(A/∼).

Exercise 3.5.15. The first part of this problem asks you to show that there is more than one homomorphism from A_{2} → A_{1} . However, this is incorrect. In fact, there is no homomorphism from A_{2} → A_{1} . (If, instead of an extra copy of the positive and negative numbers, we just had an extra copy of the natural numbers, then I believe there would be more than one homomorphism.)

There is no homomorphism A_{3} → A_{1} . This is easiest to write out if we assume the modulus k is greater than 1. This is easiest to see by contradition. Assume h: A_{3} → A_{1} is a homomorphism and consider h([k − 1] + [k − 1]). We can see that h([0]) = 0, since the homomorphism property of h requires h([n]) = h([0] + [n]) = h([0]) + h([n]) for all n. It follows from h(S[n]) = S(h[n]) that for 0 ≤ n < k, we have h([n]) = n. Now for the contradiction. Since we assume h is a homomorphism, we must have h([k − 1] + [1]) = h([k]) = 0 and, at the same time, h([k − 1] + [1]) = h([k − 1]) + h([1]) = (k − 1) + 1 = k. Since this is a contradiction, there can be no homomorphism h: A_{3} → A_{1} .

Exercise 3.5.16.

(a) We may show by induction on q that every equation of the form S^{p}0 + S^{q}0 = S^{p+q}0 or S^{p}0 ∗ S^{q}0 = S^{pq}0 is provable, for all natural numbers p and q. Then we solve the problem by induction on the structure of M. If M is 0,then it is already of the form S^{k}0. Assume that P = S^{p}0 and Q = S^{q}0 have already been proven. If M is SP, then M = S^{p+1}0. If M is P + Q, then M = S^{p}0 + S^{q}0 = S^{p+q}0. Finally, if M is P ∗ Q, then M = S^{p}0 ∗ S^{q}0 = S^{pq}0.

(b) Since each variable-free term is provably equal to a term of the form S^{k}0, we know that each equivalence class contains at least one such term. Now assume that some class contained two distinct such terms; thus we can prove S^{k}0 = S^{ℓ}0 for some k and ℓ. But the set of natural numbers, with zero, successor, addition, and multiplication, is an algebra for this specification, and no such equation holds in it; this contradicts the Soundness theorem, so there must be exactly one such term in each equivalence class.

(c) From parts (a) and (b) we know that the carrier of sort nat in the initial algebra Terms(Σ_{2}, ∅)/ ∼_{E,∅} is the set of equivalence classes {[0], [S0], [S(S0)], …}, and that the interpretation of 0 is [0], while the functions behave as S[S^{k}0] = [S^{k+1}0], [S^{k}0] + [S^{ℓ}0] = [S^{k+ℓ}0], and [S^{k}0] ∗ [S^{ℓ}0] = [s^{kℓ}0]. Thus the initial algebra is isomorphic to the algebra of natural numbers described above.

(d) Given an equation E, with free variables x_{1} … x_{n}, we may successively generate all the possible environments for the algebra of natural numbers (which we observed in part (c) is initial) — for example, by first exhausting the single environment where the sum of the values of each of the free variables is 0, then the n environments where the sum is 1, and so on (fans of combinatorics can continue the sequence if they wish). For each environment we may compute the meaning of each side of the equation; if we ever reach an environment where the two sides have different meanings, then we halt with the answer “no”. If the equation is true, this procedure will never halt, hence the test for equations holding in the initial algebra is co-r.e.

Exercise 3.6.2. If union(s, s′) = union(s′, s) [s: set, s′: set] holds in the initial algebra, then it should hold for the ground instance where s = insert(0, empty) and s′ = insert(1, empty). But

union(insert(0, empty), insert(1, empty)) = insert(0, insert(1, empty)), while

union(insert(1, empty), insert(0, empty)) = insert(1, insert(0, empty)).

With respect to the rewrite system obtained by directing the axioms these are distinct normal forms, so since the rewrite system is assumed to be confluent the two unions must not be equivalent. Hence the equation does not hold in the initial algebra.

If we add it as an axiom, it will allow us to prove that two terms that differ only in the order of insertion of atoms are equivalent, thus making the elements of the initial algebra more like sets (note that while they aren’t ordered any more, they are still more like multisets in that insert(0, insert(0, empty)) and insert(0, empty) are in distinct equivalence classes).

If we add union(s, s′) → union(s′, s) as a reduction rule, we lose both confluence and termination. Using the above example, we find that union(s, s′) → → insert(0, insert(1, empty)) and union(s, s′) → union(s′, s) → → insert(1, insert(0, empty)), which shows that it is not confluent. Termination fails simply because union(s, s′) → union(s′, s) → union(s, s′) → ….

(alternate 3.6.2 solution) Notice that an example of an algebra for this specification is lists of natural numbers: empty is nil, insert is cons, union is append, and ismem? tests whether a given natural number is in the list. Since insert(0, insert(1, empty)) and insert(1, insert(0, empty)) are distinct lists, these two ground terms must not be provably equal. Therefore these terms must be in separate equivalence classes in the initial algebra. Now, consider the terms

union(insert(0, empty), insert(1, empty)) and union(insert(1, empty), insert(0, empty))

We can prove that these are respectively equal to the first two terms, hence they must also be in separate equivalence classes in the initial algebra. Thus we have an instance of union(s, s′) = union(s′, s) which does not hold in the initial algebra, so the equation itself must not hold.

We may also use the assumption given in the problem, that the rewrite rules obtained from the equational axioms are confluent. Then since

union(insert(0, empty), insert(1, empty)) → → insert(0, insert(1, empty)) union(insert(1, empty), insert(0, empty)) → → insert(1, insert(0, empty))

and these are distinct normal forms, the two terms must not be provably equal.

Exercise 3.6.4.

(a) The specification should include at least the following:

sorts: nat, bool, tree
fctns: 0, 1, 2, …: nat

true, false: bool leaf : nat → tree node: tree × tree → tree is leaf ?: tree → bool label: tree → nat lsub, rsub: tree → tree

eqns: x: nat; t_{1}, t_{2}: tree

is leaf ?(leaf (x)) = true is leaf ?(node(t_{1}, t_{2})) = false label(leaf (x)) = x label(node(t_{1}, t_{2})) = 0 lsub(leaf (x)) = leaf (x) lsub(node(t_{1}, t_{2})) = t_{1} rsub(leaf (x)) = leaf (x) rsub(node(t_{1}, t_{2})) = t_{2}.

The equations for the label of a node and the subtrees of a leaf are arbitrary, but without making some sort of definition for those “error” cases the second part of the problem won’t work. One could also add some extra functions such as +, Eq?, and conditionals for each sort, but these are not needed for the problem.

We now show that every tree in the initial algebra is named by leaf (n) or node(t_{1}, t_{2}), where n is a numeral and t_{1}, t_{2} are trees of the desired form, by induction. To do that we need to have a stronger induction hypothesis — namely, we have to prove by induction on the structure of a term M, that if M is of sort nat , then it is provably equal to n for some numeral n; if M is of sort bool , then it is provably equal to true or false ; and if M is of sort tree , then it is provably equal to leaf (n) or node(t_{1}, t_{2}), where n is a numeral and t_{1}, t_{2} are trees of the desired form. We just discuss some steps in the induction. If we have leaf (N), where N is a term of sort nat ; this is easily equivalent to a term of the desired form (since we have by induction hypothesis that N is equivalent to a numeral). Now, if t_{1} and t_{2} are terms of sort tree that have already been shown equivalent to terms of the desired form, then obviously node(t_{1}, t_{2}) is equivalent to such a term. If we have shown that t = leaf (n) for some numeral n, then lsub(t) = rsub(t) = leaf (n), while if we have shown that t = node(t_{1}, t_{2}), then lsub(t) = t_{1} and rsub(t) = t_{2} , which are of the correct form. If we have shown that t = leaf (n) for some numeral n, then label(t) = n, numeral; while if we have shown that t = node(t_{1}, t_{2}), then label(t) = 0, which is also a numeral.

(b) One possible translation is

letrec f(t: tree): σ = if is leaf ?(t)

then let x: nat = label(t) in M

else let ⟨t_{1}: tree, t_{2}: tree⟩ = ⟨lsub(t), rsub(t)⟩ in N

                   in P.

Note that since the ML definition had the effect of binding x in M and t_{1}, t_{2} in N to the appropriate functions of t, we must do the same.

(c) Choose T_{1} ≡ leaf (n) and T_{2} ≡ node(leaf (n), leaf (n)); then with the axiom lsub(leaf (n)) = T_{1} we can prove that the PCF_{tree} expression is leaf ?(lsub(leaf (n))) is equivalent to true, while with the axiom lsub(leaf (n)) = T_{2} we can prove that it is equivalent to false.

Using the translation from the pattern matching syntax of ML we cannot get a function which applies lsub to leaf — the translation only allows lsub to be applied to arguments that are not leaves (as verified by the is leaf? test).

Exercise 3.6.7.

(a) Guttag’s statement that “error is a distinguished value with the property that the value of any operation applied to an argument list containing error is error” could be formalized with the following axioms:

is empty? error = error add error i = error add q error = error

This produces an inconsistent theory, for much the same reason as the list theory in the text. For example, we have

error = front (add error i) = i [i: item]

the first equation from the new error axioms, and the second from the original specification. Similarly,

error = remove (add q error) = q [q: queue] error = is empty? (add error i) = false error = is empty? (remove (add new error)) = true

(b) For each sort s, as outlined in the text, add a function OK_{s}: s → bool which tells whether its argument is error_{s} or not. Then write axioms to say which elements are OK , and use conditional to test for error values in equations. For the queue specification, add function symbol OK_{i} and axioms

OK_{i} a = true, OK_{i} b = true, …, OK_{i} error_{i} = false

to make every non-error item “OK ” and the error item not. You need similar axioms to make the non-error queues OK:

OK_{i} new = true OK (add q i) = if OK_{i} i then (if OK_{q} q then true else false) else false [q: queue, i: item]

(This is written using if … then … else … as syntactic sugar for cond.)

We then use OK_{q} and conditional to revise the axiom for front of a nonempty list as follows.

front(add q i) = if OK_{i} i then (if OK_{q} q then i else error_{i}) else error_{i} [q: queue, i: item]

The revised versions of is empty? (add q i) = false and remove (add q i) = q are similar.

These axioms, the revised axioms you just wrote, not the ones for part (a), plus the axioms you did not change (the first, third and fifth ones of the specification) may be shown consistent by finding a model. For example, you may interpret queues as finite sequences, plus an error queue, items and natural numbers, plus an error item, and booleans as true , false and error_{b}. The OK function should give value true on all non-error elements of the appropriate sort, and so on.

Exercise 3.7.3.

(a) The subterm at occurrence (2,1,2) is h(u, v).

(b) The subterm g(x, y) occurs at (1) and (2,2). Exercise 3.7.18. Similar to Example 3.7.16. Exercise 3.7.20. Let each carrier consist of all natural numbers greater than 2. Interpret each constant as 3, functions +, Eq? and insert as sum plus 1, and ismem^{A}(x, s) = union^{A}(x, s) = xs. For part (b), use card^{A}(s) = s^{2} . Exercise 3.7.24. (* expand answer *) There are two critical pairs. The first one, obtained by unifying 0 + x with x + y in (x + y) + z, is convergent. The second one, obtained by unifying (−x) + x with x + y in (x + y) + z, is not. The term ((−x) + x) + y reduces to both 0 + y and (−x) + (x + y). (See Plaisted AI and Log Programming Handbook chapter, page 31, section 11.4. I beleive this is also example 1 of Kunth-Bendix.) Exercise 3.7.25. We have the following critical pairs:

• ⟨¬x, ¬x⟩, unifying (1) into (1);

• ⟨(x ∨ y), ¬(¬x ∧ ¬y)⟩, unifying (2) into (1);

• ⟨(x ∧ y), ¬(¬x ∨ ¬y)⟩, unifying (3) into (1);

• ⟨(¬x ∨ ¬(y ∨ z)), ¬((x ∧ y) ∨ (x ∧ z))⟩, unifying (4) into (3);

• ⟨(¬(y ∨ z) ∨ ¬x), ¬((y ∧ x) ∨ (z ∧ x))⟩, unifying (5) into (3);

• ⟨((v ∧ (y ∨ z)) ∨ (w ∧ (y ∨ z))), (((v ∨ w) ∧ y) ∨ ((v ∨ w) ∧ z))⟩, unifying (4) into (5); and • ⟨(((v ∨ w) ∧ y) ∨ ((v ∨ w) ∧ z)), ((v ∧ (y ∨ z)) ∨ (w ∧ (y ∨ z)))⟩, unifying (5) into (4).

Chapter 4

Exercise 4.1.1. Consider the term M ≡ (λx. not(xx))(λx. not(xx)). With one β -reduction, we get

M = not((λx. not(xx))(λx. not(xx)))

i.e., M = not M. Thus, if M is equal to false, then it is equal to true and conversely. Exercise 4.3.10. (a)

(var) y: σ → τ ▷ y : σ → τ  (8)
(add var, 1) x: σ, y: σ → τ ▷ y : σ → τ  (9)
(var) x: σ ▷ x : σ  (10)
(add var, 3) x: σ, y: σ → τ ▷ x : σ  (11)
(→ Elim, 2, 4) x: σ, y: σ → τ ▷ yx : τ  (12)

(b)

(→ Intro, 5) x: σ ▷ λy: σ → τ. yx : (σ → τ) → τ  (13)
(add var, 6) x: σ, y: σ ▷ λy: σ → τ. yx : (σ → τ) → τ  (14)

(c)

(var) x: σ → σ ▷ x : σ → σ  (15)
(add var, 8) x: σ → σ, y: τ ▷ x : σ → σ  (16)
(→ Intro, 9) x: σ → σ ▷ λy: τ. x : τ → σ → σ  (17)
(→ Intro, 10) ∅ ▷ λx: σ → σ. λy: τ. x : (σ → σ) → τ → σ → σ  (18)
(var) x: σ ▷ x : σ  (19)
(→ Intro, 12) ∅ ▷ λx: σ. x : σ → σ  (20)
(→ Elim, 11, 13) ∅ ▷ (λx: σ → σ. λy: τ. x)(λx: σ. x) : τ → σ → σ.  (21)

Exercise 4.3.15.

(a) λx: a. x.

(b) λx: a → b. λy: c. x.

(c) λx: a → b. λy: b → c. λz: a. y(xz).

Exercise 4.3.16.

(a) For any implicational formula ϕ → ψ, we will call ϕ the antecedent and ψ the consequent. In classical logic, any implicational formula is true if its antecedent is false or its consequent is true. If a is true, then the given implicational formula is true by virtue of its consequent being true. Otherwise, a is false, in which case a → b is true and a is false, making the antecedent (a → b) → a false, thus making the whole implicational formula true.

(b) First we prove the general lemma that every normal form is of the form

λx_{1}: σ_{1}. λx_{2}: σ_{2}…. λx_{k}: σ_{k}. hN_{1} … N_{ℓ},

where h (the “head”) is either a constant or a variable, and each subterm N_{i} is a normal form. We prove it by induction on the formation of terms. Obviously a constant or a variable is a normal form of this form, where k = ℓ = 0. A lambda abstraction λx: σ. M will be a normal form if M is; hence if M is of the desired form then the whole term will be. An application MN will be a normal form only if M and N are, and if M isn’t a lambda abstraction, i.e., M must be a constant, variable, or application; if M and N are of the desired form, then the whole term will be. This completes the induction.

The above characterization of normal forms implies that a closed normal form of type ((a → b) → a) → a must have the form λf: (a → b) → a. M where M must be a normal form of type a and can only have f free. Since M is of type a, it cannot be a λ-abstraction, hence it must be of the form fN, where N is a normal form of type a → b with only f free. Continuing similarly, N must have the form λx: a. P, where P must be a normal form of type b with only f: (a → b) → a, x: a free. Since P is of type b, it cannot be a λ-abstraction. It thus has to be of the form fQ or x. It cannot be either, since the resulting type would then be a.

Thus, we have shown that there is no closed normal form term of type ((a → b) → a) → a, whence it follows that there is no closed term of that type.

Exercise 4.5.5. First we show that if A is an extensional applicative structure, then there is an isomorphic type frame B. It will be sufficient to construct a family of sets {B^{σ}} and, for each type expression σ, a bijection h_{σ}: A^{σ} → B^{σ}; for each type expression σ → τ, the set B^{σ → τ} must be a subset of the functions from B^{σ} to B^{τ}. The definition of the type frame B may then be completed by specifying that App_{B}^{σ,τ} f d = f(d) and Const_{B}(c) = h_{σ}(Const_{A}(c)), for each constant c of type σ in Σ.

We proceed by induction on types. For a base type σ, we let B^{σ} = A^{σ} and take h_{σ} to be the identity function; this is obviously a bijection. Now, suppose we have the sets B^{σ} and B^{τ}, and the bijections h_{σ} and h_{τ}, for some type expressions σ and τ. For each element f of A^{σ → τ}, we define the function h(f): B^{σ} → B^{τ} by specifying that h(f)(x) = h_{τ} (App_{A}^{σ,τ} f h_{σ}^{−1}(x)), for each x ∈ B^{σ}. Because A is extensional and h_{σ} and h_{τ} are bijections, we know that if h(f) = h(g) then f = g; therefore, h gives us a bijection h_{σ → τ} if we take B^{σ → τ} = h(A^{σ → τ}).

Now we show that if an applicative structure A is isomorphic to a type frame B, then it is extensional. That is, for every f and g in A^{σ → τ}, if App_{A}^{σ,τ} f d = App_{A}^{σ,τ} g d for all d ∈ A^{σ}, then f = g. So assume the antecedent is true for some f and g. We have a bijection h_{σ}: A^{σ} → B^{σ}, for each type expression σ, so App_{A}^{σ,τ} f d = h_{τ}^{−1}(h_{σ → τ} (f)(h_{σ}(d))), and similarly for g. Now, since h_{τ}^{−1} is injective and h_{σ} is surjective, this means that h_{σ → τ} (f)(x) = h_{σ → τ} (g)(x) for every x in B^{σ}. Because B^{σ → τ} is a collection of actual functions from B^{σ} to B^{τ}, this implies that h_{σ → τ} (f) = h_{σ → τ} (g). Finally, since h_{σ → τ} is injective, we have shown that f = g, as desired.

Exercise 4.5.11.

(a) The meaning of ∅ ▷ λf: b → b. λx: b. f(fx) : (b → b) →(b → b) in this model will be “the unique g ∈ A^{(b → b) →(b → b)} such that for all f ∈ A^{b → b}, g(f) is the unique function h ∈ A^{b → b} such that for all x ∈ A^{b}, h(x) is f(fx).” That is, g is the function which takes two arguments, f and x, and returns f(fx).

(b) Let the elements f_{1}, f_{2}, f_{3}, f_{4} of A^{b → b} be given by the following table:

\begin{matrix}f & f(0) & f(1) \\ f_{1} & 0 & 0 \\ f_{2} & 0 & 1 \\ f_{3} & 1 & 0 \\ f_{4} & 1 & 1. \end{matrix}

Then our function g is specified by g(f_{1}) = f_{1} , g(f_{2}) = f_{2} , g(f_{3}) = f_{2} , and g(f_{4}) = f_{4} .

(c) First we prove the general lemma that every normal form is of the form

λx_{1}: σ_{1}. λx_{2}: σ_{2}…. λx_{k}: σ_{k}. hN_{1} … N_{ℓ},

where h (the “head”) is either a constant or a variable, and each subterm N_{i} is a normal form. We prove it by induction on the formation of terms. Obviously a constant or a variable is a normal form of this form, where k = ℓ = 0. A lambda abstraction λx: σ. M will be a normal form if M is; hence if M is of the desired form then the whole term will be. An application MN will be a normal form only if M and N are, and if M isn’t a lambda abstraction, i.e., M must be a constant, variable, or application; if M and N are of the desired form, then the whole term will be. This completes the induction.

Now, as suggested in the problem statement, we note that every term has a normal form, so to enumerate the elements of a given type which are the meaning of a closed term, we only need to consider the meanings of the closed normal forms. Since there are no term constants, the head of each normal form must be a variable; in a closed normal form this must then be one of the variables x_{1} … x_{k} bound by the lambdas.

There are no closed normal forms of type b, since to get a bound variable to use as the head we need at least one lambda, which means the type of a closed normal form in our signature must be a function.

At type b → b, a closed normal form must look like λx: b. M, where M is a normal form of type b with at most x as a free variable. Since there are no closed normal forms of type b, the only choice for M is x itself; hence the only element of A^{b → b} which is the meaning of a closed term is the function called f_{2} (the identity function) in part (b).

Finally, at type (b → b) →(b → b), a normal form must look like λf: b → b. M, where M is a normal form of type b → b with at most f as a free variable. If M is not a lambda abstraction, the only choice is M ≡ f, which gives us the identity function for type b → b. Otherwise, M is of the form λx: b. N, where N is a normal form of type b (hence it is either a variable or an application), perhaps containing f and x. Thus either N ≡ x, or N ≡ fN′; where the choices for N′ are the same as those for N; hence N ≡ f^{n}x, for any n ≥ 0. (There is a slight technicality here in that if n = 1, we get the term λf: b → b. λx: b. fx, which reduces by (η) to λf: b → b. f. In fact, the above lemma gives us β -normal forms; to get βη-normal forms, there would have to be an extra condition that the innermost lambda abstraction is not an η-redex, i.e., it’s not of the form λx: σ. Nx, with x not free in N. This would only have clouded up what I’m trying to make as clear a presentation as possible, and doesn’t really change the results because it is also true that every term has a unique β -normal form.) We may show, by reasoning similar to that in parts (a) and (b), that λf: b → b. λx: b. f^{n}x is the identity function for type b → b whenever n is odd; for n even and greater than 0, it is always the function found in part (a); and for n = 0, it is the constant function which returns the element f_{2} of A^{b → b}. Hence there are three elements of A^{(b → b) →(b → b)} which are the meaning of a closed term:

\begin{matrix}F & F (f_{1}) & F (f_{2}) & F (f_{3}) & F (f_{4}) \\ g & f_{1} & f_{2} & f_{2} & f_{4} \\ id_{b → b} & f_{1} & f_{2} & f_{3} & f_{4} \\ K_{f_{2}} & f_{2} & f_{2} & f_{2} & f_{2}. \end{matrix}

Exercise 4.5.25. Prove the equation λx: null. λy: σ. λz: σ. y = λx: null. λy: σ. λz: σ. z and use (nonempty) to obtain λy: σ. λz: σ. y = λy: σ. λz: σ. z from x: null ▷ λy: σ. λz: σ. y = λy: σ. λz: σ. z : σ → σ → σ.

Chapter 5

Exercise 5.2.3. First, suppose that < is transitive, and consider two elements x and y of D such that x ≤ y and y ≤ x. Now, if x ≠ y, then by the definition of < we have that x < y and y < x. Since < is transitive, this means that x < x, which implies in part that x ≠ x; this is a contradiction, so we must have that x = y — hence ≤ is antisymmetric.

Now suppose that ≤ is antisymmetric, and take elements x, y, and z of D such that x < y and y < z. By the definition of <, this means that x ≤ y and y ≤ z; thus, since ≤ is transitive, we find that x ≤ z. Suppose that x = z: then we also have that z ≤ y, hence by antisymmetry we know y = z, which contradicts the fact that y < z. Therefore, x ≤ z and x ≠ z, so x < z and < must be transitive.

Exercise 5.2.4.

(a) • Reflexivity : Any sequence is clearly an initial segment of itself.

• Transitivity : If sequence s_{1} is an initial segment of s_{2} , and s_{2} is an initial segment of s_{3} , then clearly s_{1} is an initial segment of s_{3} .

• Antisymmetry : Suppose s_{1} ≤_{prefix} s_{2} and s_{2} ≤_{prefix} s_{1} . Since s_{1} ≤_{prefix} s_{2} , s_{2} = s_{1} s′ where s′ is some sequence. But, since s_{2} ≤_{prefix} s_{1} , we have s_{1} = s_{2} s′′ for some sequence s′′ i.e. s_{1} = s_{1} s′ s′′, which means that s′ s′′ must be the empty sequence, i.e. s′ = ε. But then s_{1} = s_{2} .

(b) S^{∗} and S^{∞} have a least element, namely the empty sequence ε. If a, b are distinct elements in S, then for any s ∈ S^{+} , if s ≠ a then s ≰_{prefix} a; otherwise s = a, and s ≰_{prefix} b. Hence, S^{+} does not have a least element.

(c) Suppose s_{1} and s_{2} have an upper bound, say s′. Then, s_{1} ≤_{prefix} s′ and s_{2} ≤_{prefix} s′ i.e.s′ = s_{1} e_{1} and s′ = s_{2} e_{2} for some sequences e_{1} and e_{2} . Then s_{1} e_{1} = s_{2} e_{2} ; hence, s_{1} is an initial segment of s_{2} or s_{2} is an initial segment of s_{1} i.e.s_{1} ≤_{prefix} s_{2} or s_{2} ≤_{prefix} s_{1} . From this we can conclude that the directed sets in all three partial orders are simply chains i.e. if D is a directed set and s_{1}, s_{2} ∈ D, then s_{1} ≤_{prefix} s_{2} or s_{2} ≤_{prefix} s_{1} , since s_{1} and s_{2} have an upper bound (in fact, in D). Moreover, note that this automatically ensures that every finite subset of D has an upper bound in D since the longest sequence in the finite subset would be an upper bound for the subset.

(d) S^{∗} and S^{+} are not cpo’s. To see this, consider the directed set :

D = { a^{n} | n ≥ 1 } for some a ∈ S.

Then D has no upper bound in S^{∗} and S^{+} . For, consider any s in either of the two cpos. Then s being a finite sequence, has a finite length |s|. But then s ≰_{prefix} a^{|s|+1} ∈ D. Hence, since D does not have an upper bound, its least upper bound does not exist either.

S^{∞} is a cpo. Suppose D is a directed set. Then ⋁ D = s, where the sequence s is defined as : the nth element of s is the nth element of any sequence s′ ∈ D, such that |s′| ≥ n, if there exists such an s′. Then s is well-defined by our characterization of directed sets in (c) and is clearly an element of S^{∞}.

Exercise 5.2.5.

(a) According to the definition, a subset S of P is directed if every finite S_{0} ⊆ S has an upper bound in S. An equivalent condition is that S be non-empty (i.e., S must contain an upper bound for the empty set, which is always a finite subset of S), and for every pair of elements x and y of S, there is an upper bound z in S (i.e., x ≤ z and y ≤ z). For the set P of partial functions on N, ordered by set inclusion, we note that h is an upper bound for f and g iff f ∪ g ⊆ h; this requires that f and g be consistent, i.e., that for any x in the domain of both f and g, f(x) = g(x). Therefore, the directed subsets of P are the nonempty sets S of pairwise consistent functions such that for any f, g ∈ S, there is an h ∈ S which contains f ∪ g.

(b) Here are a couple of examples:

S = {{⟨0, i⟩} | i ∈ N }
T = {{⟨i, i⟩} | i ∈ N }

The set S fails to be directed because no pair of functions in S is consistent — each maps 0 to a different value. All the pairs of functions in T are consistent (indeed, T has the identity function in P as the least upper bound), but T contains no upper bounds for pairs of functions itself.

(c) Let f be the union of all the functions in a directed set S. We need to show that f is itself a function in P, and that it is the least upper bound of S. To the first part, suppose that ⟨x, y⟩ and ⟨x, y′⟩ are both in f; since f is a union, there must be functions g and g′ (not necessarily distinct) in S such that ⟨x, y⟩ ∈ g and ⟨x, y′⟩ ∈ g′. Now, since S is directed, we know that g and g′ must be consistent, so y = y′; this establishes that f is a partial function. To the second part, f is an upper bound for S because for every g ∈ S, g ⊆ f. If h is another upper bound for S, then g ⊆ h for every g ∈ S, hence f = ⋃{g | g ∈ S} ⊆ h, so f is the least upper bound.

Exercise 5.2.7. Consider the set S = {⟨true, ⊥⟩, ⟨⊥, true⟩} which is not directed since the finite subset S has no upper bound in S. However, Proj_{1}S = Proj_{2}S = {⊥, true} which is directed.

Exercise 5.2.13. A useful lemma for both parts is that if a set S has an upper bound x that is in S, then x is the least upper bound of S: if y is another upper bound for S, then since x ∈ S, x ≤ y.

(a) Since we are given that ⟨P, ≤⟩ has a least element, we only need to show that every directed subset S of P has a least upper bound. Since S is directed, we know that every finite subset of S has an upper bound in S; since ⟨P, ≤⟩ is essentially flat, S must itself be a finite subset of S, so by the lemma S has a least upper bound. Thus ⟨P, ≤⟩ is a cpo.

(b) We have to show that, for every directed subset S of P, f(⋁ S) = ⋁ f(S). Since ⟨P, ≤⟩ is essentially flat, S must be finite and so by the definition of a directed set and the lemma we know that S has a least upper bound x ∈ S. Now, for any d ∈ S, we have d ≤ x, hence, by the monotonicity of f, we have f(d) ≤ f(x). Therefore, f(x) = f(⋁ S) is an upper bound for f(S), and by the lemma it must be the least upper bound, so we are done.

Exercise 5.2.12. We begin by characterizing least upper bounds in the cpo [x, y] as limits of a certain form. For any S ⊆ [x, y], define a to be an ϵ-limit of S if a is an upper bound of S (i.e., for all r ∈ S, r ≤ a) and for every ϵ > 0, S ∩ (a − ϵ, a] ≠ ∅ (i.e., every left-open neighbourhood of a intersects S).

Observation 1 Let S ⊆ [x, y] and a ∈ [x, y]. Then a is an ϵ-limit of S iff a = ⋁ S.

Proof (⇒) Let a be an ϵ-limit of S; then by definition of ϵ-limit, a is an upper bound of S. Suppose

that a is not a least-upper bound, i.e., we have b ∈ [x, y] such that b is an upper bound for S but a ≰ b. Then b < a and hence ϵ = (b − a) > 0. And, since b is an upper bound for S, we have that S ∩ (a − ϵ, a] = ∅ which is a contradiction.

(⇐) Let a be the least upper bound of S and suppose that a is not an ϵ-limit. Then, there is an ϵ > 0, such that S ∩ (a − ϵ, a] = ∅. This implies that for b = a − ϵ, we have that b is an upper bound of S and a ≰ b (since ϵ > 0), which contradicts the fact that a is a least upper bound.

We are now ready to show that any f that is monotonic and ϵ, δ-continuous is cpo-continuous. Recall that a function f: [x, y] →[x, y] is said to be ϵ, δ-continuous at a point a ∈ [x, y] if for every ϵ > 0 there is a δ > 0 such that

∀r ∈ [x, y]. |r − a| < δ ⊃ |f(r) − f(a)| < ϵ

and f is said to be ϵ, δ-continuous if it is continuous at every a ∈ [x, y]. Suppose that f: [x, y] →[x, y] is ϵ, δ-continuous and monotonic; we show that f is cpo-continuous . Consider any set S ⊆ [x, y] and let a = ⋁ S. By Observation 1, it suffices to show that f(a) is an ϵ-limit for the set f(S). Consider any ϵ > 0. Since f is continuous at a, there is a δ > 0 such that ∀r ∈ [x, y]. |r − a| < δ ⊃ |f(r) − f(a)| < ϵ. By Observation 1, for the δ > 0, we have some b ∈ S ∩ (a − δ, a]. Then, by monotonicty and ϵ, δ-continuity of f, f(b) ∈ (f(a) − ϵ, f(a)], and since f(b) ∈ f(S), we have that f(S) ∩ (f(a) − ϵ, f(a)] ≠ ∅.

To show that the converse fails, consider any a, b, c ∈ [x, y] such that b < c. Define the step function at a, δ_{a}^{b,c}: [x, y] →[x, y] as

δ_{a}^{b,c}(r) = \{ \begin{matrix}b & if r ≤ a \\ c & otherwise \end{matrix}

Then δ_{a}^{b,c} is cpo-continuous as follows. Consider any S ⊆ [x, y]. If S ⊆ [x, a] then ⋁ S ≤ a and hence δ_{a}^{b,c}(⋁ S) = b which is ⋁ δ_{a}^{b,c}(S) since δ_{a}^{b,c}(S) = {b}. Otherwise there is an r ∈ S such that r > a. Then {c} ⊆ δ_{a}^{b,c}(S) ⊆ {b, c} and thus ⋁ δ_{a}^{b,c}(S) = c (since b < c). And, ⋁ S > r > a; hence δ_{a}^{b,c}(⋁ S) = c. Clearly, δ_{a}^{b,c} is not ϵ, δ-continuous at a, where for any ϵ ≤ (c − b), we do not have a δ satisfying the required property.

Exercise 5.2.19. Let por: B_{⊥} →(B_{⊥} → B_{⊥}) be defined by

por(⊥) = f_{1}
por(true) = f_{9}
por(false) = f_{7}

Then, it can be easily seen that the above function satisfies the given equations. Also, since f_{1} ≤ f_{9} and f_{1} ≤ f_{7} , por is monotone and hence continuous, since B_{⊥} is finite.

Exercise 5.2.28. The least element of B_{⊥} → B_{⊥} is the function ⊥_{B_{⊥} → B_{⊥}} given by ⊥_{B_{⊥} → B_{⊥}} (x) =⊥_{B_{⊥}} ∀x ∈ B_{⊥}. Then, we have

f^{0}(⊥) = ⊥
f^{1}(⊥) = \{ \begin{matrix}⊥ & ↦ & ⊥ \\ true & ↦ & true \\ false & ↦ & ⊥ \end{matrix}

f^{2}(⊥) = \{ \begin{matrix}⊥ & ↦ & ⋀\{f^{1}(true), f^{1}(false)\} \\ true & ↦ & true \\ false & ↦ & f^{1}(true) \end{matrix}

= \{ \begin{matrix}⊥ & ↦ & ⊥ \\ true & ↦ & true \\ false & ↦ & true \end{matrix}

f^{3}(⊥) = \{ \begin{matrix}⊥ & ↦ & true \\ true & ↦ & true \\ false & ↦ & true \end{matrix}

Now, f^{3}(⊥) = f^{4}(⊥) = · · ·. Hence,

fix f = ⋁{f^{0}(⊥), f^{1}(⊥), …}
= f^{3}(⊥)
= \{ \begin{matrix}⊥ & ↦ & true \\ true & ↦ & true \\ false & ↦ & true \end{matrix}

Exercise 5.2.29.

Observation 2 If f(s) = s_{1} s, where s_{1} is some sequence, then f is continuous.

Proof

• f is monotonic : Suppose s ≤_{prefix} s′. Then, s is an initial segment of s′. Hence, s_{1} s is an initial segment of s_{1} s′, i.e. f(s) ≤_{prefix} f(s′).

• f is continuous : Let D be a directed set. From monotonicity, it suffices to show that f(⋁ D) is least among the upper bounds for f(D). Suppose u is an upper bound. Now, f(D) = {s_{1} d | d ∈ D}. Hence, s_{1} d ≤_{prefix} u∀d ∈ D. But then u must be of the form s_{1} u′ for some sequence u′, such that d ≤_{prefix} u′ ∀d ∈ D. Hence,

⋁ D  ≤_{prefix} u′
⇒ s_{1} ⋁ D ≤_{prefix} s_{1} u′
⇒ f(⋁ D) ≤_{prefix} u

Observation 3 Suppose h: S → S^{+} is some substitution function. Then, h^{+}: S^{∞} → S^{∞} defined by h^{+}(s) = s′, where s′ is obtained by replacing every element in s by h(s), is continuous.

Proof

• h^{+} is monotonic : Suppose s_{1} ≤_{prefix} s_{2} . Then, it can be seen that h^{+}(s_{1}) ≤_{prefix} h^{+}(s_{2}).

• h^{+} is continuous : Let D be a directed set. From monotonicity, it suffices to show that h^{+}(⋁ D) is least among the upper bounds for h^{+}(D). Suppose u is an upper bound for h^{+}(D). Then, h^{+}(d) ≤_{prefix} u∀d ∈ D. But, then u has to be of the form h^{+}(s) u′ for some sequences s and u′ such that h^{+}(d) ≤_{prefix} h^{+}(s)∀d ∈ D. Then,

d ≤_{prefix} s  ∀d ∈ D
⇒ ⋁ D ≤_{prefix} s
⇒ h^{+}(⋁ D) ≤_{prefix} h^{+}(s) (by monotonicity)
⇒ h^{+}(⋁ D) ≤_{prefix} u

(a) f is continuous by Observation 2. For the least fixed point, it can be seen by induction on i

that

f^{i}(ε) = (ab)^{i}

Hence, the least fixed point of f is the sequence given by

\begin{aligned}& ⋁\{ (ab)^{i} | i ≥ 0 \} \\ = & ababab … \end{aligned}

(b) Consider any directed set D. Then, if we take h: S → S^{+} given by h(a) = b, h(b) = b, we

have

f(⋁ D) = abab h^{+}(⋁ D)
= abab ⋁ h^{+}(D) (Observation 3)
= ⋁ abab h^{+}(D) (Observation 2)
= ⋁ f(D).

Hence, f is continuous.

For the least fixed point, it can be seen by induction on i that

f^{i+1}(ε) = abab b^{4i} ∀i ≥ 0

And, f^{0}(ε) = ε. Hence, the least fixed point is the sequence ababbbbbbbbb . . ..

(c) f is continuous by an identical argument to that given in (b). Now, again by induction on

i, it can be seen that

f^{i+1}(ε) = a ab^{1} ab^{2} … ab^{i} ∀i ≥ 0.

And, f^{0}(ε) = ε. Hence, the least fixed point is the sequence aababbabbb . . ..

Exercise 5.2.30. Recall that the least upperbound of any directed set in PN, is its union.

(a) Let D be any directed set. Then,

F (⋁ D) = F (⋃ D)
= A_{0} ∪ {f(n) | n ∈ ⋃ D}
= A_{0} ∪ {f(n) | n ∈ A for some A ∈ D}
= A_{0} ∪ ⋃_{A∈D}{f(n) | n ∈ A}
= ⋃_{A∈D}(A_{0} ∪ {f(n) | n ∈ A})
= ⋁ F (D)

(b) (i) By induction on i, it can be seen that

F^{i}(∅) = {2^{n} | 1 ≤ n ≤ i}

Hence the least fixed point is the set {2^{n} | n ≥ 1}.

(ii) Let us denote the primes by p_{1}, p_{2}, … with p_{1} = 1 being considered a prime i.e. p_{i} is the ith prime starting with 1. Then, it can be seen by induction on i that

F^{i}(∅) = {p_{k} | k ≤ i}

Hence, the least fixed point of F is the set of all primes, with 1 being included in the set.

(c) Let D be any directed set. We will first show that

⋃_{A∈D}{A′ | A′ ⊆ A finite } = {A′ | A′ ⊆ ⋃ D finite }  (22)

(⊆) Consider any A ∈ D, A′ ⊆ A. Since A ⊆ ⋃ D, we have that A′ ⊆ ⋃ D.

(⊇) Consider any finite A′ ⊆ ⋃ D. Let A′ = {a_{1}, …, a_{k}}. Since A′ ⊆ ⋃ D, there exist A_{1}, …, A_{k} ∈ D with a_{i} ∈ A_{i}, i = 1, …, k. Now, {A_{i} | 1 ≤ i ≤ k} is a finite subset of the directed set D which must therefore have an upper bound A ∈ D. Then A_{i} ⊆ A, 1 ≤ i ≤ k, and hence a_{i} ∈ A. Thus, ∃A ∈ D. A′ ⊆ A.

Now, using Equation 22

F (⋁ D) = F (⋃ D)
= A_{0} ∪ {f(A′) | A′ ⊆ ⋃ D finite }
= A_{0} ∪ ⋃_{A∈D}{f(A′) | A′ ⊆ A finite }
= ⋃_{A∈D}(A_{0} ∪ {f(A′) | A′ ⊆ A finite })
= ⋁ F (D)

(d) (i) Taking f(∅) = 0, we can prove that

⋃_{n} F^{n}(∅) = {2j | j ≥ 0}

(⊆) Trivially, by induction on n, we can show that F^{n}(∅) ⊆ {2j | j ≥ 0}. (⊇) Clearly, 0, 2 ∈ F (∅) and since F is monotonic, it follows that 2 ∈ F^{n}(∅) for every

n ≥ 1. Now, we can prove by induction on n that 2(n + 1) ∈ F^{n}(∅), for all n ≥ 1.

Thus the least fixed point of F is {2j | j ≥ 0}, i.e., the set of all even numbers.

(ii) Taking f(∅) = 1, we can prove that

⋃_{n} F^{n}(∅) = {1, 3, 5, 7} ∪ M

where

M = {3^{i}5^{j}7^{k} | at least two of i, j, k ≠ 0 }

(⊆) Trivially, by induction on n, F^{n}(∅) ⊆ {1, 3, 5, 7} ∪ M.

(⊇) Clearly, {1, 3, 5, 7} ⊆ F^{1}(∅) ⊆ F^{2}(∅) ⊆ . . .. And, if 3^{i}5^{j}7^{k} ∈ M, we can prove by

induction on i + j + k that 3^{i}5^{j}7^{k} ∈ F^{i+j+k}(∅).

Thus the least fixed point of F is {1, 3, 5, 7} ∪ M, i.e., the set containing 1, 3, 5, 7 and all multiples of 15, 21, 35.

Exercise 5.2.31.

(a) Suppose that S ⊆ D is a directed set of pre-fixed-points of f. Then f(⋁ S) = ⋁ f(S) by continuity. But since each element f(x) of f(S) is ≤ x ∈ S, we have ⋁ f(S) ≤ ⋁ S. This shows that the least upper bound of a directed set of pre-fixed-point is a pre-fixed-point.

(b) Show that if f(x) ≤ x, then for each n, we have f^{n}(⊥) ≤ x. It follows that fix f = ⋁_{n} f^{n}(⊥ ) ≤ x.

Exercise 5.2.17.

(⇒) Assume the function f: D_{1} × … × D_{n} → E is continuous. Consider the unary function f_{i}: D_{i} → E defined by taking fixed values d_{j} ∈ D_{j}, 1 ≤ j ≤ n, j ≠ i and taking

f_{i}(x) = f⟨d_{1}, …, d_{i−1}, x, d_{i+1}, …, d_{n}⟩

We have to show that f_{i} is continuous. Consider any directed set S_{i} ⊆ D_{i}. Then the set S = {⟨d_{1}, …, d_{i−1}, y, d_{i+1}, …, d_{n}⟩ | y ∈ S_{i}} is a directed subset of D_{1} × … × D_{n}.

Hence,  f(⋁ S) = ⋁ f(S)
Now,  ⋁ S = ⟨d_{1}, …, d_{i−1}, ⋁ S_{i}, d_{i+1}, …, d_{n}⟩
And,  ⋁ f(S) = ⋁{f(s) | s ∈ S}
= ⋁{f⟨d_{1}, …, d_{i−1}, y, d_{i+1}, …, d_{n}⟩ | y ∈ S_{i}}
= ⋁{f_{i}(y) | y ∈ S_{i}}
= ⋁ f_{i}(S_{i})
Thus,  f(⋁ S) = ⋁ f(S)
⇒  f⟨d_{1}, …, d_{i−1}, ⋁ S_{i}, d_{i+1}, …, d_{n}⟩ = ⋁ f_{i}(S_{i})
⇒  f_{i}(⋁ S_{i}) = ⋁ f_{i}(S_{i})

(⇐) Suppose we have a function f: D_{1} × … × D_{n} → E such that ∀i, 1 ≤ i ≤ n, we have that ∀d_{j} ∈ D_{j}, 1 ≤ j ≤ n, j ≠ i, f_{i}: D_{i} → E defined by f_{i}(x) = f⟨d_{1}, …, d_{i−1}, x, d_{i+1}, …, d_{n}⟩ is continuous. Then, consider any directed S ⊆ D_{1} × … × D_{n}. If S_{i} = Proj_{i}S, then S_{i} ⊆ D_{i} is directed and ⋁ S = ⟨⋁ S_{1}, …, ⋁ S_{n}⟩. Hence,

f(⋁ S) = f⟨⋁ S_{1}, …, ⋁ S_{n}⟩
= f_{1}(S_{1})withd_{j} = ⋁ S_{j} j ≥ 2
= ⋁ f_{1}(S_{1})
= ⋁ f⟨S_{1}, ⋁ S_{2}, …, ⋁ S_{n}⟩
⋮
= ⋁{f⟨d_{1}, …, d_{n}⟩ | d_{i} ∈ S_{i}}
= ⋁ f(S)

The last equality can be seen as follows. Since {⟨d_{1}, …, d_{n}⟩ | d_{i} ∈ S_{i}} ⊇ S, we have ⋁{f⟨d_{1}, …, d_{n}⟩ | d_{i} ∈ S_{i}} ≥ ⋁ f(S). To see the other inequality, we can show that any upper bound for the set f(S) is an upper bound for {f⟨d_{1}, …, d_{n}⟩ | d_{i} ∈ S_{i}}.

Exercise 5.2.18.

(a) Let S ⊆ D and T ⊆ E be directed. Consider P = {⟨s, t⟩ | s ∈ S, t ∈ T } ⊆ D × E, which is a directed set. Moreover, by Lemma 5.2.2, ⋁ P = ⟨⋁ Proj_{1}P, ⋁ Proj_{2}P ⟩ = ⟨⋁ S, ⋁ T ⟩, and we have the desired result.

(c) Let S ⊆ D → E and T ⊆ D be directed. Since, D → E is the set of continuous functions, note that any f: d → E ∈ S is continuous. Hence,

(⋁ S)(⋁ T) = ⋁(S(⋁ T))  (by Lemma 5.2.10)
= ⋁{f(⋁ T) | f ∈ S}
= ⋁{⋁ f(T) | f ∈ S}  (f ∈ Sis continuous)
= ⋁{f(x) | f ∈ S, x ∈ T }

Exercise 5.2.39.

(a) F ≡ (λf: nat → nat. λx: nat.(f x) + 1), so take F̄ = A[[F]]; we note that F̄(⊥) is the unique function g: N_{⊥} → N_{⊥} such that for every x ∈ N_{⊥},

g(x) =⊥_{nat → nat} (x) + 1 =⊥_{nat} +1 =⊥_{nat};

hence F̄(⊥) =⊥. Therefore, the directed set {F̄^{n}(⊥) | n ≥ 0} is just the singleton set {⊥}; its least upper bound, and hence the meaning of the fixed point of F, is the nowhere terminating function ⊥_{nat → nat} .

(b) F ≡ (λf: nat → nat. λx: nat. if Eq? x 0 then 1 else f(x − 1) + f(x − 1)), so again take F̄ = A[[F]]. Consider the function g_{n}: N_{⊥} → N_{⊥} such that

g_{n}(x) = \{ \begin{matrix}2^{x} & x < n \\ ⊥_{nat} & otherwise \end{matrix} ;

thus g_{0} =⊥, and F̄(g_{n}) = g_{n+1} . Therefore, the directed set {F̄^{n}(⊥) | n ≥ 0} is the set {g_{n} | n ≥ 0}, so the fixed point of F is the lifting of the function g: x ↦ 2^{x}.

Exercise 5.2.40. As in part (a) of the Exercise 5.2.39, we find that

A[[λf: nat → nat. λx: nat. if Eq? x 0 then 1 else f x]](⊥_{nat → nat})
= x ↦ if Eq? x 0 then 1 else ⊥_{nat → nat} (x)
= x ↦ if Eq? x 0 then 1 else ⊥_{nat}
= x ↦⊥_{nat}
=⊥_{nat → nat};

hence the fixed point will be the nowhere defined function. But according to the reduction rules (and hence according to the equational proof system),

fix(λf: nat → nat. λx: nat. if Eq? x 0 then 1 else f x) 0 → → if Eq? 0 0 then 1 else (fix …) 0 → → 1.

This corresponds to the meaning assigned to the fixed point if we take the non-strict interpretation — then we get the function whose value is 1 for argument 0, and ⊥ otherwise (and indeed, the reduction rules will never terminate if the fixed point is applied to anything other than 0).

Exercise 5.2.41. The function total? is not even monotonic. For example, consider f: x ↦⊥_{nat} and g: x ↦ 0. We have f ≤ g, but total? f = false ≰ true = total? g. Since continuity requires monotonicity, total? cannot be continuous. Since every PCF expression defines a continuous function, total? cannot be definable in PCF.

Exercise 5.2.42.

(a) Take A^{tree} to be the set of expressions generated by the following (infinite) grammar:

t : : = leaf (⊥_{nat}) | leaf (0) | leaf (1) | leaf (2) | ⋯ | node(t, t)

i.e., A^{tree} consists of binary trees whose leaves are numerals or ⊥_{nat} . Define the cpo A^{tree} = ⟨A^{tree}, ≤_{tree}⟩ with the elements of A^{tree} ordered as follows:

(1) leaf (⊥_{nat}) ≤_{tree} leaf (n), for any natural number n ∈ N.

(2) node(t_{1}, t_{2}) ≤_{tree} node(t′_{1}, t′_{2}) iff t_{1} ≤_{tree} t′_{1} and t_{2} ≤_{tree} t′_{2} .

Intuitively, a tree t_{1} is an approximation to another tree t_{2} if t_{1} possesses the same treestructure as t_{2} but may contain as leaves, ⊥_{nat} , at positions where t_{2} contains a numeral. Thus, if trees t_{1}, t_{2} have an upper bound, then they have to possess the same tree-structure. Thus, all trees in a directed set possess the same tree-structure, thereby making any directed set finite (at most of size 2^{n}, where n is the number of leaves of any element of the directed set). By Exercise 5.2.13, A^{tree} is thus a cpo. Note that A^{tree} is not pointed. The required continuous interpretation of the function symbols is then as follows:

A[[leaf ]](x) = leaf (x), for any x ∈ A^{nat}

A[[node]](t_{1}, t_{2}) = node(t_{1}, t_{2})

A[[lsub]](leaf (x)) = leaf (x) A[[lsub]](node(t_{1}, t_{2})) = t_{1}

A[[rsub]](leaf (x)) = leaf (x) A[[rsub]](node(t_{1}, t_{2})) = t_{2}

A[[label]](leaf (x)) = x

A[[label]](node(t_{1}, t_{2})) =⊥_{nat} (can be any arbitrary element of A^{nat})

A[[is leaf ?]](leaf (x)) = true A[[is leaf ?]](node(t_{1}, t_{2})) = false

Then all the above are well-defined functions on their respective domains. Continuity just follows from their monotonicity (which can be trivially verified) since there are no infinite directed sets in any of the cpo’s (recall Exercise 5.2.13).

(b) The equations are all easily seen to be satisfied, given our interpretation of the function symbols and the domains.

(c)

F =^{def} λf: tree → nat. λt: tree. if is leaf ? t then label t else f(lsub t) + f(rsub t),

Then, if F̄ = A[[F]], we have

F̄^{0}(⊥) = ⊥_{tree → nat}
F̄^{1}(⊥) = λt: tree. if is leaf ? t then label t else ⊥_{nat}
F̄^{2}(⊥) = λt: tree. if is leaf ? t then label t else

(if is leaf ? (lsubt) then label(lsubt) else ⊥_{nat})+ (if is leaf ? (rsubt) then label(rsubt) else ⊥_{nat})

= t ↦ \{ \begin{matrix}sum of labels at the leaves of \\ t if t is of depth < 2. \\ ⊥ otherwise \end{matrix}

In general,

F̄^{i}(⊥) = t ↦ \{ \begin{matrix}sum of labels at the leaves of \\ t if t is of depth < i. \\ ⊥ otherwise \end{matrix}

Hence, the least fixed point is the function

g: t ↦ sum of labels at the leaves of t

Exercise 5.2.43.

(a) Suppose A is a cpo model of PCF^{−eq} with A^{nat} finite. To simplify notation, we will write n for both the natural number n and the numeral (symbol) for n. If A^{nat} has n elements, then consider the first n + 1 numerals, 0, 1, …, n. The list of the meanings, A[[0]], …, A[[n]], of these numerals contains n + 1 elements of A^{nat}. Therefore, by the “pigeonhole principle,” there must be two distinct numerals, m_{1} and m_{2} , such that A[[m_{1}]] = A[[m_{2}]].

(b) Let A be a cpo model of PCF^{−eq} with A^{nat} finite and suppose there is a closed term EQ: nat → nat → bool defining equality. By assumption, EQ must have the following properties:

A ⊧ EQ n n = true for any numeral n,
A ⊧ EQ n m = false for distinct numerals n, m.

By part (a), we know there exist distincts numerals n and m such that A ⊧ n = m. For these particular numerals, it follows that A ⊧ EQ n n = EQ n m. Therefore, A ⊧ true = false.

(c) We first describe a model with A^{nat} finite, as suggested in the problem statement. Let A be the cpo model for PCF^{−eq} with

(i) A^{nat} = {0, 1}_{⊥}, the flat cpo obtained by lifting the set {0, 1},

(ii) A^{bool} = B_{⊥} = {true, false}_{⊥}, the flat cpo of booleans,

(iii) A[[0]] = 0 and A[[n]] = 1 for any numeral n different from 0,

(iv) A[[true]] = true and A[[false]] = false as usual, (v) + interpreted as the following function:

n +^{A} m = \{ \begin{matrix}0 & if both m and n are 0 \\ 1 & if n, m ∈ \{0, 1\} are not both 0 \\ ⊥_{nat} & otherwise (m or n is ⊥_{nat}) \end{matrix}

It is clear that +^{A} is monotonic, and therefore continuous since all directed sets are finite (recall Exercise 5.2.13).

It is easy to check that A satisfies all of the equational axioms for PCF^{−eq}. Since the only possible problem would be with the addition axioms, we will check these. Since numeral 0 has meaning 0 ∈ A^{nat},

A[[0 + 0]] = A[[0]] +^{A} A[[0]] = 0 +^{A} 0 = 0 = A[[0]].

Thus A ⊧ 0 + 0 = 0. If numeral n or m is not 0, the axiom requires that n + m = k, where k is a numeral different from 0. This is satisfied since

A[[n + m]] = A[[n]] +^{A} A[[m]] = 1 = A[[k]].

We may now use the model A to show that equality is not definable. Suppose closed term EQ defines equality. By part (b), it follows that A ⊧ true = false. But this leads to a contradiction, since A^{bool} = B_{⊥} and

A[[true]] = true ≠ false = A[[false]].

Therefore, equality must not be definable. The reader may easily check that the same argument applies if we let A^{nat} = {0}_{⊥}. However, we will need 0 ≠ 1 ∈ A^{nat} for part (d) below.

(d) The main idea is to extend the model A from part (c) with a continuous interpretation of the zero-test function. Extending the argument of part (c) to PCF^{−eq+zerop}, we show that equality is not definable. We then prove that equality is definable from predecessor, which implies that predecessor is not definable.

In this solution, we sketch the extension of the model A from part (c) to PCF^{−eq+zerop} and show how equality is definable from predecessor. We extend A by interpreting Zero? as follows:

Zero?^{A} n = \{ \begin{matrix}true & if n = 0 ∈ A^{nat}, \\ false & if n = 1 ∈ A^{nat}, \\ ⊥_{bool} & if n = ⊥_{nat} ∈ A^{nat}. \end{matrix}

It is easy to check that Zero?^{A} is continuous, using the fact that all directed subsets of A^{nat} are finite. It is also straightforward to verify that this modified model A satisfies the axioms of PCF^{−eq+zerop}:

A[[Zero? 0]] = Zero?^{A} A[[0]] = Zero?^{A}0 = A[[true]]

and for any numeral n different from 0,

A[[Zero? n]] = Zero?^{A} A[[n]] = Zero?^{A}1 = A[[false]].

It follows from the argument given in part (c) that equality is not definable in PCF^{−eq+zerop}. It remains to be shown that EQ is definable from a predecessor operation, Pred , and test for zero, Zero?. We demonstrate this directly by writing the definition of equality in PCF^{−eq+zerop}.

EQ =^{def} letrec f⟨n:nat, m:nat⟩:bool =

if Zero? n then Zero? m elseif Zero? m then false

else f⟨(Pred n), (Pred m)⟩

                            in f

Intuitively, the function f checks to see if one argument is zero and the other not. If both are nonzero, then the function is called recursively on the predecessors. This gives the correct answer since two numbers are equal iff both become zero after applying predecessor the same number of times.

Exercise 5.3.3.

(b) Let

A ≡ g: nat → nat ▷ g =⊥: nat → nat

By reflexivity, we can prove [⊥ /x]A. Now, suppose we have

[c/g]A ≡ ▷ c =⊥: nat → nat

as hypothesis. Then, if F ≡ λf: nat → nat. λx: nat. f(x + 1), we will prove [F c/g]A. By (β), we have

F c = λx: nat. c (x + 1)

Now applying congruence rules to our hypothesis c = ⊥, we will get

λx: nat. c (x + 1) = λx: nat. ⊥ (x + 1)

Using the axiom (botf )( twice along with (β) and (cong) we will get

λx: nat. ⊥ (x + 1) = ⊥

Thus using (trans), we finally get

[c/g]A ⊢ [F (c)/g]A

Now, using (fpind) we get

fix F = ⊥  (23)

Using [c/g]A as hypothesis, in an exactly similar way, we can prove

(λf: nat → nat. f) c = ⊥

i.e.,

[c/g]A ⊢ [(λf: nat → nat. f) c/g]A  (24)

Thus, using (fpind) with Equation 24, we get

fix(λf: nat → nat. f) = ⊥  (25)

From Equation 23 and Equation 25, using (sym) and (trans), we derive the desired equation.

(c) Let

A ≡ g: nat → nat → nat ▷ (g x y) + 1 = g x (y + 1) :

Now using (botf ) and (β) we can derive

(⊥ x y) + 1 = ⊥  (26)
⊥ x (y + 1) = ∗ ⊥  (27)

Hence, from Equations 26 and 27 we can get [⊥ /g]A.

Now, suppose we have [c/g]A as hypothesis, i.e.

(c x y) + 1 = c x (y + 1)  (28)

Now, using (β) and (cong), we can derive that

((F c) x y) + 1 = (if Eq? x 0 then y else c(x − 1, y + 1)) + 1

Using the distributivity of application over conditional expressions mentioned in the statement of the problem, we get

((F c) x y) + 1 = if Eq? x 0 then y + 1 else c (x − 1) (y + 1) + 1

Using the hypothesis Equation 28 and (cong) rules, we will get

((F c) x y) + 1 = if Eq? x 0 then y + 1 else c (x − 1) ((y + 1) + 1)  (29)

Using (β) and (cong) we can derive that

(F c) x (y + 1) = if Eq? x 0 then y + 1 else c (x − 1) ((y + 1) + 1)  (30)

Thus, from Equation 29 and Equation 30, using (trans) and (sym) we get [F c/g]A. Thus, using (fpind), we get the desired equation now.

Exercise 5.4.6. Suppose M → →^{left} N M. By Theorem 5.2.35, [[M]]η = [[N M]]η, i.e., [[M]]η = [[N]]η([[M]]η) which means that [[M]]η is a fixed point of [[N]]η. Since [[fix N]]η is the least fixed point it is immediate that [[M]]η ≤ [[fix N]]η for any environment η. Thus, to prove [[M]]η = [[fix N]]η it suffices to show that [[fix N]]η ≤ [[M]]η, which we’ll prove by analysing the meanings of the approximate normal forms obtained by leftmost reduction from M.

Let us use the notation M ⇝^{⊥} A to mean that A is a normal form obtained by replacing one or more subterms of M by ⊥. A useful observation is that leftmost reduction always produces better approximations. More precisely, if M → →^{left} N and M ⇝^{⊥} A, then there is some way of replacing subterms of N by ⊥ to get a normal form A′ which is at least as good an approximation as A. However, this property cannot be proved by induction; we therefore prove a stronger condition by induction in Lemma 11.4.1 below and obtain the desired property as Corollary 11.4.2.

Lemma 11.4.1 Suppose that M →^{left} M′ and M ⇝^{⊥} A. Then there is a normal form A′ such that

M′ ⇝^{⊥} A′ and

(i) For any environment η, [[A]]η ≤ [[A′]]η (ii) If A′ is a numeral, true , false , λ-abstraction, or a pair then so is A.

Proof By induction on the length of the proof of M →^{left} M′ according to the proof system of Table 2.3.

If M →^{left} M′ is an axiom, then M → M′ is a reduction axiom. By examining the form of M for each of the reduction axioms, we can see that if M ⇝^{⊥} A then [[A]]η = ⊥ and we can therefore take A′ to be ⊥ and satisfy conditions (i) and (ii). For example, if M ≡ (λx: σ. M_{1}) M_{2} , then we note that A cannot be of the form (λx: σ. A_{1}) A_{2} where M_{1} ⇝^{⊥} A_{1}, M_{2} ⇝^{⊥} A_{2} since A would then not be a normal form. Hence A is either ⊥ or ⊥ A_{2} where M_{2} ⇝^{⊥} A_{2} . In either case [[A]]η = ⊥.

The inductive step is proved by case analysis of the last rule used. We can see the necessity of condition (ii) by considering the case when the last step in the proof is

\frac{M_{1} →^{left} M′_{1}}{M_{1} M_{2} →^{left} M′_{1} M_{2}}

with M ≡ M_{1} M_{2} , M′ ≡ M′_{1} M_{2} . Suppose that M ⇝^{⊥} A. If A ≡ ⊥ then we take A′ ≡ ⊥. Otherwise, A ≡ A_{1} A_{2} with M_{1} ⇝^{⊥} A_{1}, M_{2} ⇝^{⊥} A_{2} . By induction hypothesis, we have A′_{1} with M′_{1} ⇝^{⊥} A′_{1} satisfying conditions (i) and (ii). We take A′ to be A′_{1} A_{2} . Clearly, A′ can be obtained by replacing subterms of M′ by ⊥; however, we need to check that A′ is in normal form. If A′_{1} is a λ-abstraction, then so is A_{1} (by condition (ii)) which would mean that A cannot be in normal form. Hence, A′_{1} is not a λ-abstraction and A′_{1}, A_{2} are in normal form which implies that A′ is a normal form term. And, from condition (i) for A′_{1} , we immediately get that [[A]]η ≤ [[A′]]η for any environment η. Condition (ii) is satisfied vacuously since A′ is not one of the five forms. The proof for all other inference rules is similar.

Corollary 11.4.2 If M → →^{left} M′ and M ⇝^{⊥} A then there is a normal form A′ such that M′ ⇝^{⊥} A′ and [[A]]η ≤ [[A′]]η for any environment η.

Using Corollary 11.4.2, we can now establish the following:

Proposition 11.4.3 Let N be a normal form term that is not a λ-abstraction. If M → →^{left} N M then there is a k ∈ N such that if M ⇝^{⊥} A then [[A]]η ≤ [[N^{k}⊥]]η for any environment η.

Proof By induction on the structure of M. If M is a variable, then we clearly cannot have M → →^{left} N M and the statement is satisfied vacuously. If M is a λ-abstraction or a pair, then every term that M reduces to is a λ-abstraction or a pair respectively (because of the absence of η-reduction, and (sp)-reduction in PCF), and hence we again cannot have that M → →^{left} N M. Similarly, if M is fix , M_{1} + M_{2} , or Eq? M_{1} M_{2} we can easily see that the statement is satisfied vacuously since none of these terms can reduce to an application. If M ≡ if M_{1} then M_{2} else M_{3} and M → →^{left} N M then we must have that M_{1} → →^{left} true and M_{2} → →^{left} N M, or M_{1} → →^{left} false and M_{3} → →^{left} N M. In the former case, M → →^{left} M_{2} and hence M_{2} → →^{left} N M → →^{left} N M_{2} since N is in normal form and not a λabstraction. By induction hypothesis applied to term M_{2} and using Corollary 11.4.2 applied to the fact that M → →^{left} M_{2} we have the statement of the proposition for M. The case when M_{1} → →^{left} false is similar.

This leaves us with the cases when M is a projection or application which are the most interesting. Suppose that M ≡ Proj_{i}M_{1} and M → →^{left} N M. Then it must be that M_{1} → →^{left} ⟨P_{1}, P_{2}⟩ and P_{i} → →^{left} N M. We can easily see that if Proj_{i}⟨P_{1}, P_{2}⟩ ⇝^{⊥} A then A has to be one of the terms ⊥ or Proj_{i}⊥; in either case [[A]]η = ⊥. Since M → →^{left} Proj_{i}⟨P_{1}, P_{2}⟩, it follows from Corollary 11.4.2, that if M ⇝^{⊥} A then [[A]]η ≤ ⊥ and we can take k = 0. Finally, suppose that M ≡ M_{1} M_{2} and M → →^{left} N M. Then, we have two possibilities for the leftmost reduction of M to N M. We can either have that (i) M_{1} → →^{left} λx: σ. M′ and [M_{2}/x]M′ → →^{left} N M, or (ii) M_{1} → →^{left} N and M_{2} → →^{left} M. In case (i), we can see that the meaning of any approximate normal form obtained from the term (λx: σ. M′) M_{2} is ⊥ and since M → →^{left} (λx: σ. M′) M_{2} , by an argument similar to the projection case we can take k = 0. For case (ii), we have that M_{2} → →^{left} M_{1} M_{2} → →^{left} N M_{2} and hence by the induction hypothesis applied to M_{2} we have a k_{2} satisfying the conditions of the proposition. Consider any A such that M ⇝^{⊥} A. Then either A is the term ⊥ or A_{1} A_{2} with M_{1} ⇝^{⊥} A_{1}, M_{2} ⇝^{⊥} A_{2} . Clearly [[A_{1}]]η ≤ [[M_{1}]]η and since M_{1} → →^{left} N we have that [[M_{1}]]η = [[N]]η. And, by induction hypothesis, [[A_{2}]]η ≤ [[N^{k_{2}} ⊥]]η. We can thus take k = k_{2} + 1 and satisfy the statement of the proposition for M. Now, suppose that N is a normal form and not a λ-abstraction and M → →^{left} N M. Since N is a normal form and not a λ-abstraction, we have that

M → →^{left} N M → →^{left} N (N M) → →^{left} ⋯ N^{i}(M) → →^{left} ⋯

Clearly, if N^{i}(M) ⇝^{⊥} A then [[A]]η ≤ [[N^{i}(A′)]]η for some M ⇝^{⊥} A′. By Proposition 11.4.3, [[A′]] ≤ [[N^{k}(⊥)]]η for some k, and thus [[A]] ≤ [[N^{k+i}(⊥)]]η. Because of the form of the leftmost reduction from M, we have that if M → →^{left} M′ then M′ → →^{left} N^{i}(M) for some i. Hence, by Corollary 11.4.2, if M → →^{left} M′ and M′ ⇝^{⊥} A, we have that [[A]]η ≤ [[N^{k}(⊥)]]η for some k. It therefore follows that ⋁[[lanf (M)]]η ≤ ⋁{[[N^{k}(⊥)]]η | k ≥ 0}. Since the term on the lefthand side is just [[M]]η and the one on the righthand side is [[fix N]]η, we have that [[M]]η ≤ [[fix N]]η.

Exercise 5.5.8. It is not true that if f: N → N is recursive, then f: N_{1} → N_{2} is recursive on all modest sets N_{1} and N_{2} with underlying set N. For example, let f and e_{2} , the partial enumeration function for the modest set N_{2} , be the identity. Then f: N_{1} → N_{2} is recursive iff there is some recursive g: N ⇀ N with

∀n, m ∈ N . e_{1}(n) = m ⊃ e_{2}(g(n)) = g(n) = f(m) = m.

In other words, the identity is recursive iff e_{1} is recursive. But there is no reason why e_{1} should be recursive. For example, the function

e_{1}(n) = \{ \begin{matrix}0 & if n ∉ K \\ |\{ x | x ∈ K and x < n \}| + 1 & otherwise \end{matrix}

where K = { x | ϕ_{x}(x) ↓ }, is a total surjective function that is not recursive.

Exercise 5.5.9. We assume that for any total recursive function f and natural number a, we can compute some n ∈ |f(a)| from any m ∈ |f| and i ∈ |a|. In other words, there is some recursive function App of two arguments such that for any m ∈ |f| and i ∈ |a|, App(m, i) ↓ and App(m, i) ∈ |f(a)|. By the s-m-n theorem, it follows that there is a recursive function ψ mapping m to λi. App(m, i). Since i ∈ |a| iff i = a, this means for any total recursive f and m ∈ |f|, ψ(m) is an index for f.

Suppose there is a modest set ⟨T ot, e_{tot}⟩ with T ot the set of all total recursive functions and e_{tot} a total surjective function. Since e_{tot} is total and surjective, every natural number m is the code for some total recursive function f. Therefore, { ψ(m) | m ∈ N } is a recursively enumerable set containing at least one index for every total recursive function. Since this is impossible, e_{tot} cannot be total.

Exercise 5.5.12.

(a) Successor may be interpreted as the usual successor function. Zero test may be interpreted as the function mapping 0 ↦ 1 and every nonzero argument to 0. It is essentially straightforward to check that these satisfy the equational axioms.

(b) By the s-m-n theorem, it suffices to show that given indices for functions g and h and natural number n, we can compute an index for prim g h n satisfying the equational axiom. This is most easily accomplished by induction on n.

(c) The easiest counterexample is σ = nat . Since the successor function has no fixed point (over the natural numbers), there is no acceptable interpretation for fix_{nat} .

Exercise 5.6.9. The first axiom in the exercise is equivalent to (K · x) · y = x, since every x ∈ D is “defined.” The second axiom in the exercise does not guarantee (S · x) · y ↓ for all x, y ∈ D, but is equivalent to the third axiom in the definition in the text.

Chapter 6

Exercise 6.2.1. The variables q and r must be assignable, so we will take them to be of type loc. The other two variables, m and n, are never assigned to, so for simplicity we will take them to be of type nat. The rewritten program is then

q := 0; r := m; while (cont r) ≥ n do

q := (cont q) + 1; r := (cont r) − n;

          od.

This program will put the quotient of m and n in q, and the remainder in r.

Exercise 6.2.2. The variables r, m and n are assignable, so we will take them to be of type loc. The rewritten program is then

while (cont n) ≠ 0 do r: = (cont m); while (cont r) ≥ (cont n) do

r: = (cont r) − (cont n);

                od

m: = (cont n); n: = (cont r);

          od

Exercise 6.2.3. x := (cont y) + 1; while (cont x) ≠ (cont y) do

x := cont x;

      od.

Exercise 6.3.2.

\frac{⟨M, s⟩ ⇝^{eval} true, ⟨L_{1}, s⟩ ⇝^{eval} ℓ}{⟨if M then L_{1} else L_{2}, s⟩ ⇝^{eval} ℓ}

\frac{⟨M, s⟩ ⇝^{eval} false, ⟨L_{2}, s⟩ ⇝^{eval} ℓ}{⟨if M then L_{1} else L_{2}, s⟩ ⇝^{eval} ℓ}

\frac{⟨L, s⟩ ⇝^{eval} ℓ, ⟨M, s⟩ ⇝^{eval} v}{⟨L := M, s⟩ ⇝^{exec} update^{A} s ℓ v.}

Exercise 6.3.3. (a)

\frac{⟨M, s⟩ ⇝^{eval} v}{⟨x := M, s⟩ ↦^{exec} update^{A} s η(x) v}

(b)

\frac{⟨P_{1}, s⟩ ↦^{exec} s′}{⟨P_{1}; P_{2}, s⟩ ↦^{exec} ⟨P_{2}, s′⟩}

(c)

\frac{⟨B, s⟩ ⇝^{eval} true}{⟨if B then P_{1} else P_{2}, s⟩ ↦^{exec} ⟨P_{1}, s⟩}

\frac{⟨B, s⟩ ⇝^{eval} false}{⟨if B then P_{1} else P_{2}, s⟩ ↦^{exec} ⟨P_{2}, s⟩}

(d)

\frac{⟨B, s⟩ ⇝^{eval} false}{⟨while B do P od, s⟩ ↦^{exec} s}

\frac{⟨B, s⟩ ⇝^{eval} true}{⟨while B do P od, s⟩ ↦^{exec} ⟨P; while B do P od, s⟩}

(e)

⟨x := 3; y := (cont x) + 3, s⟩
↦^{exec} ⟨y := (cont x) + 3, s′⟩
↦^{exec} s′′.

where s′ = update^{A} s η(x) 3, s′′ = update^{A} s′ η(y) 6.

(f) Let s be a store. Define stores s_{n} for n ∈ N by s_{0} = update^{A} s η(y) 0 and s_{i+1} = update^{A} s_{i} η(y) (i + 1). Then, we note the following:

\begin{matrix}& ⟨y := 0; while cont y ≠ x do y := (cont y) + 1 od, s⟩ \\ ↦^{exec} & ⟨while cont y ≠ x do y := (cont y) + 1 od, s_{0}⟩ \end{matrix} \} (a1)

If i < η(x) then

\begin{matrix}& ⟨while cont y ≠ x do y := (cont y) + 1 od, s_{i}⟩ \\ ↦^{exec} & ⟨y := (cont y) + 1; while cont y ≠ x do y := (cont y) + 1 od, s_{i}⟩ \\ ↦^{exec} & ⟨while cont y ≠ x do y := (cont y) + 1 od, s_{i+1}⟩ \end{matrix} \} (a2)

For i = η(x)

\begin{matrix}& ⟨while cont y ≠ x do y := (cont y) + 1 od, s_{i}⟩ \\ ↦^{exec} & s_{i} \end{matrix} \} (a3)

Thus, if η(x) = k, the execution of the program initially involves a sequence of the form (a1) (1 step), followed by sequences of the form (a2) (2 steps) for i = 0, …, k − 1, and finally (a3) (1 step), for a total of 1 + 2k + 1 = 2k + 2 steps.

Exercise 6.3.4. (a)

\frac{⟨P_{1}, s⟩ ↦^{exec} s′}{⟨P_{1} ∪ P_{2}, s⟩ ↦^{exec} s′}  \frac{⟨P_{2}, s⟩ ↦^{exec} s′}{⟨P_{1} ∪ P_{2}, s⟩ ↦^{exec} s′}
\frac{⟨P_{1}, s⟩ ↦^{exec} ⟨P′_{1}, s′⟩}{⟨P_{1} ∪ P_{2}, s⟩ ↦^{exec} ⟨P′_{1}, s′⟩} \frac{⟨P_{1}, s⟩ ↦^{exec} ⟨P′_{2}, s′⟩}{⟨P_{1} ∪ P_{2}, s⟩ ↦^{exec} ⟨P′_{2}, s′⟩}

(b)

\frac{⟨P_{1}, s⟩ ↦^{exec} s′}{⟨P_{1} ∥ P_{2}, s⟩ ↦^{exec} ⟨P_{2}, s′⟩}  \frac{⟨P_{2}, s⟩ ↦^{exec} s′}{⟨P_{1} ∥ P_{2}, s⟩ ↦^{exec} ⟨P_{1}, s′⟩}
\frac{⟨P_{1}, s⟩ ↦^{exec} ⟨P′_{1}, s′⟩}{⟨P_{1} ∥ P_{2}, s⟩ ↦^{exec} ⟨P′_{1} ∥ P_{2}, s′⟩} \frac{⟨P_{1}, s⟩ ↦^{exec} ⟨P′_{2}, s′⟩}{⟨P_{1} ∥ P_{2}, s⟩ ↦^{exec} ⟨P_{1} ∥ P′_{2}, s′⟩}

————————– add explicit lifting ————————- Exercise 6.4.4.

C[[x: = (cont x) + 3]] = λs: store. ⌊update s x (V[[(cont x) + 3]]s)⌋
= λs: store. ⌊update s x ((λs: store. (V[[(cont x)]]s) + (V[[3]]s))s)⌋
= λs: store. ⌊update s x ((λs: store. ((λs: store. lookup s x)s) + ((λs: store. 3)s))s)⌋
=_{β} λs: store. ⌊update s x ((lookup s x) + 3)⌋

Similarly,

C[[x: = (cont x) + 1]] = λs: store. ⌊update s x ((lookup s x) + 1)⌋
C[[x: = (cont x) + 2]] = λs: store. ⌊update s x ((lookup s x) + 2)⌋

hence C[[x: = (cont x) + 1; x: = (cont x) + 2]]

= (λs: store. ⌊update s x ((lookup s x) + 2)⌋) ⋄ (λs: store. ⌊update s x ((lookup s x) + 1)⌋)
= λs: store. (λs: store. ⌊update s x ((lookup s x) + 2)⌋) · ((λs: store. ⌊update s x ((lookup s x) + 1)⌋)s)
=_{β} λs: store. (λs: store. ⌊update s x ((lookup s x) + 2)⌋) · ⌊update s x ((lookup s x) + 1)⌋
= λs: store. ⌊update (update s x ((lookup s x) + 1)) x ((lookup (update s x ((lookup s x) + 1)) x) + 2)⌋
= λs: store. ⌊update (update s x ((lookup s x) + 1)) x (((lookup s x) + 1) + 2)⌋  by (lookup)
= λs: store. ⌊update (update s x ((lookup s x) + 1)) x ((lookup s x) + 3)⌋.

Using the equation

update (update s x a) x b = update s x b

which follows from (update)_{2} , we have that the denotations of the two programs are the same. Exercise 6.4.5. First let us define some abbreviations:

P_{1} =^{def} y := (cont x)
P_{2} =^{def} z := 1
P_{3} =^{def} while (cont y) ≠ 0 do z := (cont z) ∗ (cont y); y := (cont y) − 1 od
Q_{1} =^{def} z := (cont z) ∗ (cont y)
Q_{2} =^{def} y := (cont y) − 1

Then the denotational semantics for the whole program is C[[P_{3}]] ⋄ (C[[P_{2}]] ⋄ C[[P_{1}]]); for the individual statements, we find that

C[[P_{1}]] = λs: store.⌊update s y (lookup s x)⌋
C[[P_{2}]] = λs: store.⌊update s z 1⌋
C[[Q_{1}]] = λs: store.⌊update s z (lookup s z) ∗ (lookup s y)⌋
C[[Q_{2}]] = λs: store.⌊update s y (lookup s y) − 1⌋
C[[P_{3}]] = fix(λf: store → store_{⊥}. λs: store. if (lookup s y) ≠ 0 then (f ⋄ (C[[Q_{2}]] ⋄ C[[Q_{1}]])) s else ⌊s⌋)

Consider any environment η such that η(y) ≠ η(z) and let

F =^{def} A_{λ}[[λf: store → store_{⊥}. λs: store. if (lookup s y) ≠ 0 then (f ⋄ (C[[Q_{2}]] ⋄ C[[Q_{1}]]))s else ⌊s⌋]]η

We can now prove by induction on n that

F^{n}(⊥_{store → store_{⊥}}) s = \{ \begin{matrix}⌊update^{A} (update^{A} s η(z) b ∗ a!) η(y) 0⌋ & if a < n \\ ⊥_{store} & otherwise \end{matrix}

where a = lookup^{A} s η(y), b = lookup^{A} s η(z). Since C̄[[P_{3}]]η = ⋁ F^{n}(⊥), it now follows that

C̄[[P_{3}]]ηs = ⌊update^{A} (update^{A} s η(z) b ∗ a!) η(y) 0⌋

where a = lookup^{A} s η(y), b = lookup^{A} s η(z). Finally, if lookup^{A} s η(x) = n, we note that C̄[[P_{1}; P_{2}]]ηs = ⌊s′⌋ where s′ = update^{A}(update^{A} s η(y) n) η(z) 1. Since lookup^{A} s′ η(y) = n, lookup^{A} s′ η(z) = 1, we have that C̄[[P_{3}]]ηs′ = ⌊s′′⌋ with lookup^{A} s′′ η(z) = 1 ∗ n! = n!.

Exercise 6.4.7. (a)

C[[repeat P until B]] = fix(λf: store → store_{⊥}.(λs: store. if V[[B]]s then ⌊s⌋ else f s) ⋄ C[[P]])

(b)

C[[repeat P until B]] = fix(λf: store → store_{⊥}.(λs: store. if V[[B]]s then ⌊s⌋ else f s) ⋄ C[[P]])
= (λs: store. if V[[B]]s then ⌊s⌋ else C[[repeat P until B]]s) ⋄ C[[P]]
= (λs: store. if V[[B]]s then C[[skip]]s else C[[repeat P until B]]s) ⋄ C[[P]]

                          = C[[if B then skip else repeat P until B]] ⋄ C[[P]]
                          = C[[P; if B then skip else repeat P until B]]

(c) We want to prove fix M = (fix N) ⋄ L, where

L =^{def} C[[P]]
M =^{def} λf: store → store_{⊥}.(λs: store. if V[[B]]s then ⌊s⌋ else f s) ⋄ L
N =^{def} λf: store → store_{⊥}. λs: store. if V[[¬B]]s then (f ⋄ L)s else ⌊s⌋

We prove that M^{k}(λs: store. ⊥_{store}) = (N^{k}(λs: store. ⊥_{store})) ⋄ L for every natural number k, by induction on k.

Base Case: We first show that

(∗) (λs: store. ⊥_{store}) ⋄ L = λs: store. ⊥_{store}

Consider any s: store , then ((λs: store. ⊥_{store}) ⋄ L)s = (λs: store. ⊥_{store}) · (Ls). If Ls =⊥_{store} then (λs: store. ⊥_{store}) · (Ls) =⊥_{store} , by definition of ·. Otherwise, Ls = ⌊s′⌋ for some store s′ and (λs: store. ⊥_{store}) · (Ls) = (λs: store. ⊥_{store})s′ =⊥_{store} . In either case, we have shown that

((λs: store. ⊥_{store}) ⋄ L)s =⊥_{store}= (λs: store. ⊥_{store})s

from which (∗) follows.

Then,

M^{0}(λs: store. ⊥_{store}) = λs: store. ⊥_{store}  (definition of M^{0})
N^{0}(λs: store. ⊥_{store}) ⋄ L = (λs: store. ⊥_{store}) ⋄ L
= λs: store. ⊥_{store}  (∗)

Thus, M^{k}(λs: store. ⊥_{store}) = (N^{k}(λs: store. ⊥_{store})) ⋄ L for k = 0.

Induction Step: Assume that M^{k}(λs: store. ⊥_{store}) = (N^{k}(λs: store. ⊥_{store})) ⋄ L; then we have

M^{k+1}(λs: store. ⊥_{store}) = M(M^{k}(λs: store. ⊥_{store}))
= M((N^{k}(λs: store. ⊥_{store})) ⋄ L) (induction hypothesis)
= (λs: store. if V[[B]]s then ⌊s⌋ else ((N^{k}(λs: store. ⊥_{store})) ⋄ L) s) ⋄ L
= (λs: store. if ¬V[[B]]s then ((N^{k}(λs: store. ⊥_{store})) ⋄ L) s else ⌊s⌋) ⋄ L
= (λs: store. if V[[¬B]]s then ((N^{k}(λs: store. ⊥_{store})) ⋄ L) s else ⌊s⌋) ⋄ L
= N(N^{k}(λs: store. ⊥_{store}) ⋄ L
= (N^{k+1}(λs: store. ⊥_{store})) ⋄ L

(d) We must prove fix M = (fix N) ∘ C[[P]], where M, N and P are as in part (c). We will do this by proving the two approximations fix M ≤ (fix N) ∘ C[[P]] and (fix N) ∘ C[[P]] ≤ fix M. It is easy to see that N is equal to the following term in any cpo model.

N = λf: store → store.λs: store.if V[[B]]s then s else (f ∘ C[[P]])s.

To prove the first approximation, let A be the approximation

A ≡ x: store → store ▷ x ≤ (fix N) ∘ C[[P]] : store → store.

We will prove [fix M/x]A by the fixed point induction rule (fpind). It is easy to prove

[⊥/x]A ≡ ⊥ ≤ (fix N) ∘ C[[P]]

since this is an instance of the axiom (bot). We now assume

[c/x]A ≡ c ≤ (fix N) ∘ C[[P]]

and show

[M c/x]A ≡ M c ≤ (fix N) ∘ C[[P]].

From c ≤ (fix N) ∘ C[[P]] we obtain

M c ≤ M((fix N) ∘ C[[P]])

by the application congruence rule (acong). By β -reducing the application of M, this gives us

M c ≤ (λs: store.if V[[B]]s then s else ((fix N) ∘ C[[P]])s) ∘ C[[P]].

Now let us look at the term (fix N) ∘ C[[P]]. By one fix-reduction of fix N, followed by β -reduction, we have

(fix N) ∘ C[[P]] = (λs: store.if V[[B]]s then s else ((fix N) ∘ C[[P]])s) ∘ C[[P]].

This very conveniently matches the term on the right hand side of the approximation involving M c above. Therefore, by transitivity, we obtain

M c ≤ (fix N) ∘ C[[P]],

which gives us the second hypothesis to the fixed point induction rule.

It remains to prove the converse approximation (fix N) ∘ C[[P]] ≤ (fix M). Let A be the approximation

A ≡ x: store → store ▷ x ∘ C[[P]] ≤ (fix M) : store → store.

It is easy to establish

[⊥/x]A ≡ ⊥ ∘ C[[P]] ≤ (fix M)

since ⊥ ∘ C[[P]] = ⊥ by rule (botf ).

To complete the proof, we assume the approximation

[c/x]A ≡ c ∘ C[[P]] ≤ (fix M).

We must show that

[N c/x]A ≡ (N c) ∘ C[[P]] ≤ (fix M).

From the assumption, c ∘ C[[P]] ≤ (fix M), we obtain

M(c ∘ C[[P]]) ≤ M(fix M) = fix M

by applying M to both sides of the approximation and noting that (fix M) = fix M by the equational axiom for fix. By β -reduction, we can easily show

M(c ∘ C[[P]]) = (λs:store.if V[[B]]s then s else (c ∘ C[[P]])s) ∘ C[[P]] = (N c) ∘ C[[P]].

By transitivity, we may now obtain

(N c) ∘ C[[P]] ≤ (fix M).

This gives a proof of the approximation

[fix N/x]A ≡ (fix N) ∘ C[[P]] ≤ (fix M)

by a single use of the fixed point induction rule.

Exercise 6.5.1.

(a) Consider any environment η and store s ≠ ⊥_{store} . Suppose that η, s ⊧ x ≠ y which implies that η(x) ≠ η(y). Also, for

P =^{def} x := cont y; x := cont x + 1

we have that C̄[[P]] η s = ⌊s′⌋, where v_{y} = lookup^{A} s η(y), s′ = update^{A} s η(x) v_{y} + 1. Since η(y) ≠ η(x), lookup^{A} s′ η(y) = v_{y}. Thus,

V̄ [[cont x]] η s′ = v_{y} + 1
V̄ [[cont y]] η s′ = v_{y}

and η, s′ ⊧ cont x ≠ cont y.

(b) Let P =^{def} if cont x ≥ cont y then skip else swap

and consider any environment η and store s. Suppose that η, s ⊧ x ≠ y ≠ z which implies that η(x) ≠ η(y) ≠ η(z). Let v_{x} = lookup^{A} s η(x), v_{y} = lookup^{A} s η(x). Then, we note that

C̄[[P]] η s = \{ \begin{matrix}⌊s⌋ & if v_{x} ≥ v_{y} \\ ⌊s′⌋ & otherwise \end{matrix}

where s′ = update^{A} (update^{A} (update^{A} s η(z) v_{x}) η(x) v_{y}) η(y) v_{x}

since η(x) ≠ η(y) ≠ η(z). If v_{x} ≥ v_{y} then η, s ⊧ cont x ≥ cont y; otherwise v_{x} < v_{y} and η, s′ ⊧ cont x ≥ cont y since V̄[[cont x]]ηs′ = v_{y} and V̄[[cont y]]ηs′ = v_{x}.

(c) Let P be the given program. Then C̄[[P]] η = fix F where

F =^{def} λf: store → store_{⊥}. λs: store. if B s then f · (G s) else ⌊s⌋

with G =^{def} C̄[[x := (cont x) − 1]] η, B =^{def} V̄[[cont x ≠ 1]] η. Suppose that C̄[[P]] η s = ⌊s′⌋, i.e., (fix F) s = ⌊s′⌋. Since the cpo A_{⊥}^{store} is essentially flat, it follows that (F^{n} ⊥) s = ⌊s′⌋ for some n. By Lemma 6.4.9, it follows that Bs′ = false , i.e., V̄[[cont x]] η s′ = 1 which implies that η, s′ ⊧ cont x = 1.

(d) Consider the program

P′ =^{def} while cont m < cont n do P od

Then C̄[[P′]]η = fix G, where

G =^{def} λf: store → store_{⊥}. λs: store. if V̄[[cont m < cont n]] η s then f · (C̄[[P]] η s) else ⌊s⌋

Consider any environment η and store s such that η(m) ≠ η(n). Let a = lookup^{A} s η(m), b = lookup^{A} s η(n) and further suppose that there is an x such that a ≤ x ≤ b and f(x) = 0. Let l be the least value such that a ≤ l and f(l) = 0 and h the highest value such that h ≤ b and f(h) = 0. Take k = min(l − a, b − h) and define p to be l if l − a = k and h otherwise. Note that f(p) = 0. Then, we can prove by induction on i that

G^{i+2}(⊥)s = ⌊update^{A} (update^{A} s η(m)p) η(n) p⌋ if i ≤ k

Since k ≤ ⌊(a − b)/2⌋, it follows that

G^{⌊(a−b)/2⌋+2}(⊥)s = ⌊update^{A} (update^{A} s η(m)p) η(n) p⌋ (∗)

If we call the whole program Q, then

C̄[[Q]] η s = (fix G) · ⌊(update^{A} (update^{A} s η(m) 0) η(n) 100)⌋

and if η, s ⊧ F, it follows from (∗) that C̄[[Q]] η s = ⌊s′⌋ with lookup^{A} s′ η(n) = p. Since f(p) = 0, it follows that η, s′ ⊧ f(cont n) = 0.

Exercise 6.5.6. Consider the valid assertion y ≠ z {x := y} cont x ≠ z. If we apply the substitution [cont v/z], we get the assertion y ≠ cont v {x := y} cont x ≠ cont v which is not valid in an environment η and store s where η(x) = η(v) and lookup^{A} s η(x) ≠ η(y).

Exercise 6.5.7.

(b) We begin with some abbreviations:

F_{1} =^{def} x ≠ y ≠ z
F_{2} =^{def} cont x ≥ cont y
F_{3} =^{def} cont x ≥ cont z
F_{4} =^{def} cont y ≥ cont z
F_{5} =^{def} cont y ≥ cont x

Using the axiom for assignment and the rule of consequence, we may prove the following assertions about assignment statements.

(F_{1} ∧ F_{3}){y: = cont z}(F_{1} ∧ F_{2})
(F_{1} ∧ F_{4}){x: = cont y}(F_{1} ∧ F_{3})
(F_{1} ∧ F_{5}){z: = cont x}(F_{1} ∧ F_{4})
(F_{1} ∧ F_{2}){v: = cont v}(F_{1} ∧ F_{2}).

Since the conditional rule gives us

\frac{(F_{1} ∧ F_{2})\{skip\}F_{2}, (F_{1} ∧ ¬F_{2})\{swap\}F_{2}}{x ≠ y ≠ z\{if cont x ≥ cont y then skip else swap\}cont x ≥ cont y} ,

it suffices to prove the two hypotheses of this rule. The assertion about skip follows easily from the assertion about v: = cont v above by the rule of consequence. The required assertion about swap is proved using the sequencing rule twice, followed by the rule of consequence.

\frac{(F_{1} ∧ F_{4})\{x: = cont y\}(F_{1} ∧ F_{3}), (F_{1} ∧ F_{3})\{y: = cont z\}(F_{1} ∧ F_{2})}{(F_{1} ∧ F_{4})\{x: = cont y; y: = cont z\}(F_{1} ∧ F_{2})} ,

\frac{(F_{1} ∧ F_{5})\{z: = cont x\}(F_{1} ∧ F_{4}), (F_{1} ∧ F_{4})\{x: = cont y; y: = cont z\}(F_{1} ∧ F_{2})}{(F_{1} ∧ F_{5})\{swap\}(F_{1} ∧ F_{2})} ,
\frac{(F_{1} ∧ F_{5})\{swap\}(F_{1} ∧ F_{2}), (F_{1} ∧ ¬F_{2}) ⊃ (F_{1} ∧ F_{5}), (F_{1} ∧ F_{2}) ⊃ F_{2}}{(F_{1} ∧ ¬F_{2})\{swap\}F_{2}} .

This concludes the proof.

(c) To prove the partial correctness assertion true{while cont x ≠ 1 do x: = (cont x)−1 od}cont x = 1, we can see from the rule of consequence that it suffices to prove

true{while cont x ≠ 1 do x: = (cont x) − 1 od}(true ∧ ¬(cont x ≠ 1))

We prove this assertion using the while inference rule. An instance of the rule is

\frac{(true ∧ (cont x) ≠ 1)\{x: = (cont x) − 1\}true}{true\{while cont x ≠ 1 do x: = (cont x) − 1 od\}(true ∧ ¬(cont x ≠ 1))} .

Therefore, it suffices to prove

(true ∧ (cont x) ≠ 1){x: = (cont x) − 1}true.

This follows easily from the assignment axiom and rule of consequence.

(d) Let G =^{def} (∃x: nat)[(cont m ≤ x ≤ cont n)∧f(x) = 0]∧m ≠ n and B_{0} =^{def} cont m ≤ cont n. It is not hard to check that (G ∧ ¬B_{0}) ⊃ f(cont n) = 0. Therefore, by the while rule,

\frac{(G ∧ B_{0})\{P \}G}{G\{while B do P od\}(G ∧ ¬B_{0})} ,

it suffices to prove (G ∧ B_{0}){P }G. Working backwards, may prove this assertion by the conditional rule

\frac{(G ∧ B_{0} ∧ B_{1})\{P_{1}\}G, (G ∧ B_{0} ∧ (¬B_{1}))\{P_{2}\}G}{(G ∧ B_{0})\{P \}G} ,

and the second hypothesis here by the conditional rule

\frac{(G ∧ B_{0} ∧ (¬B_{1}) ∧ B_{2})\{P_{3}\}G, (G ∧ B_{0} ∧ (¬B_{1}) ∧ (¬B_{2}))\{P_{4}\}G}{(G ∧ B_{0} ∧ (¬B_{1}))\{P_{2}\}G} ,

where

B_{1} =^{def} Eq? f(cont m) 0
B_{2} =^{def} Eq? f(cont n) 0
P_{1} =^{def} n: = cont m
P_{2} =^{def} if B_{2} then P_{4} else P_{5}
P_{3} =^{def} m: = cont n
P_{4} =^{def} m: = (cont m) + 1; n: = (cont n) − 1

The required assertions about programs P_{1} , P_{3} and P_{4} , which are assignments and sequences of assignments, are proved as in part (b) of this problem.

Chapter 7

Exercise 7.2.20.

(a) If f ∘ Proj_{1} = g ∘ Proj_{1} , then f ∘ Proj_{1} ∘ ⟨id, id⟩ = g ∘ Proj_{1} ∘ ⟨id, id⟩. Since composition is associative and Proj_{1} ∘ ⟨id, id⟩ = id , we have f = g. Similarly if f ∘ Proj_{2} = g ∘ Proj_{2} .

(b) Suppose (f × id) ∘ (g × id) = (h × id). Writing (f × id) as ⟨f ∘ Proj_{1}, Proj_{2}⟩ and using the identity ⟨f, g⟩ ∘ h = ⟨f ∘ h, g ∘ h⟩ proved in the text, we have (f × id) ∘ (g × id) = ⟨f ∘ g ∘ Proj_{1}, Proj_{2}⟩. Expanding (h × id) similarly and applying composing Proj_{1} with both expressions, we obtain f ∘ g ∘ Proj_{1} = h ∘ Proj_{1} . By part (a), we conclude f ∘ g = h.

Chapter 8

Exercise 8.2.4. This exercise may be solved using the following lemma, which could have been given in another part of the book (but hasn’t been put there yet).

Lemma: Let Σ be a λ^{→} signature with one type constant, b, and no term constants. Then for every type σ over this signature, there is a closed term M: σ iff σ is a true formula of classical propositional logic, reading → as implication and b as false .

Note that every type σ may be written in the form σ ≡ σ_{1} → … → σ_{k} → b, for some sequence of types σ_{1}, …, σ_{k}. We will use this in the proof of the lemma below. It is interesting to observe that a propositional implication σ ≡ σ_{1} → … → σ_{k} → b is valid iff it is true when b is interpreted as false . The reason is that the implication is clearly true with b is interpreted as true . Proof We will regard b as false throughout the proof. We use induction on types to show that there exists a closed term M: σ iff σ is true.

The base case is σ ≡ b. Since we consider b false, and there is no closed term M: b, the claim holds.

For the inductive step, we show that there is a closed term M: σ → τ iff either σ is false or τ is true. If there is a closed term M: σ → τ and σ is true, then by the inductive hypothesis there is a closed term N: σ and therefore a closed term MN: τ. This shows that if there is a closed term M: σ → τ then either σ is false or τ is true. It remains to establish the reverse implication.

There are two cases to consider. If τ is true, then by the inductive hypothesis there is some closed P: τ and therefore we may write a closed term λx: σ. P of type σ → τ.

The remaining case is when σ is false. We write σ in the form σ ≡ σ_{1} → … → σ_{k} → b and observe that since the implication σ is false, all of the propositional formulas σ_{1}, …, σ_{k} must be true. Therefore, by the inductive hypothesis, there exist closed terms M_{1}: σ_{1}, …, M_{k}: σ_{k}. If we write τ in the form τ ≡ τ_{1} → … → τ_{ℓ} → b, then we may write the closed term

λx: σ. λy_{1}: τ_{1}…. λy_{ℓ}: τ_{ℓ}. xM_{1} … M_{k}.

with type

σ → τ ≡ (σ_{1} → … → σ_{k} → b) → τ_{1} → … → τ_{ℓ} → b.

This completes the proof.

Given the lemma, the exercise is solved by showing that R is logical by induction on types. For type b, this is clearly true. For type σ → τ, we know that R^{σ → τ} = A^{σ → τ} iff σ → τ is true (with b read as false ). Therefore R^{σ → τ} = A^{σ → τ} iff R^{σ} = ∅ or R^{τ} = A^{τ}. In either case, it is easy to check that for any f ∈ A^{σ → τ}, if x ∈ R^{σ} then App f x ∈ R^{τ}. The converse is also easily verified.

Exercise 8.2.2. We sketch a general approach that works for any term constants of types of the form b_{1} → … → b_{k}, where each b_{i} is a type constant and k ≥ 1. We start with relations respecting each constant whose type is a type constant and then built a relation in stages so that each R^{b} is closed under application of the given functions. Illustrated using the signature given in this exercise, we let R_{0}^{nat} = {⟨0^{A}, 0^{A}⟩, ⟨1^{A}, 1^{A}⟩}. This gives us R_{0}^{nat}(c^{A}, c^{A}) for each constant c of the signature whose type is a type constant. For each i ≥ 0, we let

R_{i+1}^{nat} = R_{i}^{nat}
∪{ ⟨+^{A}(x, y), +^{A}(x′, y′)⟩ | ⟨x, x′⟩, ⟨y, y′⟩ ∈ R_{i}^{nat} }
∪{ ⟨∗^{A}(x, y), ∗^{A}(x′, y′)⟩ | ⟨x, x′⟩, ⟨y, y′⟩ ∈ R_{i}^{nat} }

where +^{A}(x, y) = App (App + x) y, and similarly for ∗^{A}. Define R^{nat} by

R^{nat} = ⋃_{i>0} R_{i}^{nat}.

With relation R^{σ → τ} defined from R^{σ} and R^{τ} to give a logical relation, it is relatively easy to check that R^{nat → nat → nat}(+^{A}, +^{A}) and R^{nat → nat → nat}(∗^{A}, ∗^{A}). The same approach may also be used to define the smallest logical relation containing any larger R_{0}^{nat} .

Exercise 8.2.15. This exercise is more complicated than necessary. The function f(x) = 1 − x is a permutation invariant function in A^{b → b} that is not lambda definable. Since there are only two permutations on A^{b}, it is easy to check permutation invariance. We can see that f is not lambda definable by analyzing normal forms. Specifically, if M: b → b is a closed normal form without term constants, then M must have the form M ≡ λx: b. M′, where M′: b cannot contain λ. Since the only possibility is M′ ≡ x, the only lambda definable function in A^{b → b} is the identity.

Exercise 8.2.16. The proof is by induction on terms. The base case for variables and the induction step for application are identical to the corresponding cases in the proof of Lemma 8.2.5 (the basic lemma for models). However, we must check that R(K, K) and R(S, S) for each appropriate type of combinator K and S. For S, we assume R^{ρ → σ → τ} (x, x′), R^{ρ → σ}(y, y′) and R^{ρ}(z, z′). Since R is logical, we have R^{τ} (xy(yz), x′y′(y′z′)) and therefore a simple argument allows us to conclude R(S, S) from Sxyz = xy(yz). The proof for K is similar but easier.

Exercise 8.2.22. The main idea is that if we have a nontrivial equivalence relation on A^{b}, then some functions in A^{b → b} may not respect this relation. For example, let A be the full classical hierarchy over A^{b} = N (the natural numbers) and let R^{b} ⊆ N × N be the relation

R^{b}(n, m) iff n, m < 10 or n, m ≥ 10

Then we do not have R^{b → b}(succ, succ), where succ is the successor function.

Exercise 8.2.30. This follows easily from a version of Lemma 8.2.26 for terms without lambda abstraction. The proof of Lemma 8.2.26 for terms without lambda and relations that do not satisfy (β) is essentially the same as the proof of Lemma 8.2.26 in the text, since the hypothesis that R satisfies (β) is needed only for the lambda abstraction case of the induction on terms.

Exercise 8.3.3.

(a) Property (i) follows easily from the fact that H_{0} = Γ_{0} . Property (ii) is not immediate since some τ_{i} may appear in Γ_{0} . However, if x: τ_{i} ∈ H_{i}, then by axiom (empty I) we can prove M_{0} = N_{0} by adding empty(τ_{i}) to H_{i+1} . Therefore, we cannot have empty(τ_{i}) and x: τ_{i} in H. It is easy to see that if we do put empty(τ_{i}) ∈ H, then we add infinitely many variables of this type.

(b) The proof of Lemma 8.3.1 stands as written, except where it is shown that if E ⊢ Γ ▷ MN = M′N′ : τ, for every N, N′ with E ⊢ Γ ▷ N = N′ : σ, then E ⊢ Γ ▷ M = M′ : σ → τ, assuming that H provides infinitely many variables of type σ. In proving this lemma with empty types, there are two cases to consider. If H does provide infinitely many variables of type σ, then the proof proceeds as before. If not, then we use the fact that empty(σ) ∈ H.

If x is any variable not in Γ, then we have

E ⊢ Γ, empty(σ), x: σ ▷ Mx = M′x : τ

by (empty I). By lambda abstracting x in both terms and using (η), we have

E ⊢ Γ, empty(σ) ▷ M = M : τ

which completes the proof, since Γ, empty(σ) ⊆ H.

(c) Arguing as in the proof of Theorem 8.3.2, we can see that if A ⊧ Γ_{0} ▷ M_{0} = N_{0} : σ_{0} , then E ⊢ Γ ▷ M_{0} = N_{0} : σ_{0} for some finite Γ ⊆ H. We use induction on steps of the construction of H to show that for each i, Γ ▷ M_{0} = N_{0} : σ_{0} is not provable from E for any finite Γ ⊆ H_{i}. The base case, i = 0, follows using (add hyp). For the induction step, we suppose that no Γ ▷ M_{0} = N_{0} : σ_{0} is provable from E if Γ ⊆ H_{i} and consider any Γ′ ⊆ H_{i+1} .

The first case to consider is Γ′ = Γ, empty(τ_{i}) and Γ ⊆ H_{i}. By construction, there is some Γ′′ ⊆ H_{i} with E ⊢ Γ′′, x: τ_{i} ▷ M_{0} = N_{0} : σ_{0} . We may assume Γ′′ ⊆ Γ, since otherwise we may replace Γ with Γ ∪ Γ′′ ⊆ H_{i}. But if we may prove both

Γ, empty(τ_{i}) ▷ M_{0} = N_{0} : σ_{0} and Γ, x: τ_{i} ▷ M_{0} = N_{0} : σ_{0}

from E, then by rule (empty E) we may prove Γ ▷ M_{0} = N_{0} : σ_{0} , a contradiction.

The remaining nontrivial case is Γ′ = Γ, x_{1}: τ_{i}, …, x_{k}: τ_{i} with Γ ⊆ H_{i}. Since none of x_{1}, …, x_{k} may appear free in M_{0} or N_{0} , we may remove all but one variable of type τ_{i} by lambda abstraction are application of both terms to the remaining variable of type τ_{i}. Therefore we assume Γ′ = Γ, x: τ_{i}. But if E ⊢ Γ, x: τ_{i} ▷ M_{0} = N_{0} : σ_{0} , then by construction we have empty(τ_{i}) ∈ H and therefore x: τ_{i} ∉ H by property (ii). This completes the proof.

Exercise ??. The main change to the proof is in Lemma 8.3.4, part (i), where we must show that if cM_{1} … M_{k} ∈ T^{nat} and SN (M_{i}), then P^{σ}(cM_{1} … M_{k}) for each of the constants. The proof for part (ii) of this lemma, and the proof of Lemma 8.3.5 go through as before.

Two additional arguments are needed in the proof of Lemma 8.3.4, part (i), both in the base case of the induction on types. The first is for a constant c: nat from among 0, 1, . . .. Since we cannot apply c to an argument, we have SN (c) and therefore P^{nat}(c). The second addition is to show that if succ M ∈ T^{nat} and SN (M), then P^{nat}(succ M). If M reduces to a normal form that is not a numeral 0, 1, …, then succ M reduces to a normal form succ N, where N is the normal form of M. If M reduces to a numeral, say M → → \underline{m}, then

succ M → → succ \underline{m} → → \underline{m + 1}

In either case, it is easy to see that SN (succ M) and therefore P^{nat}(succ M).

Exercise 8.2.28. Write out solution from Hayashi email (in book/notes directory).

Exercise 8.2.29. Write out solution from Hayashi email. This exercise is used in a subsequent theorem.

Chapter 9

Exercise 9.3.42.

(a) Show that ∀t.t = λx.[λy.(V y)(x(V y)).

(b) (∀t.t)(λx. λy. λz. y) = λf. ∪_{i}f^{i}(λy.[λz. y) (∀t.t)(λx. λy. λz. z) = λf. ∪_{i}f^{i}(λy.[λz. z).

(c) Let W = λx. x.

Exercise 9.2.5. We show that if a typing assertion Γ ▷ M : σ about a term can be derived using U_{1} ⊆ U_{2} , then this can also be derived without U_{1} ⊆ U_{2} . The first step in proving this is to observe that if Γ ▷ τ : U_{1} is derivable in the system with U_{1} ⊆ U_{2} , then U_{1} ⊆ U_{2} is actually never used in the derivation, since no U_{1} type can have any U_{2} type as a subexpression. (This is an easy induction on the proof rules for types.) Because of the reformulation of rules, we can also see that if Γ ▷ σ : U_{2} is derivable in the system with U_{1} ⊆ U_{2} , then Γ ▷ σ : U_{2} is also derivable without U_{1} ⊆ U_{2} . With these observations about types, it is a straightforward induction on typing derivations to show that if Γ ▷ M : σ can be derived using U_{1} ⊆ U_{2} , then this can also be derived without U_{1} ⊆ U_{2} .

Exercise 9.2.12. Without the side condition on (Π Intro), we may show (λt. x)τ : τ for any type τ, using (Π Intro) and (Π Elim) as follows

\frac{\frac{x: t ▷ x : t}{x: t ▷ λt. x : Πt. t → t}}{x: t ▷ (λt. x)τ : τ}

But since (λt. x)τ →^{β} x and x: t ▷ x : τ is not derivable when τ is different from t, the subject reduction property fails.

Exercise 9.2.14. The hint is to start by showing that if a well-typed term M has a subterm of the form xτ, then x must be a free variable of M. If we have xτ inside a term with x bound, then we must have a subterm of the form λx: (…).(… xτ …). But this is impossible since the type of x must have the form Πt. σ, and the (→ Intro) rule only allows lambda abstraction over variables that have U_{1} -types. The reason we are interested in this property is that when a subterm has the form (λx: (…).(… xτ … xτ′))(λt. N), a β -reduction could create new (as opposed to copy existing) type-redexes in the term.

A similar observation is that no well-typed term can have a subterm of the form λx: τ. λt. M, since the body of a well-typed lambda abstraction can only have a U_{1} -type.

Rather than show strong normalization of λ^{→,Π} directly, we will prove weak normalization and then use parts of this argument to show strong normalization. (Weak normalization is the property that every term has a normal form.) If we begin with an arbitrary λ^{→,Π} -term, we begin by performing all possible type reductions (all β - or η-reductions that involve lambda-abstraction over type variables). Since each type reduction eliminates one λt, for some type variable t, there can only be a finite number of type reductions. If

Γ ▷ λt_{1}…. λt_{n}. M : Πt_{1}…. Πt_{n}. σ

is a term without type redexes, and M does not begin with λt, then we can show by induction on the typing derivation of M that M does not contain any λt and there is a λ^{→} term M′ which reduces in exactly the same ways as M. The only difference between M and M′ is that where M contains an application xτ_{1} … τ_{n} of a variable to some number of types, M′ will contain a variable x_{τ_{1}...τ_{n}}. This may change the number of free variables in the term, but does not change the behavior with respect to reduction. If we define M′ from M by induction on the typing derivation of M, the case for a variable or constant does not change the term. Ordinary lambda abstraction and application are unchanged, type abstraction does not occur (by the observation above), and for a type application xτ, we replace x_{τ_{1}...τ_{n}} τ_{n+1} by x_{τ_{1}...τ_{n}τ_{n+1}} . (This is the only type application case, by the hint above.) It is easy to see that every sequence of reductions of M corresponds to a sequence of λ^{→} reductions of M′ and therefore M is strongly normalizing. This shows that every λ^{→,Π} term without type redexes is strongly normalizing, and therefore every λ^{→,Π} term has a normal form.

To show that every λ^{→,Π} term is strongly normalizing, we must show that there are no infinite reduction sequences. Assume, for the sake of deriving a contradiction, that we have an infinite reduction sequence M_{0} → M_{1} → M_{2} → … of λ^{→,Π} terms. If M is any λ^{→,Π} term, let tnf (M) be the type normal form of M, which is the result of contracting all type redexes in M. It is relatively easy to show that if M → N, then either tnf (M) ≡ tnf (N), if the reduction is a type redex, or tnf (M) → tnf (N). Since type reduction is terminating (as noted above), we must therefore have an infinite sequence tnf (M_{0}) → tnf (M_{i_{1}}) → tnf (M_{i_{2}}) → … from a type normal form, which is impossible.

Exercise 9.3.3. (a)

add m̄ n̄
→ → λt. λf: t → t. λz: t. m̄tf(n̄tfz)
→ → λt. λf: t → t. λz: t. f^{m}(n̄tfz)
→ → λt. λf: t → t. λz: t. f^{m}(f^{n}z)
→ → λt. λf: t → t. λz: t. f^{m+n}z
= \overline{m + n}

Exercise 9.3.4. (a)

cond =^{def} λt. λb: Bool. λx: t. λy: t. btxy

(b)

proj_{i} =^{def} λt_{1}. λt_{2}. λp: t_{1} × t_{2}. p t_{i} (λx_{1}: t_{1}. λx_{2}: t_{2}. x_{i})

(c) Consider the function aux =^{def} λp: Bool × Nat. cond (Bool × Nat) (proj _{1}^{Bool,Nat} p) (pair_{Bool,Nat} false ¯0)

(pair_{Bool,Nat} false (succ (proj _{2}^{Bool,Nat} p)))

where proj _{i}^{Bool,Nat} =^{def} proj_{i} Bool Nat , with proj_{i} as defined in (b). Then we can define the predecessor function as

pred =^{def} λx: Nat. proj _{2}^{Bool,Nat} (x (Bool × Nat) aux (pair_{Bool,Nat}true ¯0))

(d) We can define a function monus: Nat → Nat → Nat such that monus m̄ n̄ → → \overline{m − n}, if m ≥ n

and ¯0 otherwise.

monus =^{def} λx: Nat. λy: Nat. y Nat pred x

Then m = n iff both monus m̄ n̄ and monus n̄ m̄ are 0.

Eq? =^{def} λx: Nat. λy: Nat. cond Bool (zero? (monus x y)) (zero? (monus y x)) false

Exercise 9.4.3.

(a) Let τ to be any type in which t does not occur free, say a base type, such as unit. Let σ = τ, σ′ = t. Then [τ/t]σ = [τ/t]σ′ = τ.

(b) Take Γ = {x: unit}, M = x. Then by the typing rule given in the problem we have ⟨unit, M⟩: ∃t.unit and ⟨unit, M⟩: ∃t.t with neither of the two types an α-variant of the other.

(c) Assume that Γ ▷ ⟨t = τ, M: σ⟩ : ρ. By the rule in the text, ρ has to be ∃t.σ, i.e., the type of the expression ⟨t = τ, M: σ⟩ (if typable at all) is completely determined by its syntax.

Exercise 9.4.4.

(a) Take σ = (real × real → t) ×(t × t → t) ×(t → real) ×(t → real) and τ = real × real . Then we can easily prove the typing assertions

∅ ▷ C : real × real → τ
∅ ▷ P : τ × τ → τ
∅ ▷ R : τ → real
∅ ▷ I : τ → real

Hence we can prove ∅ ▷ ⟨C, P, R, I⟩ : [τ/t]σ. Thus, we have that

∅ ▷ ⟨t = τ, ⟨C, P, R, I⟩: σ⟩ : ∃t.σ

And, since ∃t.σ = ∃.cmplx[cmplx/t]σ, we have shown that the implementation ⟨t = real × real, ⟨C, P, R, I⟩: …⟩ has the correct type.

(b) Let

N =^{def} re(plus ⟨create ⟨1.0, 2.0⟩, create ⟨3.0, 4.0⟩⟩)

which can be trivially checked to have type real , assuming the constants 1.0, 2.0, 3.0, 4.0 of type real .

(c)

abstype cmplx with create … is ⟨t = τ, ⟨C, …⟩: …⟩ in N
→ → [⟨C, P, R, I⟩/⟨create, plus, re, im⟩][τ/cmplx]N
→ → R(P ⟨C ⟨1.0, 2.0⟩, C ⟨3.0, 4.0⟩⟩)
→ → R(P ⟨⟨1.0, 2.0⟩, ⟨3.0, 4.0⟩⟩)
→ → R(⟨Proj_{1}⟨1.0, 2.0⟩ + Proj_{1}⟨3.0, 4.0⟩, …⟩)
→ → Proj_{1}(⟨1.0 + 3.0, …⟩)
→ → 1.0 + 3.0

Exercise 9.5.3. The exercise is to show that Γ ▷ Πt: U_{1}.σ : U_{2} is derivable from Γ, t: U_{1} ▷ σ : U_{2} , using the rules in this section. This is immediate, since Γ, t: U_{1} ▷ σ : U_{2} and the axiom U_{1}: U_{2} are the antecedents of the new (Π U_{2}) rule.

Exercise 9.5.5. If Γ ▷ M : Σx: σ.σ′ is derivable, then we have Γ ▷ first M : σ and Γ ▷ second M : [first M/x]σ′. Combining these using the (Σ Intro) rule, we have Γ ▷ ⟨x: σ = first M, second M: σ′⟩ : Σx: σ.σ′. We may assume, by α-converting Σx: σ.σ′, that x is not free in M.

Exercise 9.5.7. (a) This is a straightforward induction on the derivation of Γ, x: σ ▷ M : σ′ If M is a constant or a variable different from x, then this is trivial. If M is the variable x, then we use the type equality rule and σ = σ′′. The inductive steps are all straightforward.

Chapter 10

Exercise 10.2.5.

(cint → real real → realM) 2

= ((λf: real → real. λx: int. c_{real}^{real}(f(c_{int}^{real}x)))M) 2 = c_{real}^{real}(M(c_{int}^{real}2)) = M(c_{int}^{real}2) since c_{real}^{real} = λx: real. x

Exercise 10.2.8. We define the partial function mt from type assignments and terms to types, then show that for any derivable typing assertion Γ ▷ M : σ, we have mt(Γ; M) <: σ. We define the “minimum type” mt(Γ; M) of M with respect to Γ by induction on the structure of M:

mt(Γ; x) = τ if x: τ ∈ Γ
mt(Γ; c) = τ if c: τ ∈ Σ
mt(Γ; λx: τ. M) = τ → mt(Γ, x: τ; M)
mt(Γ; MN) = τ if mt(Γ; M) = σ → τ

(It might look funny that mt(Γ; MN) is defined when the application may not be well-typed, but only the case where some Γ ▷ MN : σ is derivable matters.) It is a surprisingly straightforward induction to show that if Γ ▷ M : σ, then mt(Γ; M) <: σ. In the induction step for application, for example, we assume that

\frac{Γ ▷ M : τ → σ Γ ▷ N : τ}{Γ ▷ MN : σ}

By the induction hypothesis, mt(Γ; M) = τ′ → σ′ <: τ → σ and mt(Γ; N) = τ′′ <: τ. Since we can only prove τ′ → σ′ <: τ → σ when σ′ <: σ, the induction step is proved.

Exercise 10.3.4.

(c_{⟨ℓ_{1}:real⟩ → real}^{⟨ℓ_{1}:int,ℓ_{2}:bool⟩ → real}M) R
= ((λf: ⟨ℓ_{1}: real⟩ → real. λx: ⟨ℓ_{1}: int, ℓ_{2}: bool⟩. c_{real}^{real}(f(c_{⟨ℓ_{1}:int,ℓ_{2}:bool⟩}^{⟨ℓ_{1}:real⟩}x)))M) R
= c_{real}^{real}(M(c_{⟨ℓ_{1}:int,ℓ_{2}:bool⟩}^{⟨ℓ_{1}:real⟩}R))
= M(c_{⟨ℓ_{1}:int,ℓ_{2}:bool⟩}^{⟨ℓ_{1}:real⟩}R) since c_{real}^{real} = λx: real. x

Exercise 10.3.5. This is an extension of Exercise 10.2.8. We extend the definition of mt by

mt(Γ; ⟨ℓ_{1} = M_{1}, …, ℓ_{k} = M_{k}⟩) = ⟨ℓ_{1}: mt(Γ; M_{1}), …, ℓ_{k}: mt(Γ; M_{k})⟩
mt(Γ; M ℓ_{i}) = τ_{i} if mt(Γ; M) = ⟨ℓ_{1}: τ_{1}, …, ℓ_{k}: τ_{k})⟩

The inductive proof that if Γ ▷ M : σ, then mt(Γ; M) <: σ is similar, with additional cases for ⟨ℓ_{1} = M_{1}, …, ℓ_{k} = M_{k}⟩ and M ℓ. (You need not repeat the cases from Exercise 10.2.8 but should write out the two additional cases in your solution.)

Exercise 10.4.11. The two consecutive uses of subsumption would have the form

\frac{\frac{Γ ▷ M : ρ  Σ ⊢ ρ <: σ}{Γ ▷ M : σ  Σ ⊢ σ <: τ}}{Γ ▷ M : τ}

Using transitivity instead, we would have

Σ ⊢ ρ <: σ Σ ⊢ σ <: τ

\frac{Γ ▷ M : ρ Σ ⊢ ρ <: τ}{Γ ▷ M : τ}

Since the conversion function for ρ <: τ is the composition of the functions for ρ <: σ and σ <: τ, this transformation does not change the meaning of the associated terms with explicit conversions.

Exercise 10.4.12. We show that for any typing derivation with (subsumption) following any typing rule other than (var), we may reverse the order of (subsumption) and the rule before it.

The first case we consider is a typing derivation of the form

\frac{\frac{Γ ▷ M : ρ → σ Γ ▷ N : ρ}{Γ ▷ MN : σ}}{Γ ▷ MN : τ}

with (subsumption) following (→ Elim). Since Σ ⊢ σ <: τ, by assumption, it is easy to see that

Σ ⊢ ρ → σ <: ρ → τ

Therefore, we can transform this typing derivation to the form

\frac{\frac{Γ ▷ M : ρ → σ}{Γ ▷ MN : ρ → τ Γ ▷ N : ρ}}{Γ ▷ MN : τ}

with (→ Elim) following (subsumption). Since

c_{ρ → σ}^{ρ → τ} = λf: ρ → σ. λx: ρ. c_{σ}^{τ}(fx)

it is easy to check that

(c_{ρ → σ}^{ρ → τ}M)N = (λx: ρ. c_{σ}^{τ}(Mx))N = c_{σ}^{τ}(MN)

and so the associated λ^{→} terms with conversion functions are provably equal.

The second case is a typing derivation of the form

\frac{\frac{Γ, x: σ_{1} ▷ M : σ_{2}}{Γ ▷ λx: σ_{1}. M : σ_{1} → σ_{2}}}{Γ ▷ λx: σ_{1}. M : τ_{1} → τ_{2}}

with (subsumption) following (→ Intro). This derivation assumes Σ ⊢ σ_{1} → σ_{2} <: τ_{1} → τ_{2} . Using Lemma 10.4.3, it is easy to see that we must have Σ ⊢ τ_{1} <: σ_{1} and Σ ⊢ σ_{2} <: τ_{2} . A straightforward induction on typing derivation shows that we can prove Γ, x: τ_{1} ▷M : σ_{2} , using (subsumption) after (var) to give the variable x type σ_{1} , and otherwise using exactly the same typing rules as in the derivation of Γ, x: σ_{1} ▷ M : σ_{2} . This allows us to transform the typing derivation shown above to the form

\frac{\frac{Γ, x: τ_{1} ▷ M : σ_{2}}{Γ, x: τ_{1} ▷ M : τ_{2}}}{Γ ▷ λx: τ_{1}. M : τ_{1} → τ_{2}}

with a use of (subsumption) preceding (→ Intro).

It remains to show that this transformation does not change the meaning of the associated λ^{→} terms with conversion functions. Let M̂ = Trans(Γ, x: σ_{1} ▷ M : σ_{2}) be the term obtained by translation of the initial segment of the original proof. In transforming the proof, we replaced the derivation of Γ, x: σ_{1} ▷ M : σ_{2} by a derivation of Γ, x: τ_{1} ▷ M : σ_{2} that is identical except for one use of (subsumption) after (var) to give the variable x type σ_{1} . We therefore have

Trans(Γ, x: τ_{1} ▷ M : σ_{2}) = [c_{τ_{1}}^{σ_{1}}x/x]M̂

It is now easy to see that the term resulting from the original typing derivation is

Trans(Γ ▷ λx: σ_{1}. M : τ_{1} → τ_{2})
= c_{σ_{1} → σ_{2}}^{τ_{1} → τ_{2}} Trans(Γ ▷ λx: σ_{1}. M : σ_{1} → σ_{2})
= c_{σ_{1} → σ_{2}}^{τ_{1} → τ_{2}} λx: σ_{1}. M̂

where the term resulting from the altered typing derivation is

Trans(Γ ▷ λx: τ_{1}. M : τ_{1} → τ_{2})
= λx: τ_{1}. Trans(Γ, x: τ_{1} ▷ M : τ_{2})
= λx: τ_{1}. c_{σ_{2}}^{τ_{2}}Trans(Γ, x: τ_{1} ▷ M : σ_{2})
= λx: τ_{1}. c_{σ_{2}}^{τ_{2}}[c_{τ_{1}}^{σ_{1}}x/x]M̂

However, since

c_{σ_{1} → σ_{2}}^{τ_{1} → τ_{2}} = λf: σ_{1} → σ_{2}. λx: τ_{1}. c_{σ_{2}}^{τ_{2}}(f(c_{τ_{1}}^{σ_{1}}x))

we can see that

c_{σ_{1} → σ_{2}}^{τ_{1} → τ_{2}} λx: σ_{1}. M̂ = λx: τ_{1}. c_{σ_{2}}^{τ_{2}}((λx: σ_{1}. M̂)(c_{τ_{1}}^{σ_{1}}x)) = λx: τ_{1}. c_{σ_{2}}^{τ_{2}}[c_{τ_{1}}^{σ_{1}}x/x]M̂

which gives us the desired equation.

The case for (add var) is straightforward and left to the reader.

Exercise ??. This is similar to Exercise 9.5.7(a). We show that for any term M, if Γ, x: σ ▷ M : τ is derivable, then so is Γ, x: σ′ ▷ M : τ, where σ′ <: σ. This is a straightforward induction on the derivation of Γ, x: σ ▷ M : τ If M is a constant or a variable different from x, then this is trivial. If M is the variable x, then we use subsumption and σ′ <: σ. The inductive steps are all straightforward.

Exercise 10.5.4. We show that the body of point is a subtype of the body of movable, given the assumption point <: movable about the type identifiers appearing in each expression. This follows from the recursive subtype rule, as shown below:

point <: movable ⊢ ⟨move: int → int → point, …⟩

<: ⟨move: int → int → movable⟩

μ point. ⟨move: int → int → point, …⟩

<: μ movable. ⟨move: int → int → movable⟩

Chapter 11