# Full text of "DTIC AD1020198: Backward Analysis for Higher-Order Functions Using Inverse Images"

## See other formats

Backward Analysis for Higher-Order Functions Using Inverse Images Tyng-Ruey Chuang Benjamin Goldberg Department of Computer Science New York University* February 1991 Abstract We propose a method for performing backward analysis on higher-order functional program¬ ming languages based on computing inverse images of functions over abstract domains. This method can be viewed as abstract interpretation done backward. Given an abstract semantics which supports forward analysis, we can transform it into an abstract semantics which performs backward analysis. We show that if the original abstract semantics is correct and computable, then the transformed version of the abstract semantics is also correct and computable. More specifically, given a forward abstract semantics of a higher-order functional language which is expressed in terms of Scott-closed powerdomains, we derive an backward abstraction semantics which is expressed in terms of Scott-open powerdomains. The derivation is shown to be correct and the relationships between forward analysis and backward analysis is established. We apply this method to the classic strictness analysis in functional languages and obtain promising results. We show that the time complexity of inverse image based backward analysis is not much worse than the forward analysis from which it is derived. We then compare this work with previous works of Wadler and Hughes [17], Hughes [11], and Burn [5], showing that some special restrictions and constructions in previous works have natural interpretation in the Scott-closed/Scott-open powerdomain framework. A brief outline of applying the inverse image method to other backward semantics analysis is also given. *The authors’ address: Department of Computer Science, Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, New York, NY 10012, USA. E-mail: chuang@cs.nyu.edu, goldberg@cs.nyu.edu. This paper is available as Technical Report 620 from the Department of Computer Science, New York University, at the above address. An electronic version is also available from the ftp site cs.nyu.edu. This research has been supported, in part, by the National Science Foundation (#CCR-8909634) and DARPA (DARPA/ONR #N00014-91-J1472). 1 1 Introduction Burn, Hankin, and Abramsky [6] use the Scott-closed powerdomain 1 construction to give an abstract semantics for a non-strict higher-order functional language which denotes the language’s strictness property. Their construction can be regarded as an approximation to the concrete Scott-closed powerdomain semantics of the functional language. Their approximation yields an abstract semantics that is computable and safe. That is, their strictness analysis will always terminate for well-typed programs and will not give incorrect answers (although the answers may be approximations). Their method is a forward analysis since definedness of the result of a function call is inferred from the definedness of the arguments. Backward methods for strictness analysis have been investigated by Wadler and Hughes [17], Hughes [11], Davis and Wadler [8] and Burn [5], which emphasize strictness analysis on functional languages with non-flat data types. Their methods are based on the context (or projection, a restricted notation of context) concept. A computation result is in a particular context (or, subject to a particular projection) if we know that the result will be used in a particular way. For example, if a computation result is to be discarded immediately after it is computed, then the result is said to be in the ABSENT context. Also, if we know that a computation result is in the ABSENT context, then we know that we need not carry out the computation at all. Context-based backward analyses infer the contexts of the arguments in a function call from the context of the function call. However, the formulation of a context-based backward analysis is quite complicated, especially in cases involving higher-order functions. Hughes [11] observes that context-based backward analysis for higher order functions is complicated because a context-based forward analysis is also needed to obtain satisfactory answers. Dybjer [9] uses the Scott-open powerdomain to formulate an inverse image analysis for non- strict first-order functions regarding their strictness property. Whether this method can be applied to higher-order functions remains an open question. Furthermore, it is not clear that his method can be automated. We propose here a general method for inverse image analysis for higher-order functions. This method is also based on the Scott-open powerdomain construction. In fact, our method is inspired by the work of Burn, Hankin, and Abramsky [6] and Dybjer [9]. That is, for each function /, we will derive the Scott-open powerdomain semantics of “/ -1 ”, Volf -1 ), from /’s Scott-closed powerdomain semantics, Vc{f)- If 'P'c(f) is an approximation of Vc(f) which is computable and safe, then our derivation, V'oif 1 ), is also computable and safe. Since Burn, Hankin, and Abramsky’s method is applicable to higher-order functions, our approach provides a method for backward analysis which is also applicable to higher-order functions. By incorporating the strictness analysis for non-flat data types by Wadler [16] and Burn [5], our method can also be applied to functional programs with non-flat data types. After representing the idea and giving some examples in strictness analysis, we show the time complexity of doing inverse image based backward analysis and compare our work with previous works. We show that the formulation of a backward analysis is straightforward if a forward analysis is given. We also argue that answering a query in the backward analysis costs not much more than obtaining the forward analysis. A brief outline of applying inverse image analysis to other semantic analysis is also given. 2 The Main Theorem We use bounded-complete w-algebraic epos as the semantic domains in our discussion of inverse image analysis. The definition and properties of bounded-complete w-algebraic epos can be found in Appendix A. Scott-closed and Scott-open sets are defined as follows: Definition 2.1 Let D be a domain. A subset X C D is Scott-closed if 1 The Hoare powerdomain construction, to be precise, is used in their development. 2 1. If x G A and y Cp x, then y G X; 2. If Y C X and Y is directed, then |JY G X. □ We will call the condition in clause 1 of Definition 2.1 the downward closure property. A subset is downward closed if it has the downward closure property. If X is a Scott-closed subset of a domain D, then we say X is closed in D for short. Definition 2.2 Let D be a domain. Define poset Vc(D) by 1. Pci D) = {S \ S C D,S is Scott-closed}; 2. S Q Vc (d) T iff 5 C T. □ We can also define the poset Vo(D) to be the set of all the Scott-open subsets of domain D. Definition 2.3 Let D be a domain. A subset X C D is Scott-open if 1. If x G A' and x Cp y , then y G A'; 2. If Y C D, Y is directed, and |_|Y G A', then Y fl A’ ^ 0. □ Again, we will call the condition in clause 1 of Definition 2.3 the upward closure property. A subset is upward closed if it has the upward closure property. If A' is a Scott-open subset of a domain D, then we say A' is open in D for short. Definition 2.4 Let D be a domain. Define poset Vo(D) by 1. Vo(D) = {S \ S C D, S is Scott-open}; 2. S C Vo ( D ) T iff S D T. □ In Appendix A, we show that both Vc(D) and Vo{D) are domains if D is a domain. In fact, Vc(D) and Pq(D) are complete lattices and they are isomorphic to each other. Also note that the set union operator U is the binary least upper bound operator in Vc(D), while the set intersection operator H is the binary least upper bound operator in Vo{D). An element d in a domain D has a certain property if d belongs to a particular subset of D. We will only use Scott-closed subsets and Scott-open subsets of a domain to describe the properties of the elements in the domain. This restriction may sound artificial, but is quite reasonable. A Scott-closed subset of a domain D can be viewed as a way to describe how undefined an element (or a set of elements) in D is; while a Scott-open subset of D describes how defined an element (or a set of elements) is. We give an intuitive example here. Let D be a domain, and let / G D —* D be a continuous function from D to D. In strictness analysis, we want to know whether the function application / Yp will result in Yp or not. If we use Scott-closed sets, then we can describe strictness in the following way: If the argument x is in the Scott-closed set {Yp}, then the result of / x is in the Scott-closed set {Yp}. The connection between strictness and Scott-closed powerdomains is well described in Burn, Hankin, and Abramsky [6]. Scott-open powerdomains can be used to perform strictness analysis in the backward direction. That is, strictness can be restated as follows: If the result of the function application / x must be in the Scott-open set D — {Yp}, then x must be in the Scott-open set D — {Yp}. If the argument must be defined, then a call-by-need to call-by-value transformation can be performed on function application. This backward reasoning can be viewed as partial evaluation with respect to the result, not, as it is usually done, with respect to the argument. We will describe in this paper how a backward strictness analysis can be realized by an inverse image analysis, with the aid of an existing forward strictness analysis. The connection between 3 backward strictness analysis and inverse image analysis is first described by Dybjer [9], although it is only done on first-order functions. Our contribution in this paper is to extend it into higher- order functions and, in our opinion, to do it in a cleaner way. We also relate forward analyses and backward analyses under the framework of Scott-closed/Scott-open powerdomains. Recall that, given a domain D, we have defined its Scott-closed powerdomain, Vc{D ), and Scott- open powerdomain, Vo{D). The next step is to define functions between these powerdomains, based on continuous functions over the original domains. Fact 2.5 Let D a and Dp be domains and / £ D a —» Dp. Then, 1. {x | x £ D a , fx £ B} is closed in D a if B is closed in Dp ; 2. {a; | x £ D u . fx £ B} is open in D a if B is open in Dp. □ Corollary 2.6 Let D a and Dp be domains. Let / £ D a —*■ Dp. Then, 1. {x | x £ D a , f x y} is closed in D a for each y £ Dp , 2. {x | x £ D a , f x y} is open in D a for each y £ Dp. □ Definition 2.7 Let D a and Dp be domains. Let f £ D a —>■ Dp. Define V c (f) £ V c (D a ) — V c (Dp) and LW 1 ) G V 0 (Dp) -» V 0 (D a ) by 1. (Tcif)) X = {/ x | x £ D a ,x £ X}°, where X £ V c {D a ); 2- ( Vo(f- 1 )) Y = {x | x e D a J x £ Y}, where Y £ V 0 (Dp ), □ For a subset IT of a domain D, 1T C is the least Scott-closed subset of D which contains IT (see Definition A.41). We can say that Vc(f ) defines an image function of /, based on Scott- closed powerdomains; while Vo(f~ l ) defines an inverse image function of /, based on Scott-open powerdomains. By definition, it can be shown that Vc(f) is _L-reflexive. That is, (' Vc(f )) A = 0 if and only if A = 0. Lemma 2.8 Let D a and Dp be domains. Then both Vc(f) and Volf -1 ) are well-defined and continuous for every continuous function / £ D a —>■ Dp. □ Proof. See Appendix B. O Furthermore, it can be shown that Vc(f ) is additive if / is continuous. That is, (' Vc(f )) (A'LIT) = ((Vc(f)) X) U ((V c if)) Y) for all X ,Y £ Vc{D a ). Note that additivity is a stronger condition than continuity. Lemma 2.9 Let D a and Dp be domains, / £ D a Dp, and B £ Vc(Dp). Then {x | x 6 D a ,fx £B} = |J{A | X £ V c (D a ), (V c (f)) X Q Vc (d,) B}. □ Proof. See Appendix B. O We now prove the following main theorem. Theorem 2.10 Let D a and Dp be domains. Let B £ Vo{Dp) and / £ D a Dp. Then ('Pair 1 )) B = |J{A I X £ Vc(D a ), (V c (f)) X Q Vci n,) B}. □ 4 Proof. (Voif- 1 )) B = {x | x £ D a ,f x £ B} (Definition 2.7) = {at | x £ D a ,f x £ B} (Fact A.36) = U{A' | X £V c (D a ),(T c (f)) X Qv c (D„) B} (Lemma 2.9) O The significant part of Theorem 2.10 is that it completely characterizes Voif -1 ) in terms of Vc(f), instead of in terms of function /. But from an abstract interpretation’s point of view, this characterization is not very useful because Vc(f) in general cannot be computed in finite time and the domain Vc(D a ) need not be finite. This makes (Voif -1 )) B in general not computable in finite time. The next step will be to give an approximation of Vo(f~ 1 ) by using an existing approximation of Vc(f)- The following corollary shows the relationship between the forward semantics Vcif ) and the backward semantics Voif _1 ). Corollary 2.11 Let D a and Dp be domains, / 6 D a — * Dp, A £ Pc ( D u ), and B £ Vo(Dp). Then (' Voif _1 )) (Pc(f))A Av 0 ( Da ) A, tPc(f)) (Po(f~ 1 ))B O ra(m B. □ Proof Outline. Substitute the B in Theorem 2.10 by (Vc(f))A to show that the first part is true. Also by Theorem 2.10, (Voif- 1 )) B = |J{A | X £ V c (D a ), ( V c (f )) X Q Vc (d,) Bj. Applying Vc{f) at both sides to show that the second part is true too. O A direct consequence of the above corollary is the following. Corollary 2.12 Let D a and Dp be domains, / £ D a —» Dp, A £ Vc(D a ), and B £ Vc(Dp). Then 1. if (Voif- 1 )) B 3-p 0 (L ) c) A, then (' Pc(f)) A B; 2. if (V c (f))A n ro(Dfl) B, then (Voif- 1 )) B Av oU)a) A. □ 3 An Abstract Semantics and its Inverse In Burn, Hankin, and Abramsky [6], they develop an approximation based on the Scott-closed pow- erdomain construction. They use this approximation to define an abstract semantics for determining the strictness of higher—order functions. In this section, after a brief introduction to their approach and results, we show how to take their approximation and transform it to give an approximation based on the Scott-open powerdomain construction. We then use this newly defined approximation as an abstract semantics for determining strictness, only that it now works backward. The following formulation is a little different from Burn, Hankin, and Abramsky [6] to fit the current discussion. Suppose that we are given an approximation domain V'c(D) for Vc(D), where D is a domain, such that V'c(D) is a finite complete sub-lattice of Vc(D). Note that both 0 and D are in V'c(D). That is, {0, D} C V C (D) C V C (D), V'c(D) has only a finite number of elements, and for all subsets X C V C (D), the least upper bound of X in Vc(D) is the same as the least upper bound of X in Vc(D). This property also holds for the greatest lower bound. For a continuous function / £ D a —? Dp, where D a and Dp are domains, we then give an approximation function V'c(f) f° r Vc(f) such that V'cif) is computable in finite time and ( Vc(f )) A D (Vc(f )) A for each A £ V c (D a ). 5 Definition 3.13 Let D be a domain and P'ciD) be a finite complete sub-lattice of Vc(D ). The abstraction function Absc G Vc{D) —* P'ciD) and the concretization function Goncc G P'ciD) —*■ Vc(D) are defined by Abs c X = n {Y | Y G P'ciD), X Q Vc{D] Y }, where A G V C (D)- Concc Y = Y, where Y G P'ciD). □ An interesting consequence of the above definition is that both Absc and Concc are T-reflexive and additive. Fact 3.14 Let D be a domain. Let V'c(D) be a finite complete sub-lattice of Vc(D)\ and let X G V C (D) and X' G P'ciD). Then, ( Concc o Absc) X D X; (Absc o Concc) X 1 = X'. □ Definition 3.15 Let D a and Dp be domains. Let / G D a —+ Dp. Define P'cif) = Absc°Vc(f ) o Concc■ □ P'cif) is T-reflexive and additive because Absc,Pc(f ), and Concc are T-reflexive and additive. Fact 3.16 Let D a and Dp be domain. Let / G D a Dp and A G Pc{Da)- Then (Pcif)) AC (Concc oV' c (f)o Abs c ) A. □ In short, V 1 c{D) is an abstract domain for Vc{D) and P'cif) is an abstract interpretation of Pcif)- Fact 3.16 asserts that such an abstract interpretation is safe. Suppose that V'c is an approximation based on the Scott-closed powerdomain construction as defined above. We show in the following how to turn P'c into V 0 . an approximation based on the Scott-open powerdomain construction. Definition 3.17 Let D be a domain. Define V'oiD) = {A | X G P'ciD)}- 1=1 Definition 3.18 Let D be a domain. Define the abstraction function Abso G Po(D) —* P'oiD) and the concretization function Conco G P'o{D) —*■ Po{D) by Abso X = |_|{ y I y e P'oiD),Y C Vo(D) A'}, where X G PoiD)- Conco Y = Y, where Y G P'oiD). □ Fact 3.19 Let D be a domain, X G PoiD), and X' G P'oiD). Then (Conco o Abso) X D X and (Abso ° Conco) X' = X'. □ For each function /, we can define P'oif 1 ) in terms of P'cif), as we did in Theorem 2.10. 6 Definition 3.20 Let D a and Dp are domains and let f £ D a —> Dp. Define (V'oif- 1 )) Y = jj{A | X £V' c (D a ),(V' c (f)) X Qv c (d p) F), where Y £ V'o(Dp). □ Note that, in the above definition, if P'c'if) is computable in finite time, then V'oif X ) is computable in finite time since V'c(D a ) is a finite set. The following theorem states that the above definition is safe. Theorem 3.21 Let D a and Dp be domain. Let f £ D a —* Dp and B £ Dp. Then (Voir 1 )) B C (ConcooT'oif-^aAbso) B. □ Proof. We want to show that, for every B £ Vo(Dp), U{A- 1 X £ V c (Da)AVc(f))X Qv c(Db) B} _ C Conc 0 |J{A | X £ P'/ { D„). (' P'c(f)) X Q V ‘ c {d 0 ) Abs 0 B}. That is, U{A | X £P c (D a ),(Vc(f))X Qv c (d p ) B} _ D \_\{X | A £ V'c(D a ), (V'c(f)) X Qv c( d p ) Abs 0 B}. Note that B D Abso B for every B £ Vo(Dp). Therefore, for each A' £ {A | A £ Vc(D a ), (V'c(f)) X Qv c (d,) Abs 0 B} there exists a A £ {X | A e V c (D a ),(Vc(f))X B} such that AD A'. We complete the proof by observing that Vc(D a ) is a finite complete sub-lattice of Pc(D a ) .O The following corollary shows the relationship between the forward abstract semantics V'oif X ) and the backward abstract semantics V c(f)- Corollary 3.22 Let D a and Dp be domains. Let / £ D a — » Dp, A £ V'c{D a ), and B £ V'o(Dp). Then _ (Voir 1 )) (V'c(f)) A D v , o{Da) A, (V'cif)) (V'oif- 1 )) B Qv c{ d p) B. □ The following is a direct consequence of the above corollary. Corollary 3.23 Let D a and Dp be domains, / £ D a Dp, A £ V'c(D a ), and B £ V'c(Dp). Then 1. if (V'oif- 1 )) B □•p' 0 (D c> ,) A, then ( V'cif )) A —p- c (J-V) 2. if (V'cif)) A D.v' c (Df)) B, then ( V'oif _1 )) B A. □ The reader may like to compare the above corollary with the result in Burn [5, Theorem 3.1]. The following lemma describes some degenerate cases. Lemma 3.24 Let D a and Dp be domains. Let / £ D a —>■ Dp. Then, 7 □ 1 . V'c{f)9 = 9, 2 - V'c(f) D a Qv'ciDp) Dp, 3 - V'oif- 1 ) 0 = 0 , 4. V'oif- 1 ) Dp — D a . Proof. The proofs follow immediately from Theorem 2.10, Definition 3.15, and Definition 3.20. O We now relate Burn, Hankin, and Abramsky’s forward strictness analysis to a backward strictness analysis. Fact 3.25 (Burn, Hankin, and Abramsky) Let V'c be the Scott-closed powerdomain approx¬ imation of Burn, Hankin, and Abramsky. Let D a and Dp be domain, and let / £ D a —+ Dp. Then 1- (' P'c(f)) {-L^} D v , c(Dfj ) {D Df) }\ 2. if ( P'c(f )) {J-d q } = {-L Dp}, then f ± Da = ± Df) . (That is, / is strict.) □ Theorem 3.26 Let V'c be the Scott-closed powerdomain approximation of Burn, Hankin, and Abramsky. Let V'o be defined as in Definition 3.20. Let D a and Dp be domains, and let f £ D a Dp. If _ _ (V'oif- 1 )) {-L Dp) ^v 0 (D a ) {-Ld„}, then / is strict. □ Proof Outline. By Corollary 3.23 and Fact 3.25. O 4 Examples In this section we demonstrate how to use our inverse image analysis on higher-order functions. More specifically, we show how a backward strictness analysis can be done within the framework of inverse image analysis. Given a function and an expected property of its result, we infer the property of the function’s arguments which will yield the expected result. For instance, if we expect a function application resulting a defined value, then we would like to use our inverse image analysis to determine whether the argument shall be defined or not. If the argument is shown to be defined, then the argument can be evaluated by call-by-value instead of call-by-need. We start with a modified representation of Burn, Hankin, and Abramsky’s strictness analysis. After showing the forward approximation scheme, V'c, we then reverse it into a backward approxi¬ mation scheme, V' o, which can be used in backward strictness analysis. Let {A, B) denote an element of the smashed product V'ci D u ) 44 V'd Dp ), where A £V'c(D a ), B £ V'c(Dp), and V'c{D) denoting a complete sub-lattices of the Scott-closed powerdomain Vc(D). Then, by the definition of smashed product, we have {A, 0) = (0, B) = 0 for every A £ V' c (D a ) and B £ V'c{Dp). Note that, by notation, (A, B) represents a pair of Scott-closed subsets. However, what we have in mind is to use it to represent the Scott-closed subset of the domain D a x Dp such that (A, B) = {(a, b) | (a, b) £ D a x Dp, a £ A,b £ B}. We will overload [A, B) to the above denotation. Likewise, we overload V' c (D a ) ® V'c(Dp) to denote the subset of the Scott-closed powerdomain Vc(D a x Dp) such that it now includes exactly those Scott-closed subsets denoted by ( A, B) (where A £ V'c{D a ) and B £ V' c (Dp)). 8 We run into tile same notation problem in the _L-reflexive additive function space V'c{D a )—V'o(Dp). We will use [A\ >—>■ Bi , A’i i—^■ ■ ■, A n t—> B n \, where .4.4 , /I,, £ V'c{D a ) and Bi,B2,...,B n £ V'c(Dp), not only as a notation for a _L-reflexive additive map from VciPa) to V'c{Dp), but also as a notation for the Scott-closed subset {/ | / £ D a —* Dp, f a £ Bi for all a £ A\ , f a £ B 2 for all a £ A 2 , ..., and f a £ B n for all a £ A n } of the domain D a Dp. If n is finite, it can be shown that, by the new denotation, [Ai B \, A 2 1 —+ B 2 , ■ -., A n 1 —* B n ] £ Vc(D a —» Dp). For the special case of n = 0, it is written as 0, which is also an element in Vc(D a —> Dp). Likewise, V c{Dot)*-* V c(Dp) is overloaded to denote the subset of the Scott-closed powerdo- main Vc(D a —► Dp) such that it now includes exactly those Scott-closed subsets denoted by the _L-reflexive additive maps from V'c{D a ) to V'c{Dp). Definition 4.27 Let D be a domain. V'c(D) is defined by • if D is a primitive domain B, then V'c(D) = {B, {± B }, 0}. • if D = D a x Dp , then V'ciD) - (IJ.V | X CV , c(D a )®V , c (Dp)}. • if D — D a —> Dp , then V'c(D) = | X C V'c{D a )^V' c {Dp)}. □ The definition for V'c{D a x Dp) and V'c{D a —>■ Dp) deserves some attention. The definition is to make them each a complete sub-lattice of Vc(D a x Dp) and Vc(D a —» Dp) respectively. If we simply define V' c (D a x Dp) as V 1 c (D a ) ® V'c(Dp) and V' c (D a -* Dp) as V' c (D a )»-^ V c {Dp), they will not be complete sub-lattices. Before going into the examples, recall that V'o(D) is defined as {A' | X £ V'c(D)} for every domain D. Example 4.28 Let N be the flat domain of all natural numbers. Then, we have 1. .V' C {N) = {N,{ Tiv},0}, • V' C (N x N) = { (N,N), (N,{± n }) U ({± n },N), (N, {± n }), {{J-iv}, N), {{Tjv}, {-Ljv}), 0 }, • V' C {N — N)= { [N^N, {Tjv} 1 — *■ IV, 0 0], [A t —<■ A, {J-iv} 1 —> {J-iv}, 01—^0], [A {Tjv}, {Tjv} h-*- {Tjv}, 0 1 —^ 0], 0 }• We will write, for example, [N t —>■ N, {Tjv} 1 —»■ JV, 0 0] as XX .N without explicitly mentioning that X £ V'c(N) and this function is T-reflexive. Note that XX .N denotes the set of all the continuous functions from N to N; XX .X denotes the set of all the strict continuous functions from N to N; and A X . {Tjv} denotes the set containing only the everywhere undefined function from N to N. 2. • V'o(N) = {A", {hiljv}", 0} = {0, A — {Tjv}, A'}, 9 . V'o(N x N) = { (N, N), (N, {±jy}) U ({T;v}, N), (N , {_Ljv}), {{-Ljv}, N), ({-Ljy}, {-L jv}),_ 0_ } = { 0;_ (N, {-Ljy}) n {{-Ljv}, N), (N , {-Ljv}), ({± N }, N), <{_Ljv}, {-Ljv}), (N, N) }, • V'o{N -*.N) = {XX .N, XX .X, AA'.{±jv}, 0}. Note that XX .N denotes the empty set; A A' .X denotes the set of continuous functions from N to N which are non-strict (that is, in the N —> N case, the non-Ajv constant functions); A A’ . {_Ljv} denotes the set of continuous functions from N to N which are somewhere defined; and 0 denotes, of course, the set of all the continuous functions from Lemma 4.29 Let D be a domain constructed from a finite set of primitive domains by applying a finite number of product and function space construction. (We will call D finite constructible.) Let V'c be the approximation scheme in Definition 4.27. Then, 1. V'c{D) is a finite complete sub-lattice of Vc{F> ); and V'o{F>) is a finite complete sub-lattice of Vo(D). In particular, _L v‘ 0 (D) = 0 and T v c (d) = F>. Also, ±v 0 ( D ) = D and T v 0 (d) = 0- 2. if C C V'c(D) and O C V'o(D), then \JC = \JC and (J 0 = (~)0. □ Proof Outline. A structural induction on the construction of D. O We omit the construction of V'c(f ), where / £ D a —► Dp, D a and Dp finite constructible, to save space. The construction of V'c(f) is done by a structural buildup, according to the program text defining /, from approximations of primitive functions. In cases where / is recursive defined by a functional F ( i.e., f — fix T), then fix (F is used as a safe approximation for V'c {fix F). 2 The details can be found in Burn, Hankin, and Abramsky [6]. In all cases, the approximation V' c(f) will be a computable continuous function if / is a continuous function. We observe that, if D a is not a primitive domain, an approximation V' c(f)£V'c{D a )~V' c {Dp) can be characterized by a simpler approximation without losing any accuracy. This is because V'c(f) is additive. As an example, let D a = N x N and Dp = N . Then we can characterize v'cif) ev'ciN x N)^V'c{N) by a V , c{f , )eV , c{N)®Vc(N)^V'c{N) which is only defined on V'c{N) fg Vc(X) , instead of V'c{N x N), but have the same functionality of V'cif)- This causes no problem because every X £ V'c(N x N) can be expressed as X = \_\X, where X C V C {N) ®V' C {N), and we have {V'cif)) U x = U {{V'cif')) I*})- We now give some examples. Example 4.30 Function apply £ (N —* N) x N —> N is defined as apply (f, x) = f x. By Burn, Hankin, and Abramsky’s abstract interpretation, we obtain a function V'ciapply) e V'c{{N N) x N)»-> V' C {N), which is characterized as {V'ciapply)) (F, X) = F X 2 Strictly speaking, we do not use the least fixed point of V'c {V) as an safe approximation for V'c ( fix V). Otherwise we will always end up with 0 as approximations since all functions between Scott—closed powerdomains is _L—reflexive (i.e., 0—reflexive). We will use the least fixed point above 0 of V'c(F) as an safe approximation for V'c(fi x V). 10 where (F, X) e V'c(N - N) ® V'c(N) and F X ={f x | Note that (V 1 c{apply)) 0 = 0 by Lemma 3.24. We can characterize Vc( apply) by the following table: A N F (V'c(apply)) (F, X) XX . {Tat} {-Ljv } {-Ljv} A A . A {-Ljv} N XX .N N N Now, suppose that we expect the result of apply {/, x) to be defined, i.e. it cannot be _Ljv- We use our inverse image analysis as follows: (Vojapply -1 )) (N - {-Ljy}) _ = U{(f, X) 1 (F, X) £ V'c(N - N ) ®V' c (N)AV'c{«Pply)) (F, X) Qy. ciN ) N - {T w }} = U {(F, X) | (F, X) e V' C (N - N) ® V'c(N), (V'c(apply)) (F, X) C {± N }}. Therefore, using the definition of V'c{ a PPfy), {V'o(apply~ 1 )) {X - {-Ljy}) _ = U{ 0, (A A' . {-Ljy}, N), (XX.X, {■Ljy })} = f| i( XX ■ {-Ljv}, A'), (A A' . X, {Tjv})}- Summarized in plain English, • / cannot be the everywhere undefined function, • if / is a strict function, then x cannot be _Ljv, and • if x is _LjV; then / must be a (non-Tjv) constant function, which is no worse than our intuition. □ Example 4.31 Function compose £ (N — N) x (N —+ N) —> (N —> N) is defined as compose {/, g) — \ x . f (g x). By Burn, Hankin, and Abramsky’s abstract interpretation, we obtain a function V' c ( compose) e V' C {{N -> N) x (N — A))*- V' C {N -> N), which is characterized by where {/■', G) The table ('.P'c(compose)) (F, G) — A X .F (G X), eV'e{N ->N) ® V' C (N — N). characterizing Vc{ compose) is the following: G F ( V l c( com P ose )) { F , G) A A' . {Tjv} X X . X XX .N A A'. {Ajv} A A'. {Tjv} A X . {Tjv} XX . {Tjv} A A . A A A'. {Tjv} A A . A A A . N XX .N XX .N XX .N XX .N 11 Suppose that the result of the function application compose {/. g ) is not the everywhere undefined function ( i.e. compose {/, g) ^ A A'. -Ljv)- Then, what can we say regarding / and gl Furthermore, suppose that the result is a (non-_Ljv) constant function (i.e. compose {/, g) ^ A A' .A’). Then, what should / and g be? We simply compute (V'o( compose -1 )) AA’.jTjv} and ( P'oi com post )) XX .X to get the answers. (V'oicompose- 1 )) A A. {_!_*} = XX.N), (XX.X, AA.{1 W })}, and (V'oicompose- 1 )) XX .X = p{{ A • {-Ljv}, XX .N), (XX .X, AA'.A)}. That is, if the result of compose {/, g) is not the everywhere undefined function, then • / cannot be the everywhere undefined function, • if / is strict, then g cannot be the everywhere undefined function, and • if g is the everywhere undefined function, then / must be a (non-Tjv) constant function. Also, if the result of compose {/, g) is a (non-Tjv) constant function, then • / cannot be the everywhere undefined function, • if / is strict, then g must be a (non-Tjv) constant function, and • if g is strict, then / must be a (non-_Ljv) constant function. □ It is interesting to note that Hughes [11] cites the above two examples to show why backward analysis is difficult. The difficulty is to capture the interdependency of the two parts in an input argument (/ and x in apply {/, x); and / and g in compose {/, g)). By using our inverse image analysis, we are able to give a satisfactory account of the interdependency. We proceed in analyzing some examples involving non-flat domains. The following examples are taken from Dybjer [9]. Example 4.32 Function length £ L(JV) —>■ N is defined as length [ ] =0, and length (x :: l) = 1 + length l, where L(!V) is the non-flat domain of lazy lists of natural numbers. We define V'c(L(N)) as {0, L ln j(N), L(JV)}, where L in j(N) is the Scott-closed subset of L(1V) which contains all the lists with undefined tails. In particular, L (N) includes the lists in N w to make L(TV) Scott-closed. Also, Tl^jv) £ L In f(N). As usual, Vo(L(N)) = {A' | X £V'c( L(1V))}. Using Wadler’s technique [16], we obtain V 1 c(length) £ P / C (L(1V))^ V'c(N) which is defined by (V c (length)) L mf (N) = {-Ljv}, and (V c (length)) L (N) = N. Note that (T^ci length )) 0 = 0 by Lemma 3.24. Suppose that the result of length l is not _Ljv, then (P'o(length -1 )) {_Ljy} _ = Ul L 1 L £ V'c(UN)),(V' c (length)) L Q v , c{N) {X77}} = U{£ I L £ V'ciHN)), (V c (length)) L C {± N }} = [J{0,L m f (N)} = Unf(N). That is, for the result of length l to be defined, l cannot have an undefined tail. □ 12 Example 4.33 Function last 6 L (N) — » TV is defined as /asf (*::[]) = x, and last (x :: l) = last l. V'c(tast) G V 1 V'c(N), is defined by V'c(last) L in f{N) = {-Ljv}, and V'c(last) L (N) = N. In the case that the result of last l is not _Ljv, (V o(last *)) {-Ljv} = L i n f(N). That is, l cannot have an undefined tail. Note that this answer is safe but not totally accurate. A list / with an undefined tail will make last l undefined, but not all finite-length lists (i.e. the lists without undefined tails) will make last l defined. In particular, if / = [ ], then last [ ] = _Ljv. Can we do better than what we have done? Let us define a new powerdomain V"c(L(N)) = {0, {J_l ( jv)}, {T L( jv), [ ]}, L i n j(N), L(JV)}. Also, V"o{ L(JV)) = {A' | X e?"c(L(jV))}. T"c(last) is characterized by It is not difficult to see that {V"oilasr 1 )) {1^} = U{A~ | X £ jP" c (L(AQ), (V"c(last)) X C = U{0 ; I-Ll(JV)}, UL(iV),[]}, L inf(N)} = L inJ (N) U{[]} = L inf (N) n {[ ]} That is, if last l is defined, then l cannot be the list with an undefined tail and l cannot be the null list. □ It is clear from the above example that the accuracy of our inverse image analysis will depend on the accuracy of the forward analysis from which the inverse image analysis is derived. How precise a forward analysis will suffice? The answer depends on the problem being studied and the programs being analyzed. So far, we have only discussed tail strictness, without mentioning head strictness. In the last program, we would like to know that in order for last l to be defined, the last element of l cannot be undefined. In order to do this, we would have to define a powerdomain more refined than V" c ( L(JV)). In order to capture head strictness, we can define a Scott-closed subset Lgx N (A) to include all the lists which either containing _Ljv or in N w . We then have L ln j(N) C Lgx«(^)- Also, all elements in the Scott-open set L 3 x N (?V) are of finite length and containing no _Ljv. Two more examples from Dybjer [9]. Example 4.34 Function from £iV —»■ L (N) is defined as from x = x :: (from (x + 1)). V 1 c(frorn) £ Vc(N)»-> Vc( L(iV)) 5 is defined by 13 Suppose we expect the result of from x to be a finite-length list. We calculate VP'oiJrom -)) Unf{N) = UU' | X e P'c(N),(V'c(from)) X C L inJ {N)} = u{0. {-U}, = 0 . This means that there is no x E N which will make from x a finite-length list. □ Example 4.35 Function append E L(JV) x L (N) —* L(7V) is defined as append <[ ], g) = g, append {x :: l, g) = x :: (append l g). V'c(append) E V'c(UN) x L(iV))»—► V'ciUN)), is characterized by G Unf(N) UN) F V'c( append) (F , G) L inf ( N) Unf(N) Unf(N) UN) Unf(N) UN) Suppose we expect the result of append {/, g) to be a finite-length list. We calculate {V'oiappend -1 )) L tnf (N) = U{(T, G) | (F, G)E V'c(UN)) Q V'ci UN)), (V' c ( append)) { F , G) C L mf (N)} = U{(L m/ (A-), L (N ) ), (L(N), Lj n f(N ))} = (Li n j(N), L(TV)) n <L(7V), L mf (N)). That is, for the result of append (/, g) to be a finite-length list, / cannot have an undefined tail and g cannot have an undefined tail. □ 5 Some Remarks How expensive is it to carry out the inverse image analysis described here? Also, how expressive is this analysis? In this section, We would like to make some remarks regarding these two questions. We will also state the relationships between this work and previous works, and outline other possible applications of this work. 5.1 The Time Complexity of Inverse Image Analysis At first glance it seems that backward analysis by inverse images is very expensive. It is not so. The cost of approximating an inverse image of a specific function / is only as expensive as computing V'c(f ) &om the program text defining /. To verify this claim, let us first estimate how expensive it is to get V'cif)- Suppose / is a function from domain D a to Dp. Then V'cif) i s a continuous function from V'c{D a ) to V'c(Dp). In the cases that the program defining / is recursive, we will need to find an element in the ab¬ stract domain V'c(Da) — ■ Vc(Dp) which serves as the least fixed point of a particular function in the abstract domain (V'c(Da) —> V'c(Dp)) (V'c(Da) —*■ V'c(Dp))- The worst cases time complexity for this least-fixed-point-finding procedure is proportional to the height of the domain V'c(D a ) V'c(Dp). It can be shown that the worst cases will need 0( \V'c{D a )\-heightfP 1 c(Dp))) time, where \V'c(D a )\ is the size of V'c(D a ) and height(V'c(Dp)) is the height of V'c{Dp}. By Definition 3.20, the formulation of an abstract inverse image function of / is essential free if V'cif) i s given. A naive computation of an inverse image will involve the enumeration of all the 14 elements in the abstract domain V'c(D a ), which will take time 0( \P' But this is only as expensive as (or, less expensive than) the 0(\V' c(D a )\ ■ height(V' c(Dp))) time to compute V'c(f). Let us draw a table to compare the time complexity of an abstract interpretation and its inverse image analysis. The “preprocessing” time in the following table refers to the time complexity to compute V'c(f)■, or V l o(f~ 1 ), given the program text which defines /. The “query” time is the time complexity to compute (P'cif)) A, or (' P'oif -1 )) B, given A E Vc(D a ) and B E V'o(Dp). abstract interpretation inverse image analysis preprocessing time 0(\P' c (D a )\ ■ height(V'c(Dp))) 0(\Vc(D a )\ ■ height(V c (Dp))) query time 0(1) 0(\V' c (D a )\) Note that if an abstract interpretation is performed before an inverse image analysis, then the preprocessing time for the inverse image analysis is reduced to 0(1). Also note that we have greatly simplified the computation model to make comparison in the above table. For example, the query time for an abstract interpretation is not necessary 0(1) because it depends on the structure of P'c(f)- However, since both the queries in abstract interpretation and in inverse image analysis use the same approximation V'c(f), it is reasonable to take the 0(1) assumption to make the comparison clear. We also implicitly assume that the ordering predicate, C, takes only 0(1) time for a fixed finite abstract domain. 5.2 The Expressive Power of Inverse Image Analysis How expressive is the inverse image analysis described here? Before answering this question, let us first make a brief review of backward analysis as in literature so far. A context of a domain D as described in Hughes [11] can be viewed as a continuous function from D to D. Given a program P which defines a continuous function / from domain D a to domain Dp, and given a context cp of Dp , a backward analysis based on context will try to infer from program P , as precise as possible, a context c a of D a such that cp ° / = cp o / o c a . The projection notation as described in Wadler and Hughes [17] is similar to the context notation, except that projections are required to be idempotent and less defined than the identity context. Burn [5] further restricts projection to smash projection, which either maps an element in a domain D to the element itself or maps the element to Tp, to conclude some interesting relationships between abstract interpretation and projection analysis. It is clear that context notation is more expressive than projection notation, and projection more expressive than smash projection. One important characterization of previous works is that they often operate on lifted domains and often require the functions between these lifted domain to be strict in the newly added least defined element. Also note that for a context-based (or projection-based, or smash-projection-based) backward analysis to work effectively, we must restrict the collection of contexts (or projections, or smash projections) to a finite set. We must also order these contexts properly and approximate any give context to an restricted context in the safe direction. It turns out that Scott-closed/Scott-open subsets have the exactly expressive power of strict smash projections. 3 Let domain lifted(U) be the lifted domain of a domain D. Then the poset of all the strict smash projections from lifted(D) to lifted(D) can be shown to be isomorphic to Vc(D). That is, each strict smash projection maps, beside J-iift e d(£)), the elements in a lifted Scott-closed subset of D to T ;; teC (/; . and maps each element of the lifted complement Scott-open subset to itself. Likewise, each Scott-closed subset of D defines a strict smash projection from lifted(D) to lifted(D) which maps, beside -Liift e d(), those elements in the lifted Scott-closed subset to Tiifted(D); and maps each element in the lifted complement Scott-open subsets to itself. 3 We would like to thank an anonymous functional programming researcher for pointing out this connection. Bum probably knows this, although it is not stated in [5]. This is a direct consequence of Vc(D) — D — 2 (Barendregt [3, page 20, exercise 1.3.11 (ii)]), where 2 is the two element domain. 15 Although the Scott-closed/Scott-open powerdomain possess the same expressive power of strict smash projections, it does have its advantage. One of the advantages is it leads to a natural extension to higher-order cases. Previous works have not be able to give a successfully account of higher-order backward analysis based on context (or projection, or smashed projection). By using Scott-closed/Scott-open powerdomains, we are also able to explain some special con¬ structions/restrictions in previous works. For examples, previous works lift a domain to include a new least defined element which symbolizes the computation which leading to an “abort”. And the functions between these lifted domains must be strict (or _L-reflexive in some cases) on this newly added least defined element. By using Scott-closed powerdomains, it becomes clear that the empty set element 0 in domain Vc(D) and V'c{E>) states exactly the “abort” situation; which simply says that no element in D is appropriate. Also, for a continuous function / from domain D a to Dp, it is shown that Vc(f ) and V'cif) are 0-reflexive (Lemma 3.24). It is a natural consequence in the theory of Scott-closed/Scott-open powerdomain, not as a restriction in the settings of previous works. The relationship between forward analysis and backward analysis is clearer too. For example, both Burn [5, page 154, Theorem 3.1] and we (Corollary 2.12 and 3.23) state the relationships between forward analysis and backward analysis. We think our representation is simpler. The restriction of T-reflexive abstraction maps and strict functions are gone too in our development. They are natural consequences of the theory of Scott-closed/Scott-open powerdomain. Let us draw some tables to illustrate some simple contexts and their counter-parts in Scott- closed/Scott-open powerdomains. The following table lists four contexts and their effects on the elements in a lifted domain. a FAIL ABSENT STRICT IDENTICAL e a e lifted d,d Ed -Llifted(J9) lifted _l_£) lifted d lifted d lifted Ed -Llifted(D') lifted Ed -Llifted(D') lifted _l_£) -Llifted(D) -Giftedf D) -Llifted(D') -Llifted(D') -Llifted(D) The following table shows how the four contexts are described by the approximating Scott-closed powerdomain V'c{E>) = {D, {0} and its complement Scott-open powerdomain. Scott-closed Scott-open FAIL D 0 ABSENT - - STRICT {-Lf} D-{E d ) IDENTICAL 0 D Note that ABSENT is not a smash projection and it cannot be described by Scott-closed/Scott-open subsets either. 5.3 Beyond Strictness Analysis The inverse image analysis, as described so far in this paper, always assume that the abstract interpretation is done on Scott-closed powerdomains; hence, the backward analysis is done on Scott- open powerdomains. However, it is not difficult to develop an abstract interpretation based on Scott-open powerdomains, and to have the backward analysis done on Scott-closed powerdomains. This should not come as a surprise since a Scott-closed powerdomain Vc(E>) is isomorphic to the complement Scott-open powerdomain Vo(E>). We should emphasize that a Scott-open based abstract interpretation is also a useful development. For example, it is quite useful in the constant- propagation problem. They are many possible applications of inverse image analysis, besides backward strictness anal¬ ysis, since it is a generic scheme for doing backward analysis. Given any correct and computable abstract semantic of a non-strict higher-order functional programming language, we are able to transform it into a backward version that is also correct and computable. It is not difficult to image 16 many non-standard semantics which correspond to some specific optimization opportunities. If there is a correct (Scott-closed/Scott-open powerdomain based) abstraction of an specific non-standard semantics, then, by using inverse image analysis, a correct backward version of the abstraction comes for free. 6 Conclusion We have proposed a method for performing backward analysis based on inverse images of abstract higher-order functions. Our method differs from previous works on backward analysis [8] [11] [17] in two major ways. First, our method deals with a program’s extensional representation, rather than its intensional (textual) representation. That is, for a program P, we analyze the inverse image of the function fp, which is the semantic denotation of P, as well as approximation versions of fp. This approach leads to a very clean concept for backward analysis. It frees us from the necessity of analyzing the text of a program. However, a forward analysis of a program P. based on its text, is needed before we perform backward analysis. Secondly, we are able to do backward analysis on higher-older functions in a very natural way. Also, we are able to capture the interdependency of arguments of a program regarding their effects on the result of the program. We view this an improvement over previous works, which blend abstract interpretation and backward analysis at the same time to get these results. Again, our approach (performing forward analysis to get an extensional representation of a program, then performing a backward analysis on the extensional representation) seems to be cleaner. 7 Acknowledgments The authors wish to thank Fritz Henglein, Peter Sestoft, Kei Davis and John Hughes for their assistance. A Bounded—Complete a;—Algebraic CPOs and Scott—Closed/Scott—Open Powerdomains A cpo ( complete partial order) D is bounded-complete if, for all a,j£h, if there exists a c £ D such that a Qp c and b \Zp c, then a U b exists in D. If D is bounded-complete, it follows that every countable non-empty subset of a directed subset of D has the least upper bound in D. A cpo D is lo -algebraic if the set of compact elements in D , written as K(D), is countable, and if for every element d G D, the set {e | e £ K(D), e Qp d} is directed and d = ]_|{e | e G K(D), e Qd d}. An element e in a cpo D is compact if for every directed subset X C D such that e Cp |JA’, we have e \Zp x for some x G X. We list here some technical definitions and basic properties of bound-complete w-algebraic epos, as well as the properties of Scott-open and Scott-closed powerdomains. Some of their proofs can be found in Barendregt [3], Gierz, Hofmann, Keimel, Lawson, Mislove, and Scott [10], Schmidt [14], and Stoy [15]. Fact A. 36 Let D be a domain. Then, 1. if A G Tc(D), then A G Vo(D); 2. if A G Vo(D), then A G V C (D). □ Fact A. 37 Let D be a domain. Then, 1. Tc{D) is a lattice with X n Y — X fl Y and X U Y = X U Y for every X , Y G Vc[D ); 2. Vo(D) is a lattice with X fl Y = X U Y and X U Y = A' fl Y for every A', Y G Vo{D). 17 □ Furthermore, by tile following standard result in lattice theories, Fact A. 38 Let D be a poset. If for every subset X C D , there exists dY £ D, then D is a complete lattice with |JA' = I l{a | a £ D,x Qd a for all x £ A'}. □ we are able to show the following. Corollary A. 39 Let D be a domain. Then, 1. Vc(D) is a complete lattice with dY = (~) X and \_\X = p|{y | Y £ Vc{D),Y D (J X } for every subset X C Vc(E>); 2. Vo(D) is a complete lattice with dt’ = (J X and \_\X = (J{y | Y £ Vo(D),Y C f]X] for every subset X C Vo{D). □ Remark A. 40 Let D be a domain. Then, it is not necessary true that \_\X = (J X for every subset X C Vc(D); since {JX may not be in Vc{D). It is not necessary true either that \_\X = p| X for every subset X C Pq(D): since f]X may not be in Vo{D). Also, we have T v c (p) — 0 and T v c (d) — D. It follows that T v 0 (D) — D and T -p 0 (D) =0- n Definition A. 41 Let D be a domain. Let d £ D and X C D. Define 1. [d= {a- | x £ D, x Q d d}; 2. | d = {x \ x £ D,d Qd x }; 3. [X = {y \ y £ \x,x £ A}; 4. f A - {ij | !) £ ? x. x £ A}; 5. X c = C]{Y | Y £ V C (D),Y D X} □ l d is usually called the lower set of d; j d is called the upper set of d. Note that [ d is Scott-closed in D for each d £ D. However, j d is Scott-open in D iff d is a compact element in D. Also, by definition, X c is the least Scott-closed subset of D which contains X. Some properties of lower/upper sets are stated in the following facts. Fact A. 42 If O is open in D, then O = [JO for some subset O C {f e \ e £ K(D)}. □ Fact A. 43 Let D be a domain. Let x £ D and A', T' C D. Let X be a directed subset of Vc(D). Then, 1. if x £ X c but x ^ J, A, then x cannot be compact; 2. if A C y, then A c Q Vo (d) Y c ; 3. |J* = (U*) C ; 4. if A' C [JX and X is directed, then |JA £ \_\X. □ We now show that both Vc{D) and Vo(D) are domains if D is a domain. Lemma A. 44 Let D be a domain. Then 1. Vc(D) is a domain with K(Vc(D)) — {(JT | X is a finite subset of {j e | e £ A'(D)}}; 2. Vo{D) is a domain with K(Vo{D )) = {E \ E £ K(Vc(E>))}. □ 18 Proof. We need to show that both Vc{D) and Vo{D) are bounded-complete and w-albebraic. Since both Vc{D ) and Vo{D) are complete lattices, they are bounded-complete. It remains to show that both Vc(D) and Vo{D) are w-algebraic. Let £ = \ X is a, finite subset of {J. e | e G A'(D)}}. 1. We will show that £ C K(Vc{E>)), £ is countable, and for every A' G Vc{E>), X - [_|{A | E G £, E C-p c (.D) A'}. Then, it follows that Vc{D) is w-algebraic with K(Vc{D)) = £. Suppose £ <£. K(Vc{E>)). Then there exists a E £ £ such that E is not a compact element of Vc{D). Therefore, there exists a directed subset X C Vc(E>) such that E C-p c (.D) \_\X but E %.V C {D) A’ for every A’ G X. That is, there exists a compact such that e G \_\X but e (^y^X. But, by Fact A.43, this cannot be true. Therefore, £ C K(Vc{D)). It is easy to show that £ is countable, given that K{D) is countable. It remains to show that for every A' G Vc{E>), the set {E \ E ^£,E Q-p c (D) A} is directed and A' = jJlA | E G £■ E C-p c (£>) A'}. Let £q = {E \ E G £, E C-p c (£>) A'}. It is clear that £o is directed. It suffices to show that A Q-p c (D) [J^o to complete the proof. Suppose that A' U'S’o- Then, there exists a non^compact x G A' but x ^ j_|£o. Since D is algebraic, we have x = \_\E, where E = {e \ e G K(D),e x} is directed. But E C jjifo- Hence, x = JJA G \_\£o, a contradiction. We conclude that Vc(D) is w-algebraic. 2. Let X = {A, | 1 < i < n} be a directed subset of Vo(D). Let X denote the directed subset {Aj | 1 < i < n] of Vc(D). We first show that |JA = \_\X. U£_ = [J{^\ Y ev 0 (D),Y Cf]X] = Ci{Y \Y eVo(D),Y_Qf\X} = f]{Y' I Y 1 eVc(D),Y> Cf)X] = ni y/ \Y' eVciD)^ C\JX] = nij' l y/ ev c (D),Y' D(J*} = u* It remains to show that K(Vo(E>)) = {E \ E G K(Vc{E>))} = £. It suffices to show that £ C I\{Vo{D )) and for every A G Vo(E>), we have A' = ]_|{T? | E G £, E Q-p 0 (D) A}. Suppose that £ <£. K(To{E>)). Then there exists a E G £ such that E $ K(Vo(E>)) => there exists a E G £ and a directed subset X C Vo(D) such that E Qvo(D) U X > b ^t E % Vo ( D ) X for every A G X =>• there exists a £G f and a directed subset X C Vo(E >) such that E Qvc(D) U X > but E %v c {D) X for every A G X =>• there exists a E G £ and a directed subset X' C Vc{D) such that E Qv c (D) U*', bllt E %v c {D) X' for every X' G X’ . But this cannot be true because each element in £ is a compact element of Vc(E>). It remains to show that for every A' G Vo{D), we have A' = |_|{Ti7 | /. G £.'E Qv 0 (d) A'}. Let £ 0 = {E | E C £. E Q-p 0 (D) A}. It suffices to show that A' Q-p 0 (D) U^o to complete the proof. 19 Since X G Vc{D) and Vc(D) is u>-algebraic with K(Vc(D )) = £, we have X ^iVc(D) U{a | Ee£,E ^Vc(D) A} X ET’c (D) U{£ | E<ES,E ^iVa(D) A} X ^Vc(D) U{^ \ Me£,E ^Vo(D) A} => X ^Vc(D) U^O => X ^Vc(D) U^O => X —Vo{D) U^o. The following two facts deal with continuous functions between domains. Fact A.45 Let D a and Dp be domains. Then / is a continuous function from D a to Dp iff / x — |_|{/ e | e G K{D de ),e Q Da a;}, where x G D a . □ Fact A.46 D a —? Dp, the continuous function space from D a to Dp, is a domain if both D a and Dp are domain. □ B Image Functions and Inverse Image Functions Lemma B.47 let D a and Dp be domains. Then both Vc(f ) and Vo(f _1 ) are well-defined and continuous for every continuous function / G D a —>■ Dp . □ Proof. By Definition A.41, Vc(f) is well-defined. By Fact 2.5, Vo(f~ 1 ) is well-defined. It remains to show both Vc(f ) and Vo{f~ l ) are continuous. 1. In order to prove that Vcif ) is continuous, it suffices to show that (Vc(f)) QvaW?) U (W)){£h where £ = {E \ E G K(Vc(D a )), E A'}. Since C (J {(Vc(f)) {£}), by Fact A.43, we have (/{U^» C (U((^(/))i^)) C =U(^(/))^}- Also, we have (Vcif)) = (_|^}) c . Therefore, it suffices to show that (/{[j£l) C Qvc{d,) (/{ \j£}f to complete the proof. Suppose that it is not true. Then, there exists a b G (/{U^}) C but ^ ^ (/{U^}) C - Since Dp is w-algebraic, we let b = |_|B, where B = {e* | ei G K(Dp), e, G (/{] |^}) ,e s Q Dp b} = {e* I a G K{Dp),ti G f{\_\£},ei Q D/3 6} (by Fact ATS). For each e; G B, we know that e; = / a 2 - for some a, G [_]£. Again, since D a is w-algebraic, we let ai = IJAj, where j | Cj j G X(D a ^, G | | U-i j - = { e i,j I e i,j e K(D a ),e itj G a,} (by Fact A.43). 20 Hence, f{Ai} C f{{J£} for each A { . Therefore, we get (J /{TJ £ (/{1J^}) C - Since / is continuous, we have e; = / U A i ~ U f\ A i] e (f{[j£}) C . Hence, B C (/{ [j £}) c . And we have b = [JB £ (/{U^D** a contradiction. 2. We want to show that (w 1 )) U^ = U(^(r 1 ))w, for every directed subset y C Vo{Dp). By Fact A.42, each Y £ y can be written as (J{'f e | e £ K(Dp ), e £ Y}. We then have = [j{Y \Y eTo(Dp),YCf]y} = Ul y \Y eVo(Dp),Y Q[}{\e \ e e K(Dp),e e f]y}} = \J{U\eeK(D p ),eef]y}- On the other hand, we have u {Vo{r i )){y} = {j{Y\YeVo(Dp),YCf](Vo(f- 1 )Uy}} = {J{Y\YeVo(D p ),YCf-'{f)y}}. Hence, it suffices to show that r/W : )) Uit e I e e K ( D f>l e e = U y I y e ^o(Dp),Y c rMf) to complete the proof. Let e x be a compact element in D a . Then, &e(B 0 (r 1 )} {J{U\eeK(D p %eef)y} there exists e y £ K(Dp) such that e y Qd 3 f £x and e y £ p |y <£> there exists e y G K(Dp) such that f e x £ \e y and '\ e x C f~ 1 {'\e y } C C Uin V C /V-i/A.j.V C / : .' ' Since both of the above two sets are Scott-open, by Fact A.42, we conclude that they are the same. O Lemma B.48 Let D a and Dp be domain, / £ D a —» Dp, and B be closed in Dp. Then {* I * G D a ,fx G B} = |J{A | X G V c (D a ), (V c (f))X Qv c (d,) B}. □ Proof. Let X = {A' | X £ Vc{D a ), (Vc{f))X Q-PciDp) B}. We will show that | x £ D a , fx £ B} C |_]T and |_|T C {a: | x £ D a , /a; £ B}. We first note that X is closed in Vc(D a ) by Corollary 2.6. We will show that X is also a directed subset of Vc[Da)- Therefore, \_\X £ X. By the definition of X, we then have (Vc(f))(\_\X) Q-p c (Df,) B. That is, (Vc{f))(UX) C B. To show that X is a directed subset of Vc{D a ), we observe that for every A'o, A'i £ X, • A'o U A'i = A'o U A'i is closed in Vc(D a ) and . (V c (f)){ A'o □ AY) = (V c (f))X o U (V c (f))X 1 Qv c (d,) B. 21 That is, A'o U X\ G X; hence, X is directed. Suppose that a G \_\X. Then / a G {/ x \ x G D a ,x G ( |A 1 }. But {/ x \ x G D a , x G |_]T} — (-Pc(mUX) — B- We then have / a G B; hence, a G {« | a; G D a ,f x G 5}. That is, |_]T C {a- | a; G D a ,fx G 5}. Suppose that a G {* | i G D a ,fx G 5}. Then ('Pc(/)) J. a E7-p c (.D,) B. By the definition of X, we have Ja G X. Therefore, [a Q-p c (D ) \_\X; hence, a G \_\X. That is, {a? | a; G D a ,f x G B} C U-V- This completes the proof. O References [1] 17th Annual ACM Symposium on Principles of Programming Languages. A. C. M., January 1990. San Francisco, California, U. S. A. [2] Samson Abramsky and Chris Hankin, editors. Abstract Interpretation of Declarative Languages. Elliss Horwood, 1987. [3] Hendrik Pieter Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984. [4] D. Bj0rner, A. P. Ershov, and N. D. Jones, editors. Partial Evaluation and Mixed Computation. North-Holland, 1988. [5] Geoffrey L. Burn. A relationship between abstract interpretation and projection analysis (ex¬ tended abstract), pages 151-156. In [1], [6] Geoffrey L. Burn, Chris L. Hankin, and Samson Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7(3):249-278, 1986. [7] Kei Davis and John Hughes, editors. Function al Programming: Proceedings of the 1989 Glasgow Workshop. Glasgow, Scotland, U. K., Springer-Verlag, 1990. [8] Kei Davis and Philip Wadler. Backward strictness analysis: Proved and improved, pages 12-30. In [7], [9] Peter Dybjer. Inverse image analysis, pages 21-30. In [13]. [10] Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980. [11] John Hughes. Backwards analysis of functional programs, pages 187-208. In [4]. [12] Gilles Kahn, editor. Functional Programming Languages and Computer Architecture. Portland, Oregon, U. S. A., September 1987. Lecture Notes in Computer Science, Volume 274, Springer- Verlag. [13] Thomas Ottmann, editor. Automata, Languages and Programming. Karlsruhe, F. R. G., July 1987. Lecture Notes in Computer Science, Volume 267, Springer-Verlag. [14] David A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986. [15] Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Lan¬ guage Theory. The M. I. T. Press Series in Computer Science. M. I. T. Press, 1977. [16] Philip Wadler. Strictness analysis on non-flat domains (by abstract interpretation over finite domains), chapter 12, pages 246-265. In [2], [17] Philip Wadler and R. J. M. Hughes. Projections for strictness analysis, pages 383-407. In [12]. 22