Goal independency and call patterns in the analysis of logic programs

Maurizio Gabbrielli CWI Roberto Giacobazzi ^{∗} École Polytechnique

Abstract

We propose an abstract semantics for the goal independent analysis of properties of “procedure calls” in SLD derivations (call patterns). This can be used to derive information useful for logic program optimizations. Keywords: Logic programs, abstract interpretation, procedure calls.

1 Introduction

In this paper we consider a new application in the area of abstract interpretation based on the s-semantics approach [12, 3]. Several abstract interpretation frameworks based on this approach have been defined [15], including those based [2, 6] on the original s-semantics (modeling computed answer substitutions) [11]. Starting from the simplified version of an existing concrete semantics [14], here we propose an abstract semantics to analyse, in a goal independent way, properties of call patterns. Call patterns are the atoms which are selected during the SLD derivation and can be seen as the “procedure calls” of logic languages. Informations on them are therefore useful to improve the efficiency of programs executions. In the case of logic programs, two main approaches to abstract interpretation exist, namely the top-down and the bottom-up ones. The top-down approach propagates the information as SLD-resolution does. The bottom-up approach ([18]) propagates the information as in the computation of the least fixpoint of the immediate consequences operator T_{P}. The ability to determine call pattern information is usually associated to goal dependent top-down methods. As we will argue in this paper, the choice of an adequate (concrete) semantics allows us to determine goal independent information on the call patterns and this information can be computed both top-down and bottom-up. It is worth noting that goal independent information can be useful to optimize the code in program compilation, just because it does not depend on a specific goal. The s-semantics approach to abstract interpretation was started by defining a framework for bottom-up abstract interpretation [2] based on a concrete semantics, which correctly models computed answer substitutions. The methodology can be described as follows. (1) Select an observable o, such that the property to be considered by the analysis is an abstraction α(o) of o. (2) Select a concrete semantics O_{o} correct w.r.t. o. O_{o} can equivalently be determined by either a operational top-down construction or a bottom-up construction, obtained by computing the least fixpoint of an immediate consequences operator. (3) Define a suitable abstraction O_{α(o)} of O_{o}, by providing the abstract versions of the operators involved in the top-down and bottom-up definitions and by proving the correctness theorems. (4) The result of the analysis for a specific goal G can be determined by exploiting the AND-compositionality property of the semantics. Namely, the result can be obtained by executing G in O_{α(o)}(P). If we are interested in properties of the answer substitutions we have to choose a concrete semantics correct w.r.t. answer substitutions such as the ssemantics [11]. Note that this is not the case for the least Herbrand model. If we are concerned with the problem of determining properties of the call patterns, we should use a concrete semantics which gives us more information on the computation than just the computed answers. Namely, we should model an observable consisting of all the procedure calls. Therefore in the following we first show a simplification of the resultants semantics defined in [14]. This simplified semantics models call patterns and, likewise the original definition, is goal independent and parametric w.r.t. the (local) selection rule. Then we define an abstract version of such a semantics which inherits all the properties of the concrete definition, and which allows to describe properties (such as groundness and sharing of variables) of call patterns. Since the semantic objects we use are clauses, we can use arguments similar to those in [13] to guarantee finiteness of the semantics and therefore termination of the analysis. The problem of goal independency in call patter analysis has been recently underlined in [8], by modifying the early transformational techniques given in [6]. As we will argue at the end of section 3, if one is interested in a goal independent characterization, our solution is both simpler and more general.

2 Preliminaries and notation

In the following we assume familiarity with the standard definitions and notation for logic programming (see [1] for an introduction) and abstract interpretation [10]. Let Σ be a possibly infinite set of symbols. We denote by Σ^{∗} the family of finite-length strings (sequences) from symbols in Σ, including the empty string Λ. Sequences are typically denoted by ⟨a_{1}, ..., a_{n}⟩ or simply a_{1}, ..., a_{n} for symbols a_{i} in Σ. The concatenation of sequences π_{1} and π_{2} is denoted π_{1} :: π_{2}. The sequence of symbols with first element s followed by the sequence S is denoted s|S. The length of a sequence S is denoted |S|. The set of objects a_{i} indexed on a set of symbols Σ is denoted {a_{i}}_{i∈Σ}. If Σ is totally ordered, the corresponding ordered sequence of objects a_{i} is denoted ⟨a_{i}⟩_{i∈Σ}. The set of n-tuples of symbols in Σ is denoted Σ^{n}. If R ⊆ A × A is a binary transitive relation then the transitive closure of R is denoted by R^{∗}. If ∼ is an equivalence relation on X, we denote by [x]_{∼} the equivalence class of x ∈ X. When clear from the context we abbreviate [x]_{∼} by [x] and often abuse notation by letting the elements of a set denote their corresponding equivalence classes. The powerset of a set S is denoted by ℘(S). Throughout, Σ, Π and V ar will respectively denote a set of function symbols, a set of predicate symbols and a denumerable set of variables (i.e. a first order language). The non-ground term algebra over Σ and V ar is denoted T erm(Σ, V ar) or T erm for short. The set of atoms constructed from predicate symbols in Π and terms from T erm is denoted Atom(Π, Σ, V ar) or Atom for short. The set of clauses constructed from elements of Atom(Π, Σ, V ar) is denoted Clause(Π, Σ, V ar) or Clause for short. Moreover we denote by Klause(Π, Σ, V ar) (Klause) the set of Krom (or binary) clauses, i.e. clauses containing at most one atom in the body. The notations t̄, x̄ will be used to denote tuples of terms and distinct variables respectively, while B̄ denotes a (possibly empty) conjunction of atoms. The set of variables that occur in a syntactic object (e.g. terms, atoms, clauses, etc.) t is denoted var(t). Moreover we denote by pred(t) the set of predicate symbols occurring in the syntactic object t (if any). The empty substitution is denoted ε. If Θ is a set of substitutions, then SΘ = {Sθ|θ ∈ Θ}. The set of idempotent substitutions is denoted Sub and, given a pair of syntactic objects s and t, mgu(s, t) denotes an idempotent most general unifier for the equation s = t (if any), otherwise fail. A variable renaming is a substitution which is a bijection on V ar. Syntactic objects t_{1} and t_{2} are variant, denoted t_{1} ∼ t_{2}, if, for some variable renaming ρ, t_{1}ρ = t_{2}. In the following, for a syntactic object (goal, clause etc.) s and a set of equivalence classes of objects I, 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. We write θ_{1} ≤ θ_{2} iff there exists a substitution σ such that θ_{1} = θ_{2}σ.

∗The work of R. Giacobazzi has been partly supported by the EEC Human Capital and Mobility individual grant: “Semantic Definitions, Abstract Interpretation and Constraint Reasoning”.

3 A concrete semantics for call patterns

We show now a specialized version of the construction in [14] which provides a base collecting semantics for abstraction. The semantics described below models call patterns and therefore it is simpler than the original general definition which models resultants, that will be needed to treat correct call patterns (its abstract version will be shown in section 5). The operational semantics for logic programs is given by SLD derivation which can be formalized in terms of (the transitive closure of) the transition relation on goals shown below. A pair in the relation corresponds to the reduction of a goal with a renamed clause from the program. A selection rule is a function (on the “histories” of SLD-derivations, see [1]) which selects in any goal G (in a derivation) an atom. In the following we will denote by R(G) the atoms selected by R in G.

Definition 3.1 Let P be a logic program, R be a selection

rule and ϑ ∈ Sub. The relation ⇝^{ϑ}_{P,R}⊆ Atom^{∗} × Atom^{∗} is

the smallest relation such that G ⇝^{ϑ}_{P,R} G′ iff

1. G = ⟨a_{1}, …, a_{i}, …, a_{k}⟩ and R(G) = a_{i}, 1 ≤ i ≤ k; 2. there exists h ← B̄ ∈ P renamed apart from G such

that ϑ = mgu(a_{i}, h);

3. G′ = (⟨a_{1}, …, a_{i−1}⟩ :: B̄ :: ⟨a_{i+1}, …, A_{k}⟩)ϑ.

If in the SLD derivation G ⇝^{ϑ}_{P,R}^{∗} G′ the goal G′ is empty (denote by □) we say that G has a refutation (in P). A call pattern is an atom selected in a goal of a derivation. Clearly call patterns depend on the selection rule.

Definition 3.2 (Call pattern) Let P be a program, R be a selection rule and G be a goal. The atom A is an R-call pattern for the goal G in P iff G ⇝^{ϑ}_{P,R}^{∗} G′ and R(G′) = A. The R-call pattern A is called correct iff there exists a derivation as before and G′ has a refutation.

A semantics for resultants was given in [4] by enhancing the standard semantic objects modeling computed answers (i.e. non ground atoms [11]). This is obtained by using clauses as semantic objects since a clause naturally represents a partial computation (from the head to the body). Such a semantics was extended by considering the selection rule, thus modeling also (possibly correct) call patterns in [14]. If we consider plain call patterns, such an extension can be simplified since we only need to use a domain based on Krom clauses. As shown in the following, this clause domain leads to a very simple finiteness property which is very useful in abstract interpretation. In the remaining of this section Klause denotes the set of ∼-equivalence classes of Krom clauses.

Definition 3.3 An interpretation is any subset of Klause. ℑ is the set of interpretations.

The following is the top-down definition of the semantics for call patterns.

Definition 3.4 Let P be a positive program and R be a selection rule.

O_{R}(P) = \{ A ← B ∈ Klause | \begin{matrix}p(x̄) ⇝^{ϑ}_{P,R}^{∗} B̄, \\ A = p(x̄)ϑ \\ B is selected by R in B̄ \end{matrix} \}

The correctness of the bottom-up semantics and its equivalence with the operational semantics, is achieved by considering only “local” selection rules. A local selection rule is defined in [19] as a rule which always selects in a resolvent N one of the most recently introduced atoms in the derivation from the goal to N. The atom A is introduced in the resolvent N if A is in the body of the clause used to obtain N from its parent in the derivation. This definition was refined in [14] by requiring also an ordering to be given (by the function ϕ in definition 3.5) for the selection of one of the atoms in the bodies, and therefore for the selection of one the most recently introduced atoms. In order to distinguish the different occurrences of the same atom in a derivation, every atom in the derivation is superscripted by an index which denotes the level of the derivation where the atom is introduced. Namely, the atoms in the goal are superscripted by 0. If the atom A_{j}^{i} in a resolvent R̃ is replaced by B_{1}, …, B_{n} in a derivation step, then the B_{j}’s are superscripted by i + 1.

Definition 3.5 [14] Let ϕ be a given bijection on the set of integer numbers. A selection rule R is called local and based on ϕ if it selects in the resolvent G = A_{1}^{h_{1}}, …, A_{n}^{h_{n}} the atom A_{j}^{h_{j}}, 1 ≤ j ≤ n, such that, for any k ∈ {1, …, n} with j ≠ k, h_{j} ≥ h_{k} and if h_{j} = h_{k} then ϕ(j) > ϕ(k).

Note that the PROLOG leftmost rule is “local” (with ϕ(i) = −i). Local rules produce SLD trees with a simple structure, suitable for efficient searching techniques [19]. We show now the immediate consequences operator modeling call patterns. Let id denote the interpretation { p(x̄) ← p(x̄) | p ∈ Π } where each clause is a tautology. Note that the reduction of a goal with any of the clauses in id is basically a “no-op”. According to definition 3.5 if A_{j} is the atom selected by a local rule R in the resolvent G = A_{1}, …, A_{n}, then all the atoms derived by A_{j} are evaluated before the atoms A_{i}, i ≠ j. Therefore, the ordering ϕ can also be used “locally” on the body of any clause used in the bottom-up “computation” of G. This is why we can use such an ordering also in the bottom-up “computation” defined by T_{P}^{R}. Namely, when considering a clause H ← B_{1}, …, B_{n} in the definition of T_{P}^{R}(X), we take any partition J, I of the indexes {1, …, n} such that, according to the ordering induced by ϕ, the atoms B_{j}, j ∈ J, are (completely) evaluated before the atoms B_{i}, i ∈ I. Moreover, the atom B_{k} for k ∈ I has the maximal value ϕ(k) among the B_{i}’s, and hence it is the first to be evaluated after the B_{j}’s. Hence we unify the B_{j}’s with facts in X and we unify B_{k} with a clause H_{k} : −B ∈ X ∪ id. Since H_{k} : −B ∈ X ∪ id means that the goal H_{k} leads to the call pattern B, the previous construction corresponds to a partial derivation, performed according to the rule R, for the head H which gives the call pattern Bϑ.

Definition 3.6 Let P be a program, R be a local selection rule based on ϕ and X ∈ ℑ. Then T_{P}^{R}(X) =

\{ (H ← B)ϑ | \begin{matrix}C = H ← B_{1}, …, B_{m} ∈ P, \\ I, J is a partition of \{1, .., m\} s.t. \\ k ∈ I and for any j ∈ J, i ∈ I, k ≠ i: \\ ϕ(j) > ϕ(k) > ϕ(i), \\ H_{k} ← B | ⟨H_{j} ← true⟩_{j∈J} < <_{C} X ∪ id, \\ ϑ = mgu(H_{k}|⟨H_{j}⟩_{j∈J} , B_{k}|⟨B_{j}⟩_{j∈J}), \end{matrix} \}

The fixpoint semantics F_{R}(P) is the least fixpoint of T_{P}^{R}. Since the operator T_{P}^{R} is continuous on the lattice of interpretations (ℑ, ⊆) its least fixpoint can be obtained as usual in ω steps by taking the limit of the Kleene sequence. The following theorem shows the equivalence of the operational and the fixpoint semantics. Proposition 3.8 shows that the semantics F_{R}(P) actually models the call patterns of SLD derivations which use the selection rule R.

Theorem 3.7 Let P be program and R be a local selection rule. Then F_{R}(P) = O_{R}(P).

Proposition 3.8 Let P be a program, G = A_{1}, …, A_{m} be a goal and R be a local selection rule based on ϕ. A is an R-call pattern for G in P iff the following condition hold

1. there exists a partition I, J of {1, ..., m} such that k ∈ I and for any j ∈ J, i ∈ I, k ≠ i: ϕ(j) > ϕ(k) > ϕ(i),

2. for each j ∈ J there exist H_{k} ← B | ⟨H_{j} ← true⟩_{j∈J} < <_{G} F_{R}(P) ∪ id such that ϑ = mgu(A_{k}|⟨A_{j}⟩_{j∈J}, H_{k}|⟨H_{j}⟩_{j∈J}) and A = Bϑ.

It is worth noting that when considering programs defined on a finite domain (i.e. on a finite signature containing only constants) the set of ∼ equivalence classes of Krom clauses is finite. Therefore, for such a class of programs the least fixpoint of T_{P}^{R}(X) is reached in a finite number of steps and F_{R}(P) is finite. This is useful for abstract interpretation, since often the abstract domains have such a finiteness property (see section 4).

In [6] call patterns are characterized (for the case of the leftmost selection rule only) by a transformational approach. A program P and a goal G are transformed (by using a transformation similar to the magic set transformation) into a program P_{G}, such that every call pattern of G in P is a success pattern, i.e. an atom which has a refutation in P_{G}. Call patterns can then be obtained from the (bottom up) denotation S(P_{G}) which describes the success patterns, according to the following

Theorem 3.9 [6] Let P be a program and G be a goal. If p(t̄) is a leftmost call pattern for G in P, then the atom p^{C}(t̄) ∈ S(P_{G}), while the converse does not hold.

If we compare S(P_{G}) and F_{R}(P), we get the following results: a) F_{R}(P) characterizes all and only the call patterns of a goal G in P (proposition 3.8) while this is not the case for S(P_{G}) (theorem 3.9). b) S(P_{G}) characterizes the call patterns of a specific goal G, while F_{R}(P) is goal independent. The patterns for any goal G can be determined from F_{R}(P) according to proposition 3.8. c) S(P_{G}) is only defined for the leftmost selection rule, while F_{R}(P) is defined for every local rule. d) F_{R}(P) can naturally be extended to cope with correct call patterns (see section 5). All the above properties are inherited by the abstract semantics. In particular, because of a), the analysis based on S(P_{G}), although safe, is in general less accurate than one based on F_{R}(P). The problems mentioned in a) and b) have recently been solved in [8] by modifying the transformation and by using techniques taken from the compositional semantics in [4]. The result turns out to be essentially our F_{R}(P) semantics (in the case of the leftmost rule), yet it is obtained through a more complex construction, which cannot easily be generalized to other selection rules and to correct call patterns.

4 The abstract semantics

In this section we generalize the previous semantics for call patterns to handle possibly abstract semantic objects. The idea is to modify the base concrete semantics so as to maintain the features common to all the (possibly abstract) semantics, leaving some aspects unspecified. In order to model also correct call patterns, the same kind of construction can de done by taking the semantics for resultants defined in [14] as the concrete reference semantics. The resulting framework is a powerful tool for dealing with a variety of analysis and optimization problems since it allows approximations, in a goal independent way, of both computed answers and call patterns. All the properties of the concrete semantics can be lifted to the abstract case, and the concrete semantics itself can be viewed as a specific (simple) instance of the framework.

4.1 Abstract domains and operators

We follow the standard approach to abstract interpretation of logic programs by generalizing the notion of substitution. We approximate sets of concrete substitutions in ℘(Sub) by (abstract) descriptions of substitutions in a lattice ASub_{⊑_{A}}. Since the standard theory of abstract interpretation is formalized in terms of Galois insertions [10], by specifying the relation between abstract and concrete semantic objects, we assume (℘(Sub), α_{S}, γ_{S}, ASub) to be a Galois insertion^{1}. We introduce a monotonic, associative and commutative operator ⊗ on ASub such that for every set of equations c_{1} and c_{2}: α_{S}(mgu(c_{1}, c_{2})) ⊑_{A} α_{S}(mgu(c_{1})) ⊗ α_{S}(mgu(c_{2})). Abstract semantic objects are defined on descriptions of sets of substitutions. Let LG ⊆ Atom(Π, ∅, V ar)^{∗} and LC ⊆ Clause(Π, ∅, V ar) be the sets of flat goals and flat clauses, i.e. syntactic objects with no function and constant, where no variable occurs twice. Moroever, as in the concrete case, LK ⊆ Klause(Π, ∅, V ar) is the set of flat Krom clauses. Abstract goals are pairs in LG × ASub, abstract clauses are pairs in LC × ASub and abstract Krom clauses are pairs in LK × ASub. The notation < < is extended to abstract objects. Let I^{a} be an abstract interpretation. The meaning of I^{a} is specified by the following concretization function

1i.e. α_{S} and γ_{S} are monotonic functions, α_{S}∘γ_{S} = id and γ_{S}∘α_{S} ⊇ id.

γ(I^{a}) = \{ cθ | \begin{matrix}⟨c; κ⟩ ∈ I^{a} \\ θ ∈ γ_{S}(κ) \end{matrix} \}

Several abstract objects may represent the same concrete interpretation (i.e. γ may not be injective). A similar problem was solved in [7], where abstract clauses were used to support compositionality in the analysis, by defining an equivalence relation ∼_{γ} on ℘(LC × ASub) such that I_{1}^{a} ∼_{γ} I_{2}^{a} iff γ(I_{1}^{a}) = γ(I_{2}^{a}). Notice that the equivalence ∼_{γ} provides variable restriction and equivalence up to renaming. Let AInt = ℘(LK × ASub)/_{∼_{γ}}. In the following we often omit ∼_{γ} equivalence classes. AInt is a complete lattice and there exists a Galois insertion: (ℑ, α, γ, AInt) (α is induced by γ in the usual way). The same holds if we replace K by C, i.e. if we consider (concrete and abstract) domains based on clauses rather than Krom clauses. In the following we extend the scope of α and γ on goals and abstract goals respectively.

Definition 4.1 The abstract unification operator is a function mgu^{a} : (LG × ASub) × (LG × ASub) → ASub such that for any ⟨B̄, κ⟩ and ⟨Ḡ, κ′⟩: mgu^{a}(⟨B̄, κ⟩, ⟨Ḡ, κ′⟩) = α_{S}(mgu(B̄, Ḡ)) ⊗ κ ⊗ κ′.

4.2 Goal independent abstract semantics for call patterns

We will now show the (top-down and bottom-up) abstract semantics for call patterns. The construction and the motivations are exactly the same of section 3, modulo the replacement of concrete objects by abstract ones. Therefore we give the definitions and the results with few additional explanations. The abstract operational semantics is defined, as expected, by using an abstract derivation rule which is the abstract counterpart of definition 3.1.

Definition 4.2 (abstract derivation rule) Let P be a logic program and R be a selection rule. The relation ⟶^{R}_{P} ⊆ (LG × ASub) × (LG × ASub) is the smallest relation such

that G ⟶^{R}_{P} G′ iff

1. G = ⟨A_{1}, …, A_{i}, …, A_{k}; κ⟩, 1 ≤ i ≤ k;

2. R(G′) = A_{i}

3. ⟨H ← B̄; κ_{c}⟩ < <_{G} α(P) such that κ′ = mgu^{a}(⟨A_{i}; κ⟩, ⟨H; κ_{c}⟩); and

4. G′ = ⟨⟨A_{1}, …, A_{i−1}⟩ :: B̄ :: ⟨A_{i+1}, …, A_{k}⟩; κ′⟩.

Definition 4.3 Let P be a program and R be a selection rule. We define

O_{R}^{a}(P) = \{ ⟨p(x̄) ← B; κ⟩ | \begin{matrix}⟨p(x̄); α_{S}(ε)⟩ ⟶^{R}_{α(P)}^{∗} ⟨B̄; κ⟩ \\ and B is selected by R in B̄ \end{matrix} \}

Definition 4.4 Let P be a program, R be a local selection rule based on ϕand I^{a} ∈ AInt. T_{P}^{R}(I^{a}) =

\{ C^{a} | \begin{matrix}C = ⟨H ← B_{1}, …, B_{m}; κ_{0}⟩ ∈ α(P) \\ I, J is a partition of \{1, .., m\} such that \\ k ∈ I and for each j ∈ J and i ∈ I, k ≠ i: \\ ϕ(j) > ϕ(k) > ϕ(i) \\ ⟨H_{k} ← B; κ_{k}⟩|⟨H_{j} ← true; κ_{j}⟩_{j∈J} < <_{C} I^{a} ∪ α(id) \\ κ = mgu^{a}(⟨H_{k}|⟨H_{j}⟩_{j∈J}; κ′⟩, ⟨B_{k}|⟨B_{j}⟩_{j∈J}; κ_{0}⟩) \\ κ′ = κ_{k} ⊗_{j∈J} κ_{j} and C^{a} = ⟨H ← B; κ⟩ \end{matrix} \}

The corresponding fixpoint abstract semantics F_{R}^{a}(P) extends the one in [2] with call patterns. The equivalence with the top-down semantics is stated by the following theorem.

Theorem 4.5 (Equivalence) Let P be program and R be a local selection rule. Then F_{R}^{a}(P) = O_{R}^{a}(P)

Theorem 4.6 (correctness) If P is a program and R is a local selection rule, then F_{R}(P) ⊆ γ(F_{R}^{a}(P)).

In order to ensure termination of the analysis we have now to impose some conditions which guarantee the finiteness of the abstract semantics. We call finite^{2} an abstract domain of substitutions ASub such that, for any flat clause c, { [⟨c; κ⟩]_{∼_{γ}} | κ ∈ ASub } is finite. For example, P rop ([9]) is a finite abstract domain. If the abstract domain is finite then also the semantic domain LK × ASub is finite. Therefore, as in the case of the concrete semantics for finite domain programs, the (least) fixpoint iteration of T_{P}^{R} terminates. By using the results in section 3, the correctness of the abstract semantics and the above remarks, we obtain the following theorem which shows how the abstract call pattern semantics can be used for program analysis.

Theorem 4.7 Let P be a program, G be a goal and R be a local selection rule based on ϕ. Let G^{a} = α(G) = ⟨A_{1}, …, A_{m}; κ⟩ be the corresponding abstract goal on a finite abstract domain. Then F_{R}^{a}(P) is finite and if A is an R-call pattern for G in P, then A ∈ γ(⟨A^{a}⟩) where

1. there exists a partition I, J of {1, ..., m} such that k ∈ I and for each j ∈ J, i ∈ I, k ≠ i: ϕ(j) > ϕ(k) > ϕ(i),

2. for each j ∈ J there exist ⟨⟨H_{K} ← B; κ_{k}⟩|⟨⟨H_{j} ← true; κ_{j}⟩⟩_{j∈J}⟩ < <_{G^{a}} F_{R}^{a}(P) ∪ α(id) such that κ′′ = mgu^{a}(⟨A_{k}|⟨A_{j}⟩_{j∈J}; κ⟩, ⟨H_{k}|⟨H_{j}⟩_{j∈J}; κ′⟩) where κ′ = κ_{k} ⊗_{j∈J} κ_{j}, and A^{a} = ⟨B; κ′′⟩.

5 A semantics for resultants and correct call patterns

As previously discussed, in order to model correct call patterns we need a more informative semantics, conveying information on the successful termination of the partial computation where the call pattern occurs. This kind of information is given by the resultants semantics in [14]:

O_{R,R}(P) = \{ A ← B̄ ∈ Clause | \begin{matrix}p(x̄) ⇝^{ϑ}_{P,R}^{∗} B̄, \\ A = p(x̄)ϑ \end{matrix} \}

where P is a program R is a computation rule and sets of (equivalence classes of) clauses are used as interpretations. Clearly such a semantics generalizes that of definition 3.4. Moreover, essentially because of the completeness of the ssemantics [11], a goal B_{1}, …, B_{n} successfully terminates in P iff there exist n atoms A_{i} in O_{R,R}(P) such that B_{1}, …, B_{n} and A_{1}, …, A_{n} unify. Therefore we can characterize correct call pattern by extending proposition 3.8 in the obvious way. We show the abstract semantics for resultants obtained by generalizing O_{R,R}(P). The abstraction is performed as in the previous section (using abstract clauses instead of abstract Krom clauses). The following definitions and results are the abstract counterpart of those in [14] and we refer to that paper for further details. The abstract semantics is obtained by taking all the abstract resultants for atomic generic goals.

2The same kind of domains were called compositionally tractable in [13].

O_{R,R}^{a}(P) = { ⟨p(x̄) ← B̄; κ⟩ | ⟨p(x̄); α_{S}(ε)⟩→^{R}_{α(P)}^{∗} ⟨B̄; κ⟩ }

In order to obtain an equivalent fixpoint semantics we again have to consider local rules. The motivations for the definition of the following operator are similar to those given for definition 3.6. The only difference is that here we have generic (abstract) clauses in the interpretations. Therefore, given a clause H ← B_{1}, …, B_{n} and a partition J, I of the indexes {1, …, n}, we unify the B_{j}’s with facts in I^{a}, B_{k} with a clause in I^{a} ∪ α(id) and we do not change the B_{i}’s different from B_{k}. This corresponds to an (abstract) partial derivation, performed according to the rule R, for the head H in any possible goal.

Definition 5.1 Let P be a program, R be a local selection rule based on ϕ and I^{a} ∈ AInt. T_{P}^{R,R}(I^{a}) =

\{C^{a}| \begin{matrix}C = ⟨H ← B_{1}, …, B_{m}; κ_{0}⟩ ∈ α(P) \\ I, J is a partition of \{1, .., m\} such that \\ k ∈ I and for each j ∈ J and i ∈ I, k ≠ i: \\ ϕ(j) > ϕ(k) > ϕ(i) \\ ⟨K_{k} ← B̄_{k}; κ_{k}⟩|⟨H_{j} ← true; κ_{j}⟩_{j∈J} < <_{C} I^{a} ∪ α(id) \\ κ = mgu^{a}(⟨H_{k}|⟨H_{j}⟩_{j∈J}; κ′⟩, ⟨B_{k}|⟨B_{j}⟩_{j∈J}; κ_{0}⟩) \\ κ′ = κ_{k} ⊗_{j∈J} κ_{j}, B̄′_{I} = ⟨B_{i}⟩_{i∈I,i<k}, \\ B̄′′_{I} = ⟨B_{i}⟩_{i∈I,i>k}, C^{a} = ⟨H ← B̄′_{I} :: B̄_{k} :: B̄′′_{I}; κ⟩ \end{matrix}\}

T_{P}^{R,R} is continuous. Its least fixpoint is denoted F_{R,R}^{a}(P). The following theorem states the equivalence of the two characterizations. Proposition 5.3 shows that, as in the concrete case, the abstract fixpoint semantics F_{R,R}^{a}(P) actually collects all the information on the abstract SLD derivations based on the selection rule R.

Theorem 5.2 (Equivalence) Let P be a program and R be a local selection rule. Then F_{R,R}^{a}(P) = O_{R,R}^{a}(P).

Proposition 5.3 Let P be a program, G^{a} = ⟨A_{1}, …, A_{m}; κ⟩ be a goal and R be a local selection rule based on ϕ. Then

G^{a} ⟶^{R}_{P}^{∗} H^{a} iff

1. there exists a partition I, J of {1, …, m}, such that k ∈ I, and for each j ∈ J, i ∈ I with k ≠ i, ϕ(j) > ϕ(k) > ϕ(i),

2. there exist ⟨H_{k} ← B̄_{i}; κ_{i}⟩ | ⟨H_{j} ← true; κ_{j}⟩_{j∈J} < <_{G^{a}} F_{R}^{a}(P),

3. κ′′ = mgu^{a}(⟨H_{k}|⟨H_{j}⟩_{j∈J}; κ′⟩, ⟨A_{k}|⟨A_{j}⟩_{j∈J}; κ⟩) such that κ′ = κ_{i} ⊗_{j∈J} κ_{j} and ⟨⟨A_{i}⟩_{i∈I,i<k} :: B̄_{k} :: ⟨A_{i}⟩_{i∈I,i>k}; κ′′⟩ ∼_{γ} H^{a}.

Theorem 5.4 (correctness) If P is a program and R is a local selection rule, then O_{R,R}(P) ⊆ γ(F_{R,R}^{a}(P)).

In order to have a terminating analysis we can again turn to finite abstract domains. Note however that even if the abstract domain is finite, the previous fixpoint computation for the abstract semantics can be non-terminating, because arbitrarily long bodies can be introduced in clauses by unfolding ^{3}. However, in the case of finite domains we can force termination of the fixpoint iteration of T_{P}^{R,R} (denoted T_{P}^{R,R} ↑ n∗) by using the results given in [13]. In the case of (correct) call patterns, there exists (according to theorem 4.7) the fixpoint iteration of T_{P}^{R} terminates describing all the (possibly non-correct) call patterns. Therefore also the finite interpretation T_{P}^{R,R} ↑ n∗ (even if it is not a fixpoint) models all the call patterns. Moreover, since it contains clauses, it allows us to identify correct call patterns. This remark can be formally stated as follows.

Theorem 5.5 Let P be a program, G be a goal and R be a local selection rule based on ϕ. Let G^{a} = α(G) = ⟨A_{1}, …, A_{m}; κ⟩ be the corresponding abstract goal on a finite abstract domain. If A is a correct R-call pattern for G in P, then A ∈ γ(⟨A^{a}⟩) where:

1. there exists a partition I, J of {1, ..., m} such that k ∈ I and for each j ∈ J, i ∈ I, k ≠ i: ϕ(j) > ϕ(k) > ϕ(i),

2. for each j ∈ J there exist ⟨⟨H_{k} ← B_{1}, …, B_{z}; κ_{k}⟩ |⟨⟨H_{j} ← true; κ_{j}⟩⟩_{j∈J}⟩ < <_{G^{a}} F_{R,R}^{a}(P)∪α(id) such that κ′′ = mgu^{a}(⟨A_{k}|⟨A_{j}⟩_{j∈J}; κ⟩, ⟨H_{k}|⟨H_{j}⟩_{j∈J}; κ′⟩) where κ′ = κ_{k} ⊗_{j∈J} κ_{j}, A^{a} = ⟨B_{l}; κ′′⟩ with ϕ(l) > ϕ(h) for h = 1, …, z, 1 ≤ l ≤ z and h ≠ l,

3. there exists a set S such that ⟨C_{s} ← true; κ_{s}⟩_{s∈S} < <_{G^{a}} F_{R,R}^{a}(P) and mgu^{a}(⟨⟨C_{s}⟩_{s∈S}; κ′′′⟩, ⟨⟨A_{i}⟩_{i∈I,i<k} :: B_{1}, …, B_{z} :: ⟨A_{i}⟩_{i∈I,i>k}; κ′′⟩ ≠ fail, where κ′′′ = ⊗_{s∈S}κ_{s}.

Moreover if A is an R-call pattern for G in P, then A ∈ γ(⟨A^{a}⟩) where A^{a} is determined according to conditions 1 and 2 only.

6 An example

We show the applicability of the goal independent data-flow analysis for call patterns in the case of ground dependency. We consider the abstract domain P rop [9], consisting of (equivalence classes of) propositional formulas over a set of connectives ∧, ∨ and ↔. P rop provides a concise representation for abstract substitutions which describes ground dependency relations among their arguments. A propositional formula with connectives {↔, ∨, ∧} is associated with each substitution. For example, the formula x represents a substitution ϑ such that ϑ(x) is ground, while x ↔ y∧z represents a substitution ϑ such that var(ϑ(x)) = var(ϑ(y))∪var(ϑ(z)) (x is ground iff y and z are ground). ∨ is used to represent sets containing substitutions exploiting different ground dependencies. We call ground dependency any element in P rop. We say that a truth assignment ξ satisfies a propositional formula f, written ξ ⊧ f iff ξ(f) is a tautology. Define the truth assignment asg : Sub → V ar → {true, false} such that, given a substitution θ, 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

γ_{P rop}(κ) = { θ ∈ Sub | θ′ ≤ θ ⇒ asg(θ′) ⊧ κ }

Consider the following program to reverse a list, and the leftmost selection rule:

3A similar problem was considered in compositional analysis of modular logic programs [7], where an additional layer of abstraction was required.

append([], L, L).
append([H|Y], X2, [H|Z]) ⟵ append(Y, X2, Z).
nrev([], []).
nrev([H|L], R) ⟵ nrev(L, L1), append(L1, [H], R).

The corresponding abstract clauses (abstract program) is

⟨nrev(x_{1}, x_{2}) ⟵ true; x_{1} ∧ x_{2}⟩. ⟨nrev(x_{1}, x_{2}) ⟵ nrev(x_{3}, x_{4}), append(x_{5}, x_{6}, x_{7});

x_{1} ↔ (x_{6} ∧ x_{3}) ∧ x_{4} ↔ x_{5} ∧ x_{2} ↔ x_{7}⟩

⟨append(x_{1}, x_{2}, x_{3}) ⟵ true; x_{1} ∧ x_{2} ↔ x_{3}⟩. ⟨append(x_{1}, x_{2}, x_{3}) ⟵ append(x_{4}, x_{5}, x_{6});

x_{1} ↔ (h ∧ x_{4}) ∧ x_{3} ↔ (h ∧ x_{6}) ∧ x_{2} ↔ x_{5}⟩

The abstract semantics for call patterns for nrev contains (only) the clause ⟨nrev(x_{1}, x_{2}) ⟵ append(x_{3}, x_{4}, x_{5}); x_{1} ↔ (x_{3} ∧ x_{4}) ∧ x_{2} ↔ x_{7}⟩ i.e. any call to nrev with the first argument ground will lead to a call pattern for append with the first two arguments ground. Moreover, any call to nrev with the second argument ground will lead to a call pattern for append with the third argument ground.

Acknowledgments

We thank Giorgio Levi who gave us the idea of analysing call patterns in a goal independent way.

Address:

• Maurizio Gabbrielli CWI, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands, e.mail: gabbri@cwi.nl

• Roberto Giacobazzi LIX, École Polytechnique, 91128 Palaiseau cedex,

France, e.mail: giaco@lix.polytechnique.fr

References

[1] 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.

[2] 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.

[3] A. Bossi, M. Gabbrielli, G. Levi, and M. Martelli. The s-semantics approach: Theory and applications. Journal of Logic Programming, 1994. To appear.

[4] A. Bossi, M. Gabbrielli, G. Levi, and M. C. Meo. Contributions to the Semantics of Open Logic Programs. In Proc. of the Int’l Conf. on Fifth Generation Computer Systems 1992, pages 570–580, 1992.

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

[6] M. Codish, D. Dams, and E. Yardeni. Bottom-up Abstract Interpretation of Logic Programs. Technical report, Dept. of Computer Science, The Weizmann Institute, Rehovot, 1990. To appear in Theoretical Computer Science.

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

[8] M. Codish and B. Demoen. Analysing logic programs using “prop”-ositional logic programs and a magic wand. In Proceedings of the 1993 International Logic Programming Symposium, MIT Press, 1993.

[9] 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.

[10] 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 ACM Symp. Principles of Programming Languages, pages 238–252, 1977.

[11] 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.

[12] M. Gabbrielli. The Semantics of Logic Programming as a Programming Language. PhD thesis, Dipartimento di Informatica, Università di Pisa, 1992.

[13] M. Gabbrielli, R. Giacobazzi, and D. Montesi. Modular logic programs over finite domains. In D. Saccà, editor, Proc. Eight Italian Conference on Logic Programming, 1993.

[14] M. Gabbrielli and M. C. Meo. Fixpoint Semantics for Partial Computed Answer Substitutions and Call Patterns. In H. Kirchner and G. Levi, editors, Algebraic and Logic Programming, Proc. of the Third Int’l Conf., volume 632 of LNCS, pages 84–99. Springer-Verlag, Berlin, 1992.

[15] R. Giacobazzi. Semantic Aspects of Logic Program Analysis. PhD thesis, Dipartimento di Informatica, Università di Pisa, 1992.

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

[17] 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.

[18] K. Marriott and H. Søndergaard. Bottom-up Abstract Interpretation of Logic Programs. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 733–748. The MIT Press, Cambridge, Mass., 1988.

[19] L. Vieille. Recursive query processing: the power of logic. Theoretical Computer Science, 69:1–53, 1989.