A.16 Lemma
|
| < Free Open Study > |
|
A.16 Lemma
If 
, and 
, then for some D0 and some C <: D we have C0 <: D0 and 
, this : D0 ⊢ t : C.
Proof: By induction on the derivation of mbody(m, C0). The base case (where m is defined in C0) is easy since m is defined in CT(C0) and the well-formedness of the class table implies that we must have derived 
, this : C0 ⊢ t : C by T-METHOD. The induction step is also straightforward.
We are now ready to give the proof of the type safety theorem.
Proof of Theorem 19.5.1: By induction on a derivation of t → t′, with a case analysis on the final rule. Note how stupid warnings are generated in the T-DCAST subcase, second from the end.
| Case E-PROJNEW: | |
From the shape of t, we see that the final rule in the derivation of Г ⊢ t : C must be T-FIELD, with premise 
, for some D0, and that C = Di. Similarly, the last rule in the derivation of 
must be T-NEW, with premises 
and 
, and with D0 = C0. In particular, Г ⊢ vi : Ci, which finishes the case, since Ci <:Di.
| Case E-INVKNEW: | |
The final rules in the derivation of Г ⊢ t: C must be T-INVK and T-NEW, with premises
By Lemma A.16, we have 
, this : D0 ⊢ t0 : B for some D0 and B, with C0 <: D0 and B <: C. By Lemma A.15, Г, 
, this : D0 ⊢ t0 : B. Then, by Lemma A.14, 
, 
for some E <: B. By transitivity of <:, we obtain E <: C. Letting C′ = E completes the case.
| Case E-CASTNEW: | |
The proof of 
must end with T-UCAST since ending with T-SCAST or T-DCAST would contradict the assumption C0 <: D. The premises of T-UCAST, give us 
and D = C, finishing the case.
The cases for the congruence rules are easy. We show just one:
| Case RC-CAST: | t = (D)t0 | | |
There are three subcases according to the last typing rule used.
| Subcase T-UCAST: | Г ⊢ t0: C0 | C0 <: D | D = C |
By the induction hypothesis, 
for some 
. By transitivity of <:, 
. Therefore, by T-UCAST, 
(with no additional stupid warning).
| Subcase T-DCAST: | Г ⊢ t0 : C0 | D <: C0 | D = C |
By the induction hypothesis, 
for some 
. If 
or 
, then 
by T-UCAST or T-DCAST (without any additional stupid warning). On the other hand, if both 
and 
, then, 
with a stupid warning by T-SCAST.
| Subcase T-SCAST: | Г ⊢ t0 : C0 | D ≮: C0 | C0 ≮: D | D = C |
By the induction hypothesis, 
for some 
. Then, both 
and 
also hold. Therefore 
with a stupid warning.
20.1.1 Solution
Tree = μX. <leaf:Unit, node:{Nat,X,X}>; leaf = <leaf=unit> as Tree; ▸ leaf : Tree node = λn:Nat. λt1:Tree. λt2 :Tree. <node={n,t1,t2}> as Tree; ▸ node : Nat → Tree → Tree → Tree isleaf = λl:Tree. case l of <leaf=u> ⇒ true | <node=p> ⇒ false; ▸ isleaf : Tree → Bool label = λl:Tree. case l of <leaf=u> ⇒ 0 | <node=p> ⇒ p.1; ▸ label : Tree → Nat left = λl:Tree. case l of <leaf=u> ⇒ leaf | <node=p> ⇒ p.2; ▸ left : Tree → Tree right = λl:Tree. case l of <leaf=u> ⇒ leaf | <node=p> ⇒ p.3; ▸ right : Tree → Tree append = fix (λf:NatList→NatList→NatList. λl1:NatList. λl2:NatList. if isnil l1 then l2 else cons (hd l1) (f (tl l1) l2)); ▸ append : NatList → NatList → NatList preorder = fix (λf:Tree→NatList. λt:Tree. if isleaf t then nil else cons (label t) (append (f (left t)) (f (right t)))); ▸ preorder : Tree → NatList t1 = node 1 leaf leaf; t2 = node 2 leaf leaf; t3 = node 3 t1 t2; t4 = node 4 t3 t3; l = preorder t4; hd l; ▸ 4 : Nat hd (tl l); ▸ 3 : Nat hd (tl (tl l)); ▸ 1 : Nat
20.1.2 Solution
fib = fix (λf: Nat→Nat→Stream. λm:Nat. λn:Nat. λ_:Unit. {n, f n (plus m n)}) 0 1; ▸ fib : Stream
20.1.3 Solution
Counter = μC. {get:Nat, inc:Unit→C, dec:Unit→C, reset:Unit→C, backup:Unit→C}; c = let create = fix (λcr: {x:Nat,b:Nat}→Counter. λs: {x:Nat,b:Nat}. {get = s.x, inc = λ_:Unit. cr {x=succ(s.x),b=s.b}, dec = λ_:Unit. cr {x=pred(s.x),b=s.b}, backup = λ_:Unit. cr {x=s.x,b=s.x}, reset = λ_:Unit. cr {x=s.b,b=s.b} }) in create {x=0,b=0}; ▸ c : Counter
20.1.4 Solution
D = μX. <nat:Nat, bool:Bool, fn:X→X>; lam = λf:D→D. <fn=f> as D; ap = λf:D. λa:D. case f of <nat=n> ⇒ divergeD unit | <bool=b> ⇒ divergeD unit | <fn=f> ⇒ f a; ifd = λb:D. λt:D. λe:D. case b of <nat=n> ⇒ divergeD unit | <bool=b> ⇒ (if b then t else e) | <fn=f> ⇒ divergeD unit; tru = <bool=true> as D; fls = <bool=false> as D; ifd fls one zro; ▸ <nat=0> as D : D ifd fls one fls; ▸ <bool=false> as D : D
Readers who feel concerned about the fact that we can code ill-typed terms in this system should note that what we've done is to construct a data structure for representing the object language of untyped terms in the metalanguage of the simply typed lambda-calculus with recursive types. The fact that we can do this is no more surprising than the fact (which we've been using in the implementation chapters throughout the book) that we can represent terms of various typed and untyped lambda-calculi as data structures in ML.
20.1.5 Solution
lam = λf:D→D. <fn=f> as D; ap = λf:D. λa:D. case f of <nat=n> ⇒ divergeD unit | <fn=f> ⇒ f a | <rcd=r> ⇒ divergeD unit; rcd = λfields:Nat→D. <rcd=fields> as D; prj = λf:D. λn:Nat. case f of <nat=n> ⇒ divergeD unit | <fn=f> ⇒ divergeD unit | <rcd=r> ⇒ r n; myrcd = rcd (λn:Nat. if iszero 0 then zro else if iszero (pred n) then one else divergeD unit);
20.2.1 Solution
Here are some of the more interesting examples in iso-recursive form:
Hungry = μA. Nat → A; f = fix (λf: Nat→Hungry. λn:Nat. fold [Hungry] f); ff = fold [Hungry] f; ff1 = (unfold [Hungry] ff) 0; ff2 = (unfold [Hungry] ff1) 2; fixT = λf:T→T. (λx:(μA.A→T). f ((unfold [μA.A→T] x) x)) (fold [μA.A→T] (λx:(μA.A→T). f ((unfold [μA.A→T] x) x))); D = μX. X→X; lam = λf:D→D. fold [D] f; ap = λf:D. λa:D. (unfold [D] f) a; Counter = μC. {get:Nat, inc:Unit→C}; c = let create = fix (λcr: {x:Nat}→Counter. λs: {x:Nat}. fold [Counter] {get = s.x, inc = λ_:Unit. cr {x=succ(s.x)}}) in create {x=0}; c1 = (unfold [Counter] c).inc unit; (unfold [Counter] c1).get;
21.1.7 Solution
-
E2 ()
=
{a}
E2({a,b})
=
{a,c}
E2({a})
=
{a}
E2({a,c})
=
{a,b}
E2({b})
=
{a}
E2{b,c})
=
{a,b}
E2({c})
=
{a,b}
E2({a,b,c})
=
{a,b,c}
The E2-closed sets are {a} and {a,b,c}. The E2-consistent sets are , {a}, and {a,b,c}. The least fixed point of E2 is {a}. The greatest fixed point is {a,b,c}.
21.1.9 Solution
To prove the principle of ordinary induction on natural numbers, we proceed as follows. Define the generating function 
by
-
F(X) = {0} È {i + 1 | i Î X}.
Now, suppose we have a predicate (i.e., a set of numbers) P such that P(0) and such that P(i) implies P(i +1). Then, from the definition of F, it is easy to see that X ⊆ P implies F(X) ⊆ P, i.e., P is F-closed. By the induction principle, μF ⊆ P. But μF is the whole set of natural numbers (indeed, this can be taken as the definition of the set of natural numbers), so P(n) holds for all 
.
For lexicographic induction, define 
to be
| F(X) | = | {(m,n) | "(m′,n′) < (m,n), (m′,n′) Î X}. |
Now, suppose we have a predicate (i.e., a set of pairs of numbers) P such that, whenever P(m′,n′) for all (m′,n′) < (m,n), we also have P(m,n). As before, from the definition of F, it is easy to see that X ⊆ P implies F(X) ⊆ P, i.e., P is F-closed. By the induction principle, μF ⊆ P. To finish, we must check that μF is indeed the set of all pairs of numbers (this is the only subtle bit of the argument). This can be argued in two steps. First, we remark that 
is F-closed (this is immediate from the definition of F). Second, we show that no proper subset of 
is F-closed-i.e., 
is the smallest F-closed set. To see this, suppose there were a smaller F-closed set Y, and let (m,n) be the smallest pair that does not belong to Y; by the definition of F, we see that F(Y) ⊈ Y, i.e., Y is not closed-a contradiction.
21.2.2 Solution
Define a tree to be a partial function T Î {1,2}* → {→, ×, Top} satisfying the following constraints:
-
T(*) is defined;
-
if T(π,σ) is defined then T(π) is defined.
Note that occurrences of the symbols →,×,Top in the nodes of a tree are completely unconstrained, e.g. a node with Top can have non-trivial children, etc. As in §21.2, we overload the symbols →, ×, and Top to be also operators on trees.
The set of all trees is taken as the universe U. The generating function F is based on the familiar grammar for types:
F(X) = {Top} È {T1×T2 | T1,T2 Î X} È {T1→T2 | T1,T2 Î X}. It can be seen from the definitions of T and U that T ⊆ U, so it makes sense to compare the sets in the equations of interest, T = vF and Tf = μF. It remains to check that the equations are true.
T ⊆ vF follows by the principle of coinduction from the fact that T is F-consistent. To obtain vF ⊆ T, we need to check, for any T Î vF, the two last conditions from Definition 21.2.1. This can be done by induction on the length of π.
μF ⊆ Tf follows by the principle of induction from the fact that Tf is F-closed. To obtain Tf ⊆ μF, we argue, by induction on the size of T, that T Î Tf implies T Î μF. (The size of T Î Tf can be defined as the length of the longest sequence π Î {1,2}* such that T(π) is defined.)
21.3.3 Solution
The pair (Top, Top × Top) is not in vS. To see this, just observe from the definition of S that this pair is not in S(X) for any X. So there is no S-consistent set containing this pair, and in particular vS (which is S-consistent) does not contain it.
21.3.4 Solution
For an example of a pair of tree types that are related by vS but not by μS, we can take the pair (T,T) for any infinite type T. Consider the set pairs R = {(T(π),T(π)) |π Î {1,2}*}. An examination of the definition of S easily gives R ⊆ S(R), and applying the principle of coinduction gives R ⊆ vS. Then (T,T) Î vS because (T,T) Î R. On the other hand, (T,T) ∉ μS because μS relates only finite types-this can be established by taking R′ to be the set of all pairs of finite types and obtaining μS ⊆ R′ by the principle of induction.
There are no pairs (S,T) of finite types that are related by vSf, but not by μSf, because the two fixed points coincide. This follows from the fact that, for any S,T Î Tf, (S,T) Î vSf implies (S,T) Î μSf. (Since T is a finite tree, the latter statement follows, in turn, be obtained by induction on T. One needs to consider the cases of T being Top, T1 × T2,T1→T2, inspect the definition of Sf, and use the equalities Sf(vSf) = vSf and Sf(μSf) = μSf.)
21.3.8 Solution
Begin by defining the identity relation on tree types: I = {(T,T) | T Î T}. If we can show that I is S-consistent, then the coinduction principle will tell us that I ⊆ vS-that is, vS is reflexive. To show the S-consistency of I, consider an element (T,T) Î I, and proceed by cases on the form of T. First, suppose T = Top. Then (T,T) = (Top,Top), which is in S(I) by definition. Suppose, next, that T = T1×T2. Then, since (T1,T1), (T2,T2) Î I, the definition of S gives (T1×T2,T1×T2) Î S(I). Similarly for T = T1→T2.
21.4.2 Solution
By the coinduction principle, it is enough to show that U × U is FTR-consistent, i.e., U × U ⊆ FTR(U × U). Suppose (x,y) Î U × U. Pick any z Î U. Then (x,z), (z,y) Î U × U, and so, by the definition of FTR, also (x,y) Î FTR(U × U).
21.5.2 Solution
To check invertability, we just inspect the definitions of Sf S and make sure that each set G(S,T) contains at most one element.
In the definitions of Sf and S each clause explicitly specifies the form of a supportable element and the contents of its support set, so writing down 
and supportS is easy. (Compare with the support function for Sm in Definition 21.8.4.)
21.5.4 Solution
21.5.6 Solution
No, an x Î vF \ μF does not have to lead to a cycle in the support graph: it can also lead to an infinite chain. For example, consider 
defined by F(X) = {0} È {n | n + 1 Î X}. Then μF = {0} and 
. Also, for any n Î vF \ μF, that is for any n > 0, support(n) = {n + 1}, generating an infinite chain.
21.5.13 Solution
First, consider partial correctness. The proof for each part proceeds by induction on the recursive structure of a run of the algorithm:
-
From the definition of lfp, it is easy to see that there are two cases where lfp(X) can return true. If lfp(X) = true because X = , we have X ⊆ μF trivially. On the other hand, if lfp(X) = true because lfp(support(X)) = true, then, by the induction hypothesis, support(X) ⊆ μF, from which Lemma 21.5.8 yields X ⊆ μF.
-
If lfp(X) = false because support(X) ↑, then X ⊈ μF by Lemma 21.5.8. Otherwise, lfp(X) = false because lfp(support(X)) = false, and, by the induction hypothesis, support(X) ⊈ μF. By Lemma 21.5.8, X ⊈ μF.
Next, we want to characterize the generating functions F for which lfp is guaranteed to terminate on all finite inputs. For this, some new terminology is helpful. Given a finite-state generating function F Î P(U) → P(U), the partial function 
(or just height) is the least partial function satisfying the following condition:[2]
(Note that height(x) is undefined if x either participates in a reachability cycle itself or depends on an element from a cycle.) A generating function F is said to be finite height if heightF is a total function. It is easy to check that, if y Î support(x) and both height(x) and height(y) are defined, then height(y) < height(x).
Now, if F is finite state and finite height, then lfp(X) terminates for any finite input set X ⊆ U. To see this, observe that, since F is finite state, for every recursive call lfp(Y) descended from the original call lfp(X), the set Y is finite. Since F is finite height, h(Y) = max{height(y) | y Î Y} is well defined. Since h(Y) decreases with each recursive call and is always non-negative, it serves as a termination measure for lfp.
21.8.5 Solution
The definition of Sd is the same as that of Sm, except that the last clause does not contain the conditions T ≠ μX.T1 and T ≠ Top. To see that Sd is not invertible, observe that the set G(μX.Top,μY.Top) contains two generating sets, {(Top,μY.Top)} and {(μX.Top, Top)} (compare the contents of this set for the function Sm).
Because all the clauses of Sd and Sm are the same, except the last, and the last clause of Sm is a restriction of the last clause of Sd, the inclusion vSm ⊆ vSd is obvious. The other inclusion, vSd ⊆ vSm, can be proved using the principle of coinduction together with the following lemma, which establishes that vSd is Sm-consistent.
[2]Observe that this way of phrasing the definition of height can easily be rephrased as the least fixed point of a monotone function on relations representing partial functions.
|
| < Free Open Study > |
|
EAN: 2147483647
Pages: 262