Logical optimality of groundness analysis.
In the context of the abstract interpretation theory, we study the relations among various abstract domains for groundness analysis of the logic programs. We reconstruct the well-known domain as a logical domain in a fully automatic way and we prove that it is the best abstract domain which can be set up from the property of groundness by applying logic operators only. We propose a new notion of optimality which precisely captures the relation between and its natural concrete domain. This notion enables us to discriminate between the various abstract domains for groundness analysis from a computational point of view and to compare their relative precision. Finally, we propose a new domain for groundness analysis which has the advantage of being independent from the specific program and we show it optimality. Copyright 2002 Elsevier Science B.V.
Introduction
In the logic programming field, groundness is probably the most important instance
of static analysis. Many domains have been proposed in order to study
groundness of (pure) logic programs, from the very simple domain G by Jones
and Sndergaard [13], to more complex ones, like
The latter is the most widely used, since it is able to characterize both pure
groundness, i.e., if a variable is instantiated to a ground term, and groundness
relations between different variables, i.e., whether the groundness of a variable
depends on the groundness of other variables. In this paper, we show a different
way of building the abstract domain Pos, which directly comes from the definition
of groundness. From our construction, we derive many useful properties,
such as a normal form for its elements and a result of optimality. Moreover, we
answer to some open questions such as "why Pos is considered optimal" from a
computational point of view.
1.1 Motivations
Pos is certainly a well studied domain for groundness analysis of logic programs
[13,15,4,2]. In standard literature, the domain Pos is built in 3 steps: First
consider the set of (classic) propositional formulas built from a finite set V ar and
connectives ";  and ); second select only the positive formulas (which are true
when all variables are set to true); third quotient w.r.t. classic logical equivalence.
The domain so obtained is then related to the concrete one (sets of substitutions
closed by instantiation) through a suitable concretization function, explicitly
proving that it induces a Galois insertion. This method of constructing domains
suffers from many drawbacks. The most important one is that the domain has to
be "invented" in some way (a procedure which is usually not formally related to
the property we analyze) and then has to be explicitly proved that the domain
so created is an abstraction of the concrete one and is actually useful for the
analysis. As logic programs compute substitutions and groundness is a property
closed by instantiation, the most natural choice for the concrete domain is sets
of substitutions closed by instantiation, denoted by  # (Sub).
Propositional formulas used in the construction of Pos do not reflect the
logic in the concrete domain. In order to understand this apparent asymmetry
between Pos and its natural concrete domain, we just need to make the following
observations.
- From an algebraic point of view, Pos is a boolean algebra (with connectives
therefore we can not inherit Pos algebraic
properties from the concrete domain.
- When we try to compare the logical operations on Pos to the corresponding
ones on  # (Sub), we find that only the meet (") on Pos come from the
meet on  # (Sub) (set intersection). In fact, the join () of Pos is not the
restriction of the concrete join (set union). For instance, as proved in [8],
the concretization of the formula x  (x , y) is not the union of the concretization
of x and x , y. Moreover, in the concrete domain, we can not
have a notion of (classic) implication, since it is not a boolean algebra. So
there is no way to inherit the implication ) from a corresponding operation
of  # (Sub).
- Finally, the last step in the construction of Pos is the quotient w.r.t. classic
logic equivalence. For the same motivation in the previous point, it is impossible
to define such an equivalence on  # (Sub) (otherwise it would be a
boolean algebra). Therefore, also this step in the construction of Pos does
not come from the properties of the concrete domain.
1.2 The intuition behind our reconstruction of Pos
The main problem of the previous construction is that  # (Sub) is not a boolean
algebra. In particular, it does not allow us to define an operation of classic
implication. Instead,  # (Sub) is rich enough to allow us to define a notion of
intuitionistic implication (or relative pseudo-complement). The intuitionistic implication
is a generalization of the classic one which leads to a weaker notion of
complement called pseudo-complement. Moreover, intuitionistic implication is
independent from the join operation , i.e., a does not hold. Thus
becomes an algebra with three operations ", [ and ! which correspond
precisely to the ",  and ! of intuitionistic logic.
In this paper we show that Pos can be constructed by using only the definition
of groundness. The simplest domain defining the property of groundness
is the least abstract domain containing V ar, which is by Jones and
Sndergaard [13], where each variable v denotes the set of substitutions which
ground v. In the first part of the paper, we show that Pos is exactly the least abstract
domain which contains all the (double) intuitionistic implications between
elements of G
\Gamma!
\Gamma! G). This result generalizes a similar one on
in [11] which proves that Def is the least abstract domain which contains
all the intuitionistic implications between elements of G, i.e.,
\Gamma! G.
Our formalization of Pos enjoys the following properties.
- Pos is built by using only the definition of groundness (the domain G) and the
properties of the concrete domain. We need no more to use boolean algebra,
positive formulas, nor to quotient the resulting set. The construction of the
abstract domains G; Def; Pos now follows a unique, precise logic: The logic
structure of the concrete domain. Moreover, we do not need anymore to
prove that these domains are indeed abstractions of the concrete one, since
it follows by construction. Also the relations among all the domains are now
automatically derivable.
- The operations which characterize Pos are now exactly the same of the
concrete one: " and ! in Pos are the restrictions of " and ! in  # (Sub)
and no other operation is considered in Pos.
We immediately obtain a theorem of representation for Pos which states
that every element of Pos is an implication between two elements of
by using the characterization of every element of Pos is an implication
of implications between elements of G, independently from the cardinality of
ar.
- This result allows us to answer to some open questions on Pos. The join on
Pos differs from the join on  # (Sub) but, in some cases, they coincide.
W hy Pos contains exactly those concrete joins?
Our representation theorem states that the join on Pos is precise if and only
if it can be written as an intuitionistic implication.
Since Pos is now a sub-algebra of  # (Sub) w.r.t. the " and ! operations,
all the properties of Pos are directly derivable from the properties of the
concrete domain. In particular, since  # (Sub) is a model of intuitionistic
propositional logic, it follows that also Pos is. Therefore we gain from logic
an axiomatization for Pos.
In the second part of the paper, we use our formalization of Pos in order to
understand why Pos can be considered a "good" domain. To this end, we try
to refine Pos. We wonder which is the domain which contains the implications
between formulas in Pos and find out an important closure property of Pos, i.e.,
that Pos \Psi
This implies that Pos can not be further refined w.r.t.
intuitionistic implication. Therefore Pos is exactly the least abstract domain
closed w.r.t. " and !.
We then consider the disjunctive completion of Pos,
(Pos), which includes
all unions of formulas in Pos. [8] proved that Pos is strictly contained in
(Pos).
We try to refine this result by allowing implications between disjunctive formulas
and prove that it can not be further refined since
\Gamma!
b (Pos).
1.3 Related work
Many works have been devoted to the study of groundness analysis. The first
ones concentrated much on the definition of groundness and basic properties
[13,7], while the last ones studied different characterizations of various abstract
domains. [15] proposed propositional formulas to represent groundness relations.
Many authors followed this approach [4,2] and contributed to develop and study
the domains others focused on the abstract operations or
slightly different characterizations [16,14].
All these authors share the same They construct abstract domains
independently from the property to be analyzed (i.e., from the semantics or concrete
domain) and then prove some properties of the abstraction. Their attention
is focused entirely on the representation of formulas in the abstract domains. This
forces to work always up to isomorphism.
Our idea is to concentrate exclusively on the property of groundness. We
re-construct the domain Pos in a systematic way and show that it is possible
to avoid ad hoc characterizations in the construction process of new domains.
Our work is based on the Heyting completion refinement operator [11]. A first
example in this direction has been presented in [11], where Heyting completion is
used to construct the abstract domain An attempt of building the domain
Pos starting from the disjunctive completion of the domain G (by Jones and
Sndergaard [13]) is shown in [11]. Also in this case, the construction does not
directly come from the property of groundness, but from a domain more complex
than G.
Preliminaries
Throughout the paper we assume familiarity with lattice theory (e.g. see [3,12]),
abstract interpretation [5,6,17] and logic programming [1].
2.1 Notation and basic notions
and C be sets. A n B denotes the set-theoretic difference between A
and B, A ae B denotes proper inclusion and, if X ' A, X is the set-theoretic
complement of X . The powerset of A is denoted by (A). If A is a poset, we
usually denote by A the corresponding partial order. A complete lattice A
with partial ordering A , least upper bound A (join), greatest lower bound
"A (meet), least element ?A , and greatest element ?A , is denoted by hA; A
being A complete, the join and meet operations
are defined on (A). If A is (partially) ordered and I ' A then # I
denotes the set of order-ideals of A, where I ' A is
an order-ideal if I =#I .  # (A) is a complete lattice with respect to set-theoretic
inclusion, where the join is set union and the meet is set intersection. We write
to mean that f is a total function from A to B. In the following
we sometimes use Church's lambda notation for functions, so that a function
f will be denoted by x:f(x). If C ' A then Cg. By
we denote the composition x:g(f(x)). Let
lattices. A function f : A 7\Gamma! B is additive
if for any C ' A,
2.2 Abstract interpretation and Galois connections
The standard Cousot and Cousot theory of abstract interpretation is based on
the notion of Galois connection [5]. If C and A are posets and ff : C 7\Gamma! A,
are monotonic functions, such that 8c 2 C: c C fl(ff(c)) and 8a 2
A: ff(fl(a)) A a, then we call the quadruple hC; fl; A; ffi a Galois connection
(G.c.) between C and A. If in addition 8a 2 A:
is a Galois insertion (G.i.) of A in C. In the setting of abstract interpretation,
C and A are called, respectively, concrete and abstract domain, and they are
assumed to be complete lattices. Any G.c. hC; fl; A; ffi can be lifted to a G.i.
by identifying in an equivalence class those objects in A having the same image
(meaning) in C.
Let L be a complete lattice hL; playing the role of the
concrete domain. An (upper) closure operator on L is an operator ae : L 7\Gamma! L
monotonic, idempotent and extensive (viz. 8x 2 L: x L ae(x)) [17]. Each closure
operator ae is uniquely determined by the set of its fixpoints, which is its image
ae(L). ae(L) is a complete lattice with respect to L , but, in general, it is not a
complete sublattice of L, since the join in ae(L) might be different from L . ae(L)
is a complete sublattice of L iff ae is additive.
is the set of fixpoints of a closure operator on L iff X is a Moore-
family of L, i.e. ?L 2 X and X is completely meet-closed (viz. for any non-empty
X). For any X ' L, we denote by
c
(X) the Moore-closure of X ,
i.e. the least subset of L containing X , which is a Moore-family of L. We denote
by hMoore(L); v; u; t; f ? g; Li the complete lattice of all Moore-families of L.
The ordering v is the inverse of set inclusion ('), u is the least Moore-family
which contains set union, (X; Y:
c
t is set intersection (").
The equivalence between G.i., closure operators and Moore-families is well
known [3]. However, closure operators and Moore-families are often more practical
and concise than G.i.'s to reason about abstract domains, being independent
from representation choices for domain objects [6]. Any G.i. hL; fl; A; ffi
is uniquely determined (up to isomorphism) by the closure operator fl ffiff, and,
conversely, any closure operator uniquely determines a G.i. (up to isomorphism).
The complete lattice of all abstract domains (identified up to isomorphism) on
L is therefore isomorphic to Moore(L). The order relation on Moore(L) corresponds
precisely to the order used to compare abstract domains with regard to
their precision: If A and B are abstractions of L, then A is more precise than B
Moore-families.
2.3 Logic programming
Let V be a (denumerable) set of variables. We fix a first-order language L, with
variables ranging in V . T erm is the set of terms of L. For any syntactic object
s, vars(s) denotes the set of its variables. A term t is ground if
The set of idempotent substitutions, i.e., finite mappings from V to terms in
L, is denoted by Sub. Substitutions are lifted to terms in the usual way. If ff is a
substitution, dom(ff) denotes the set f v 2 V j ff(v) 6= v: g, which is always finite
by definition. By fi ffi ff we denote the substitution v:ff(fi(v)). Objects in Sub
are partially ordered by instantiation: a  b iff 9' 2 Sub: a = b'.
2.4 Intuitionistic logic and Heyting algebras
Let L be a complete lattice and a; b 2 L. The pseudo-complement (or intuitionistic
implication) of a relatively to b, if it exists, is the unique element
such that for any x 2 L: a "L x L b iff x L a ! b. Relative
pseudo-complements, when they exist, are uniquely given by a
g. A complete lattice A is a complete Heyting algebra (cHa)
if it is relatively pseudo-complemented , that is a ! b exists for every a; b 2 A.
From a logical point of view, an Heyting algebra L is an algebra equipped with
three operations which satisfies the following equations
for every a; b; c 2 L:
a
a
Meet, join and relative pseudo-complement of Heyting algebras precisely correspond
to conjunction, disjunction and intuitionistic implication of intuitionistic
logic (see Birkhoff [3]).
An example of cHa is the complete lattice h # (Sub); '; [; "; Sub; ;i. The
logical operations  and " correspond to [ and " operations (set intersection
and set union). Given a; b 2  # (Sub), the intuitionistic implication a
is also given by ([3])
Example 1. Let x; and
g.
For instance, given a binary functor f , the substitution f x / f(y; w) g belongs
to does not.
3 Domains refinements
3.1 Reduced product
The reduced product [6] of abstract domains corresponds to the meet operation
(u) of closure operators. Given two abstract domains X;Y , the reduced product
of X and Y , denoted by X uY , is the least abstract domain which includes both
3.2 Disjunctive completion
The disjunctive completion [6] of an abstract domain A is the least (most ab-
stract) domain which includes A and which is a complete (join-)sublattice of L,
viz. no approximation is induced by considering the join of abstract objects. The
disjunctive completion of A is defined as the most abstract domain which is an
additive closure and includes A (cf. [6,10]):
and X is additive g:
Proposition 2. If L is a cHa and A is finite,
g.
3.3 Heyting completion
Heyting completion [11] is a refinement operator which has been recently introduced
in order to logically interpret the Cousot and Cousot's reduced power
refinement [6]. In this section we recall the definition and some basic results on
Heyting completion refinement [11]. The aim of this refinement is to enhance
domains to represent relational or negative information. The idea is to enrich an
abstract domain by adding all the relative pseudo-complements (or intuitionistic
implications) built from every pair of elements of the given domain. From a
logical point of view, the new domain is the collection of intuitionistic formulas
built from the " and ! connectives, without nested implication.
For the sake of simplicity, we recall the definition only in case the concrete
domain L is a cHa. Given two abstract domains A and B, the Heyting completion
of A wrt B (denoted by A \Psi
\Gamma! B) is precisely captured by the least Moore family
containing all the relative pseudo-complements (without nesting):
A \Psi
The Heyting completion refinement is reductive on the second argument
\Gamma! A v A) and argumentwise monotonic (if A v B and C v D then
A \Psi
\Gamma!
\Gamma! D).
We recall some basic algebraic properties of Heyting completion with respect
to other domain operations. In particular, we consider reduced product (u) and
disjunctive completion (
of abstract domains. In the following of the paper,
Proposition 3. Let L be a cHa.
1. A \Psi
\Gamma! (B u
\Gamma! B) u
\Gamma! C)
2.
\Gamma! (B \Psi
\Gamma! C)
3.
A is finite.
Groundness:
Many domains have been proposed in order to study groundness of pure logic
programs. If V ar is the (finite) set of variables of interest, the simplest one is
ar), due to Jones and Sndergaard [13], where each ar denotes the set
of substitutions which ground every variable in V . This domain is certainly the
most intuitive one and represents exactly the property we want to analyze, since
it is built from the definition of groundness itself. Unfortunately, G is not very
useful for groundness analysis, since it fails in capturing the groundness relations
between different variables, i.e., the domain is able to represent the "result" of
a groundness analysis, but not to be used for "computing"' the analysis itself.
Other domains, based on (classic) propositional logic, have been proposed in
order to enrich G. Pos is the most widely used domain for groundness analysis
[13,15,4,2]. Pos is able to characterize both pure groundness, i.e. whether a
variable is instantiated to ground terms during program execution, and the relations
between the groundness of different program variables, providing in this
sense a clear example of relational analysis. Pos is the set of (classic) propositional
formulas built from V ar, by using the connectives
w.r.t. (classic) logical equivalence (KL). If we denote by F orm(V ar; ffi) the set
of formulas built from V ar by using the connective ffi, then Pos can be defined
in different ways [4,2]:
The domain Def [2] is built by considering all the formulas whose models
are closed under intersection and taking the quotient of this set w.r.t. (classic)
logical equivalence. Def has been also characterized as the set of formulas which
are conjunctions of definite clauses, always quotiented w.r.t. (classic) logical
equivalence.
i2I
ar g =KL
For the sake of notation, note that also the domain can be defined
as a domain of formulas by using the connective " to represent subsets:
We can relate the three domains to the concrete one by using the same concretization
function. The concrete domain considered in all cases is  # (Sub) (which is
a cHa). The interpretation of the connectives is the classical one: OE  / if and
only if / is a logical consequence of OE. We say that I ' V ar is a model for
OE, denoted I j= OE, if OE is true in the interpretation which assigns true to all
the variables in I and false to the other ones [2]. For the sake of simplicity we
grounds OE to denote f x 2 V ar j Sub. The
concretization function is [4]:
As usual, we shall abuse of notation and call G, and Pos the corresponding
subsets of  # (Sub): fl Sub (G), fl Sub (Def) and fl Sub (Pos).
5 Implicational groundness analysis
We start listing some well known facts about G, Pos. A first result on
the reconstruction of abstract domains as implicational ones was proved in [11].
The authors proved that is precisely the Heyting completion of G.
\Gamma! G (5.1)
In this section we prove that also Pos is an implicational domain which depends
only on the simple domain G. We shall prove that
\Gamma!
\Gamma! G. Therefore
by 5.1,
\Gamma! G. In order to prove it, we need to better understand
the relations among the logical operations in Pos and in  # (Sub). Since Pos is a
Moore family on  # (Sub), the meet operation (") on Pos must be the restriction
of the meet operation on  # (Sub), which is set intersection. It follows that, for
every formula OE i 2 Pos,
i2I
i2I
It is well known that the join operation () of Pos is not the restriction of the
concrete one on  # (Sub), which is set union [8]. But the isomorphism holds if
we consider variables only.
Lemma 4.
A similar result holds also for the implication. In general, the classic implication
does not coincide with the intuitionistic one. If we consider implications between
a conjunction of variables and a disjunction of variables only, then they
are isomorphic.
Lemma 5.
i2I
i2I
The idea is to find a normal form for elements in Pos which allows disjunction
only between variables and (classic) implication only between a conjunction and
a disjunction of variables. It is well known that every (classic) formula can be put
in conjunctive normal form, i.e., it can be written as conjunction of disjunctions.
Moreover, every disjunction is a clause, therefore we can write it as a unique
implication, by putting all the negated variables on the left and the positive
ones on the right.
Lemma 6. In Pos, every formula OE is equivalent to a formula of the form:
The next step is to transform every formula in Pos into a formula of  # (Sub),
which is not a boolean algebra, as next example shows.
Example 7. In a boolean algebra (a " b)
and
ar. Consider in  # (Sub) the
g. We show
that strictly contained in (X " Y In fact, the
substitution belongs to (X " Y but not to (X ! Z)
nor to (Y ! Z).
We remind that  # (Sub) is a cHa [3], i.e., it is an algebra equipped with three
operations: Meet, join and intuitionistic implication. Meet and join on  # (Sub)
are set intersection and set union, while intuitionistic implication is given by
[3]. This allows us to deal with
formulas in  # (Sub) by simply using its operations as connectives.
The previous representation lemma, together with the isomorphism relations
shown in Lemmata 4 and 5, allows us to directly transform every formula of Pos
into a formula of  # (Sub).
Example 8. Let x  (x , y) be a formula in Pos. We look for its concretization
First we transform x (x , y) in normal form, which always
exists by Lemma 6.
Next we transform y ) x by using Lemma 5 and obtain fl Sub (y
which is a formula in  # (Sub).
As shown by the above example, we have a constructive method to transform
formulas in Pos into formulas in  # (Sub). Thus we obtain an image of
Pos on the concrete domain. Let
generic element of Pos (Lemma 6). The concretization of OE, fl Sub (OE) is precisely
Therefore, we can compute the concrete
image of Pos, as shown by the following theorem.
Theorem 9.
i2I
Our aim is to describe the domain Pos by using the Heyting completion refinement
only. Therefore, we look for a normal form for concrete objects which
uses meets and intuitionistic implications only, that is a normal form which does
not use the disjunctive operation. Note that, in the formulas on the concrete
domain, disjunctions are computed between variables only. The last step of the
construction is then to find a representation in  # (Sub) for unions of variables
in terms of intuitionistic implications. The next lemma shows that a (concrete)
disjunction is always equivalent to a (double) implication.
Lemma 10. Let
holds.
Therefore we obtain a transformation of formulas in Pos into formulas in  # (Sub)
which use " and ! only. In particular, note that the ! is used with at most
two levels of nesting. This suggests to construct Pos as a double implication.
Theorem 11.
\Gamma!
\Gamma! G
By 5.1 and properties of Heyting completion (Proposition 3.2 and monotonicity),
we immediately obtain:
Corollary 12.
\Gamma!
For domains G, and Pos are depicted below.
O O O O O O O
x y
x"y
true
O O O O O O O
O O O O O O O
O O O O O O O
x$y
x y
x"y
true
O O O O O O O
O O O O O O O
O O O O O O O
O O O O O O O
x$y
x y
x"y
true (x!y)!y
G G \Psi
\Gamma!
\Gamma! G
The first important consequence of Theorem 11 is that the domain Pos is
constructed by using only the definition of groundness (G) and the logical properties
of the concrete domain. We do not need to "invent" the domain, to prove
that it is actually an abstraction of  # (Sub), nor to prove that it refines G, since
all these properties hold by construction. In our framework, Pos arises as the
natural refinement of G and
Another consequence is the normal form for elements in fl Sub (Pos). This
result allows us to get rid of Pos and deal directly with fl Sub (Pos). In fact, when
we use a formula of Pos, actually we use an equivalence class w.r.t. (classic)
logic equivalence (KL). In our formalization, we do not need to use equivalence
1 Note that x i;k ; y j;k denote sets of substitutions.
classes any longer. Moreover, the "form" of concrete formulas is indeed very
natural and preserves the intuitive meaning of abstract formulas. Finally, note
that our normal form states that every formula in fl Sub (Pos) can be written
by using only two levels of nesting for the implication and no disjunctions. This
yields a precise upper bound to the length of the formula. It is worth noticing that
both the normal form and the upper bound are independent from the cardinality
of V ar.
6 Optimality of Pos
An abstract domain is a collection of points selected from the concrete domain.
Some points are used to represent the result of the analysis, while the other ones
are used only during the computation. For instance, in Pos the points which
represent the final result of groundness analysis are those in G only, since the
other ones do not provide groundness information. From equations 2.1, 2.2 and
2.3, it is obvious that only axioms 2.2 produce a result which belongs to G (i.e.,
formulas with conjunctions only). This suggests that an abstract domain, to be
optimal, should contain all and only those formulas which have an implicational
form, since implications only can be reduced to formulas in G. Therefore, to
obtain an optimal domain, we have to include all (and only) the implications
in the abstract domain. This concept is precisely captured by the notion of
implicational domain equation.
An abstract domain X is optimal w.r.t. a given domain A (and the operation
") if it is the least (most abstract) solution of the implicational domain equation
\Gamma!
The solution, which always exists, is the most abstract domain X which is more
concrete than A and is closed under \Psi
\Gamma!. Moreover, it turns out to be the most
refined abstract domain we can obtain by using Heyting completion refinement.
6.1 Solution to the equation
In the previous section, starting from the result
\Gamma! G, we have shown
that
\Gamma!
\Gamma! G. A question which naturally arises is: what is the
domain Pos \Psi
\Gamma! Pos? By Proposition 3.2 we know that Pos \Psi
\Gamma! G.
More generally, we wonder which is the most abstract domain which is more
precise than G and closed w.r.t. Heyting completion, i.e., which is the solution
to the equation:
\Gamma! X).
The next theorem answers both questions, since Pos is already closed w.r.t.
Heyting completion. Therefore, it is precisely the least (most abstract) solution
to the equation.
Theorem 13.
\Gamma! Pos
The theorem states that we can not further refine Pos with Heyting completion
refinement. This result comes from properties of substitutions, since, in the
concrete domain  # (Sub), join and implication operations are not completely
independent from each other (see Lemma 10).
Moreover this theorem yields a representation result for elements in Pos.
It precisely states that an element of  # (Sub) belongs to Pos if and only if
it can be written by using meets and implications only. This is much stronger
than the previous one since it completely characterizes the image of Pos. Differently
from previous characterizations of Pos [2,4], all these results hold on
the concrete domain, that is we can directly deal with formulas without using
any isomorphisms. Therefore, the concretization function fl Sub becomes, in our
construction, the identity function.
This result allows us to answer the question "why Pos is considered optimal
without being disjunctive", also from an intuitive point of view. From the
previous characterization, we know that a disjunctive formula belongs to Pos if
and only if it can be put in implicational form. From a logic point of view, the
elements useful for the analysis are implications only (as they can be reduced
by modus ponens). Since a good domain should contain all and only those joins
which are indeed useful, we would include those joins which can be reduced only,
which are exactly the joins that Pos contains. This explains the result in [9] that
Pos is complete (or precise) w.r.t.
b (Pos), that is Pos is the "optimal" domain
for groundness analysis.
6.2 On disjunctive completion
We proved that we can not further refine Pos by Heyting completion and [9]
showed that it is pointless to use
b (Pos) instead of Pos.
The idea is to refine Pos by disjunctive completion and then to refine it by
Heyting completion, i.e., to find the solution of the equation
b (Pos) u
\Gamma! X). The next theorem claims that also
b (Pos) is closed w.r.t. Heyting
completion.
Theorem 14.
\Gamma!
Therefore,
b (Pos) is the "biggest" domain we can obtain by disjunctive and
Heyting completion refinements and, in view of the result of completeness of
w.r.t.
b (Pos), we have proved that Pos is definitely the best domain for
groundness analysis.
Conclusions
In this paper we have reconstructed Pos by using the properties of the concrete
domain only. With our formalization, we automatically obtain the properties of
Pos by construction. We show that we can get rid of the construction of Pos
with positive formulas and equivalence classes and use directly the operations
which naturally arise from the concrete domain. Moreover, we show a result of
optimality for Pos by proving that it contains exactly all and only the elements
really useful to the analysis. This result is very surprising if we consider that the
domain Pos was built without following any formal notion of optimality.
The main feature of our construction is that it can easily be applied to other
kind of analyses of logic programs, since it depends only on the properties of the
concrete domain. We trust that (many) other analyses can be naturally formalized
in this way, in particular analyses of properties closed under instantiation,
such as type analysis, where the semantics (concrete domain) is always  # (Sub).



--R

Introduction to logic programming.
Boolean functions for dependency analysis: algebraic properties and efficient representation.
Lattice theory.
abstract domain for groundness analysis.
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
Systematic design of program analysis frameworks.
Static inference of modes and data dependencies in logic programs.
Improving abstract interpretations by systematic lifting to the powerset.
The Powerset Operator on Abstract Interpretations.
Compositional optimization of disjunctive abstract interpretations.
Intuitionistic implication in abstract interpretation.

A Semantics-based Framework for the Abstract Interpretation of Prolog
Denotational abstract interpretation of logic programs.
Abstract interpretation of logic programs: the denotational approach.
Precise and efficient groundness analysis for logic programs.
Some results on the closure operators of partially ordered sets.
--TR
Proofs and types
Static inference of modes and data dependencies in logic programs
Algebraic properties of idempotent substitutions
Logic programming
Abstract interpretation and application to logic programs
Precise and efficient groundness analysis for logic programs
Denotational abstract interpretation of logic programs
Improving abstract interpretations by systematic lifting to the powerset
A unifying view of abstract domain design
A logical model for relational abstract domains
The powerset operator on abstract interpretations
Abstract interpretation
Systematic design of program analysis frameworks
Compositional Optimization of Disjunctive Abstract Interpretations
Completeness in Abstract Interpretation
Intuitionistic Implication in Abstract Interpretation
"Optimal" Collecting Semantics for Analysis in a Hierarchy of Logic Program Semantics

--CTR
Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Making abstract domains condensing, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.33-60, January 2005
Andy King , Lunjin Lu, A backward analysis for constraint logic programs, Theory and Practice of Logic Programming, v.2 n.4-5, p.517-547, July 2002
Giorgio Levi , Fausto Spoto, Pair-independence and freeness analysis through linear refinement, Information and Computation, v.182
Patricia M. Hill , Fausto Spoto, Deriving escape analysis by abstract interpretation, Higher-Order and Symbolic Computation, v.19 n.4, p.415-463, December  2006
abstract domain;abstract interpretation;heyting completion;intuitionistic logic;static analysis;groundness;logic programming