Abductive Analysis of Modular Logic Programs

ROBERTO GIACOBAZZI, Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, Italy. E-mail: giaco@di.unipi.it

Abstract

We introduce a practical method for abductive analysis of modular logic programs. This is obtained by reversing the deduction process, which is usually applied in static-dataflow analysis of logic programs, on generic, possibly abstract, domains for analysis. The approach is validated in the framework of abstract interpretation. The abduced information provides an abstract specification for program modules which can be of assistance both in top-down development of programs and in compile-time optimization. To the best of our knowledge this is the first application of abductive reasoning in dataflow analysis of logic programs.

Keywords: Static analysis, abstract interpretation, logic programming, modular logic programs, abduction, program specification.

1 Introduction

Dataflow analysis by abstract interpretation is typically intended to statically derive approximated information (analysis) about run-time properties of programs, by applying rules (clauses) to initial states (goals), with the inference of a result. In logic programming, this deductive approach to program analysis is usually based on abstract unfolding (i.e. replacement + abstract unification) and it is shared by most of the frameworks proposed in the literature (e.g., see [3, 6, 7, 8, 14, 29]). A similar deductive method is also applied by Codish et al. [8] in compositional analysis in presence of modules. Compositional abstract interpretation is essential for large program development so that altering one module does not require re-analysis of the entire program. A logic program is viewed as consisting of a set of modules, each module defining a subset of the program’s predicates.

J. Logic Computat., To appear 1997 \begin{matrix}c \\ ◯ \end{matrix}Oxford University Press

2 Abductive Analysis of Modular Logic Programs

The abstract meaning of a module corresponds to its analysis and composition of abstract meanings corresponds to composition of analyses. Analyses are constructed by abstract interpretation of the compositional semantics in [5]. Deduction is obtained by iterating unfolding of program clauses with particular definitions for their extensional part. These definitions can either be assumed imported from other modules (leaving them “open”) or as part of the deduction itself in the fixpoint iteration. In compositional analysis and semantics, abstract and concrete semantic objects have then a clause-like form.

While deduction is a common aspect in both compositional and non compositional dataflow analysis of logic programs, the reverse of deduction makes sense in modular logic programming. The process of reversing deduction is logically justified by the abductive reasoning (an excellent survey on the wide literature on abduction is in [27]). Abductive reasoning is formulated as follows: “given a set of rules (clauses) P and a conjunction of atoms (an observation or simply a goal) G, find the set of atoms Q (the hypothesis) such that G is a logical consequence of P ∪ Q” (see [27, 30]). Atoms in Q are indicated as abducible information. In this paper we consider abduction in the context of static program analysis. We join abductive reasoning and abstract interpretation to derive program properties of modules, once the specification of the properties of their composition is given. We call this analysis abductive. The idea is to show which abstract properties a program module Q (or the semantics of Q) have to satisfy, so that the composition with a program module P (i.e., P ∪ Q) satisfies a given observation.

Abductive analysis is particularly useful in analysis and development of modular logic programs, as it provides a systematic method to analyze module interaction. Indeed, the applicability of transformation or optimization techniques to program modules usually depends on the definition of their “imported” (open) predicates. We specify this dependency by a kind of “precondition” on the semantics of each module, which can be statically derived by abductive analysis. The resulting abstract specification can be interpreted as a constraint on the possible semantics for the open predicates of a module, which has to be satisfied in order to perform program transformations and optimizations. This specification can also be used as a guide in top-down development of module extensions which are consistent with the intended program behavior. Indeed, there is an interesting relation between abduction and specification techniques based on weakest-prespecifications ([23]). We prove that abductive analysis precisely corresponds to compute an abstract weakest-prespecification with respect to program composition defined by set-union of clauses, i.e., the weakest observation that must be met by the program module Q in order that the composition P ∪Q will accomplish the original task specified by its specification. A semantic account of this is provided by showing that abstract abduction corresponds to the abstract weak-op-inverse (cf. [23]) of the traditional T_{P}-based semantics of computed answer substitutions introduced in [16]. This result further justifies the use of abductive analysis in systematic program development.

The rest of this paper is structured as follows: Section 2 presents some preliminary definitions and notations. Section 3 resumes some results on compositional semantics and analysis of modular logic programs. The main contribution is in Section 4, where we characterize abduction as composition inverse, and we introduce a practical method for abductive analysis of modular logic programs. Termination of abductive analysis is discussed in Section 5, while applications are discussed in Section 6. Section 7 concludes. The Appendix contains proofs of related results. This paper is the extended version of [19].

2 Preliminaries

In the following we assume familiarity with the standard definitions and notation for logic programs [2], constraint logic programs [26, 21], abstract interpretation [11, 12] and lattice theory [4].

2.1 Mathematical notation

Let A and B be sets. The powerset of A is denoted by ℘(A). Sequences in A^{∗} are typically denoted by ⟨a_{1}, …, a_{n}⟩ or simply a_{1}, …, a_{n}, for a_{i}’s symbols in A. We let ⟨a_{i}⟩_{i=1}^{n} denote the sequence a_{1}, …, a_{n}. The empty sequence is denoted Λ. Concatenation of sequences s_{1}, s_{2} ∈ A^{∗} is denoted s_{1} :: s_{2}. a|s denotes a sequence with first element a. The set A equipped with a partial order ≤ is denoted ⟨A, ≤⟩. If A is a poset, we usually denote ≤_{A} the corresponding partial order. By x < y we mean x ≤ y and x ≠ y. If I ⊆ A then ↓ I = {x ∈ A | ∃y ∈ I . x ≤_{A} y}. For x ∈ A, ↓ x is a shorthand for ↓ {x}. ℘^{↓}(A) 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. A complete lattice A with partial ordering ≤, least upper bound ∨, greatest lower bound ∧, least element ⊥ = ∨∅ = ∧A, and greatest element ⊤ = ∧∅ = ∨A, is denoted ⟨A, ≤, ∨, ∧, ⊤, ⊥⟩. In the following we will often abuse notation by denoting lattices with their poset notation.

We write f : A → B to mean that f is a total function of A into B. The identity operator λx.x is often denoted id. By g ∘ f we denote the composition of the functions f and g, i.e., ∀x. (g ∘ f )(x) = g(f (x)). The set of fixpoints of a function f is denoted fp(f ), and the least fixpoint (if it exists) is denoted lfp(f ). The ordinal power of an operator f on a complete lattice ⟨A, ≤, ∨, ∧, ⊤, ⊥⟩ is defined as f ↑ 0(X ) = X , f ↑α(X ) = f (f ↑(α − 1)(X )) for every successor ordinal α, and f ↑α(X ) = ∨_{δ<α}f ↑δ(X ) for every limit ordinal α. We omit X if X = ⊥. It is known that when f is continuous, lfp(f ) = f ↑ ω. If A and B are posets and α : B → A, γ : A → B are monotone maps such that for any x ∈ B and y ∈ A, x ≤_{B} γ(α(x)) and α(γ(y)) ≤_{A} y, then we call the quadruple (B, α, A, γ) a Galois connection between B and A. If in addition for any y ∈ A, α(γ(y)) = y, then we call (B, α, A, γ) a Galois insertion of A in B. In the following we call (B, α, A, γ) a Galois insertion. In the setting of abstract interpretation, B and A are called, respectively, the concrete and the abstract domain, and they are assumed to be complete lattices, whereas α and γ are called the abstraction and the concretization maps, respectively. If (B, α, A, γ) is a Galois insertion, then the concretization and abstraction mappings, γ and α, are 1-1 and onto, respectively. Moreover, in any Galois connection α is additive and γ is co-additive, viz. for any X ⊆ B and Y ⊆ A: α(∨_{B}X ) = ∨_{A}α(X ) and γ(∨_{A}Y ) = ∨_{B}γ(Y ). Any Galois connection may be lifted to a Galois insertion identifying in an equivalence class those values of the abstract domain with the same concrete meaning. This process is known as reduction of the abstract domain.

2.2 Logic programming

Throughout, we assume a fixed (non-trivial) set of function symbols Σ, a fixed set of predicate symbols Π and a fixed denumerable set of variables Var, defining a first-order language L. With each function symbol f ∈ Σ and predicate symbol p ∈ Π is associated a unique natural number called its arity: A (predicate or function) symbol f with arity n is written f /n. The set of terms over Σ and Var is denoted Term. Herbrand constraints are finite conjunctions of equations between terms. The system of such Herbrand constraints is denoted by H. Constraints are (possibly infinite) disjunctions of Herbrand constraints. We often view a disjunction of Herbrand constraints as a set of Herbrand constraints. We let false denote the unsatisfiable constraint (e.g., the empty disjunction) and true the always satisfiable constraint (e.g., the empty conjunction). We write θ ≤ θ′ if θ logically implies θ′. C denotes the set of disjunctions of Herbrand constraints over Term modulo logical equivalence. Thus C is a complete lattice ordered by ≤ with bottom element false and top element true, and ∧ as glb. We abuse by denoting (C, ∧) the corresponding concrete constraint system. The set of atoms constructed from predicate symbols in Π and terms from Term is denoted Atom. It is well known that “ordinary” logic programs can be characterized as constraint logic programs on H (see, for example, [26]). This simplifies somehow the presentation. A goal is of the form σ [] ā, where σ is a Herbrand constraint and ā is a sequence of atoms. We occasionally abuse notation and treat the sequence of atoms ā as a set, and write b ∈ ā to refer to an element of this set. The empty sequence of atoms is denoted by true. A (constrained) Horn clause is an object of the form h ⟵ σ [] b̄ where h is an atom (the head), and σ [] b̄ is a goal (the body). When σ = true we write h ⟵ b̄. The set of clauses constructed from elements of Atom is denoted Clause. We will abuse by considering unit clauses and atoms as equivalent notions. We say that a clause h ⟵ σ [] b̄ is normalized if σ is in solved form and h ⟵ b̄ is linear, i.e., contains no multiple occurrences of any variable, and flat, i.e., contains no function symbols or constants. The set of variables occurring in a syntactic object (viz. a term, atom, clause) t is denoted var(t). In the following we assume finitary syntactic objects only, which are syntactic objects s such that var(s) is a finite set. The set of predicates in a syntactic object s is denoted pred(s). A logic program (or module) is a finite set of clauses.

A substitution is a mapping from Var to Term which acts as the identity almost everywhere. The satisfiability of a Herbrand constraint σ, denoted H ⊧ σ, is determined by computing a solution (a set of equations in solved form or most general unifier) of σ. In the following of this paper we will often abuse notation by using ⊧ to denote different notions of satisfiability. We let the reader to distinguish them according to the context. We fix a partial function mgu which maps a pair of syntactic objects to an idempotent most general unifier of the objects if it exists. For a syntactic object t and constraint σ, we write σ(t) to denote tθ where θ = mgu(σ). For a set of constraints Θ, Θ(t) = {σ(t)|σ ∈ Θ}. A syntactic object t is more general than t′ (denoted t′ ≤ t) iff there exists a substitution θ such that t′ = tθ. Syntactic objects t_{1} and t_{2} are equivalent up to renaming, denoted t_{1} ∼ t_{2}, iff t_{1} ≤ t_{2} and t_{2} ≤ t_{1}. Θ_{1} ∼ Θ_{2} iff for any syntactic object s: Θ_{1}(s) ∼ Θ_{2}(s). Term_{/∼}, Atom_{/∼}, Clause_{/∼} and C_{/∼} are all complete lattices with respect to ≤. With abuse of notation, they will be often denoted Term, Atom, Clause and C. Moreover, since all the definitions in the paper are independent on syntactic variable names, we will let the corresponding objects to denote their equivalence classes by renaming. In particular, following Bossi et al. [5], we consider sets of clauses modulo the following notion of equivalence between clauses: We say that (h ⟵ σ [] b̄) ≈ (h′ ⟵ σ′ [] b̄′) iff there exists a permutation b̄′′ of atoms in b̄′ such that σ(h ⟵ b̄) ∼ σ′(h′ ⟵ b̄′′). This identifies clauses which differ syntactically (up to permutation of atoms in the body), yet providing the same implicational relationship between the clause body and its head. For simplicity of exposition, we will abuse notation and assume that a clause represents its equivalence class under ≈, and write Clause rather than Clause_{/≈}. For a syntactic object s and a set of equivalence classes of objects I under ∼ or ≈, we denote by ⟨c_{1}, …, c_{n}⟩ <<_{s} I that c_{1}, …, c_{n} are representatives of elements of I renamed apart from s and from each other.

3 Concrete and abstract semantics for composition

In the following, we summarize the main results in concrete semantics for composition in [5] and compositional analysis in [8]. If P_{1}, …, P_{n} are logic program modules, then P = ∪_{i=1}^{n}P_{i} is a modular logic program. Such a program is said to be predicate disjoint if no predicate is defined in more than one module. We assume that modular programs are predicate disjoint unless otherwise specified. This assumption, considered also in [8, 27], somewhat simplifies the presentation. For a logic program (or module) P, open(P) denotes the set of predicates that occur in the body of a clause in P but are not defined in P (we often call them abducible predicates)^{1}.

1The predicate disjoint restriction has the advantage that abducible information (for open(P))

is basic [27], i.e. it is not defined in terms of other abducible information. For a set of abducible predicates, we can always transform P (as suggested in [27]) in such a way that it does not have definitions for them: For each abducible predicate p, we can introduce a new predicate δ_{p} and add

3.1 Concrete semantics

The base semantics is the compositional bottom-up semantics of Bossi et al. [5], instantiated to the case of predicate disjoint modules. In [5], an interpretation is any element in Int = ℘(Clause). Programs and interpretations have then the same structure (i.e. sets of clauses). The concrete semantics is formalized in terms of unfolding of clauses unf : Int ×Int → Int, specifying every possible way to unfold each literal in each clause of P_{1} once using clauses in P_{2} (see [28]):

unf (P_{1}, P_{2}) = \{ h ⟵ σ′ [] b̄_{1} :: ⋯:: b̄_{n} | \begin{matrix}c = h ⟵ σ [] g_{1}, …, g_{n} ∈ P_{1} \\ ⟨h_{i} ⟵ σ_{i} [] b̄_{i}⟩_{i=1}^{n} <<_{c} P_{2} \\ σ′ = σ ∧ ∧_{i=1}^{n} (σ_{i} ∧ \{g_{i} = h_{i}\}) \\ H ⊧ σ′ \end{matrix} \}

unf is a binary associative operator (see [15]) on Int, which is additive on its first argument and continuous on its second one. This operator is of interest as it can be applied to formalize both top-down and bottom-up semantics for logic programs (cf. [28]). A bottom-up semantics for open logic programs is defined in [5] in terms of “iterated unfolding” — that is, repeatedly unfolding the clauses in a program until further unfolding produces no change. The fixpoint semantics of a program P is given by the function F : Int → Int, defined as F(P) = lfp(T_{P}), where T_{P} : Int → Int is defined as T_{P}(I ) = unf (P, I ∪ Φ_{P}), and where for any program P,

Φ_{P} = { p(x̄) ⟵ p(x̄) | p ∈ open(P) } .

The idea of Bossi et al. [5], is to unfold only those predicates which have a definition, so that the meaning of a program becomes dependent on the meaning of its open predicates. Technically, this is obtained by adding the tautological clauses Φ_{P} for the open predicates of a program P and unfolding all predicates in the body of a clause. Notice that the unfolding of an open predicate in a clause body with a tautological clause is basically a “no-op”. Moreover, note that if open(P) = ∅ then Φ_{P} = ∅ and T_{P}(I ) = unf (P, I ). When I consists of unit clauses (facts), the fixpoint operator gives precisely the (non-ground) fixpoint semantics of Falaschi et al. [16]. The following theorem (see Theorem 2.13 and Corollary 4.15 in [5]) formalizes the notion of compositional semantics based on clause unfolding and provides the basis for the compositional analyses described below.

Theorem 3.1 [concrete composition [5]] Let P_{1} and P_{2} be modules. Then: F(P_{1} ∪ P_{2}) = F(F(P_{1}) ∪ F(P_{2})).

Example 3.2 Consider the following modular logic program with modules P_{lg} and P_{num}:

the clause p(x) ⟵ δ_{p}(x). The resulting program is such that p ∉ open(P) but δ_{p} ∈ open(P) (i.e. δ_{p} becomes abducible). It is worth noting that this restriction still allows mutually recursive modules.

P_{lg} gt(s(X),0) :- num(X).  P_{num} num(0).
     gt(s(X),s(Y)) :- gt(X,Y).        num(s(X)) :- num(X).
     le(0,Y) :- num(Y).
     le(s(X),s(Y)) :- le(X,Y).

The unfoldings of P_{lg} specify the relations “less or equal” and “greater than” on a domain of values specified by the predicate num which is open. Evaluation of F(P_{lg}) proceeds as follows:

(1) \begin{matrix}gt(s(X ), 0) ⟵ num(X ) \\ le(0, Y ) ⟵ num(Y ) \end{matrix} (2) \begin{matrix}gt(s(s(X )), s(0)) ⟵ num(X ) \\ le(s(0), s(Y )) ⟵ num(Y ) \end{matrix} ....

Since open(P_{num}) = ∅, F(P_{num}) = {num(0), num(s(0)), num(s(s(0))), …}. The meaning of P_{lg} ∪ P_{num} can be evaluated directly or by applying Theorem 3.1. In both cases the result corresponds to the standard meaning as provided by the semantics of [16].

3.2 Abstract semantics and deductive analysis

The relevance of compositionality in logic program analysis has been firstly addressed in [8] by introducing a framework which is based on the compositional semantics F, and which formalizes the analysis in terms of the standard theory of abstract interpretation ([12]). In this section we briefly introduce some notions and results from [8, 18]. For the sake of completeness, we include in the appendix the proofs of those results which are relevant for abductive analysis. We follow [8] by assuming that (Int, α, AInt, γ) is a Galois insertion, and that the abstract semantics F^{A} : AInt → AInt safely mimics F, i.e. for each I ∈ Int: α(F(I )) ⊑ F^{A}(α(I )). The abstract semantics of a program module P is F^{A}(α(P)).

Theorem 3.3 [correctness of compositional analysis [8]] Let (Int, α, AInt, γ) be a Galois insertion, and F^{A} : AInt → AInt be a monotonic and safe approximation of F. Then, for any program module P_{1}, P_{2} ∈ Int:

α(F(P_{1} ∪ P_{2})) ⊑ F^{A}(F^{A}(α(P_{1})) ⊔ F^{A}(α(P_{1})))

Proof. See the Appendix.

A safe approximation of F can be obtained by abstracting unfolding. The definition of the function F^{A} is given in [8] in terms of abstract unfolding of clauses, which is clause unfolding relatively to an abstract operator of unification, defined on an abstract domain of substitutions. We generalize the approach in [8], by abstracting unfolding on arbitrary domains of constraints. We firstly introduce the notion of abstract constraint system, which generalizes in a single algebraic structure both the notion of abstract unification and the domain of abstract substitution.

Definition 3.4 [abstract constraint system] An abstract constraint system (A, ⊗), is a complete lattice ⟨A, ⪯⟩, the domain of abstract constraints, together with a binary associative and commutative operator ⊗, such that (C, α_{A}, A, γ_{A}) forms a Galois insertion, and ⊗ is correct with respect to ∧, i.e. α_{A}(c_{1} ∧ c_{2}) ⪯_{A} α_{A}(c_{1}) ⊗ α_{A}(c_{2}).

An abstract constraint system (A, ⊗) is noetherian if A does not contain an infinite ascending chain of constraints with a bounded set of free variables. Formally, this condition can be specified by assuming that there is no infinite set {κ_{i}}_{i≥0} ⊆ A such that γ_{A}(κ_{i})(s) ⊂ γ_{A}(κ_{i+1})(s) for some syntactic object s and i ≥ 0. Analogously, a constraint system is finite if there is no infinite set {κ_{i}}_{i≥0} ⊆ A such that γ_{A}(κ_{i})(s) ≠ γ_{A}(κ_{j} )(s) for some syntactic object s and i ≠ j (for more details on noetherian and finite constraint systems see [21]). In the following we assume noetherian abstract constraint systems A, where ⊗ and ⊕ are the greatest lower bound and least upper bound in ⟨A, ⪯⟩.

Example 3.5 The running example of abstract domain throughout the paper is Pos ([1, 10]), defined by Marriott and Søndergaard for ground dependency analysis. We restrict the definition of Pos to a finite (non-empty) set of variables of interest V ⊆ Var. Pos_{V} is the finite lattice (indeed Boolean lattice) of positive Boolean functions on V , where a Boolean function f is positive if f (true, …, true) = true. In the following we will often denote Pos the domain Pos_{V} for some finite (non-empty) set V ⊆ Var. Pos is ordered by logical implication →, and therefore the lub and glb in Pos are given by logical disjunction and conjunction respectively. The domain Pos can therefore be represented by propositional formulae, with basic connectives ∧, ∨ and ↔. Pos provides a concise representation for abstract substitutions which describe ground dependency relations among their arguments. The generalization to Herbrand constraints is straightforward (e.g. see [21]). A propositional formula with connectives {↔, ∨, ∧} is associated with each constraint. For example, the formula x represents any constraint ϑ such that ϑ(x) is ground, while x ↔ (y ∧ z) represents any constraint ϑ such that var(ϑ(x)) = var(ϑ(y)) ∪ var(ϑ(z)) (x is ground iff y and z are ground). ∨ is used to represent sets containing substitutions, and exploiting different ground dependencies. We call ground dependency any element in Pos. We say that a truth assignment ξ satisfies a propositional formula f , written ξ ⊧ f iff ξ(f ) is a tautology. Define the truth assignment asg : C → Var → {true, false} such that, given θ ∈ C, asg(θ)(x) = true iff θ(x) is ground (i.e. var(θ(x)) = ∅). Note that ground dependencies are closed under instantiation, namely if θ grounds x then any θ′ ≤ θ grounds x too. Thus γ_{Pos}(κ) = {θ ∈ C | θ′ ≤ θ ⇒ asg(θ′) ⊧ κ}. The corresponding structure is (Pos, ∧) which is well known to be finite, correct and to form a Galois insertion with the concrete constraint system (C, ∧) (e.g. see [10]), indeed being a finite abstract constraint system.

Abstract semantic objects are descriptions (on A) of clauses. An abstract clause is an object of the form h ⟵ κ [] b̄ such that κ ∈ A and h ⟵ true [] b̄ is normalized. The set of abstract clauses on A is denoted Clause^{A}. An abstract interpretation is then a set of abstract clauses in ℘(Clause^{A}) modulo reduction, viz. modulo equivalence under concretization^{2}: I_{1}^{a} ≅ I_{2}^{a} iff γ(I_{1}^{a}) = γ(I_{2}^{a}), where γ : ℘(Clause^{A}) → ℘(Clause) is such that for any I^{a} ∈ ℘(Clause^{A}):

γ(I^{a}) = \{ h ⟵ σ [] b̄ | \begin{matrix}h ⟵ κ [] b̄ ∈ I^{a} \\ σ ∈ γ_{A}(κ) \end{matrix} \} .

We denote AInt_{A} the set of abstract interpretations on A, and we will often omit A when this is clear from the context. It is worth noting that, from the definition of γ, ≅ includes variable hiding and equivalence up to renaming. This construction induces a Galois insertion (Int, α, AInt, γ) as proved in [8]. In particular ⟨AInt, ⊑ , ⊔, ⊓, [Clause^{A}]≅, [∅]≅⟩ is a complete lattice. The abstract unfolding operator unf^{A} : AInt × AInt → AInt is defined in [8] as:

unf^{A}(P_{1}^{a}, P_{2}^{a}) = \{ h ⟵ κ′ [] b̄_{1} :: ⋯:: b̄_{n} | \begin{matrix}c = h ⟵ κ [] g_{1}, …, g_{n} ∈ P_{1}^{a} \\ ⟨h_{i} ⟵ κ_{i} [] b̄_{i}⟩_{i=1}^{n} <<_{c} P_{2}^{a} \\ κ′ = κ⊗ ⊗_{i=1}^{n} (κ_{i} ⊗ α_{A}(g_{i} = h_{i})) \end{matrix} \} .

The following lemmata specify the basic algebraic properties of abstract unfolding.

Lemma 3.6 For any abstract constraint system (A, ⊗), unf^{A} is left-additive.

Proof. See the Appendix.

≅ is a congruence relation with respect to unf^{A}, i.e. unf^{A} is well-defined. Therefore, in the following, we let sets of abstract clauses to denote their equivalence classes under ≅.

Lemma 3.7 If P_{1}^{a} ≅ Q_{1}^{a} and P_{2}^{a} ≅ Q_{2}^{a} then unf^{A}(P_{1}^{a}, P_{2}^{a}) ≅ unf^{A}(Q_{1}^{a}, Q_{2}^{a}).

Proof. See the Appendix.

As well as concrete unfolding, unf^{A} is associative, and right-continuous.

Lemma 3.8 For any abstract constraint system (A, ⊗), unf^{A} is associative and right-continuous.

Proof. See the Appendix.

Componentwise correctness of abstract unfolding is a consequence of correctness of abstract constraint systems.

2The name abstract interpretation is clearly overloaded here. In the following we leave to the reader to distinguish, according to the context, between abstract interpretation as the theory developed in [11] and as the abstraction of (logical) interpretations of Horn clause logic.

Lemma 3.9 [unfolding correctness] Let (A, ⊗) be an abstract constraint system. Then, for every I_{1}, I_{2} ∈ Int,

α(unf (I_{1}, I_{2})) ⊑ unf^{A}(α(I_{1}), α(I_{2}))

Proof. See the Appendix.

The abstract semantics F^{A} : AInt → AInt is defined for a program module P as F^{A}(α(P)) = lfp(T_{α(P)}^{A}) where T_{α(P)}^{A} : AInt → AInt is defined by T_{α(P)}^{A}(I^{a}) = unf^{A}(α(P), I^{a} ⊔ α(Φ_{P})). By Lemma 3.9, because α is additive in any Galois connection, and λI^{a}.unf^{A}(α(P), I^{a}) is continuous: F^{A} is correct with respect F, therefore satisfying the hypothesis of Theorem 3.3.

Proposition 3.10 For any I ∈ Int: α(F(I )) ⊑ F^{A}(α(I )).

The following example shows a simple compositional analysis of modular logic programs (see [8] for more details).

Example 3.11 The deductive compositional analysis for ground dependencies for P_{lg} and P_{num} in Example 3.2 are respectively:

F^{Pos}(α(P_{lg})) = \{ \begin{matrix}gt(x, y) ⟵ y [] num(x) \\ le(x, y) ⟵ x [] num(y) \end{matrix} \}
F^{Pos}(α(P_{lg})) = {num(x) ⟵ x [] true}

The analysis for the program P_{lg} ∪ P_{num} can be obtained by composing the analysis for P_{lg} and P_{num}. This provides an approximation for the concrete semantics F(P_{lg} ∪ P_{num}).

α(F(P_{lg} ∪ P_{num})) ⊑ F^{Pos}(F^{Pos}(α(P_{lg})) ⊔ F^{Pos}(α(P_{num})))
⊑ \{ \begin{matrix}gt(x, y) ⟵ y ∧ x [] true \\ le(x, y) ⟵ x ∧ y [] true \\ num(x) ⟵ x [] true \end{matrix} \}

4 Abductive analysis

In this section we introduce the notion of abductive analysis of modular logic programs. We firstly investigate the relation between abduction of program composition in the following section.

4.1 Abduction as composition inverse

Given a program module P, our goal is to find a specification (property) for open(P) once a reasonable specification of P is given^{3}. A formal account of this process can be given in terms of the well known Dijkstra’s weakest precondition or weakest prespecification [23].

Definition 4.1 f^{−} is a weak-op-inverse of f : D → D′ iff (D, f , D′, f^{−}) is a Galois connection.

This terminology has been introduced in [23] to generalize the inverse of sequential command composition ; on specifications. In this context, given a program specification R, the weak-op-inverse f_{R}^{−} of f_{R} = λX .X ; R (when it exists) provides the weakestprespecification, i.e. the weakest specification that must be met by the subprogram P in order that, given the specification W , P; R will accomplish the task W . It is immediate that: f^{−} exists iff f is additive, and f^{−} is uniquely determined by f (e.g. see [12]).

Let F : Int → Int be an idempotent operator which is compositional (in the sense of Theorem 3.1), i.e. for any P_{1}, P_{2} ∈ Int: F(P_{1} ∪ P_{2}) = F(F(P_{1}) ∪ F(P_{2})) (e.g. the unfolding-based semantics in [5] meets these requirements). In this case, the semantics of P is F(P).

Definition 4.2 [program properties] A program property is any element in ℘(Int). A program P satisfies a property P ∈ ℘(Int) (written P ⊧ P) iff F(P) ∈ P.

An additive semantics for logic programs can be provided by lifting F on program properties. For any property X ∈ ℘(Int), we define the deductive semantics for composition for a program P, as follows: S_{P}(X) = {F(P ∪ X ) | X ∈ X }. The weak-op-inverse of S_{P} exists and it is uniquely defined as S_{P}^{−}(X) = {Y | F(P ∪ Y ) ∈ X }.

The following result provides an alternative view of abduction, relating abducible information with weak-op-inverses of deductive semantics for composition.

Theorem 4.3 Q ⊧ S_{P}^{−}(P) iff P ∪ Q ⊧ P.

3We are considering a rather simple notion of abduction, which is specialized for positive logic programs without integrity constraints.

Proof. Let P and Q be programs and P ∈ ℘(Int):

Q ⊧ S_{P}^{−}(P) iff F(Q) ∈ { Y | F(P ∪ Y ) ∈ P }

[ definition ]

iff F(P ∪ F(Q)) ∈ P

[ definition ]

iff F(F(P) ∪ F(Q)) ∈ P

[ idempotence ]

iff F(P ∪ Q) ∈ P

[ compositionality ]

iff P ∪ Q ⊧ P

[ definition ]

S_{P}^{−} is often useless even when computed on abstract domains as it is not constructively defined from F. In the following of this section we provide: (1) a concise definition of program properties that can easily cope with abstract domains; and (2) a practical method to approximate abduction on abstract domains, providing terminating abductive analysis of modular logic programs. We will be mainly concerned with properties of successful computations, therefore we will always refer to properties as collections of sets of unit-clauses, representing success patterns, in ℘(Int).

4.2 Program properties as (abstract) observations

We introduce the notion of abstract observation for a module in a Galois insertion (Int, α, AInt, γ). Intuitively, an abstract observation for a program has to describe the meaning of its defined predicates, so that they satisfy a given property. In our case, abstract observations for a program module P will be abstract goals on the predicates defined in P. A goal κ [] b̄ is then intended to describe any program P providing meaning for the atoms in b̄, so that the constraint κ is satisfied in any successful derivation for b̄ in P.

Example 4.4 The abstract observation x ↔ y [] p(x, y) is intended to describe any possible definition for p: p(x, y) ⟵ κ, such that κ → (x ↔ y). It is easy to see that any program with abstract semantics: p(x, y) ⟵ x ∧ y satisfies the observation.

In the concrete semantics, for a program P and goal G = σ [] b̄, G has a successful derivation in P iff, by extending G to a clause: ans ⟵ G with a new atom ans such that var(ans) = var(b̄), there exists ans ⟵ σ′ [] true ∈ unf ({ans ⟵ G}, F(P)) (e.g. see [28]). In this case we say that σ′ is the answer constraint. In the following, for any set of variables V , we denote ans(V ) a flat and linear atom such that var(ans(V )) = V . To simplify the notation, for any syntactic object s, we denote ans(s) the atom ans(var(s)), and we will omit V when it can be deduced from the context. We extend this notation to abstract goals (observations) and programs: Let P be a program module and G^{a} be an abstract observation (or simply an abstract goal), the goal G^{a} has an abstract successful derivation in α(P) iff ans ⟵ κ [] true ∈ unf^{A}({ans ⟵ G^{a}}, F^{A}(α(P))). The correctness of abstract successful derivations is a consequence of the following lemma.

Lemma 4.5 Let unf^{A} be a safe and monotone approximation for unf in (Int, α, AInt, γ), and F^{A} be the corresponding abstract fixpoint semantics. For a program module P and goal G^{a}:

unf (γ({ans ⟵ G^{a}}), F(P)) ⊆ γ(unf^{A}({ans ⟵ G^{a}}, F^{A}(α(P)))).

Proof. Note that by correctness in Proposition 3.10, F(P) ⊆ γ(F^{A}(α(P))). The proof follows by unf^{A} correctness (Lemma 3.9) and monotonicity:

unf (γ({ans ⟵ G^{a}}), F(P)) ⊆ unf (γ({ans ⟵ G^{a}}), γ(F^{A}(α(P))))

[ monotonicity ]

⊆ γ(unf^{A}({ans ⟵ G^{a}}, F^{A}(α(P))))

[ correctness ] .

We are now able to formally define when a program satisfies an abstract observation. Intuitively a program satisfies an abstract observation κ [] b̄ if κ is weaker than (logically implied by) any successful (abstract) derivation for b̄ in α(P). This is formalized by the following

Definition 4.6 A program P satisfies an abstract observation κ [] b̄ with respect to a set of variables V , assuming an abstract constraint κ̃, denoted P ⊧κ̃ ; V κ [] b̄, iff for each

ans(V ∪ var(b̄)) ⟵ κ′ [] b̄′ ∈ unf^{A}({ans(V ∪ var(b̄)) ⟵ κ̃ [] b̄}, F^{A}(α(P))),

we have b̄′ = true and γ_{A}(κ′)(ans(V ∪ var(b̄))) ⊆ γ_{A}(κ)(ans(V ∪ var(b̄))).

κ̃ in Definition 4.6 represents the current store (constraint) of the computation. The evaluation of the goal b̄ is therefore obtained with respect to κ̃. The distinction between κ̃ and κ is essential in order to distinguish between the current store of the computation, and what is required to be satisfied in the observation. The condition γ_{A}(κ′)(ans(V ∪ var(b̄))) ⊆ γ_{A}(κ)(ans(V ∪ var(b̄))) specifies that κ′ is stronger than κ when restricted to the variables in V ∪ var(b̄). If P ⊧κ̃ ; V κ [] b̄ and V ⊆ var(b̄) and κ̃ = true, we simply say that P satisfies κ [] b̄ (denoted P ⊧ κ [] b̄).

The following example shows the relevance of the set V in the relation P ⊧_{V} G^{a}.

Example 4.7 Consider the abstract observation x [] p(y). It is easy to see that for any program P = {p(y) ⟵ κ [] true} (i.e. where κ defines a constraint on y): P ⊧ x [] p(y) (viz. (∃_{x} x) ∧ κ = κ) but P |̸=_{{x}} x [] p(y) (viz. x ∧ κ ≠ κ).

The notion of observation and the relation ⊧ can be easily extended to cope with abstract programs P^{a} (viz. interpretations in AInt) in the obvious way, i.e. by substituting F^{A}(α(P)) with F^{A}(P^{a}) in Definition 4.6.

Example 4.8 Consider the goal G^{a} = x ↔ z [] p(x, y), p(y, z) and the program

P^{a} = {p(x, y) ⟵ x ↔ y [] true}

F^{Pos}(P^{a}) = P^{a}, moreover, unf^{Pos}({ans ⟵ p(x, y), p(y, z)}, F^{Pos}(P^{a})) = {ans ⟵ (x ↔ y) ∧ (y ↔ z) [] true}, and because ((x ↔ y) ∧ (y ↔ z)) → (x ↔ z) is a tautology, we can conclude that P^{a} ⊧ G^{a}.

Proposition 4.9 [downward closure of observations] Given an abstract observation G^{a}, κ̃ ∈ A, V ⊆ Var and I^{a}, J^{a} ∈ AInt defining the same set of predicates: If I^{a} ⊧κ̃ ; V G^{a} and γ(J^{a}) ⊆ γ(I^{a}) then J^{a} ⊧κ̃ ; V G^{a}.

Proof. Assume I^{a} ⊧κ̃ ; V G^{a} and γ(J^{a}) ⊆ γ(I^{a}), where G^{a} = κ [] b̄. It is worth noting that γ(J^{a}) ⊆ γ(I^{a}) iff J^{a} ⊑ I^{a} (cf. [12]). By definition, for each

ans(V ∪ var(b̄)) ⟵ κ′ [] b̄′ ∈ unf^{A}({ans(V ∪ var(b̄)) ⟵ κ̃ [] b̄}, F^{A}(α(γ(I^{a}))))

we have b̄′ = true and γ_{A}(κ′)(ans(V ∪ var(b̄))) ⊆ γ_{A}(κ)(ans(V ∪ var(b̄))). By Galois insertions, α(γ(I^{a})) = I^{a}, and by monotonicity of unf^{A} and F^{A} we have

unf^{A}(C , F^{A}(J^{a})) ⊑ unf^{A}(C , F^{A}(I^{a}))

where C = {ans(V ∪ var(b̄)) ⟵ κ̃ [] b̄}. Therefore, by definition of ⊑, for each

ans(V ∪ var(b̄)) ⟵ κ′′ [] b̄′ ∈ unf^{A}({ans(V ∪ var(b̄)) ⟵ κ̃ [] b̄}, F^{A}(J^{a}))

we have: b̄′ = true and γ_{A}(κ′′)(ans(V ∪ var(b̄))) ⊆ γ_{A}(κ′)(ans(V ∪ var(b̄))), for some

ans(V ∪ var(b̄)) ⟵ κ′ [] true ∈ unf^{A}({ans(V ∪ var(b̄)) ⟵ κ̃ [] b̄}, F^{A}(I^{a})).

The thesis follows because by hypothesis:

γ_{A}(κ′)(ans(V ∪ var(b̄))) ⊆ γ_{A}(κ)(ans(V ∪ var(b̄))).

An abstract program property (i.e. an element in ℘(AInt)) can be associated with each abstract observation G^{a}, κ ∈ A and V ⊆ Var:

P_{V}^{κ} (G^{a}) = {I^{a} ∈ AInt | I^{a} ⊧_{V}^{κ} G^{a} and I^{a} contains only facts}

It is well known (e.g. see [12]) that, if ⟨Int, ⊆⟩ is a complete lattice, and (Int, α, AInt, γ) is a Galois insertion, then I^{a} ⊑ J^{a} iff γ(J^{a}) ⊆ γ(I^{a}), and ⟨AInt, ⊑⟩ is a complete lattice. By Proposition 4.9, P_{V}^{κ} (G^{a}) is an abstract program property which is downward closed with respect to ⊑, viz. an order-ideal in ℘^{↓}(AInt). Goals, or equivalently observations, are therefore adequate to concisely represent program properties which are order-ideals of interpretations. Of course, observations cannot describe arbitrary program properties (viz. elements in ℘(AInt)), as (℘(AInt), λx. ↓ x, ℘^{↓}(AInt), id) is a Galois insertion, i.e. ℘^{↓}(AInt) is a strict abstraction of ℘(AInt). The following result is a straightforward consequence of Lemma 4.5 and Proposition 4.9.

Corollary 4.10 Let P be a program, G^{a} be an observation, κ ∈ A and V ⊆ Var. Then

1. P ⊧_{V}^{κ} G^{a} ⇔ F^{A}(α(P)) ∈ P_{V}^{κ} (G^{a})

2. P ⊧_{V}^{κ} G^{a} ⇒ α(F(P)) ∈ P_{V}^{κ} (G^{a}).

The above notion of satisfiability for abstract observations can be extended to concrete goals and concrete derivations in the obvious way. The following result specifies a relation between satisfiability and concrete derivations for a program.

Theorem 4.11 [correctness of abstract observations] If a program module P satisfies an abstract observation κ [] b̄, then for any successful derivation for b̄ in P with answer constraint σ, σ(b̄) ∈ γ_{A}(κ)(b̄).

Proof. Assume P satisfies the abstract observation κ [] b̄. Then, by definition, for each ans(b̄) ⟵ κ′′ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P))):

γ_{A}(κ′′)(ans(b̄)) ⊆ γ_{A}(κ)(ans(b̄)).

By γ_{A} monotonicity and because γ_{A}(κ′′)(ans(b̄)) ⊆ γ_{A}(κ)(ans(b̄)) implies γ_{A}(κ′′)(b̄) ⊆ γ_{A}(κ)(b̄), then for each ans(b̄) ⟵ σ [] true ∈ γ(unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P)))):

σ(b̄) ∈ γ_{A}(κ′′)(b̄) ⊆ γ_{A}(κ)(b̄).

By Lemma 4.5, for each ans(b̄) ⟵ σ [] true ∈ unf ({ans(b̄) ⟵ b̄}, F(P)):

σ(b̄) ∈ γ_{A}(κ)(b̄)

which concludes the proof.

4.3 Abductive program analysis

In the case of program modules with open predicates, any abstract observation specifies implicitly an abstract observation on the semantics of the open predicates. The abstract observations for the open predicates of a module P can be derived from any observation of P via unfolding. Notice that given an abstract observation G^{a} for P, unf^{A}({ans ⟵ G^{a}}, F^{A}(α(P))) contains only abstract observations for predicates in open(P), thus specifying a set of abstract observations for the open predicates. We say that Q extends P iff open(Q) = ∅ and open(P ∪Q) = ∅, namely when Q provides a complete definition for the meaning of the open predicates in P.

Correctness as specified in Theorem 3.3 is not enough to define abductive analysis based on F^{A}. Indeed, the relation α(F(P ∪ Q)) ⊑ F^{A}(F^{A}(α(P)) ⊔ F^{A}(α(Q))) does not specify how F^{A} distributes over module composition. For abductive analysis we distinguish between two forms of composition.

Definition 4.12 [compositional correctness and completeness] Let F^{A} be a safe approximation for F in a Galois insertion (Int, α, AInt, γ). F^{A} is compositional correct iff F^{A}(α(P ∪ Q)) ⊑ F^{A}(F^{A}(α(P)) ⊔ F^{A}(α(Q))). F^{A} is compositional complete iff F^{A}(α(P ∪ Q)) = F^{A}(F^{A}(α(P)) ⊔ F^{A}(α(Q))).

The reason of this distinction will be more clear in Section 5, where the weaker notion of compositional correctness characterizes the loss of precision resulting from some termination strategies. In the following, when not specified otherwise, we assume compositional correctness for F^{A}. The following theorem justifies the use of “abstract abduction” for abductive analysis of modular logic programs.

Theorem 4.13 [abductive analysis I] Let P, Q be program modules such that Q extends P, and κ [] b̄ be an abstract observation for P. If for each ans ⟵ κ̃ [] ḡ ∈ unf^{A}({ans ⟵ b̄}, F^{A}(α(P))): Q ⊧κ̃ ; var(b̄) κ ⊗ κ̃ [] ḡ, then P ∪ Q ⊧ κ [] b̄.

Proof. The proof is based on unf^{A} associativity (Lemma 3.8) and compositional correctness. To simplify the notation, in this proof we denote by ⪯_{s} the preorder on abstract constraints such that κ ⪯_{s} κ′ iff γ_{A}(κ)(s) ⊆ γ_{A}(κ′)(s). Notice that by the properties of ⊗ and because γ_{A} is co-additive in any Galois connection, then for each κ, κ′ ∈ A: γ_{A}(κ⊗κ′)(s) = γ_{A}(κ)∧γ_{A}(κ′)(s). Moreover, note that ⊗ is still the greatest lower bound in A/_{=s} , where =_{s} is the equivalence relation induced by ⪯_{s}. By definition: Q ⊧_{var(b̄)}^{κ′} κ′ ⊗ κ [] ḡ, where ans(b̄) ⟵ κ′ [] ḡ ∈ unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P))), iff for each ans(b̄ :: ḡ) ⟵ κ′′ [] true ∈ unf^{A}({ans(b̄ :: ḡ) ⟵ κ′ [] ḡ}, F^{A}(α(Q))): κ′′ ⪯_{b̄::ḡ} κ′ ⊗ κ. By the unf^{A} definition the previous condition is satisfied iff for each

ans(b̄ :: ḡ) ⟵ κ′′ [] true ∈ unf^{A}(unf^{A}({ans(b̄ :: ḡ) ⟵ b̄}, F^{A}(α(P))), F^{A}(α(Q)))

κ′′ ⪯_{b̄::ḡ} κ′ ⊗ κ, where ans(b̄ :: ḡ) ⟵ κ′ [] ḡ ∈ unf^{A}({ans(b̄ :: ḡ) ⟵ b̄}, F^{A}(α(P))). By unf^{A} associativity (see Lemma 3.8), for each

ans(b̄ :: ḡ) ⟵ κ′′ [] true ∈ unf^{A}({ans(b̄ :: ḡ) ⟵ b̄}, unf^{A}(F^{A}(α(P)), F^{A}(α(Q)))) κ′′ ⪯_{b̄::ḡ} κ′ ⊗ κ where ans(b̄ :: ḡ) ⟵ κ′ [] ḡ ∈ unf^{A}({ans(b̄ :: ḡ) ⟵ b̄}, F^{A}(α(P))). Because κ′′ ⪯_{b̄::ḡ} κ′ ⊗ κ implies κ′′ ⪯b̄ κ′ ⊗ κ and κ′ ⊗ κ ⪯b̄ κ, then for each

ans(b̄) ⟵ κ′′ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, unf^{A}(F^{A}(α(P)), F^{A}(α(Q))))

κ′′ ⪯b̄ κ. By the hypothesis, Q extends P, namely open(Q) = ∅ and open(P ∪ Q) = ∅. Thus:

unf^{A}(F^{A}(α(P)), F^{A}(α(Q))) = F^{A}(F^{A}(α(P)) ∪ F^{A}(α(Q))).

Moreover, by compositional correctness:

F^{A}(α(P ∪ Q)) = F^{A}(α(P) ∪ α(Q)) ⊑ unf^{A}(F^{A}(α(P)), F^{A}(α(Q))).

Thus, for each ans(b̄) ⟵ ξ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P ∪Q))) there exists

ans(b̄) ⟵ κ′′ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, unf^{A}(F^{A}(α(P)), F^{A}(α(Q))))

such that ξ ⪯b̄ κ′′. Hence, because κ′′ ⪯b̄ κ, we obtain that for each

ans(b̄) ⟵ ξ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P ∪ Q))) : ξ ⪯b̄ κ

which concludes the proof.

An abstract observation for the open predicates of a module P can then be derived by solving the required observation for P in the compositional analysis of the module itself. Notice that, because Q extends P, Q can also be joined with the semantics of all the modules that define predicates in open(P). The converse of Theorem 4.13 is valid only for compositional complete abstract semantics.

Theorem 4.14 [abductive analysis II] Let P, Q be program modules such that Q extends P, F^{A} be compositional complete and κ [] b̄ be an abstract observation for P. P ∪ Q ⊧ κ [] b̄ iff for each ans ⟵ κ̃ [] ḡ ∈ unf^{A}({ans ⟵ b̄}, F^{A}(α(P))): Q ⊧κ̃ ; var(b̄) κ ⊗ κ̃ [] ḡ.

Proof. The proof is analogous to that of Theorem 4.13. By substituting compositional correctness with compositional completeness in the proof of Theorem 4.13, we obtain that

ans(b̄) ⟵ ξ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P ∪ Q)))

iff

ans(b̄) ⟵ ξ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, unf^{A}(F^{A}(α(P)), F^{A}(α(Q))))

Therefore, by hypothesis, we have that for each

ans(b̄) ⟵ ξ [] true ∈ unf^{A}({ans(b̄) ⟵ b̄}, unf^{A}(F^{A}(α(P)), F^{A}(α(Q))))

ξ ⪯b̄ κ. By associativity (Lemma 3.8) we have that for each

ans(b̄) ⟵ ξ [] true ∈ unf^{A}(unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P))), F^{A}(α(Q)))

ξ ⪯b̄ κ. Hence, for each

ans(b̄ :: ḡ) ⟵ κ̃ [] ḡ ∈ unf^{A}({ans(b̄) ⟵ b̄}, F^{A}(α(P)))

we have

ans(b̄ :: ḡ) ⟵ ξ [] true ∈ unf^{A}({ans(b̄ :: ḡ) ⟵ κ̃ [] ḡ}, F^{A}(α(Q)))

and ξ ⪯b̄ κ. We can assume without loss of generality that κ does not affect variables in ḡ. Therefore we have ξ ⪯_{b̄::ḡ} κ, which implies that ξ ⊗ κ̃ ⪯_{b̄::ḡ} κ ⊗ κ̃. It is worth noting that ξ ⊗ κ̃ = ξ, as ξ is obtained by unfolding of ans(b̄ :: ḡ) ⟵ κ̃ [] ḡ. Hence, for each

ans(b̄ :: ḡ) ⟵ ξ [] true ∈ unf^{A}({ans(b̄ :: ḡ) ⟵ κ̃ [] ḡ}, F^{A}(α(Q)))

ξ ⪯_{b̄::ḡ} κ ⊗ κ̃, and therefore by definition: Q ⊧κ̃ ; var(b̄) κ ⊗ κ̃ [] ḡ.

It is worth noting that this result provides an efficient and concise way to approximate, on generic abstract domains, the weak-op-inverse of program composition (cf. Theorem 4.3).

Example 4.15 Let P = {p(x, z) ⟵ q(x, y), q(y, z)} be an open program, and G^{a} = x ↔ y [] p(x, y) be an abstract observation for P. As shown in Example 4.8, Q = {q(x, y) ⟵ x ↔ y [] true} satisfies the abstract observation for the open predicate q: x ↔ z [] q(x, y), q(y, z) which is obtained by solving the observation G^{a} in the compositional abstract semantics for P. By Theorem 4.13: P ∪ Q satisfies G^{a}.

The unfolding of an abstract observation for a module P into the abstract semantics of P produces a set of abstract observations for the open predicates, yet specifying relations on the original predicates defined in P. Projecting out this information (on the variables of the new observation only) may lead to an inconsistent result, as shown in the following example.

Example 4.16 Consider the program P = {p(x, y) ⟵ q(y)} and the abstract observation x [] p(x, y). By unfolding we obtain the observation x [] q(y). Intuitively, no definition for q can instantiate x to ground. This property is correctly modeled by the abductive analysis. However, as shown in Example 4.7, projecting out x can lead to a contradiction, because for any Q = {q(x) ⟵ κ [] true}: Q ⊧ x [] q(y), but Q |̸=_{{x}} x [] q(y).

This approach provides a “goal-directed” way of figuring out what the properties we should analyze a module Q for, given that we know the relevant properties (e.g. from the perspective of allowing certain optimizations) of another module P.

Example 4.17 Consider the definition for gt and le in Example 3.2 (i.e. P_{lg}) and an abstract observation for gt and le which assumes their arguments being all ground:

x ∧ y ∧ z ∧ w [] gt(x, y), le(z, w).

Consider the abduced abstract observation for the open predicate num:

ans(x, y, z, w) ⟵ κ [] num(x′), num(w′) ∈

unf^{Pos}({ans ⟵ gt(x, y), le(z, w)}, F^{Pos}(α(P_{lg})))

where κ = (x ↔ x′) ∧ y ∧ z ∧ (w ↔ w′). Intuitively, num has to be ground to satisfy the observation for gt and le. Indeed, if P_{num} = {num(x) ⟵ x [] true}, then: P_{num} ⊧_{{x,y,z,w}}^{κ} x ∧ y ∧ z ∧ w ∧ κ [] num(x′), num(w′).

5 Termination in Abductive Analysis

Termination in abductive analysis boils down into termination of compositional analysis. The first step is to restrict abstract constraint systems to the point of becoming finite or to satisfy the ascending chain condition. However, as observed in [8], compositional analysis based on unfolding may not terminate even with finite or noetherian abstract domains for substitutions (or constraints). This, because the fixpoint iteration may introduce clauses with bodies containing an arbitrary number of open atoms.

Example 5.1 Consider the standard program P_{anc} with par open:

anc(X,Y) :- par(X,Y).
anc(X,Y) :- par(Y,Z),anc(Z,X).

It is immediate to prove that

1. T_{α(Panc)}^{Pos} ↑ 1 = {anc(x_{1}, x_{2}) ⟵ (x_{1} ↔ x_{3}) ∧ (x_{2} ↔ x_{4}) [] par(x_{3}, x_{4})}

2. T_{α(Panc)}^{Pos} ↑ 2 = \{ \begin{matrix}anc(x_{1}, x_{2}) ⟵ & (x_{1} ↔ x_{3}) ∧ (x_{2} ↔ x_{4}) [] par(x_{3}, x_{4}) \\ anc(x_{1}, x_{2}) ⟵ & (x_{1} ↔ x_{6}) ∧ (x_{2} ↔ x_{3}) ∧ (x_{5} ↔ x_{4}) \\ & [] par(x_{3}, x_{4}), par(x_{5}, x_{6}) \end{matrix} \}

⋮

Some solutions to this problem have been proposed in [8, 17].

In [8] an additional (and orthogonal) layer of abstraction, the ⋆-abstraction^{4}, is applied to deal with unbounded clause bodies in the abstract semantics. This approach provides finitary descriptions for arbitrary large clauses, but makes the analysis less precise. Clause bodies are restricted to contain at most one occurrence of each (open) predicate symbol. In this case, since Π is usually finite, the domain of abstract interpretations AInt results a finite-height lattice. The ⋆-abstracted compositional semantics is denoted F_{⋆}^{A}. This semantics is compositional correct (see [8, 18]), therefore, by Theorem 4.13, it can be correctly used in abstract abduction. The ⋆-abstraction is specific for some abstract domain for analysis. We will see the case for ground dependencies in Example 5.3 below.

4This technique was originally proposed in [9] as state-approximation for suspension analysis of concurrent logic programs.

The approach in [17] is instead oriented to provide a compositional complete abstract semantics, which is domain independent. This is obtained by taking, as semantics for P, the result of a finite number of iterations of the T_{α(P)}^{A} operator, without reaching the fixpoint. While this would not be correct in general, for finite abstract constraint systems (e.g. for Pos [1] or Sharing [25]) the resulting denotation has the same compositionality properties of the concrete fixpoint semantics. The fixpoint iteration sequence T_{α(P)}^{A}↑n (n ≥ 1) is stopped when T -stability is reached, i.e. whenever for each Q ∈ AInt containing only unit clauses with predicates in open(P): unf^{A}(T_{α(P)}^{A}↑n, Q) = unf^{A}(T_{α(P)}^{A}↑(n + 1), Q). This corresponds to test if the same patterns for the intensional part of clauses in T_{α(P)}^{A}↑n and T_{α(P)}^{A}↑(n +1) are generated, once any definition for their extensional (open) part is provided. In this case, any additional unfolding step does not add information with respect to the possible extensions of P. The T -stable semantics is denoted F_{T}^{A} and it is proved to be compositional complete in [17, 18].

Example 5.2 Consider the Example 5.1. It is easy to prove that T_{α(Panc)}^{Pos} ↑ 1 is not T -stable, while T_{α(Panc)}^{Pos} ↑ 2 is T -stable. Take for instance

Q = {par(x_{1}, x_{2}) ⟵ x_{1} ← x_{2} [] true}

then:

unf^{A}(T_{α(Panc)}^{Pos} ↑ 1, Q) = {anc(x_{1}, x_{2}) ⟵ x_{1} ← x_{2} [] true}
unf^{A}(T_{α(Panc)}^{Pos} ↑ 2, Q) = \{ \begin{matrix}anc(x_{1}, x_{2}) ⟵ x_{1} ← x_{2} [] true \\ anc(x_{1}, x_{2}) ⟵ x_{1} → x_{2} [] true \end{matrix} \}

Therefore unf^{Pos}(T_{α(Panc)}^{Pos} ↑ 1, Q) ≠ unf^{Pos}(T_{α(Panc)}^{Pos} ↑ 2, Q). However, for any set of unit clauses Q ∈ AInt, unf^{Pos}(T_{α(Panc)}^{Pos} ↑ 2, Q) = unf^{Pos}(T_{α(Panc)}^{Pos} ↑ 3, Q).

The following example shows the applicability of T -stable and ⋆-abstracted semantics in abductive analysis.

Example 5.3 In this example we consider the simpler abstract domain Dep adopted from [9]. Elements in Dep_{V} are propositional formulae on V , for any finite nonempty set V ⊆ Var, with connectives ∧ and ↔, ordered by logical implication. It is straightforward to derive Dep by abstractaction of Pos. In the following of this example we assume a kind of merge over all paths MOP abstract interpretation, i.e. interpretations can only contain single occurrences for any clause. Therefore, any two clauses h ⟵ κ [] b̄ and h ⟵ κ′ [] b̄ generated for h ⟵ b̄ in F^{Dep} are “merged” into (approximated by) a single clause h ⟵ κ ⊕ κ′ [] b̄. This restriction reduces the search space for T -stability, even if it may be cause of a loss of precision (see [21] for a formal treatment of MOP in analysis of constraint logic programs). Moreover, as proved in [8], ⋆-abstraction for Dep with MOP is compositional correct. Consider the “naive reverse” routine P_{rev} where the append procedure is open.

P_{rev}

     rev([],[]).
     rev([X|Xs],Zs) :- rev(Xs,Ys), append(Ys,[X],Zs).

A finite compositional abstract semantics can be obtained by iterating unfolding until a T -stable sequence is reached. This is obtained after two iterations:

F_{T}^{Dep}(α(P_{rev})) = \{ \begin{matrix}rev(x_{1}, x_{2}) ⟵ x_{1} ∧ x_{2} [] true \\ rev(x_{1}, x_{2}) ⟵ x_{1} ↔ x_{6} ∧ x_{2} ↔ x_{7} ∧ x_{5} [] append(x_{5}, x_{6}, x_{7}) \end{matrix} \}

A ⋆-abstracted semantics is generated by collapsing all occurrences of the same predicate in a body to one “canonical” atom. The collapsing of a sequence p(x̄_{1}), …, p(x̄_{n}) of atoms is an atom p(x̄) with x̄ ≠ x̄_{i} and a dependency relation κ such that each argument x_{j} of p(x̄) represents the set of the j^{th} arguments (x_{ij} for i = 1 … n) in p(x̄_{1}), …, p(x̄_{m}), i.e.

κ = ∧_{xj ∈x̄} (x_{j} ↔ ( ∧_{i=1}^{n} x_{ij} ))

Therefore we have:

F_{⋆}^{Dep}(α(P_{rev})) = \{ \begin{matrix}rev(x_{1}, x_{2}) ⟵ x_{1} ∧ x_{2} [] true \\ rev(x_{1}, x_{2}) ⟵ x_{1} ↔ x_{6} ∧ x_{7} ↔ (x_{2} ∧ x_{5}) [] append(x_{5}, x_{6}, x_{7}) \end{matrix} \}

By Theorem 4.13 with abstract observation G^{a} = x_{1} ↔ x_{2} [] rev(x_{1}, x_{2}) for P_{rev}, we abduce the observations

ans(x_{1}, x_{2}) ⟵ κ̃_{i} [] append(x_{5}, x_{6}, x_{7}) ∈ unf^{Dep}({ans ⟵ rev(x_{1}, x_{2})}, F_{i}^{Dep}(α(P_{rev})))

for i ∈ {⋆, T }, where: κ̃_{T} = x_{1} ↔ x_{6} ∧ x_{2} ↔ x_{7} ∧ x_{5} and κ̃_{⋆} = x_{1} ↔ x_{6} ∧ x_{7} ↔ (x_{2} ∧ x_{5}).

It is easy to observe that for i ∈ {⋆, T }: (κ_{i}∧x_{5}∧(x_{6} ↔ x_{7})) → (x_{1} ↔ x_{2}). Therefore, for any definition Q of append with semantics {append(x_{1}, x_{2}, x_{3}) ⟵ x_{1} ∧ (x_{2} ↔ x_{3}) [] true} and i ∈ {⋆, T }:

Q ⊧κ̃i ; {x_{1},x_{2}} (x_{1} ↔ x_{2}) ∧ κ̃_{i} [] append(x_{5}, x_{6}, x_{7})

Therefore, by Theorem 4.13 ^{5}, P_{rev} ∪ Q satisfies the observation G^{a}. Note that the standard definition of append, i.e., {append(x_{1}, x_{2}, x_{3}) ⟵ (x_{1} ∧ x_{2}) ↔ x_{3} [] true} satisfies the abduced observation for i = T , i.e., (κ_{T} ∧ (x_{5} ∧ x_{6}) ↔ x_{7}) → (x_{1} ↔ x_{2}), while being κ_{⋆} weaker than κ_{T} , we need a stronger definition for append to satisfy the observation for i = ⋆.

5For T-stable semantics (i = T) we can also apply Theorem 4.14 and obtain a necessary condition on the semantics of append.

6 Applications

In this section we consider some applications of abductive analysis in typical dataflow analysis problems in logic programming.

6.1 Invariance of module composition

In addition to correctness of abductive analysis, Theorem 4.13 gives also a characterization of the invariance of module composition with respect to an abstract observation. A module P is invariant with respect to open(P) for an abstract observation G^{a} iff for each extension Q of P: P ∪ Q ⊧ G^{a}.

Proposition 6.1 Let κ [] b̄ be an abstract observation for a program module P. If for each ans ⟵ κ′ [] ḡ ∈ unf^{A}({ans ⟵ b̄}, F^{A}(α(P))): γ_{A}(κ′)(b̄ :: ḡ) = γ_{A}(κ ⊗ κ′)(b̄ :: ḡ) then P is invariant with respect to open(P) for κ [] b̄.

Proof. Immediate by ⊗ monotonicity and Theorem 4.13.

Example 6.2 Consider an “insertion sort” routine defined in terms of the following modules

P_{sort}

      sort([],[]).
      sort([X|Xs],Ys) :- sort(Xs,Zs),ins(X,Zs,Ys).

P_{ins}

      ins(X,[],X).
      ins(X,[Y|Ys],[Y|Zs]) :- gt(X,Y),ins(X,Ys,Zs).
      ins(X,[Y|Ys],[X,Y|Ys]) :- le(X,Y).

P_{gl}  gt(s(X), X). gt(s(X), Y) :- gt(X, Y). gt(s(X), s(Y)) :- gt(X, Y).      le(X, X). le(X, s(Y)) :- le(X,Y). le(s(X), s(Y)) :- le(X, Y).

The compositional semantics for P_{sort} (insert is open) and P_{ins} (gt and le are open) are obtained in two steps as T -stable semantics:

F_{T}^{Pos}(α(P_{sort})) = \{ \begin{matrix}sort(x_{1}, x_{2}) ⟵ x_{1} ∧ x_{2} [] true \\ sort(x_{1}, x_{2}) ⟵ (x_{1} ↔ x_{5}) ∧ (x_{2} ↔ x_{7}) ∧ x_{6} [] insert(x_{5}, x_{6}, x_{7}) \end{matrix} \}

F_{T}^{Pos}(α(P_{ins})) =

insert(x_{1}, x_{2}, x_{3}) ⟵ (x_{1} ↔ x_{3}) ∧ x_{2} [] true
insert(x_{1}, x_{2}, x_{3}) ⟵ x_{3} ↔ (x_{1} ∧ x_{2}) ∧ x_{1} ↔ x_{4} ∧ x_{2} → x_{5} [] le(x_{4}, x_{5})
insert(x_{1}, x_{2}, x_{3}) ⟵ x_{3} ↔ (x_{1} ∧ x_{2}) ∧ x_{1} ↔ x_{4} ∧ x_{2} ↔ x_{5} [] gt(x_{4}, x_{5})
insert(x_{1}, x_{2}, x_{3}) ⟵ x_{3} ↔ (x_{1} ∧ x_{2}) ∧ x_{1} ↔ x_{4} ↔ x′_{4} ∧ x_{2} → (x_{5} ∧ x′_{5})
[] gt(x_{4}, x_{5}), le(x′_{4}, x′_{5})

The semantics of P_{gl} is:

F_{T}^{Pos}(α(P_{lg})) = \{ \begin{matrix}gt(x_{1}, x_{2}) ⟵ x_{1} ↔ x_{2} [] true \\ le(x_{1}, x_{2}) ⟵ x_{1} ↔ x_{2} [] true \end{matrix} \} .

Given the abstract observation G^{a} = x_{1} ↔ x_{2} [] sort(x_{1}, x_{2}), we abduce

ans(x_{1}, x_{2}) ⟵ κ̃ [] insert(x_{5}, x_{6}, x_{7}) ∈ unf^{Pos}({ans ⟵ sort(x_{1}, x_{2})}, F_{T}^{Pos}(α(P_{sort})))

where κ̃ = x_{1} ↔ x_{5} ∧ x_{2} ↔ x_{7} ∧ x_{6}. As before, it is easy to observe that the program P_{ins} ∪ P_{gl} satisfies the abduced observation, i.e.

P_{ins} ∪ P_{gl} ⊧κ̃ ; {x_{1},x_{2}} (x_{1} ↔ x_{2}) ∧ κ̃ [] insert(x_{5}, x_{6}, x_{7}).

By Theorem 4.13, P_{sort} ∪ P_{ins} ∪ P_{gl} satisfies the observation G^{a}.

However, notice that P_{sort} ∪P_{ins} is invariant with respect to gt and le for the observation (on sort) G^{a}. To prove this invariance, we apply Proposition 6.1. F_{T}^{Pos}(α(P_{sort}∪ P_{ins})) contains the following definitions for sort:

sort(x_{1}, x_{2}) ⟵ x_{1} ↔ x_{2} [] true
sort(x_{1}, x_{2}) ⟵ (x_{1} ↔ x_{2} ↔ x′_{4}) ∧ x′_{5} [] le(x′_{4}, x′_{5})
sort(x_{1}, x_{2}) ⟵ (x_{1} ↔ x_{2} ↔ x′_{4}) ∧ x′_{5} [] gt(x′_{4}, x′_{5})
sort(x_{1}, x_{2}) ⟵ (x_{1} ↔ x_{2} ↔ x′_{4} ↔ x′′_{4}) ∧ x′_{5} ∧ x′′_{5} [] gt(x′_{4}, x′_{5}), le(x′′_{4}, x′′_{5})

Note that, for each

ans ⟵ κ′ [] b̄ ∈ unf^{Pos}({ans ⟵ sort(x_{1}, x_{2})}, F_{T}^{Pos}(α(P_{sort} ∪ P_{ins})))

we have κ′ = κ′∧(x_{1} ↔ x_{2}). Therefore, independently on the definition Q of gt and le: P_{sort} ∪P_{ins} ∪Q ⊧ G^{a}. This is enough to conclude that a different definition for gt and le, e.g. P_{lg} in Example 3.2, does not affect the ground dependency of sort. Moreover, note that both P_{gl} and P_{lg}, when composed with P_{sort}, produce (only) ground bindings for the first and second argument of sort.

6.2 Call patterns

Abductive analysis can be used in conjunction with call pattern information. This is achieved by applying the same Magic Sets transformation M suggested in [7]. Recall that for a program P and goal G, σ ∈ C is a call pattern for a predicate p in P ∪{G} iff there exists an SLD-derivation from G to b|G′ with computed constraint σ and where pred(b) = {p}.

Let P be a program and G be the goal A_{1}, …, A_{n}. It is well known that call patterns depend on the selection rule [2]. The magic-set transformed program M(P, G) for the Prolog left-to-right selection rule, is obtained by transforming P ∪ {G} as follows^{6}:

1. replace G by the clauses

Ac_{i} ⟵ Aa_{1}, …, Aa_{i−1}

for 1 ≤ i ≤ n.

2. replace each clause H ⟵ B_{1}, …, B_{m} (m ≥ 0) in P by the clauses

Bc_{i} ⟵ H c, Ba_{1}, …, Ba_{i−1}

for 1 ≤ i ≤ m, and

H a ⟵ H c, Ba_{1}, …, Ba_{m}

M characterizes the call patterns of P with initial goal G as successful computations of the transformed program M(P, G) (cf. [7]). Therefore, properties can be specified for call patterns as well as for success patterns in M(P, G). In particular, it is immediate from the transformation M that for any program P and goal G, if p ∈ open(P), then pa ∈ open(M(P, G)). Note however that if P and Q are program modules, and G is a goal then M(P, G) and M(Q, G) may not be in general predicate disjoint, as they may share predicates with call pattern annotations. In the following we assume that pc ∈ open(M(P, Q)) whenever p ∈ open(P).

Abductive analysis can characterize the dependency between call patterns in P∪{G}, and success patterns for the open predicates in P. The following proposition is an immediate application of Theorem 4.13.

Proposition 6.3 Let P, Q be program modules such that Q extends P, G be a goal, and κ [] bc be an abstract observation for M(P, G). If for each ans ⟵ κ̃ [] ḡ ∈ unf^{A}({ans ⟵ bc}, F^{A}(α(M(P, G)))): M(Q, G) ⊧κ̃ ; var(bc) κ ⊗ κ̃ [] ḡ, then M(P ∪ Q, G) ⊧ κ [] bc.

Proof. The proof is immediate by Theorem 4.13, and because for any program module P and Q and goal G: M(P, G) ∪ M(Q, G) = M(P ∪ Q, G).

A consequence of Proposition 6.3 is that for any call pattern σ for b in P ∪ Q ∪ {G}: σ(b) ∈ γ(κ)(b). This claim can be immediately proved by applying the equivalence between successful computations for bc in M(P ∪ Q, G) and call patterns for b in P ∪ Q ∪ {G}, as proved in [7].

We show abductive analysis for call patterns by a simple example Example 6.4 Consider the program P_{rev} in Example 5.3, and an initial call (goal) G for rev with first argument ground. α(M(P_{rev}, G)) with left-to-right selection rule is:

6In the following a and c annotations state respectively for success and call.

revc(x_{1}, x_{2}) ⟵ x_{1} [] true
reva(x_{1}, x_{2}) ⟵ x_{1} ∧ x_{2} [] revc(x_{1}, x_{2})
revc(x_{1}, x_{2}) ⟵ x_{3} → x_{1} [] revc(x_{3}, x_{4})
appendc(x_{1}, x_{2}, x_{3}) ⟵ x_{4} ↔ (x_{2}, ∧x_{6}) ∧ x_{1} ↔ x_{7} ∧ x_{3} ↔ x_{5} [] revc(x_{4}, x_{5}), reva(x_{6}, x_{7})
reva(x_{1}, x_{2}) ⟵ x_{1} ↔ x_{3} ↔ (x_{5} ∧ x_{8}) ∧ x_{2} ↔ x_{4} ↔ x_{9} ∧ x_{6} ↔ x_{7} []
revc(x_{3}, x_{4}), reva(x_{5}, x_{6}), appenda(x_{7}, x_{8}, x_{9})

Here, the abstract observation x_{1} ∧ x_{2} [] appendc(x_{1}, x_{2}, x_{3}) specifies that any call pattern for append in the left-to-right execution of G in P_{rev} must have the first two arguments ground. By abduction we can characterize the semantics of append (in this case appenda) so that this observation is satisfied. The compositional abstract semantics F_{T}^{Pos}(α(M(P_{rev}, G))) contains the following clauses for append (it is worth noting that open(M(P_{rev}, G)) = {appenda, appendc}):

appendc(x_{1}, x_{2}, x_{3}) ⟵ x_{1} ∧ x_{2}
appendc(x_{1}, x_{2}, x_{3}) ⟵ x_{2} ∧ x_{8} ∧ x_{7} ∧ x_{1} ↔ x_{9} [] appenda(x_{7}, x_{8}, x_{9})

The abduced observation is ans(x_{1}, x_{2}, x_{3}) ⟵ κ [] appenda(x_{7}, x_{8}, x_{9}) where κ = x_{2} ∧ x_{8} ∧ x_{7} ∧ x_{1} ↔ x_{9}. Therefore, by Theorem 4.13, only success patterns κ′ such that (κ ∧ κ′) → (κ ∧ x_{1} ∧ x_{2}) are allowed for appenda, namely:

appenda(x_{7}, x_{8}, x_{9}) ⟵ x_{7} ∧ x_{8} ∧ x_{9}
appenda(x_{7}, x_{8}, x_{9}) ⟵ x_{9} ↔ (x_{7} ∧ x_{8})
appenda(x_{7}, x_{8}, x_{9}) ⟵ x_{9} ↔ x_{7}
appenda(x_{7}, x_{8}, x_{9}) ⟵ x_{9} ↔ x_{8}

It is worth noting that both P_{app} and P′_{app} below satisfy this requirement.

P_{app}

append([],X,X).
append([X|W],Y,[X|Z]):-append(W,Y,Z).

P′_{app}

append([],[],[]).
append([],[X|Y],[X|Y]):-append([], Y, Y).
append([X|W],Y,[X|Z]):-append(W,Y,Z).

Therefore, any call pattern for append in P_{rev} ∪ P_{app} or P_{rev} ∪ P′_{app} with initial goal for rev having the first argument ground, will have the first two arguments ground.

6.3 Optimizing T -stability tests

Abductive analysis can be used in conjunction with ⋆-abstraction to reduce the search space for T -stability check. We sketch this idea in this section.

It is known that while T -stable semantics provides a compositionally complete abstract semantics (i.e. with no loss of precision), testing for T -stability is expensive. Indeed, this test is performed by searching over any possible definition (semantics) for open predicates. The search space is huge—often exponential in the number of arguments of open predicates. Here we propose an improvement by statically restricting (by abduction) the number of possible semantics that the open predicates can have, according to a given program specification. This leads to a notion of relative T -stability, where only a fixed number of possible patterns are allowed to be imported from open predicates. In this case, if P is a program module and Q ⊆ AInt contains interpretations having only unit clauses with predicates in open(P), then T_{α(P)}^{A}↑n is T -stable with respect to Q iff for each Q ∈ Q: unf^{A}(T_{α(P)}^{A}↑n, Q) = unf^{A}(T_{α(P)}^{A}↑(n + 1), Q). It is clear that a T -stable semantics T_{α(P)}^{A}↑n with respect to Q is compositional with respect to any program module which extends P and has semantics in Q. Therefore, once an observation for P has been fixed, in order to have an useful T -stability notion, we need at least that Q contains the set of all possible extensions Q of P such that P ∪ Q satisfies the original observation. Q above can be for instance the result of the abductive analysis on P based on the less precise ⋆-abstraction. We show this by an example.

Example 6.5 Consider the program module P_{rev} defined in Example 5.3 with append open, and F_{⋆}^{Dep}(α(P_{rev})). Assume the observation G^{a} = x_{1} ↔ x_{2} [] rev(x_{1}, x_{2}) on P_{rev}, then

ans(x_{1}, x_{2}) ⟵ κ̃ [] append(x_{5}, x_{6}, x_{7}) ∈ unf^{Dep}({ans ⟵ rev(x_{1}, x_{2})}, F_{⋆}^{Dep}(α(P_{rev})))

where κ̃ = (x_{1} ↔ x_{6}) ∧ x_{7} ↔ (x_{5} ∧ x_{2}). Denote Q the set of possible definitions for append that satisfy the observation, i.e.

Q = { Q | Q ⊧κ̃ ; {x_{1},x_{2}} κ̃ ∧ (x_{1} ↔ x_{2}) [] append(x_{5}, x_{6}, x_{7}) }
= { append(x_{5}, x_{6}, x_{7}) ⟵ κ | κ ∈ K }

where

K = \{ κ | \begin{matrix}κ ∈ Dep_{\{x_{5},x_{6},x_{7}\}} \\ (κ ∧ κ̃) → (κ̃ ∧ (x_{1} ↔ x_{2})) \end{matrix} \} = \{ \begin{matrix}x_{6} ∧ x_{7} , x_{5} ∧ x_{6} ∧ x_{7} \\ x_{5} ∧ (x_{7} ↔ x_{6}) \\ x_{7} ∧ (x_{5} ↔ x_{6}) \end{matrix} \}

It is worth noting that |K| < |Dep_{{x_{5},x_{6},x_{7}}}|. Q provides a restricted search space for possible definitions of append all leading to a definition of rev where the first argument is ground iff the second is. A T -stable compositional semantics for P_{rev} can be efficiently computed relatively to Q. It is compositional complete with respect to any of the definitions of append in Q. However, note that because of compositional correctness of ⋆-abstraction, (i.e., because of the application of Theorem 4.13), Q does not provide (in general) a complete characterization of extensions for P_{rev} that satisfy G^{a}.

7 Conclusions

We believe that the main application field of abductive analysis is dataflow analysis of module interaction. This is obtained by statically deriving, by abduction, a set of constraints on each single module, given a constraint on their composition. Constraints are goals, and therefore the same engine for deductive analysis (i.e. unfolding) can be used for the abductive analysis. The implementation costs of abductive analysis are therefore reduced. Of course, the use of the Bossi semantics in [5] as a base semantics for abduction is only one of the possibilities provided in the literature. Different frameworks for abductive analysis can be defined by modifying abductive logic programming (e.g. [27]) to cope with abstract interpretation. This may provide an interesting alternative approach for abductive analysis by abstract compilation ([24]). In a recent work, Giacobazzi and Ranzato [22] proved that most well known compositional semantics for logic programs, like the semantics in [5], can be obtained systematically by abstraction from a given operational semantics of logic programs. The idea is that any semantics of logc programs (and more in general of a programming language, see [13]), can be viewed as an abstraction of a fixed, more concrete, operational semantics which is basically SLD resolution (e.g. see [20]). Therefore, composing abstractions corresponds to compose semantics. In [22] the authors proved that compositionality for logic program semantics can be systematically achieved by composing, by a suitable functional combination operator, the abstractions corresponding to more abstract, possibly non compositional semantics. The resulting framework is powerful enough to encode well known compositional semantics for logic programming as functional composition of simpler non-compositional ones, and provide an interesting link between semantics and well known function spaces. For instance, the Bossi semantics in [5] can be viewed as the semantics of the functional composition of the standard non-compositional s semantics for computed answer substitutions in [16]. Moreover, other more concrete semantics, like the semantics for computed answers, call patterns, partial answers etc. can be all functionally composed in the same way, yet providing new compositional semantics for logic programs. It is worth noting that in this framework, any semantics which can be obtained by functional composition of simpler ones can also be used as a basis for different forms of abductive analysis.

Acknowledgments

The stimulating discussions with Mike Codish, Patrick Cousot, Saumya Debray and Giorgio Levi are gratefully acknowledged. This work has been done while the author was visiting the LIX, Laboratoire d’Informatique, École Polytechnique, Paris. He thanks LIX , and in particular Radhia Cousot, for the kind hospitality. This work has been partly supported by the EEC Human Capital and Mobility individual grant: “Semantic Definitions, Abstract Interpretation and Constraint Reasoning”, N. ER-BCHBICT930822.

References

[1] T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Boolean functions for dependency analysis: algebraic properties and efficient representation. In Proc. of SAS ’94, LNCS 864, pp. 266–280, 1994.

[2] K. R. Apt. Introduction to Logic Programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 495–574. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.

[3] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems, 15(1):133–181, 1993.

[4] G. Birkhoff. Lattice Theory. AMS Colloq. Public. vol. XXV, 3rd ed., 1967.

[5] A. Bossi, M. Gabbrielli, G. Levi, and M. C. Meo. A Compositional Semantics for Logic Programs. Theoretical Computer Science, 122(1–2):3–47, 1994.

[6] M. Bruynooghe. A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming, 10:91–124, 1991.

[7] M. Codish, D. Dams, and E. Yardeni. Bottom-up Abstract Interpretation of Logic Programs. Theoretical Computer Science, 124(1):93–126, 1994.

[8] M. Codish, S. K. Debray, and R. Giacobazzi. Compositional Analysis of Modular Logic Programs. In Proc. Twentieth Annual ACM Symp. Principles of Programming Languages, POPL ’93, pages 451–464. ACM Press, 1993.

[9] M. Codish, M. Falaschi, and K. Marriott. Suspension Analysis for Concurrent Logic Programs. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on Logic Programming, pages 331– 345. The MIT Press, Cambridge, Mass., 1991.

[10] A. Cortesi, G. Filè, and W. Winsborough. Prop revisited: Propositional Formula as Abstract Domain for Groundness Analysis. In Proc. Sixth IEEE Symp. on Logic In Computer Science, pages 322–327. IEEE Computer Society Press, 1991.

[11] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. Fourth Annual ACM Annual ACM Symp. Principles of Programming Languages, POPL ’77, pp. 238–252, 1977.

[12] P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. Sixth Annual ACM Symp. Principles of Programming Languages, POPL ’79, pages 269–282, 1979.

[13] P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM Symposium on Principles of Programming Languages (POPL ’92), pages 83–94. ACM Press, 1992.

[14] S. K. Debray. Efficient Dataflow Analysis of Logic Programs. Journal of the ACM, 39(4):949–984, 1992.

[15] F. Denis and J.-P. Delahaye. Unfolding, Procedural and Fixpoint Semantics of Logic Programs. In C. Choffrut and M. Jantzen, editors, STACS 91, volume 480 of Lecture Notes in Computer Science, pages 511–522. Springer-Verlag, Berlin, 1991.

[16] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Theoretical Computer Science, 69(3):289–318, 1989.

[17] M. Gabbrielli, R. Giacobazzi, and D. Montesi. Modular logic programs over finite domains. In D. Saccà, editor, Proc. Eight Italian Conference on Logic Programming, pages 663–678, 1993. Also available as Technical Report LIX – Ecole Polytechnique

LIX/RR/94/04, URL http://www.di.unipi.it/∼giaco/papers.html.

[18] R. Giacobazzi. Semantic Aspects of Logic Program Analysis. PhD thesis, Di-

partimento di Informatica, Università di Pisa, 1993.  TD – 18/93.  URL

http://www.di.unipi.it/∼giaco/papers.html.

[19] R. Giacobazzi. Abductive Analysis of Modular Logic Programs. In M. Bruynooghe, editor, Proc. of the Eleventh International Logic Programming Symposium, ILPS ’94, pages 377– 391. The MIT Press, Cambridge, Mass., 1994.

[20] R. Giacobazzi. “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics. In C. Puech, editor, Proceedings of the 13th International Symposium on Theoretical Aspects of Computer Science (STACS ’96), LNCS 1046, pages 503–514. Springer-Verlag, 1996.

[21] R. Giacobazzi, S. Debray, and G. Levi. Generalized Semantics and Abstract Interpretation for Constraint Logic Programs. Journal of Logic Programming, 25(3):191-248, Dicembre 1995.

[22] R. Giacobazzi and F. Ranzato. Functional dependencies and Moore-set completions of abstract interpretations and semantics. In J. Lloyd, editor, Proceedings of the 1995 International Logic Programming Symposium (ILPS ’95), pages 321–335. The MIT Press, 1995.

[23] C.A.R. Hoare, I.J. Hayes, H. Jifeng, C.C. Morgan, A.W. Roscoe, J.W. Sanders, I.H. Sorensen, J.M. Spivey, and B.A. Sufrin. Laws of programming. Comm. of the ACM, 30(8):672–686, 1987.

[24] M. Hermenegildo, R. Warren, and S.K. Debray. Global flow analysis as a practical compilation tool. Journal of Logic Programming, 13(4):349–366, 1992.

[25] D. Jacobs and A. Langen. Static Analysis of Logic Programs for Independent AND Parallelism. Journal of Logic Programming, 13(2 & 3):291–314, 1992.

[26] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. Fourteenth Annual ACM Symp. on Principles of Programming Languages, POPL ’87, pages 111–119. ACM, 1987.

[27] A.C. Kakas, R.A. Kowalski, and F. Toni. Abductive Logic Programming. Journal of Logic and Computation, 2(6):719–770, 1993.

[28] G. Levi. Models, Unfolding Rules and Fixpoint Semantics. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 1649–1665. The MIT Press, Cambridge, Mass., 1988.

[29] K. Marriott and H. Søndergaard. Bottom-up Dataflow Analysis of Normal Logic Programs. Journal of Logic Programming, 13(2 & 3):181–204, 1992.

[30] D. Poole. A logical framework for default reasoning. Artificial Intelligence, 36:27–47,

A Appendix: Proofs of related results

The appendix contains the proofs of selected lemmata and theorems which are essential for deductive and abductive analysis.

Theorem 3.3 [Codsh et al., [8]] Let (Int, α, AInt, γ) be a Galois insertion, and F^{A} : AInt → AInt be a monotonic and safe approximation of F. Then, for any program module P_{1}, P_{2} ∈ Int:

α(F(P_{1} ∪ P_{2})) ⊑ F^{A}(F^{A}(α(P_{1})) ⊔ F^{A}(α(P_{1})))

Proof. Assume the premise of the theorem and let P_{1}, P_{2} ∈ Int. Recall that α is additive in any Galois insertion.

α(F(P_{1} ∪ P_{2})) = α(F(F(P_{1}) ∪ F(P_{2})))

[ Theorem 3.1 ]

⊑ F^{A}(α(F(P_{1}) ∪ F(P_{2})))

[ safety ]

= F^{A}(α(F(P_{1})) ⊔ α(F(P_{2})))

[ α additivity ]

⊑ F^{A}(F^{A}(α(P_{1})) ⊔ F^{A}(α(P_{2})))

[ safety and monotonicity ]

Lemma 3.6 [Giacobazzi, [18]] For any abstract constraint system (A, ⊗), unf^{A} is left-additive.

Proof. Left-additivity follows immediately by definition.

Lemma 3.7 [Giacobazzi, [18]] If P a_{1} ≅ Qa_{1} and P a_{2} ≅ Qa_{2} then unf^{A}(P a_{1}, P a_{2}) ≅ unf^{A}(Qa_{1}, Qa_{2}).

Proof. Because γ is (by definition) an additive extension of γ_{A} on abstract clauses, and unf^{A} is left-additive, we can prove the lemma for the more simple case where P a_{1} and Qa_{1} are singletons. We assume, without loss of generality, that the clauses in P a_{1}, Qa_{1}, P a_{2} and Qa_{2} do not share common variables. Let P a_{1} = {c} and Qa_{1} = {c′}, where c = h ⟵ κ [] g_{1}, …, g_{n} and c′ = h′ ⟵ κ′ [] g′_{1}, …, gn^{′}. Then

h ⟵ σ [] b̄_{1} :: ⋯:: b̄_{n} ∈ γ(unf^{A}(P a_{1}, P a_{2}))

iff ⟨h_{i} ⟵ κ_{i} [] b̄_{i}⟩n_{i=1} < <_{c} P a_{2}

σ ∈ γ_{A}(κ⊗ ⊗_{i=1}^{n} (κ_{i} ⊗ α_{A}(g_{i} = h_{i})))

Because the concretization is always a co-additive function in any Galois connection, the condition above is satisfied iff

⟨h_{i} ⟵ κ_{i} [] b̄_{i}⟩n_{i=1} < <_{c} P a_{2}

σ ∈ γ_{A}(κ) ∧ ∧n_{i=1}(γ_{A}(κ_{i}) ∧ γ_{A}(α_{A}(g_{i} = h_{i})))

By definition:

σ = σ_{κ} ∧ ∧n_{i=1}(σ_{κi} ∧ σ_{=})

for some σ_{κ} ∈ γ_{A}(κ), σ_{κi} ∈ γ_{A}(κ_{i}) and σ_{=} ∈ γ_{A}(α_{A}(g_{i} = h_{i})).

Because we assume that P a_{1}, Qa_{1}, P a_{2} and Qa_{2} contain renamed apart clauses, and P a_{1} ≅ Qa_{1} and P a_{2} ≅ Qa_{2}, then the condition above implies that there exist:

⟨hi^{′} ⟵ κi^{′} [] b̄′_{i}⟩n_{i=1} < <_{c′} Qa_{2}

δ_{κ′} ∈ γ_{A}(κ′)

δ_{κi^{′}} ∈ γ_{A}(κi^{′})

δ_{=} ∈ γ_{A}(α_{A}(gi^{′} = hi^{′}))

such that if δ = δ_{κ′} ∧ ∧n_{i=1}(δ_{κi^{′}} ∧ δ_{=}) then

h ⟵ σ [] b̄_{1} :: ⋯:: b̄_{n} ∼ h′ ⟵ δ [] b̄′_{1} :: ⋯:: b̄′_{n}

Note that

h′ ⟵ δ [] b̄′_{1} :: ⋯:: b̄′_{n} ∈ γ(unf^{A}(Qa_{1}, Qa_{2})).

This concludes the proof, by proving that γ(unf^{A}(P a_{1}, P a_{2})) ⊆ γ(unf^{A}(Qa_{1}, Qa_{2})). The other inclusion is similar.

Lemma 3.8 [Giacobazzi, [18]] For any abstract constraint system (A, ⊗), unf^{A} is associative and right-continuous.

Proof. The proof of continuity for the function λI^{a}.unf^{A}(P^{a}, I^{a}) for any P^{a} ∈ AInt is not immediate, as AInt is not in general noetherian, even if A is noetherian. However, the proof can be based on the finiteness property of abstract constraint systems (for the more general case of noetherian or non-noetherian abstract constraint systems see [21]).

Let D ⊆ AInt be a (possibly infinite) chain and let h ⟵ κ′ [] b̄_{1}, …, b̄_{n} ∈ unf^{A}(P^{a}, ⊔D). Then, by the definition there exist c = h ⟵ κ [] g_{1}, …, g_{n} < < P^{a} and ⟨h_{i} ⟵ κ_{i} [] b̄_{i}⟩n_{i=1} < <_{c} ⊔D such that κ′ = κ ⊗ ⊗n_{i=1}(κ_{i} ⊗ α_{A}(g_{i} = h_{i})). Because A is noetherian, for each i = 1, …, n there exists I_{i} ∈ D such that h_{i} ⟵ κ_{i} [] b̄_{i} < <_{c} I_{i}. The rest of this proof is standard.

The proof of associativity follows from the basic properties of ⊗ (i.e. associativity and commutativity). Let P^{a}, Q^{a}, W^{a} ∈ AInt, we prove that

unf^{A}(unf^{A}(P^{a}, Q^{a}), W^{a}) = unf^{A}(P^{a}, unf^{A}(Q^{a}, W^{a})).

By the definition:

c ∈ unf^{A}(unf^{A}(P^{a}, Q^{a}), W^{a})

iff c = h ⟵ κ [] ḡ_{1_{1}} :: …:: ḡ_{nmi} where

h ⟵ κ_{P} [] a_{1}, …, a_{n} ∈ P^{a}
ai^{′} ⟵ κ_{Qi} [] b_{i_{1}}, …, b_{imi} ∈ Q^{a} for i = 1, …, n
bij^{′} ⟵ κ_{Wij} [] ḡ_{ij} ∈ W^{a} for i = 1, …, n and j = 1, …, m_{i}

are clauses which share no variable, and by defining κ′ = κ_{Q_{1}} ⊗ … ⊗ κ_{Qn} and κ′′ = κ_{W_{1_{1}}} ⊗ … ⊗ κ_{Wnmn} , we have:

κ = κ_{P} ⊗ κ′⊗ ⊗_{i=1}^{n} α_{A}(a_{i} = ai^{′}) ⊗ κ′′⊗ ⊗_{i=1}^{n} ⊗_{j =1}^{mi} α_{A}(b_{ij} = bij^{′}).

Analogously: c ∈ unf^{A}(P^{a}, unf^{A}(Q^{a}, W^{a})) iff c = h ⟵ κ̃ [] ḡ_{1_{1}} :: …:: ḡ_{nmi} where

h ⟵ κ_{P} [] a_{1}, …, a_{n} ∈ P^{a}
ai^{′} ⟵ κ_{Qi} [] b_{i_{1}}, …, b_{imi} ∈ Q^{a} for i = 1, …, n
bij^{′} ⟵ κ_{Wij} [] ḡ_{ij} ∈ W^{a} for i = 1, …, n and j = 1, …, m_{i}

are clauses which share no variable and

κ̃ = κ_{P} ⊗ κ′ ⊗ κ′′⊗ ⊗_{i=1}^{n} ⊗_{j =1}^{mi} α_{A}(b_{ij} = bij^{′}) ⊗ ⊗_{i=1}^{n} α_{A}(a_{i} = ai^{′}).

In both cases, we can choose without loss of generality the same variables for corresponding clauses. Thus, by ⊗ commutativity and associativity, κ̃ = κ, which concludes the proof.

Lemma 3.9 [Giacobazzi, [18]] Let (A, ⊗) be an abstract constraint system. Then, for every I_{1}, I_{2} ∈ Int,

α(unf (I_{1}, I_{2})) ⊑ unf^{A}(α(I_{1}), α(I_{2}))

Proof. It is equivalent to prove that:

unf (γ(I a_{1}), γ(I a_{2})) ⊆ γ(unf^{A}(I a_{1}, I a_{2}))

Assume h ⟵ σ [] b̄_{1} :: …:: b̄_{n} ∈ unf (γ(I a_{1}), γ(I a_{2})). By the definition this is true iff

c = h ⟵ ϑ [] g_{1}, …, g_{n} ∈ γ(I a_{1})

⟨h_{i} ⟵ ϑ_{i} [] b̄_{i}⟩n_{i=1} < <_{c} γ(I a_{2})

σ = ϑ ∧ ∧_{i=1}^{n} (ϑ_{i} ∧ g_{i} = h_{i}) and H ⊧ σ

By γ definition, there exist h ⟵ κ [] g_{1}, …, g_{n} ∈ I a_{1}, such that ϑ ∈ γ_{A}(κ) and ⟨h_{i} ⟵ κ_{i} [] b̄_{i}⟩n_{i=1} < <_{c} I a_{2} such that for each i = 1, …, n: ϑ_{i} ∈ γ_{A}(κ_{i}). By ⊗ correctness and because (C, α_{A}, A, γ_{A}) is a Galois insertion:

ϑ ∧ ∧_{i=1}^{n} (ϑ_{i} ∧ g_{i} = h_{i}) ∈ γ_{A} (κ ⊗ ⊗_{i=1}^{n} (κ_{i} ⊗ α_{A}(g_{i} = h_{i})))

This concludes the proof.