Skip to main content

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