Building Complete Abstract Interpretations in a Linear Logic-based Setting

Roberto Giacobazzi^{†} Francesco Ranzato^{‡,}^{⋆} Francesca Scozzari^{†}

†Dipartimento di Informatica, Università di Pisa Corso Italia 40, 56125 Pisa, Italy

                {giaco,scozzari}@di.unipi.it

‡Dipartimento di Matematica Pura ed Applicata, Università di Padova

Via Belzoni 7, 35131 Padova, Italy

                     franz@math.unipd.it

Abstract. Completeness is an important, but rather uncommon, property of abstract interpretations, ensuring that abstract computations are as precise as possible w.r.t. concrete ones. It turns out that completeness for an abstract interpretation depends only on its underlying abstract domains, and therefore it is an abstract domain property. Recently, the first two authors proved that for a given abstract domain A, in all significant cases, there exists the most abstract domain, called least complete extension of A, which includes A and induces a complete abstract interpretation. In addition to the standard formulation, we introduce and study a novel and particularly interesting type of completeness, called observation completeness. Standard and observation completeness are here considered in the context of quantales, i.e. models of linear logic, as concrete interpretations. In this setting, we prove that various kinds of least complete and observationally complete extensions exist and, more importantly, we show that such complete extensions can all be explicitly characterized by elegant linear logic-based formulations. As an application, we determine the least complete extension of a generic abstract domain w.r.t. a standard bottom-up semantics for logic programs observing computed answer substitutions. This general result is then instantiated to the relevant case of groundness analysis.

1 Introduction

It is widely held that the ideal goal of any semantics design method is to find sound and complete representations for some properties of concrete (actual) computations. Abstract interpretation is one such methodology, where soundness is always required, while completeness more rarely holds. Completeness issues in abstract interpretation have been studied since the Cousot and Cousot seminal paper [5]. The intuition is that a complete abstract interpretation induces an

⋆ The work of Francesco Ranzato has been supported by an individual post-doctoral grant from Università di Padova, Italy.

abstract semantics which is as precise as possible relatively to its underlying abstract domains and to the concrete interpretation of reference. The paradigmatic rule of signs is a typical and simple example of an abstract interpretation which is (sound and) complete for integer multiplication but merely sound for integer addition [13].

Although in static program analysis decidability issues often force to sacrifice completeness for achieving termination and/or efficiency, examples of complete abstract interpretations are common in other fields of application. For instance, several complete abstractions of algebraic polynomial systems have been studied by Cousot and Cousot in [7] and many complete abstract interpretations can be found in comparative program semantics [3,6,9]. Moreover, being completeness a notion relative to the concrete semantics of reference, complete abstract interpretations which are more concrete than a certain, possibly approximated and decidable, property of interest, yield an absolute upper bound for the precision that one can achieve in computing that property. Thus, complete abstract interpretations may play a useful rôle in static program analysis as well. These argumentations probably stimulated the recent trend of research on completeness in abstract interpretation [2,10,11,13,15,17,18].

One key feature of completeness in abstract interpretation is that this property uniquely depends upon the abstraction function. Let us denote by L_{C} the so-called lattice of abstract interpretations of a concrete domain C (cf. [4,5]), where, for all A, B ∈ L_{C}, A ⊑ B means that A is more precise (i.e. concrete) than B. Let us consider the simple case of an abstract interpretation f^{♯} : A → A of a concrete semantic function f : C → C, where the abstract domain A ∈ L_{C} is related to C by an adjoint pair of abstraction and concretization maps α : C → A and γ : A → C. Then, f^{♯} is (sound and) complete if α ∘ f = f^{♯} ∘ α. It is easily seen that if f^{♯} is complete then the best correct approximation f^{b} of f in A, i.e. f^{b} =^{def} α ∘ f ∘ γ : A → A, is complete as well, and, in this case, f^{♯} indeed coincides with f^{b} (cf. [10]). Thus, given an abstract domain A ∈ L_{C}, one can define a complete abstract semantic function f^{♯} : A → A over A if and only if f^{b} : A → A is complete. This simple observation makes completeness an abstract domain property, namely a characteristic of the abstract domain. It is then clear that a key problem consists in devising systematic and constructive methodologies for transforming abstract domains in such a way that completeness is achieved and the resulting complete abstract domains are as close as possible to the initial (noncomplete) ones. This problem has been first raised in a predicate-based approach to abstract interpretation by Mycroft [13, Section 3.2], who gave a methodology for deriving the most concrete domain, called “canonical abstract interpretation”, which is complete and included in a given domain of properties. More recently, the first two authors proved in [10] that when the concrete semantic function f is continuous, any domain A can always be extended into the most abstract domain which includes A and is complete for f — the so-called least complete extension of A. Analogously, [10] solved the aforementioned problem raised by Mycroft, by showing that, for any given domain A, the most concrete domain which is complete and included in A — the so-called complete kernel of A — exists for any monotone semantic function. Very recently, we improved considerably such results, by providing explicit constructive characterizations for least complete extensions and complete kernels of abstract domains [11].

In this paper, we are concerned with completeness problems arising when concrete semantic binary^{1} operations of type C_{1} × C_{2} → C are assumed to give rise to a generalized form of quantales, called typed quantales. Quantales are well-known algebraic structures which turn out to be models of intuitionistic linear logic [16,19]. In this logical setting, we provide elegant linear logic-based solutions to a number of interesting completeness problems for abstract interpretations. Such solutions find relevant applications in static program analysis and comparative semantics, for instance in logic programming, where unification — the prime computational step of any logic program semantics — turns out to be a binary operation in a quantale of substitutions, or in data structure analysis, considering binary data constructors such as cons for lists. More in detail, a typed quantale ⟨C, C_{1}, C_{2}, ⊗⟩ consists of three complete lattices C, C_{1} and C_{2}, and of an operation ⊗ : C_{1} × C_{2} → C which is additive (i.e., preserves lub’s) on both arguments. When C = C_{1} = C_{2}, typed quantales boil down to standard quantales ⟨C, ⊗⟩. The main feature of (typed) quantales is that they support a notion of left and right linear implication between domain’s objects: Given a ∈ C_{1} and b ∈ C, there exists a unique greatest object a ⇾ b ∈ C_{2} which, when combined by ⊗ with a, gives a result less than or equal to b. In other terms, the following right modus ponens law a ⊗ x ≤ b ⇔ x ≤ a ⇾ b holds. Analogous left implicational objects exist for a correspoding left modus ponens law.

When solving completeness problems in a setting where concrete interpretations are typed quantales, implicational domain objects allow to elegantly characterize complete abstract domains in a variety of situations. Our first result provides a characterization based on linear implications between domain’s objects of the least complete extension of any abstract domain of any quantale. Then, we consider the following completeness problem over typed quantales: Given a typed quantale ⟨C, C_{1}, C_{2}, ⊗⟩, a fixed abstraction A ∈ L_{C}, with corresponding abstraction map α_{A} : C → A, and a pair of abstract domains ⟨A_{1}, A_{2}⟩ ∈ L_{C_{1}} × L_{C_{2}}, does there exist the most abstract pair of domains ⟨A′_{1}, A′_{2}⟩ ∈ L_{C_{1}} × L_{C_{2}}, with corresponding abstraction maps α_{A_{i}} : C_{i} → A_{i} (i = 1, 2), such that ⟨A′_{1}, A′_{2}⟩⊑_{L_{C_{1}} ×L_{C_{2}}} ⟨A_{1}, A_{2}⟩ and α_{A}( ⊗ ) = α_{A}(α_{A′_{1}}( ) ⊗ α_{A′_{2}}( ))? Here, the observation domain A is fixed, and we are thus looking for the most abstract pair of domains in L_{C_{1}} × L_{C_{2}} which is more concrete than an initial pair ⟨A_{1}, A_{2}⟩ and simultaneously induces a complete abstract interpretation w.r.t. ⊗. This is termed an observation completeness problem. Again, solutions to this observation completeness problem are built in terms of linear implications between domains.

To illustrate the practical scope of our results, we first consider a simple example in data structure analysis involving abstract domains for lists. In particular, our results are applied in order to solve various observation completeness problems concerning abstract domains useful for detecting irredundant lists of

1 Clearly, a generalization to n-ary operations would be straightforward.

objects. Then, in the context of logic program semantics, we consider an immediate consequences operator T_{P} defined in terms of unification and union of sets of idempotent substitutions, and characterizing computed answer substitutions in a s-semantics style (cf. [1,8]). As usual, unification turns out to be the key operation to take into account in order to build least complete extensions of abstract domains. Sets of idempotent substitutions and unification give rise to a unital commutative quantale: Given an abstract domain A, we show how the least complete extension of A w.r.t. this quantale naturally induces the least complete extension of A w.r.t. T_{P} functions. This permits to give explicitly, in terms of linear implications, the least complete extension, for any T_{P}, of a generic domain abstracting sets of substitutions. As a remarkable instance of our construction, we characterize the least complete extension of the plain groundness domain w.r.t. computed answer substitutions s-semantics.

2 Basic notions

The lattice of abstract interpretations. In standard Cousot and Cousot’s abstract interpretation theory, abstract domains can be equivalently specified either by Galois connections (GCs), i.e. adjunctions, or by upper closure operators (uco’s) [5]. In the first case, the concrete and abstract domains C and A (both assumed to be complete lattices) are related by a pair of adjoint functions of a GC (α, C, A, γ). Also, it is generally assumed that (α, C, A, γ) is a Galois insertion (GI), i.e. α is onto or, equivalently, γ is 1-1. In the second case instead, an abstract domain is specified as a uco on the concrete domain C, i.e. a monotone, idempotent and extensive operator on C. These two approaches are equivalent, modulo isomorphic representation of domain’s objects. Given a complete lattice C, it is well known that the set uco(C) of all uco’s on C, endowed with the pointwise ordering ⊑, is a complete lattice ⟨uco(C), ⊑, ⊔, ⊓, λx.⊤_{C}, id⟩ (id denotes the identity function). Let us also recall that each ρ ∈ uco(C) is uniquely determined by the set of its fixpoints, which is its image, i.e. ρ(C) = {x ∈ C | ρ(x) = x}, and that ρ ⊑ η iff η(C) ⊆ ρ(C). Moreover, a subset X ⊆ C is the set of fixpoints of a uco on C iff X is meet-closed, i.e. X = ⋏(X) =^{def} {⋀_{C} Y | Y ⊆ X} (note that ⊤_{C} = ⋀_{C} ∅ ∈ ⋏(X)). Often, we will identify closures with their sets of fixpoints. This does not give rise to ambiguity, since one can distinguish their use as functions or sets according to the context. In view of the equivalence above, throughout the paper, ⟨uco(C), ⊑⟩ will play the rôle of the lattice L_{C} of abstract interpretations of C [4,5], i.e. the complete lattice of all possible abstract domains of the concrete domain C. For an abstract domain A ∈ L_{C}, ρ_{A} ∈ uco(C) will denote the corresponding uco on C, and if A is specified by a GI (α, C, A, γ) then ρ_{A} =^{def} γ ∘ α. The ordering on uco(C) corresponds to the standard order used to compare abstract domains with regard to their precision: A_{1} is more precise than A_{2} (i.e., A_{1} is more concrete than A_{2} or A_{2} is more abstract than A_{1}) iff A_{1} ⊑ A_{2} in uco(C). Lub and glb on uco(C) have therefore the following reading as operators on domains. Suppose {A_{i}}_{i∈I} ⊆ uco(C):

(i) ⊔_{i∈I}A_{i} is the most concrete among the domains which are abstractions of all the A_{i}’s, i.e. it is their least (w.r.t. ⊑) common abstraction; (ii) ⊓_{i∈I}A_{i} is the most abstract among the domains (abstracting C) which are more concrete than every A_{i}; this domain is also known as reduced product of all the A_{i}’s.

Quantales and linear logic. Quantales originated as algebraic foundations of the so-called quantum logic. They have been successively considered for the latticetheoretic semantics of Girard’s linear logic (see [16] for an exhaustive treatment of quantales). We introduce a mild generalization of the notion of quantale, which, up to knowledge, appears to be new. A typed quantale is a multisorted algebra ⟨C, C_{1}, C_{2}, ⊗⟩, where C, C_{1}, C_{2} are complete lattices and ⊗ : C_{1}×C_{2} → C is a function such that (⋁_{i} x_{i}) ⊗ c_{2} = ⋁_{i}(x_{i} ⊗ c_{2}) and c_{1} ⊗ (⋁_{i} x_{i}) = ⋁_{i}(c_{1} ⊗ x_{i}). In other terms, a typed quantale is a 3-sorted algebra endowed with a “product” ⊗ which distributes over arbitrary lub’s on both sides. Thus, for any c_{1} ∈ C_{1} and c_{2} ∈ C_{2}, both functions c_{1} ⊗ and ⊗ c_{2} have right adjoints denoted, resp., by c_{1} ⇾ and ⇽ c_{2}. Hence, for all c ∈ C, c_{1} ⊗ c_{2} ≤ c ⇔ c_{2} ≤ c_{1} ⇾ c, and, dually, c_{1} ⊗c_{2} ≤ c ⇔ c_{1} ≤ c ⇽ c_{2}. Two functions ⇾: C_{1} ×C → C_{2} and ⇽: C ×C_{2} → C_{1} can be therefore defined as follows:

c_{1} ⇾ c =^{def} ⋁ {z ∈ C_{2} | c_{1} ⊗ z ≤ c}; c ⇽ c_{2} =^{def} ⋁ {y ∈ C_{1} | y ⊗ c_{2} ≤ c}.

Any typed quantale ⟨C, C_{1}, C_{2}, ⊗⟩ enjoys the following main properties: For all c ∈ C, {x_{i}}_{i∈I} ⊆ C, c_{1} ∈ C_{1}, {y_{i}}_{i∈I} ⊆ C_{1}, c_{2} ∈ C_{2} and {z_{i}}_{i∈I} ⊆ C_{2}:

(i) c_{1} ⊗ (c_{1} ⇾ c) ≤ c  (ii) (c ⇽ c_{2}) ⊗ c_{2} ≤ c
(iii) c_{1} ⇾ (⋀_{i∈I} x_{i}) = ⋀_{i∈I}(c_{1} ⇾ x_{i}) (iv) (⋀_{i∈I} x_{i}) ⇽ c_{2} = ⋀_{i∈I}(x_{i} ⇽ c_{2})
(v) (⋁_{i∈I} y_{i}) ⇾ c = ⋀_{i∈I}(y_{i} ⇾ c)  (vi) c ⇽ (⋁_{i∈I} z_{i}) = ⋀_{i∈I}(c ⇽ z_{i})

When C = C_{1} = C_{2} and ⊗ is associative, a typed quantale is called quantale. It is well known that quantales turn out to be models of noncommutative intuitionistic linear logic [16,19]. A quantale ⟨C, ⊗⟩ is called commutative when ⊗ is commutative, and this is equivalent to require that, for all a, b ∈ C, a ⇾ b = b ⇽ a. Also, a commutative quantale ⟨C, ⊗⟩ is called unital if there exists an object 1 ∈ C such that 1 ⊗ a = a = a ⊗ 1, for all a ∈ C. For a quantale ⟨C, ⊗⟩, the following additional properties hold for all a, b, c ∈ C:

(vii) a ⇾ (c ⇽ b) = (a ⇾ c) ⇽ b
(viii) b ⇾ (a ⇾ c) = (a ⊗ b) ⇾ c
(ix) (c ⇽ b) ⇽ a = c ⇽ (a ⊗ b)

3 Completeness problems in abstract interpretations

Let ⟨C, C_{1}, C_{2}, ⊗⟩ be a concrete interpretation, i.e. C, C_{1} and C_{2} are concrete semantic domains provided with a semantic operation ⊗ : C_{1} × C_{2} → C. When C = C_{1} = C_{2}, we adopt the simpler notation ⟨C, ⊗⟩. Given the abstractions A_{1} ∈ L_{C_{1}}, A_{2} ∈ L_{C_{2}} and A ∈ L_{C}, let us recall [5] that the best correct approx-

imation ⊗^{b} : A_{1} × A_{2} → A of ⊗ is defined as ⊗^{b} =^{def} α_{C,A} ∘ ⊗ ∘ ⟨γ_{A_{1},C_{1}}, γ_{A_{2},C_{2}}⟩.

It has been shown in [10] that completeness for an abstract interpretation is a property depending only on the underlying abstract domains. In our setting, this means that an abstract interpretation ⟨A, A_{1}, A_{2}, ⊗^{♯}⟩, with ⊗^{♯} : A_{1} × A_{2} → A, is complete for ⟨C, C_{1}, C_{2}, ⊗⟩ iff ⟨A, A_{1}, A_{2}, ⊗^{b}⟩ is complete and ⊗^{♯} = ⊗^{b}. In other terms, the best correct approximation induced by the underlying abstract domains determines the property of being complete. Hence, we find more convenient, elegant and, of course, completely equivalent, to reason on completeness by using abstract domains specified by the closure operator approach.

Full completeness problems. Within the closure operator approach, given a concrete interpretation ⟨C, ⊗⟩, an abstraction A ∈ L_{C} is complete when the equation ρ_{A}∘⊗∘⟨ρ_{A}, ρ_{A}⟩ = ρ_{A}∘⊗ holds. Giacobazzi and Ranzato [10] stated the following full completeness problem, here specialized to binary semantic operations: Given an abstract domain A ∈ L_{C}, does the following system with variable ρ admit a most abstract solution?

\{ \begin{matrix}ρ ⊑ A \\ ρ ∘ ⊗ ∘ ⟨ρ, ρ⟩ = ρ ∘ ⊗ \end{matrix}  (1)

Hence, a solution to the above full completeness problem is the necessarily unique (up to domain isomorphism) most abstract domain which includes A and induces a complete abstract interpretation. Following [10], such most abstract solution to System (1) is called the least complete extension of A w.r.t. ⊗. It is shown in [10] that if ⊗ is continuous in both arguments, then least complete extensions of any A exist.

Full completeness problems clearly make sense only for concrete interpretations of type ⟨C, ⊗⟩. When generic concrete interpretations of type ⟨C, C_{1}, C_{2}, ⊗⟩ are considered, different abstractions are involved in a completeness equation, and therefore various completeness problems arise by fixing some of these abstractions. In the following, we introduce three such completeness problems, which turn out to be of particular interest. Such completeness problems still depend only on best correct approximations of the concrete operation, and therefore the corresponding completeness notions are again abstract domain properties.

Observation completeness problems. Let ⟨C, C_{1}, C_{2}, ⊗⟩ be a concrete interpretation. An observation domain is any abstraction of the range C of ⊗. Observation completeness problems arise when in a completeness equation an observation domain is fixed. Hence, let us consider a fixed observation domain A ∈ L_{C}. The observation completeness problem for a pair ⟨A_{1}, A_{2}⟩ ∈ L_{C_{1}} × L_{C_{2}} admits solution when there exists the most abstract solution in L_{C_{1}} × L_{C_{2}} of the following system:

\{ \begin{matrix}⟨η, μ⟩ ⊑ ⟨A_{1}, A_{2}⟩ \\ ρ_{A} ∘ ⊗ ∘ ⟨η, μ⟩ = ρ_{A} ∘ ⊗ \end{matrix}  (2)

Let us remark that, by using adjunctions, the observation completeness equation ρ_{A} ∘ ⊗ ∘ ⟨η, μ⟩ = ρ_{A} ∘ ⊗ is equivalent to require that for all x ∈ C_{1} and y ∈ C_{2}, α_{C_{1},η}(x) ⊗^{b} α_{C_{2},μ}(y) = α_{C,A}(x ⊗ y).

When in addition to the observation domain we also fix one (or more, if we would deal with n-ary operations) of the abstractions of the argument domains of ⊗, we obtain yet different completeness problems. In the left observation completeness problem, A ∈ L_{C} and A_{2} ∈ L_{C_{2}} are fixed, and the solution to this problem for a given A_{1} ∈ L_{C_{1}} exists when the following system with variable η admits a most abstract solution in L_{C_{1}}:

\{ \begin{matrix}η ⊑ A_{1} \\ ρ_{A} ∘ ⊗ ∘ ⟨η, ρ_{A_{2}}⟩ = ρ_{A} ∘ ⊗ ∘ ⟨id, ρ_{A_{2}}⟩ \end{matrix}  (3)

Of course, right observation completeness problems are analogously formulated. It turns out that a left observation completeness equation ρ_{A} ∘ ⊗ ∘ ⟨η, ρ_{A_{2}}⟩ = ρ_{A} ∘ ⊗ ∘ ⟨id, ρ_{A_{2}}⟩ formulated in terms of GIs amounts to require that for any x ∈ C_{1} and y ∈ A_{2}, α_{C_{1},η}(x) ⊗^{b} y = α_{C,A}(x ⊗ γ_{A_{2},C_{2}}(y)). Hence, a left observation completeness equation ρ_{A} ∘ ⊗ ∘ ⟨η, ρ_{A_{2}}⟩ = ρ_{A} ∘ ⊗ ∘ ⟨id, ρ_{A_{2}}⟩ states that completeness for the abstractions A ∈ L_{C}, η ∈ L_{C_{1}} and A_{2} ∈ L_{C_{2}} holds when the semantic operation ⊗ acts over C_{1} × A_{2}. Examples of observation completeness problems will be considered and solved later in Section 5.

4 Quantales and solutions to completeness problems

When concrete interpretations are quantales and typed quantales, solutions to the above completeness problems exist and can be characterized explicitly and elegantly in terms of linear implications.

Let ⟨C, C_{1}, C_{2}, ⊗⟩ be a typed quantale playing the rôle of concrete interpretation. In this setting, solutions to completeness problems will be characterized by exploiting two basic domain transformers ⇾^{⋏}: uco(C_{1}) × uco(C) → uco(C_{2}) and ⇽^{⋏} : uco(C) × uco(C_{2}) → uco(C_{1}), defined by lifting left and right linear implications ⇾ and ⇽ to abstract domains as follows: For any A_{1} ∈ L_{C_{1}}, A_{2} ∈ L_{C_{2}}, A ∈ L_{C}:

\begin{matrix}A_{1} ⇾^{⋏}A =^{def} ⋏(\{a_{1} ⇾ a ∈ C_{2} | a_{1} ∈ A_{1}, a ∈ A\}); \\ A⇽^{⋏}A_{2} =^{def} ⋏(\{a ⇽ a_{2} ∈ C_{1} | a ∈ A, a_{2} ∈ A_{2}\}). \end{matrix}

Hence, A_{1} ⇾^{⋏}A is defined to be the most abstract domain in L_{C_{2}} containing all the linear implications from A_{1} to A. From the logic properties of linear implication recalled in Section 2, it is not too hard to derive the following useful distributivity laws for ⇾^{⋏} and ⇽^{⋏} over reduced product of abstract domains.

Proposition 1. For all {B_{i}}_{i∈I} ⊆ L_{C},

A_{1} ⇾^{⋏}(⨅_{i∈I} B_{i}) = ⨅_{i∈I}(A_{1} ⇾^{⋏}B_{i}) and (⨅_{i∈I} B_{i})⇽^{⋏}A_{2} = ⨅_{i∈I}(B_{i} ⇽^{⋏}A_{2}).

Solutions to full completeness problems. Solutions to full completeness problems exist and are characterized in terms of linear implications among domain’s objects as stated by the following result.

Theorem 2. A⊓(C ⇾^{⋏}A)⊓(A⇽^{⋏}C)⊓((C ⇾^{⋏}A)⇽^{⋏}C) is the most abstract solution of System (1).

Solutions to observation completeness problems. Let us first consider left observation completeness problems. A left observation completeness equation can be characterized as follows.

Theorem 3. ρ_{A} ∘ ⊗ ∘ ⟨η, ρ_{A_{2}}⟩ = ρ_{A} ∘ ⊗ ∘ ⟨id, ρ_{A_{2}}⟩ ⇔ η ⊑ A⇽^{⋏}A_{2}.

Thus, as an immediate consequence, left observation completeness problems admit the following solutions.

Corollary 4. A_{1} ⊓ (A⇽^{⋏}A_{2}) is the most abstract solution of System (3).

Of course, dual results can be given for right observation completeness problems. In this case, the most abstract solution therefore is A_{2} ⊓ (A_{1} ⇾^{⋏}A).

The above results for left and right observation completeness turn out to be useful for solving observation completeness problems. In fact, an observation completeness equation is characterized as an independent combination of left and right observation completeness equations as follows.

Theorem 5. ρ_{A} ∘ ⊗ ∘ ⟨η, μ⟩ = ρ_{A} ∘ ⊗ ⇔ ⟨η, μ⟩ ⊑ ⟨A⇽^{⋏}C_{2}, C_{1} ⇾^{⋏}A⟩.

As a straight consequence, we get the following result.

Corollary 6. ⟨A_{1} ⊓ (A⇽^{⋏}C_{2}), A_{2} ⊓ (C_{1} ⇾^{⋏}A)⟩ is the most abstract solution of System (2).

4.1 The case of unital commutative quantales

When we deal with unital and commutative quantales — i.e. models of intuitionistic linear logic [16,19] — the above solutions to full completeness problems given by Theorem 2 can be significantly simplified by exploiting the logical properties of linear implication. In a unital commutative quantale ⟨C, ⊗⟩, the following additional properties hold: For any a, b, c ∈ C:

\begin{matrix}– a ⇾ (b ⇾ c) = b ⇾ (a ⇾ c) & – 1 ⇾ a = a \\ – c ≤ (c ⇾ a) ⇾ a & – ((c ⇾ a) ⇾ a) ⇾ a = c ⇾ a \end{matrix}

Therefore, from these properties it is not hard to check that for all a ∈ C, λc.(c ⇾ a) ⇾ a ∈ uco(C). This turns out to be the key observation in order to give a more compact form to solutions of full completeness problems on unital commutative quantales. Moreover, the objects of such solutions enjoy a clean logical characterization in terms of linear implications as specified by the third point of the next result.

Theorem 7. Let ⟨C, ⊗⟩ be a unital commutative quantale.

1. C ⇾^{⋏}A is the most abstract solution of System (1);

2. If B ∈ L_{C} is such that B ⊑ C ⇾^{⋏}A, then C ⇾^{⋏}A = B ⇾^{⋏}A;

3. For all c ∈ C, c ∈ C ⇾^{⋏}A ⇔ c = ⋀_{a∈A}(c ⇾ a) ⇾ a.

5 An application in data structure completeness

In this section, we consider some examples of completeness problems in abstract interpretation of list data structures. For the sake of practicality, we consider lists of natural numbers, even if our discussion holds more in general for lists of objects of arbitrary type.

Consider the structure ⟨℘(list(ℕ)), ℘(ℕ), ℘(list(ℕ)),::⟩, where list(ℕ) is the set of all finite lists of natural numbers, ℘(list(ℕ)) and ℘(ℕ) are complete lattices w.r.t. set-inclusion, and :: : ℘(ℕ) × ℘(list(ℕ)) → ℘(list(ℕ)) is a “collecting” version of concatenation defined as follows:

N :: L =^{def} {[n|l] | n ∈ N, l ∈ L},

where ∅ :: L = N :: ∅ = ∅. It is clear that this structure is a typed quantale.

We say that a list is irredundant if it does not contain two occurrences of the same object. An abstract domain ρ ∈ uco(℘(list(ℕ))) for detecting irredundant lists can be defined by ρ =^{def} { list(ℕ), Irr }, where Irr ⊆ list(ℕ) is the set of irredundant lists over ℕ. We consider ρ as an observation domain and we look for the most abstract solution ⟨X, Y ⟩ ∈ uco(℘(ℕ))×uco(℘(list(ℕ))) to the following observation completeness problem:

ρ ∘ :: ∘ ⟨ρ_{X}, ρ_{Y} ⟩ = ρ ∘ ::

Here, we dropped the first constraint of the generic System (2), since it amounts to the trivial constraint ⟨ρ_{X}, ρ_{Y} ⟩ ⊑ ⟨{ ℕ }, { list(ℕ) }⟩ which is always satisfied. By Corollary 6, the most abstract solution of this observation completeness equation exists. This will be the most abstract pair of domains ⟨X, Y ⟩ for which abstract concatenation in X and Y results to be complete when observing irredundancy as represented by ρ. By Corollary 6, the solution ⟨X, Y ⟩ is as follows.

X = { ℕ } ⊓ (ρ⇽^{⋏}℘(list(ℕ)))
= ρ⇽^{⋏}℘(list(ℕ))
= ⋏({L ⇽ M | L ∈ ρ, M ∈ ℘(list(ℕ))})
(since, for all M, list(ℕ) ⇽ M = list(ℕ))
= ⋏({Irr ⇽ M | M ∈ ℘(list(ℕ))})
(since, for all n ∈ ℕ, Irr ⇽ {[n]} = ℕ ∖ {n})
= ℘(ℕ)

Y = { list(ℕ) } ⊓ (℘(ℕ)⇾^{⋏}ρ)
= ℘(ℕ)⇾^{⋏}ρ
= ⋏({N ⇾ L | N ∈ ℘(ℕ), L ∈ ρ})
(since, for all N, N ⇾ list(ℕ) = list(ℕ))
= ⋏({N ⇾ Irr | N ∈ ℘(ℕ)})
(since, by (v) in Section 2, ⋂_{i}(N_{i} ⇾ Irr) = (⋃_{i} N_{i}) ⇾ Irr)
= {N ⇾ Irr | N ∈ ℘(ℕ)}
= ⋃_{N⊆ℕ} {L ∈ ℘(list(ℕ)) | l ∈ L ⇔ (l ∈ Irr and ∀n ∈ N. n is not in l)}

Thus, in order to be complete for concatenation when observing irredundancy, X must coincide with the concrete domain ℘(ℕ), while it suffices that Y contains all the sets of irreduntant lists which do not contain some set of numbers. Note that Y coincides with the set of all the sets of irredundant lists closed by permutation of their objects, and this is a strict abstraction of the concrete domain ℘(list(ℕ)).

Let us now consider the standard abstract domain η ∈ uco(℘(ℕ)) for parity analysis given by η =^{def} { ℕ, even, odd, ∅ }. We consider the following left and right observation completeness problems: We look respectively for the the most abstract domains X ∈ uco(℘(ℕ)) and Y ∈ uco(℘(list(ℕ))) such that:

(i) ρ ∘ :: ∘ ⟨ρ_{X}, ρ⟩ = ρ ∘ :: ⟨id, ρ⟩ (ii) ρ ∘ :: ∘ ⟨η, ρ_{Y} ⟩ = ρ ∘ :: ⟨η, id⟩

Here again, there are no upper bound constraints for X and Y. By Corollary 4 (and its dual), we get the following solutions:

X = { ℕ } ⊓ (ρ⇽^{⋏}ρ)
= ρ⇽^{⋏}ρ
= ⋏({ list(ℕ) ⇽ list(ℕ), list(ℕ) ⇽ Irr, Irr ⇽ list(ℕ), Irr ⇽ Irr })
= { ℕ, ∅ },
Y = { list(ℕ) } ⊓ (η ⇾^{⋏}ρ)
= η ⇾^{⋏}ρ
= ⋏({ ℕ ⇾ Irr, even ⇾ Irr, odd ⇾ Irr, ∅ ⇾ Irr })
= { { [] }, Irr_{even}, Irr_{odd}, list(ℕ) },

where Irr_{even} =^{def}{l ∈ list(ℕ) | l ∈ Irr and l does not contain even numbers} and Irr_{odd} =^{def} {l ∈ list(ℕ) | l ∈ Irr and l does not contain odd numbers}. Thus, for problem (i), in order to get completeness, it is enough to check whether a given set of numbers is empty or not, while, for problem (ii), we only need to consider sets of irreduntant lists which do not contain either even or odd numbers.

6 Complete semantics for logic program analysis

In this section, we determine the least complete extension of any logic program property w.r.t. a bottom-up semantics characterizing computed answer substitutions, which turns out to be equivalent to the well-known s-semantics [8]. This complete semantics can be thought of as a logic program semantics which is “optimal” (i.e. neither too concrete nor too abstract) for characterizing a given property of interest. The problem of determining optimal semantics for program analysis was raised in [9]. We show that such optimal semantics can be obtained by solving a full completeness problem relatively to the operation of unification on sets of substitutions.

Completeness for an abstract domain, in general, depends both on the considered concrete domains and on the semantic operation defined on them. However, the following important result shows that, under certain conditions, completeness is instead independent from the choice of the concrete semantics.

Theorem 8. Let α ∈ L_{C} and f, g : C → C such that f ⊑ g ⊑ α ∘ f. Then, α is complete for f iff α is complete for g.

We will exploit this result for computing our least complete extension of abstract domains w.r.t. s-semantics. The idea is that of considering a “simplified” and more concrete version, denoted by T_{P}, of the immediate consequences operator T_{P}^{s} of s-semantics, which does not take into account variable renaming. This will simplify a lot the technical development of this section. Hence, s-semantics results to be an abstract interpretation of our T_{P} semantics: If r denotes the closure under variable renaming of sets of substitutions, then we have that T_{P}^{s} = r ∘ T_{P}. Then, leaving out the details, if α denotes the least complete extension, relatively to T_{P}, of any domain A abstracting computed answer substitutions, since T_{P} ⊑ r ∘ T_{P} = T_{P}^{s} ⊑ α ∘ T_{P} holds, we can apply Theorem 8, from which we get that α not only is complete for T_{P}^{s}, but actually α turns out to be the least complete extension of A relatively to T_{P}^{s}.

6.1 Notation

Let V be an infinite, recursively enumerable (r.e.) set of variables, Σ be a set of function symbols and Π be a set of predicate symbols, defining a r.e. first-order language L. Term denotes the set of terms of L. If s is any syntactic object and σ and θ are substitutions, then vars(s) denotes the set of variables occurring

in s, dom(σ) =^{def} {v ∈ V | σ(v) ≠ v}, rng(σ) =^{def} ∪ {vars(σ(x)) | x ∈ dom(σ)}, sσ

denotes the application of σ to s, and σ ∘ θ denotes the standard composition of θ and σ (i.e., σ ∘ θ = λx.(θ(x))σ). The set of idempotent substitutions modulo renaming (i.e., θ ∼ σ iff there exists β and δ such that θ = σ ∘ β and σ = θ ∘ δ) on L is denoted by Sub. Objects in Sub are partially ordered by instantiation, denoted by ⪯. By adding to Sub an extra object τ as least element, one gets a complete lattice ⟨Sub^{τ} , ⪯, ∨, ∧, ϵ, τ⟩, where ∨ is least general anti-instance, ∧ is standard unification and ϵ is the empty substitution (see [14] for more details). The set of most general atoms is given by GAtom =^{def} {p(X̄) | p ∈ Π}, where X̄ is a tuple of distinct variables. We consider logic programs in normalized form, that is, a generic Horn clause is p(X̄) : −c, q_{1}(X̄_{1}), …, q_{n}(X̄_{n}), where all the tuples of variables are distinct and c ∈ Sub is an idempotent substitution binding variables to terms.

6.2 T_{P} -completeness

Our basic semantic structure is the unital commutative quantale ⟨℘(Sub), ⊗⟩, where ⟨℘(Sub), ⊆⟩ is a complete lattice, ⊗ : ℘(Sub) × ℘(Sub) → ℘(Sub) is the obvious lifting of unification ∧ to sets of substitutions, i.e. it is defined by: X ⊗ Y =^{def} {x ∧ y | x ∈ X, y ∈ Y }, and {ϵ} ∈ ℘(Sub) is the unit of ⊗. It is immediate to check that ⟨℘(Sub), ⊗⟩ actually is a unital commutative quantale [16, Example 10, p. 18]. In the following, we will slightly abuse notation by applying the operation ⊗ also to substitutions.

As mentioned above, we consider a bottom-up semantics based on an immediate consequences operator T_{P} which is more concrete than the standard operator T_{P}^{s} of s-semantics. In fact, T_{P} is defined using only the operations of unification ⊗ and union of sets of idempotent substitutions. The s-semantics operator T_{P}^{s} can be recovered from T_{P} by a simple step of abstract interpretation considering the closure of sets of substitutions over variables renaming.

We consider a concrete semantic domain CInt of functions — as usual, called interpretations — which map most general atoms to sets of substitutions: CInt =^{def} GAtom → ℘(Sub), which ordered pointwise is trivially a complete lattice. Often, we will find convenient to denote an interpretation I ∈ CInt by the set {⟨p(X̄), I(p(X̄))⟩ | p ∈ Π}. Then, for any program P, the immediate consequences operator T_{P} : CInt → CInt is defined as follows: For any I ∈ CInt,

T_{P} (I)(p(Ȳ)) = ⋃_{C≪P}(c ⊗ ( ⨂_{i=1..n} I(q_{i}(X̄_{i}))) ⊗ {Ȳ = X̄}),

where C = p(X̄) : −c, q_{1}(X̄_{1}), …, q_{n}(X̄_{n}). Here, C ≪ P denotes that the clause C of P is renamed apart with fresh variables, and I(q_{i}(X̄_{i})) is intended modulo renaming.

If ρ ∈ uco(℘(Sub)) is any abstraction on sets of substitutions, a corresponding abstraction on interpretations ⟅ρ⟆ ∈ uco(CInt) which acts accordingly to ρ can be defined as follows: For any I ∈ CInt, ⟅ρ⟆(I) =^{def} {⟨p(X̄), ρ(c)⟩ | ⟨p(X̄), c⟩ ∈ I}. Note that ⟅·⟆ is monotone, i.e., for all ρ, η ∈ uco(℘(Sub)), if ρ ⊑ η then ⟅ρ⟆ ⊑ ⟅η⟆.

Given a basic abstract domain of properties of interest π ∈ uco(⟨℘(Sub), ⊆⟩), our goal is therefore to find the most abstract domain which contains π (more precisely, ⟅π⟆) and is complete for any T_{P} operator. Our strategy consists in characterizing the least complete extension of π for the basic operations involved in the definition of T_{P}, and then to show that, under reasonable hypotheses, this domain turns out to be the right one. Since every abstract domain is trivially always complete for lub’s, it turns out that union of sets of substitutions is troubleless, and therefore it is enough to concentrate on unification ⊗. Indeed, the following result shows that completeness for ⊗ implies completeness for any T_{P}.

Theorem 9. Let ρ ∈ uco(℘(Sub)). If ρ is complete for ⊗ then ⟅ρ⟆ is complete for any T_{P}.

By Theorem 7, given π ∈ uco(℘(Sub)), the least complete extension of π w.r.t. the quantale operation ⊗ exists and is the domain ℘(Sub)⇾^{⋏}π of linear implications from ℘(Sub) to π. This complete domain ℘(Sub)⇾^{⋏}π results to be the right one whenever the abstract domain π satisfies the following weak decidability property.

Definition 10. π ∈ uco(℘(Sub)) is decidable if any S ∈ π is a r.e. set. □

It should be clear that decidability is a reasonable requirement for most abstract domains used in program analysis: In fact, for such a decidable abstraction (of sets) of substitutions, an effective procedure for checking whether a substitution belongs to (is approximated by) an abstract object is available. As announced, the following key result shows that least complete extensions of decidable abstract domains w.r.t. unification ⊗ actually are least complete extensions for T_{P} operators as well.

Theorem 11. Let π ∈ uco(℘(Sub)) be decidable. Then, ⟅℘(Sub)⇾^{⋏}π⟆ is the least complete extension of ⟅π⟆ for any T_{P}.

As we discussed just after Theorem 8, it turns out that, for any decidable π ∈ uco(℘(Sub)), ⟅℘(Sub)⇾^{⋏}π⟆ actually is the least complete extension of ⟅π⟆ for any immediate consequences operator T_{P}^{s} of s-semantics. In fact, if r ∈ uco(℘(Sub)) is the closure under renaming of sets of substitions, namely variables in the range of substitutions are renamed in each possible way, then T_{P}^{s} = r ∘ T_{P}; moreover, ⟅℘(Sub)⇾^{⋏}π⟆ clearly induces a semantic transformer less precise than T_{P}^{s}, i.e. T_{P}^{s} ⊑ ⟅℘(Sub)⇾^{⋏}π⟆ ∘ T_{P}. Hence, by Theorems 8 and 11, we get the following desired consequence.

Corollary 12. Let π ∈ uco(℘(Sub)) be decidable, such that T_{P}^{s} ⊑ π ∘T_{P} for any P. Then, ⟅℘(Sub)⇾^{⋏}π⟆ is the least complete extension of ⟅π⟆ for any T_{P}^{s}.

6.3 Complete semantics for groundness analysis

Groundness analysis is arguably one of the most important analysis for logicbased programming languages. Groundness analysis aims to statically detect whether variables will be bound to ground terms in successful derivations. By instantiating the results above, we are able to characterize the least complete extension of the basic abstract domain representing plain groundness information w.r.t. any immediate consequences operator of s-semantics. The resulting semantics can be therefore interpreted as the “optimal” semantics for groundness analysis.

If V ⊆ V is a finite set of variables of interest, the simplest abstract domain for representing plain groundness information of variables in V is G_{V} =^{def} ⟨℘(V), ⊇⟩, as first put forward by Jones and Søndergaard [12]. The intuition is that each W ∈ G_{V} represents the set of substitutions which ground every variable in W. G_{V} is related to the concrete domain ℘(Sub) by the following concretization map: For each W ∈ G, γ_{G_{V}} (W) =^{def} {θ ∈ Sub | ∀v ∈ W. vars(θ(v)) = ∅}. As usual, we shall abuse notation by denoting with G_{V} ∈ uco(℘(Sub)) the corresponding isomorphic image γ_{G_{V}} (G_{V}) in ℘(Sub).

A variable independent abstract domain G ∈ uco(CInt) for representing plain groundness information can be therefore defined as follows:

G(I) =^{def} {⟨p(X̄), GX̄(c)⟩ | ⟨p(X̄), c⟩ ∈ I}.

It is easy to check that G actually is a uco on the concrete semantic domain CInt. Furthermore, G is clearly decidable and T_{P}^{s} ⊑ G ∘ T_{P}. Thus, as an easy consequence of Corollary 12, we can prove the following result, where V ⊂_{f} V means that V is a finite subset of V.

Theorem 13. ⨅_{V ⊂_{f} V} ⟅℘(Sub)⇾^{⋏}G_{V} ⟆ is the least complete extension of G for any T_{P}^{s}.

References

1. A. Bossi, M. Gabbrielli, G. Levi, and M. Martelli. The s-semantics approach: theory and applications. J. Logic Program., 19-20:149–197, 1994.

2. P. Cousot. Completeness in abstract interpretation (Invited Talk). In Proc. 1995 Joint Italian-Spanish Conference on Declarative Programming, pages 37–38, 1995.

3. P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation (Invited Paper). In Proc. of the 13th Int. Symp. on Math. Found. of Programming Semantics (MFPS’97), vol. 6 of Electronic Notes in Theor. Comput. Sci., 1997.

4. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM POPL, pages 238–252, 1977.

5. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th ACM POPL, pages 269–282, 1979.

6. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proc. 19th ACM POPL, pages 83–94, 1992.

7. P. Cousot and R. Cousot. Abstract interpretation of algebraic polynomial systems. In Proc. 6th Int. Conf. on Algebraic Methodology and Software Technology (AMAST’97), LNCS 1349, pages 138–154, 1997.

8. M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative modeling of the operational behavior of logic languages. Theor. Comput. Sci., 69(3):289–318, 1989.

9. R. Giacobazzi. “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics. In Proc. 13th Int. Symp. on Theor. Aspects of Comput. Sci. (STACS’96), LNCS 1046, pages 503–514, 1996.

10. R. Giacobazzi and F. Ranzato. Completeness in abstract interpretation: a domain perspective. In Proc. 6th Int. Conf. on Algebraic Methodology and Software Technology (AMAST’97), LNCS 1349, pages 231–245, 1997.

11. R. Giacobazzi, F. Ranzato and F. Scozzari. Complete abstract interpretations made constructive. In Proc. 23rd Int. Symp. on Math. Found. of Comp. Sci. (MFCS’98), LNCS, 1998.

12. N.D. Jones and H. Søndergaard. A semantics-based framework for the abstract interpretation of Prolog. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 123–142. Ellis Horwood Ltd, 1987.

13. A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. ACM Conf. on Partial Evaluation and Program Manipulation (PEPM’93), pages 179–185, 1993.

14. C. Palamidessi. Algebraic properties of idempotent substitutions. In Proc. 17th Int. Colloq. on Automata, Languages and Programming (ICALP’90), LNCS 443, pages 386–399, 1990.

15. U.S. Reddy and S.N. Kamin. On the power of abstract interpretation. Computer Languages, 19(2):79–89, 1993.

16. K.I Rosenthal. Quantales and their Applications. Longman Scientific & Technical, 1990.

17. R.C. Sekar, P. Mishra, and I.V. Ramakrishnan. On the power and limitation of strictness analysis. J. ACM, 44(3):505–525, 1997.

18. B. Steffen. Optimal data flow analysis via observational equivalence. In Proc. 14th Int. Symp. on Math. Found. of Comp. Sci. (MFCS’89), LNCS 379, pages 492–502, 1989.

19. D. Yetter. Quantales and (noncommutative) linear logic. J. Symbolic Logic, 55(1):41–64, 1990.