Detecting Determinate Computations by Bottom-up Abstract Interpretation ^{∗}

Roberto Giacobazzi , Laura Ricci Dipartimento di Informatica Università di Pisa Corso Italia 40, 56125 Pisa

{giaco,ricci}@di.unipi.it

Abstract

One of the most interesting characteristics of logic programs is the ability of expressing nondeterminism in an elegant and concise way. On the other hand, implementation of nondeterminism poses serious problems both in the sequential and in the concurrent case. If determinate computations are detected through a static analysis, a noticeable reduction of the execution time may be obtained. This work describes a static analysis to detect determinate computations. The analysis does not require the knowledge of the activating modes of the predicate and it derives determinacies which may be inferred from the success set of the program.

1 Introduction

One of the main features of logic programming is the ability to compute a set of output bindings for each variable of a query. While this characteristic supports an elegant and concise definition of non-deterministic behaviours, it poses serious problems both in a sequential and in a concurrent implementation of the language. In several cases, the ability of logic programs to compute multiple bindings is not exploited: in this case a logic program has a determinate behaviour, i.e. it produces a single output value for a given query, or for a class of queries satisfying some properties. Recently, some analyses [6, 4, 11, 10, 12] have been proposed to statically detect when a computation is determinate. The knowledge of determinate computations, i.e. determinacies, supports optimization of the program execution time [5] end of bottom-up evaluators [10].

Even if the analysis to detect determinancies is related to the control features of the language implementation, we show that determinancies may be inferred by a bottom up analysis that does not require any knowledge of the type and activating modes of a predicate. The analysis derives those determinacies that may be inferred from the success set of the program. The definition of the analysis requires the investigation of the relation between the input values of a predicate and those returned by the refutation of the predicate itself. Some recent proposals [1, 6, 8, 12] characterize such a relation through the notion of dependence. This notion has been exploited, for instance, to describe the relation between the groundness of a set of arguments of a predicate upon invocation and the groundness of another set of arguments, after the refutation of the predicate. We refine such notion through that of deterministic ground dependence. A ground dependence from a set of input arguments to a set of output ones is deterministic if, whenever the input arguments are ground, the refutation binds any output argument to a single ground term. The definition of deterministic ground dependences supports a refined notion of functionality, i.e. functionality is inferred with respect to subsets of arguments rather than to whole predicates. The analysis has been defined and validated through a bottomup abstract interpretation technique. It integrates the theory of hypergraphs with the semantics of logic programs in order to obtain a powerful program analysis tool. The information useful to characterize deterministic computations is produced by applying an abstract interpretation which returns an abstract model of the program. This approximation is obtained by the finite computation of the least fixpoint of an abstraction of the immediate consequence operator T_{P}. In order to have such an abstraction, a suitable set of abstract domains and operators, supporting the definition of T_{P}, is given.

∗To appear in European Conference on Programming ESOP’92

Section 2 introduces some basic notions on hypergraph theory and semantics of logic programs, Section 3 formally defines the abstract domains and abstract operators for the analysis and abstract fixpoint semantics for deterministic dependences analysis, Section 4 shows some significant examples, while Section 5 deals with some concluding remark.

2 Preliminaries

We assume the reader familiar with the notions of lattice theory, hypergraph theory [2], semantics of logic programs [7] and the basic concepts of logic programming [9].

In the following we will denote by S/{s} the set S where the element {s} has been removed.

A hypergraph G is a pair (N , E) where N = {v_{1}, ..., v_{n}} is a (finite) set of nodes and E = {e_{1}, ..., e_{m}} is a set of hyperarcs, where for each i = 1, ..., m, e_{i} = ⟨T, H⟩ such that T ⊆ N (the tail) and H ∈ N (the head). In the following we denote by T ail(e) and Head(e) the tail and the head of any hyperarc e. The “tail” and “head” notions are extended to deal with sets of hyperarcs. A hyperarc e is satisfied by a set of nodes N′ iff T ail(e) ⊆ N′. A graph Ψ is a hypergraph (N_{Ψ}, E_{Ψ}) where ∀e ∈ E_{Ψ}, |T ail(e)| = 1 (we denote by |T | the number of elements is T). Given a graph Ψ, the nodes n and n′ are connected in Ψ iff there exists a path π ⊆ E_{Ψ} where π = {e_{1}, ..., e_{k}} such that n = T ail(e_{1}), n′ = Head(e_{k}) and ∀j = 1, ..., k − 1, Head(e_{j}) = T ail(e_{j+1}). The connection between the nodes n and n′ (by means of a path π) in a graph Ψ will be denoted by: n ↦_{Ψ}^{π} n′. The graph, denoted by Ψ_{G}, associated with the hypergraph G = (N , E) is obtained by reducing each hyperarc: ⟨{s_{1}, ..., s_{m}}, h⟩ ∈ E, in a set of arcs {⟨s_{1}, h⟩..., ⟨s_{m}, h⟩}. In the following we will denote by ℑ_{G}(n′, n) = {π | n′ ↦_{Ψ_{G}}^{π} n} the set of paths π defining a connection from n′ to n in the graph Ψ_{G} associated with the hypergraph G.

Given a hypergraph G = (N , E), let E′ ⊆ E. The sets of nodes N′ and the node n are connected in G, by means of the hyperarcs in E′, denoted by N′ →_{G}^{E′} n, iff all the hyperarcs in E′ are satisfied by N′ ∪ Head(E′), ∀i ∈ N′ : ℑ_{(N ,E′)}(i, n) ≠ ∅ and ∀e ∈ E′, ∀i ∈ T ail(e) : i ∉ N′, ∃n̄ ∈ N′ such that ℑ_{(N ,E′/{e})}(n̄, i) ≠ ∅. We call E′ a connection from N′ to n in G. A connection E′ from N′ to n in a hypergraph G is minimal iff for each e ∈ E, N′ ↛_{G}^{E′/{e}} n.

Example 2.1 Let us consider the following hypergraph and some connections with v_{5}

[figure: G = v_{1} v_{2} v_{3} v_{4} v_{5}; a; b; c; d; e; {v_{4}} →_{G}^{{d,c,e,a}} v_{5}, {v_{3}} →_{G}^{{c,e,a}} v_{5}, {v_{1}, v_{2}} →_{G}^{{a}} v_{5}, ...; while ∀E′ ⊆ {a, b, c, d, e}: {v_{1}} ↛_{G}^{E′} v_{5}, {v_{5}} ↛_{G}^{E′} v_{5}.]

Notice that the definition of connection requires that any node in the tail of an hyperarc which is not in the set of starting nodes N′ can be reached from some starting node, without using the hyperarc itself. This condition avoids considering, in a connection, a hyperarc (e.g. a), such that each non-starting node (v_{2}) in the tail can only be reached from some starting node (v_{1}) by means of a path using the hyperarc itself (the hyperarc becomes auto-satisfied). As a consequence ∄E′ ⊆ {a, b, c, d, e} : {v_{1}} →_{G}^{E′} v_{5}.

The declarative semantics of logic programs in [7] is based on an extended Herbrand Universe containing also non-ground terms. It allows to declaratively characterize the ability of logic programs to compute answer substitutions (which are non-ground in general). Let us consider the set Cons of term constructors, and a denumerable set V ar of variables. The free Cons-algebra on V ar is denoted as T_{Cons}(V ar). A substitution ϑ is a mapping from V ar into T_{Cons}(V ar), such that {x ∈ V ar | ϑ(x) ≠ x} is finite. ε denotes the empty substitution. ϑ_{|G} denotes the restriction of the substitution ϑ to the variables occurring in G, which is extended as an identity, for any x ∈ V ar(G) such that ϑ(x) is undefined. We denote by mgu a total function which maps a pair of syntactic objects (e.g. atoms, terms,...) to an idempotent most general unifier of the objects, if such exists; fail otherwise. The extended Herbrand Universe U_{P} is defined as T_{Cons_{P}} (V ar)/ ≈, where t_{1} ≈ t_{2} iff ∃ ϑ_{1}, ϑ_{2} | t_{1}ϑ_{1} = t_{2} ∧ t_{2}ϑ_{2} = t_{1}. Let P red be a finite set of predicate symbols. An atom is an object of the form p(t_{1}, ..., t_{n}) where t_{1}, ..., t_{n} ∈ T_{Cons_{P}} (V ar) and p is an n-ary predicate symbol (i.e. p ∈ P red^{n}). The set of atoms is denoted Atoms. We denote by V ar(a) the set of variables in any syntactic object a. The Base of interpretations B_{P} is Atoms/_{≈} where ≈ extends to atoms in the obvious way. An interpretation I is any subset of B_{P}. Standard results on model-theoretic and fixpoint semantics apply to the extended domains as well as in the ground case [7]. In particular, the fixpoint semantics for a logic program P (denoted as F(P)) is defined by means of an immediate consequences operator T_{P} [7]. It derives possibly non-ground atoms by means of a bottom-up inference rule which is based on unification, as in the top-down SLD resolution.

We assume the reader familiar with the basic notions of abstract interpretation as defined in [3]. In the following an abstract interpretation supporting our analysis for definite logic programs is developed according to a bottom-up technique [1] based on an abstraction of the declarative and fixpoint semantics in [7].

3 Abstract Domains

This section introduces an analysis for ground and ground-deterministic dependences. Informally, a ground dependence does exist between a set of arguments T of an atom A and another argument h, iff whenever the arguments in T are ground, the refutation of A produces a set of ground bindings for h. A ground dependence is determinate, i.e. deterministic ground dependence, iff the refutation produces at most one binding for h. Consider the logic program

append([], X, X) : −.
append([X|Xs], Y, [X|Y s]) : −append(Xs, Y, Y s).

the refutation of the goal append([a|[]], [b|[]], Z) in the program produces only one binding for Z ({Z = [a|b|[]]}), while the goal append(X, Y, [a|b|[]]) produces multiple bindings for X and Y ({X = [a|[]], Y = [b|[]]}, {X = [a|b|[]], Y = []}, etc.). In the first case the groundness of the first two arguments uniquely determines the groundness of the third one, while, in the second case, a non-deterministic dependence does exist between the third argument and the first one and between the third and the second one.

Let P be a definite logic program, we denote by U_{P}^{♯} = {g, ng} the abstract universe of terms where g represents the ground term set, and ng the possibly non-ground one. Two terms are ground-equivalent (≈_{ground}) iff both are ground or non-ground terms. As a consequence, U_{P}^{♯} can be considered as a set of abstract objects representing equivalence classes of terms, modulo ground equivalency. It is trivial to prove that U_{P}^{♯} is a finite lattice since for each ground term there exists a non-ground term which is greater than it (i.e. g ≤_{g} ng). The elements in U_{P}^{♯} will be denoted as t^{♯}.

Definition 3.1 A dependence representation D is a triple (N , V, E), where

• (N , E) is a hypergraph such that

N is a finite set of symbols called the domain of the representation (Dom(D)),

E is a set of labelled hyperarcs of the form ⟨T, h⟩_{l}, where l ∈ {d,?, ⊥},

• V ⊆ N × U_{P}^{♯} such that |V| = |N | ∧ ∀(s, t^{♯}), (s′, t^{′♯}) ∈ V, s ≠ s′.

A dependence is a hyperarc in a dependence representation. An autodependence is a dependence ⟨T, h⟩_{l} such that h ∈ T. Dependence representations which are defined over the same domain N are called homogeneous.

The hypergraph notation is useful to represent dependence information in a concise way. Dependence representations are hypergraphs enhanced with a suitable set of labels (for nodes and hyperarcs). Since both the elements of V and the elements of E are defined on the same set of nodes N, we will often omit the reference to the underlying set of nodes when this can be deduced by the context. Labels associated with nodes will correspond to the mode information (a mode analysis is considered in our framework), while the labels associated with the dependence notion represent the type of the corresponding dependence (d and ? mean deterministic and don’t know respectively, while ⊥ means undefined). Hyperarc labels can be structured as a lattice, ({d,?, ⊥}, ≤_{d}), where d ≤_{d}? and ⊥ ≤_{d} d. Let Ψ be a graph with labelled arcs and π_{v}^{h} be a path from the node v to h in Ψ. We denote by Λ(π_{v}^{h}) the set of labels in the path π_{v}^{h}. This notation naturally extends to sets of hyperarcs.

Definition 3.2 Given a dependence representation D = (N , V, E), a hyperarc e ∈ E is redundant in D iff e = ⟨T, h⟩_{?} and h ∈ T, or e = ⟨T, h⟩_{l} and ∃T′ ⊆ T, T ≠ ∅, ∃E′ ⊆ E, e ∉ E′ such that T′ →_{(N ,E)}^{E′} h and lub_{≤_{d}}(Λ(E′)) ≤_{d} l.

A hyperarc is redundant in a dependence representation iff it does not add any information to the representation itself (i.e. either it is an autodependence labelled by ?, or there exists a connection with the same target which is more concise (T′ ⊆ T) and captures a stronger dependence relation). Notice that a connection is deterministic iff all its labels are d. In the following we will use a suitable graphical notation for dependence representations.

Example 3.1 Let us consider the non-redundant dependence representation

[figure: (v_{1}, ng), (v_{2}, ng), (v_{3}, ng); d; d; d; d] .

Note that the hyperarcs ⟨{v_{2}, v_{3}}, v_{1}⟩_{d}, ⟨{v_{1}, v_{3}}, v_{2}⟩_{d} and the autodependences ⟨{v_{3}}, v_{3}⟩_{d}, ⟨{v_{1}, v_{2}}, v_{2}⟩_{d}, ⟨{v_{1}, v_{2}, v_{3}}, v_{1}⟩_{d}, ⟨{v_{1}, v_{2}, v_{3}}, v_{2}⟩_{d}, ⟨{v_{1}, v_{2}, v_{3}}, v_{3}⟩_{d}, ⟨{v_{1}, v_{2}}, v_{1}⟩_{d}, ⟨{v_{2}, v_{3}}, v_{2}⟩_{d}, ⟨{v_{2}, v_{3}}, v_{3}⟩_{d}, ⟨{v_{2}}, v_{2}⟩_{?} are redundant if added to the previous dependence representation. As an example, ⟨{v_{3}}, v_{3}⟩_{d} is redundant since v_{3} can be reached by the node itself without considering that autodependence. Of course, all the previous dependences are redundant even if they are labelled with ?.

3.1 Abstract Atoms

Definition 3.3 An abstract atom is a pair of the form (p, D_{p}) (usually denoted as p(D_{p})) where p is an n-ary predicate symbol in P red and D_{p} is a non-redundant dependence representation such that Dom(D_{p}) = {1, ..., n} (the nodes represent the argument positions in the atom).

Definition 3.4 The abstract base, denoted as B_{P}^{♯}, is the set of non-redundant abstract atoms p(D_{p}), for each p ∈ P red.

Definition 3.5 An α-interpretation is any subset of the abstract base having at most one occurrence for each predicate symbol. We will denote such a set as Ξ^{♯} (Ξ^{♯} ⊆ 2^{B_{P}^{♯}}).

To make the analysis more concise we will return non-redundant dependences and we will approximate success patterns with their least upper bound, allowing in each αinterpretation at most one abstract atom per predicate symbol [1, 8].

Definition 3.6 Let p(D_{p}), p(D′_{p}) be two abstract atoms, where D_{p} = ({1..n}, V_{p}, E_{p}), D′_{p} = ({1..n}, V′_{p}, E′_{p}), V_{p} = {(1, t_{1}^{♯}), ..., (n, t_{n}^{♯})} and V′_{p} = {(1, t_{1}^{′♯}), ..., (n, t_{n}^{′♯})}.

p(D_{p}) ⊑ p(D′_{p}) iff

• ∀i = 1, ..., n : t_{i}^{♯} ≤_{g} t_{i}^{′♯} • ∀⟨T′, h⟩_{l′} ∈ E′_{p} either t_{h}^{′♯} = ng, t_{h}^{♯} = g and ∀e ∈ E_{p} : Head(e) ≠ h or ⟨T′, h⟩_{l′} is

redundant in ({1..n}, V_{p}, E_{p} ∪ {⟨T′, h⟩_{l′}}).

Proposition 3.1 ⊑ is a partial ordering.

Let I_{1}^{♯}, I_{2}^{♯} ∈ Ξ^{♯}, I_{1}^{♯} ≤_{α} I_{2}^{♯} iff ∀p(D_{p}) ∈ I_{1}^{♯}, ∃p(D′_{p}) ∈ I_{2}^{♯}: p(D_{p}) ⊑ p(D′_{p}).

Example 3.2

{ q(ng, ng, ng)^{}^{?} } ≤_{α} {q(ng, ng, ng)}, { p(ng, g, ng, ng)^{}^{d} } ≤_{α} { p(ng, ng, ng, ng)^{}^{d} },

{ [figure: p(ng, ng, ng, ng); d; d]} ≤_{α} { [figure: p(ng, ng, ng, ng); ?; d] }.

Since each α-interpretation includes at most one atom for each predicate symbol, it is easy to prove that ≤_{α} is a partial ordering and whenever I_{1}^{♯} ⊆ I_{2}^{♯}, then I_{1}^{♯} ≤_{α} I_{2}^{♯}. Moreover, since P red is finite and for each n-ary predicate symbol p ∈ P red there always exists a finite set of abstract atoms in B_{P}^{♯} defined on p, it is easy to prove that (Ξ^{♯}, ≤_{α}) is a finite lattice [1].

3.2 Abstract Substitutions

To develop an abstract interpretation based upon a declarative semantics, we also have to reconsider the substitution notion within the abstract framework [1].

Given a finite set of variables V, we denote by Subst_{V} the set of substitutions ϑ defined on V̄ for each V̄ ⊆ V. Let Φ_{1}, Φ_{2} ∈ 2^{Subst_{V}}, Φ_{1} ≤_{S} Φ_{2} iff (∀ϑ ∈ Φ_{1}, ∃ϑ′ ∈ Φ_{2} | ϑ ≤ ϑ′) ∧ (∀ϑ ∈ Φ_{2}, ∃ϑ′ ∈ Φ_{1} | ϑ ≤ ϑ′ ⇒ Φ_{1} ⊆ Φ_{2}).

Definition 3.7 An abstract substitution ϑ^{♯} is a non-redundant dependence representation such that Dom(ϑ^{♯}) = V (the nodes are the symbols of variables in V).

Thus, an abstract substitution ϑ^{♯} can be represented as a hypergraph of bindings of the form (X/t^{♯}) where X ∈ V and t^{♯} ∈ U_{P}^{♯}.

Given a finite set V_{n} of variable symbols {x_{1}, ..., x_{n}} such that x_{i} ≠ x_{j} for each i ≠ j: Subst_{V_{n}}^{♯} denotes the set of abstract substitutions defined on the set of variables V_{k}, for each V_{k} ⊆ V_{n}. We can deal with a finite set of variables because of the bottom-up approach. In fact, in this kind of analysis the meaningful substitutions are only those referring the finite amount of variables occurring in program clauses. Let Σ_{V_{n}}^{♯} ⊆ 2^{Subst_{Vn}^{♯}} such that ∀Φ^{♯} ∈ Σ_{V_{n}}, Φ^{♯} contains at most one abstract substitution ϑ^{♯} such that Dom(ϑ^{♯}) = V_{k}, for each V_{k} ⊆ V_{n}. Note that any element in Σ_{V}^{♯} can be handled as an α-interpretation. As a matter of fact, abstract substitutions can be considered as abstract atoms having a different predicate symbol of arity k for each V_{k} ⊆ V_{n}. Thus, since the preorder ⊑ can be defined between any homogeneous dependence representations, independently from the domain, an ordering relation ≤_{Σ} can be defined by extending the ≤_{α} on the domain of sets of abstract substitutions. It is easy to prove that [1] given a finite set of variables V_{n}, (Σ_{V_{n}}^{♯}, ≤_{Σ}) is a finite lattice.

3.3 Galois Connections

Let I ∈ 2^{B_{P}} and p ∈ P red. In the following we denote by I ↓ p the set of atoms in I having the same predicate symbol p.

Let I ↓ p = {p(t_{1_{1}}, ..., t_{1_{n}}), ..., p(t_{m_{1}}, ..., t_{m_{n}})}. We define an abstraction map

abs : 2^{B_{P}} → Ξ^{♯} such that abs(I) = ∪_{p∈P red} abs(I ↓ p) where abs(I ↓ p) = ∅ if I ↓ p = ∅ and

abs(I ↓ p) = p(D_{p}) such that D_{p} = ({1..n}, V_{p}, E_{p}) otherwise; where

• V_{p} = \{(i, t_{i}^{♯}) | i = 1, ..., n\} where t_{i}^{♯} = \{ \begin{matrix}g & iff ∀j = 1, ..., m, V ar(t_{j_{i}}) = ∅, \\ ng & otherwise, \end{matrix}

• Let T = {i_{1}, ..., i_{k}}; ⟨T, h⟩_{l} ∈ E_{p} iff ⟨T, h⟩_{l} is non-redundant in D_{p} and

– ∀j = 1, ..., m, V ar(t_{j_{h}}) ⊆ ∪_{i∈T} V ar(t_{j_{i}}),

– l = \{ \begin{matrix}d & iff ∀ r, f ∈ \{1, ..., m\}, r ≠ f , mgu(t_{r_{i_{1}}}, ..., t_{r_{i_{k}}} , t_{f_{i_{1}}}, ..., t_{f_{i_{k}}}) = fail, \\ ? & otherwise. \end{matrix}

Example 3.3 Let I = {q(a, b), q(b, b), q(c, d)}, then abs(I) = { [figure: q( g , g ); d; d; ?]}.

In this case, the groundness of the first argument of q uniquely determines the groundness of itself, moreover it uniquely determines the groundness of the second one. Since both the abstract arguments are ground, this information is relevant only because of the deterministic label (d) associated with the hyperarc. The (non-redundant) dependence from the second to the first argument is irrelevant and can be discarded by the analysis.

Autodependences allow to detect the source of determinism in an atom. As a matter of fact, a deterministic autodependence represents a set of arguments containing at least a deterministic term (i.e. a single choice term). The framework is designed in order to handle general (possibly auto) dependences. However, in order to let the paper more readable, in the following we will often omit any (possibly non-redundant) auto dependence in abstract objects, thus showing only the inter-argument dependences, which are more relevant for the analysis point of view.

Example 3.4 Let I = {p(X, X, d), p(a, b, c)}, abs(I) = { [figure: p(ng, ng, g); ?; d; ?] }.

The non-redundant autodependences ⟨{3}, 3⟩_{d}, ⟨{1, 2}, 1⟩_{d} and ⟨{1, 2}, 2⟩_{d} (which are not shown) show that the first two arguments and the third one deterministically determines their own groundness (the sets of argument positions {1, 2} and {3} are the two sources of the determinism for the predicate p in I). As a matter of fact, for any concrete atom p(t_{1}, t_{2}, t_{3}) having either the first two arguments or the third one ground, there exists at most one possiblity of unifying it with atoms in I.

Let I = {p(f(X, Y), Z, g(X, Y, Z)), p(a, b, c)}, the dependence representation associated with abs(I) is shown in example 3.1, where v_{1} = 1, v_{2} = 2 and v_{3} = 3.

Analogously we can define a monotonic abstraction map abs_{Σ} : 2^{Subst_{V}} → Σ_{V}^{♯}. There are no concretization maps conc such that (abs, conc) is a Galois connection between interpretations and α-interpretations. Thus, in order to define a Galois connection between the concrete and the abstract domain of computation, we have to consider sets of interpretations as single objects. Let us consider the following partial ordering relations defined on sets of interpretations and α-interpretations respectively:

• ∀D_{1}, D_{2} ∈ 2^{(2^{B_{P}})}, D_{1} ⪯ D_{2} iff (∀I_{1} ∈ D_{1} ∃I_{2} ∈ D_{2} | I_{1} ⊆ I_{2}) ∧ (∀I_{2} ∈ D_{2} ∃I_{1} ∈ D_{1} | abs(I_{2}) ≤_{α} abs(I_{1}) ⇒ D_{1} ⊆ D_{2}),

• ∀D_{1}^{♯}, D_{2}^{♯} ∈ 2^{Ξ^{♯}}, D_{1}^{♯} ⪯_{α} D_{2}^{♯} iff (∀I_{1}^{♯} ∈ D_{1}^{♯}, ∃I_{2}^{♯} ∈ D_{2}^{♯} | I_{1}^{♯} ≤_{α} I_{2}^{♯}) ∧ (∀I_{2}^{♯} ∈ D_{2}^{♯}, ∃I_{1}^{♯} ∈ D_{1}^{♯} | I_{2}^{♯} ≤_{α} I_{1}^{♯} ⇒ D_{1}^{♯} ⊆ D_{2}^{♯}).

It is easy to prove that (2^{(2^{B_{P}})}, ⪯) and (2^{Ξ^{♯}}, ⪯_{α}) are complete lattices.

Proposition 3.2 The pair of functions (α, γ) such that

• α : 2^{(2^{B_{P}})} → 2^{Ξ^{♯}} where α(D) = {abs(I) | I ∈ D},

• γ : 2^{Ξ^{♯}} → 2^{(2^{B_{P}})} where γ(D^{♯}) = {I | ∃I^{♯} ∈ D^{♯} ∧ abs(I) = I^{♯}},

holds the conditions on the Galois insertion [3] between (2^{(2^{B_{P}})}, ⪯) and (2^{Ξ^{♯}}, ⪯_{α}).

3.4 Abstract Unification (α-mgu)

The abstract most general unifier α-mgu : B_{P}^{n} ×B_{P}^{♯^{n}} → Subst_{V}^{♯} ∪{fail}, takes two n-tuples of concrete and abstract atoms respectively and returns an abstract substitution which is defined on the set of variables of the concrete atoms. It spreads ground information on the variables of the concrete atoms and it generates a dependence between a set of variables T and a variable x iff there exists a connection, in the abstract atom, between the nodes corresponding with the variables in T and the node corresponding with a term having x as variable. The resulting dependence is deterministic if such a connection contains only deterministic labels. Furthermore, it is enough to have a deterministic connection to return a deterministic dependence.

Definition 3.8 Let E′ be a connection between a set of nodes N′ and a node n ∈ N in a dependence representation D = (N , V, E). E′ is relevant iff lub_{≤_{d}}(Λ(E′)) ≠ ⊥.

The notion of minimality naturally extends to relevant connections (i.e. a minimal relevant connection is any connection E′ such that ∀e ∈ E′, E′/{e} is not a relevant connection). Let us consider the concrete and the abstract atoms, p(t_{1}, ..., t_{n}) and p(D_{p}) respectively, where D_{p} = ({1..n}, V_{p}, E_{p}) and let R ⊆ {1, ..., n} be the set of indexes such that ∀i ∈ R, V ar(t_{i}) = ∅. We define a dependence representation associated with the unification process: D_{α−mgu} = (N_{α−mgu}, V_{α−mgu}, E_{α−mgu}) where

• N_{α−mgu} = {1, ..., n} ∪ V ar(p(t_{1}, ..., t_{n})) ∪ {⊗_{i} | i ∈ R},

• V_{α−mgu} = V_{p} ∪ {(⊗_{i}, g) | ∃i ∈ {1..n} : V ar(t_{i}) = ∅} ∪ {(x, ng) | ∃x ∈ V ar(t_{1}..t_{n})};

• E_{α−mgu} = E_{p} ∪ {⟨{⊗_{i}}, i⟩_{⊥}, ⟨{i}, ⊗_{i}⟩_{⊥} | ∃i ∈ {1..n} : V ar(t_{i}) = ∅} ∪ {⟨{x_{1}, ..., x_{k}}, i⟩_{⊥}, ⟨{i}, x_{1}⟩_{⊥}, ..., ⟨{i}, x_{k}⟩_{⊥} | ∃i ∈ {1..n} : V ar(t_{i}) = {x_{1}, ..., x_{k}}}.

The abstract unification process works on this dependence representation and consists of the following two steps:

1. Ground information propagation It is an iterative process on the hypergraph G_{α−mgu} = (N_{α−mgu}, E_{α−mgu}) which changes the labels in V_{α−mgu}. The process replaces any labelled node (v, ng) ∈ V_{α−mgu} with (v, g) iff there exists a hyperarc e ∈ E_{α−mgu} such that Head(e) = v and ∀v_{i} ∈ T ail(e) : (v_{i}, g) ∈ V_{α−mgu} [1]. The process halts when no more labels can be changed.

2. α-substitution definition This process considers the transformed hypergraph and returns an abstract substitution ϑ^{♯} = (V ar(t_{1}, ..., t_{n}), V_{ϑ}, E_{ϑ}) such that V_{ϑ} = {(x, t^{♯}) ∈ V_{α−mgu} | x ∈ V ar(t_{1}, ..., t_{n})}, ∀x_{k} ∈ V ar(t_{1}, ..., t_{n}), ⟨T, x_{k}⟩_{l} ∈ E_{ϑ} iff ⟨T, x_{k}⟩_{l} is non-redundant in ϑ^{♯} and if Ē is the set of minimal relevant connections from T to x_{k}, then Ē ≠ ∅ and l = glb_{≤_{d}} { lub_{≤_{d}}(Λ(E′)) | E′ ∈ Ē }.

The condition lub_{≤_{d}}(Λ(π)) ≠ ⊥ avoids the introduction of irrelevant hyperarcs, labelled by ⊥. As a matter of fact, we are only interested in those connections E′ containing at least a hyperarc in E_{p}. Notice that D_{α−mgu} can be redundant.

Example 3.5 Let D_{α−mgu} = [figure: (X, ng); (1, ng); ?; ⊥] , and E′_{1} = {⟨{X}, 1⟩_{⊥}, ⟨{1}, X⟩_{⊥}, ⟨{1}, 1⟩_{?}}, E′_{2} = {⟨{X}, 1⟩_{⊥}, ⟨{1}, X⟩_{⊥}}. Note that ∀i = 1, 2 : {X} →_{D_{α−mgu}}^{E′_{i}} X, but since E′_{2} contains only undefined (⊥) hyperarcs, only E′_{1} is “relevant” in the unification process.

Example 3.6 The ground information propagation applied to the dependence representation associated with the abstract unification of p(f(X, Y), a) and p(ng, ng)_{}_{?} is (⊥ labels are omitted):

[figure: (1, ng); (2, ng); (X, ng); (Y, ng); (⊗_{2}, g); ?; ⟹; (1, g); (2, g); (X, g); (Y, g); (⊗_{2}, g); ?]

It is easy to extend the previous abstract unification algorithm to any n-tuple (n ≥ 1) of atoms, as shown in the following example.

Example 3.7 Let us consider the abstract unification of the concrete and abstract atoms

p(X, Y), q(Y, Z, W), r(Z, X) and p(ng, ng)^{}^{d} , [figure: q(ng, ng, ng); ?; d] , r(ng, ng)_{}_{?} .

Since there exist shared variables between the concrete atoms p(X, Y), q(Y, Z, W), r(Z, X), the unification hypergraph contains multiple connections between the corresponding variables and the abstract terms (the predicate symbol is subscripted in any corresponding argument position). The corresponding dependence representation is

[figure: (2_{r}, ng); (1_{p}, ng); (2_{p}, ng); (1_{q}, ng); (2_{q}, ng); (3_{q}, ng); (1_{r}, ng); (X, ng); (Y, ng); (Z, ng); (W, ng); d; d; ?; ?]

The resulting abstract substitution is: [figure: (Z/ng, Y/ng, X/ng, W/ng); ?; d; d].

Proposition 3.3 (α-mgu monotonicity)

Let A be an atom. Given a pair of abstract atoms A^{♯}, A^{′♯} such that {A^{♯}} ≤_{α} {A^{′♯}}, α-mgu(A, A^{♯}) ≤_{Σ} α-mgu(A, A^{′♯}).

3.5 Substitution Application (α-apply)

In order to develop a deterministic ground dependence analysis we have to define the application of abstract substitutions (returned by the abstract unification process) to concrete atoms, i.e. α-apply : 2^{(B_{P} ×Subst_{V}^{♯} )} → Ξ^{♯}. Given a set of pairs of concrete atoms (having the same predicate symbol) and abstract substitutions, it returns an abstract atom which collects the deterministic ground information belonging to this set.

Let S ∈ 2^{(B_{P} ×Subst_{V}^{♯} )} such that S ↓ p = {(p(t_{1_{1}}, ..., t_{1_{n}}), ϑ_{1}^{♯}), ..., (p(t_{m_{1}}, ..., t_{m_{n}}), ϑ_{m}^{♯})}, and let N_{i_{j}} = {x(j) | x ∈ V ar(t_{i_{j}})} be the set of variables in t_{i_{j}}, indexed according to the corresponding argument position.

For each pair (p(t_{i_{1}}, ..., t_{i_{n}}), ϑ_{i}^{♯}) where ϑ_{i}^{♯} = (N_{ϑ_{i}}, V_{ϑ_{i}}, E_{ϑ_{i}}), we generate a dependence representation D_{α−apply_{i}} = (N_{α−apply_{i}}, V_{α−apply_{i}}, E_{α−apply_{i}}) such that:

• N_{α−apply_{i}} = N_{ϑ_{i}} ∪ ( ∪_{j=1}^{n} N_{i_{j}});

• V_{α−apply_{i}} = V_{ϑ_{i}} ∪ {(x(j), ng) | ∃j = 1..n : x(j) ∈ N_{i_{j}}};

• E_{α−apply_{i}} = E_{ϑ_{i}} ∪ {⟨{x(j)}, x⟩_{⊥}, ⟨{x}, x(j)⟩_{⊥}|∃(x, t^{♯}) ∈ V_{ϑ_{i}}, ∃j = 1..n : x(j) ∈ N_{i_{j}}} (if ∃(x, t^{♯}) ∈ V_{ϑ_{i}}, ∃j = 1..n : x(j) ∈ N_{i_{j}}, x(j) is a linked variable).

Example 3.8 The dependence representation associated with the pair

(p(f(X, Y), Z, f(X, U)), [figure: (Z/ng, U/ng, Y/g); d; d; d] ) is:

[figure: (X(1), ng); (Y (1), ng); (Z(2), ng); (X(3), ng); (U(3), ng); (Y, g); (Z, ng); (U, ng); d; d; d; F ree; F ree]

Let us consider a ground information propagation on G_{α−apply_{i}} = (N_{α−apply_{i}}, E_{α−apply_{i}}), i = 1, ..., m, which is analogous to the α-mgu case. We define

α-apply(S) = ∪_{p∈P red} α-apply(S ↓ p)

where α-apply(S ↓ p) = \{ \begin{matrix}∅ & if S ↓ p = ∅ \\ p(D_{p}) & otherwise \end{matrix} , such that D_{p} = (\{1..n\}, V_{p}, E_{p}) and

•  ∀(j, t_{j}^{♯}) ∈ V_{p} : t_{j}^{♯} = \{ \begin{matrix}g & iff & ∀i = 1, ..., m : N_{i_{j}} = ∅ \\ & & (the term was already ground) \\ & & or the nodes in N_{i_{j}} are labelled g, \\ ng & otherwise, \end{matrix}

• e = ⟨{r_{1}, ..., r_{k}}, h⟩_{l} ∈ E_{p} iff e is non-redundant in D_{p} and for each i = 1, ..., m:

– F ree(N_{i_{h}}) ⊆ ∪_{u=r_{1}}^{r_{k}} F ree(N_{i_{u}}), where F ree(N_{i_{j}}) is the set of variables x such that x(j) is not linked with any node in the hypergraph G_{α−apply_{i}};

– for each linked node y(h) ∈ N_{i_{h}}, there exists T ⊆ ∪_{u=r_{1}}^{r_{k}} N_{i_{u}} such that, if Ē_{i_{y(h)}}^{T} is the set of minimal relevant connections from T to y(h) in G_{α−apply_{i}}, then Ē_{i_{y(h)}}^{T} ≠ ∅;

– l = \{ \begin{matrix}d & iff ∀z, f ∈ \{1, ..., m\}, z ≠ f : mgu(t_{z_{r_{1}}}, ..., t_{z_{r_{k}}} , t_{f_{r_{1}}}, ..., t_{f_{r_{k}}}) = fail, \\ & ∃y(h) ∈ N_{i_{h}}, ∃T ⊆ ∪_{u=r_{1}}^{r_{k}} N_{i_{u}} : Ē_{i_{y(h)}}^{T} ≠ ∅ ∧ \\ & d = glb_{≤_{d}} \{ lub_{≤_{d}}(Λ(E′)) | E′ ∈ Ē_{i_{y(h)}}^{T}) \} , \\ ? & otherwise. \end{matrix}

Example 3.9 The following examples show the results of the application of the α-apply operator in some interesting cases:

S_{1} = {(p(X, Z), (X/ng, Z/ng)^{}^{d}  ), (p(f(X), K), (X/ng, K/ng)^{}^{d}  )}, α-apply(S_{1}) =

{ p(ng, ng)^{}^{?} };

S_{2} = {(p(f(X, Y), Z, f(X, U)), [figure: (Z/ng, U/ng, Y/g); d; d; d] ), (p(0, X, X), ∅)}, α-apply(S_{2}) =

{ [figure: p(ng, ng, ng); ?; ?; d; d] } (see example 3.8).

Let I be a finite set of atoms, and S = I × {∅}. By α-apply definition we have α-apply(S) = abs(I).

Proposition 3.4 (α-apply monotonicity)

Given two sets of pairs of concrete atoms (having the same predicate symbol) and abstract substitutions {(A_{1}, ϑ_{1}^{♯}), ..., (A_{k}, ϑ_{k}^{♯})} and {(A_{1}, ϑ_{1}^{′♯}), ..., (A_{k}, ϑ_{k}^{′♯})}, such that ∀i = 1, ..., k : ϑ_{i}^{♯} ≤_{Σ} ϑ_{i}^{′♯}, it follows that

α-apply({(A_{i}, ϑ_{i}^{♯}) | i = 1, ..., k}) ≤_{α} α-apply({(A_{i}, ϑ_{i}^{′♯}) | i = 1, ..., k}).

3.6 Abstract Interpretation

The approximation of the concrete fixpoint semantics is given in terms of the fixpoint of a finitely converging monotonic operator defined in terms of α-mgu and α-apply.

Definition 3.9 Given a logic program P, let I^{♯} be an interpretation. The abstract immediate consequence operator associated with the program P, T_{P}^{♯} : Ξ^{♯} → Ξ^{♯}, is defined as follows

T_{P}^{♯} (I^{♯}) = α-apply(\{ (p(t̄), ϑ^{♯}) | \begin{matrix}∃p(t̄) : −B_{1}, ..., B_{n} ∈ P, ∃B_{1}^{′♯}, ..., B_{n}^{′♯} ∈ I^{♯}, \\ ϑ^{♯} = α − mgu(B_{1}, ..., B_{n}, B_{1}^{′♯}, ..., B_{n}^{′♯}), \\ ϑ^{♯} ≠ fail \end{matrix} \}).

The correctness of T_{P}^{♯} (abs(T_{P} (I)) ≤_{α} T_{P}^{♯} (abs(I))) follows by the correctness of α-mgu and α-apply. Let lfp(f) denote the least fixpoint of a given function f. Since the lattice (Ξ^{♯}, ≤_{α}) is finite, there exists a finite positive number k such that F^{♯}(P) = lfp(T_{P}^{♯}) = T_{P}^{♯} ↑ k.

Let us consider the concrete and the abstract operators

• T_{P} : 2^{(2^{B_{P}})} → 2^{(2^{B_{P}})}, such that T_{P} (D) = {T_{P} (I) | I ∈ D},

• T_{P}^{♯} : 2^{Ξ^{♯}} → 2^{Ξ^{♯}} such that T_{P}^{♯}(D^{♯}) = {T_{P}^{♯} (I^{♯}) | I^{♯} ∈ D^{♯}}.

It is esay to prove that for each logic program P, {F(P)} and {F^{♯}(P)} are fixpoints of T_{P} and T_{P}^{♯} respectively (T_{P} ↑ ω = {F(P)} and T_{P}^{♯} ↑ k = {F^{♯}(P)}). Thus, by T_{P}^{♯} correctness: α(T_{P} ↑ ω) ⪯_{α} T_{P}^{♯} ↑ k (or equivalently [3] T_{P} ↑ ω ⪯ γ(T_{P}^{♯} ↑ k)).

4 Applications

In the following example [14] we show the overall analysis by describing the composition of the operators defined in Section 3. Consider the predicate r defined as follows

r(g(X), g(X)) : −.
r(f(X), g(Y)) : −r(Y, X).

Let us examine the behaviour of our analysis:

T_{r}^{♯^{1}}(∅) = α-apply({(r(g(X), g(X)), ∅)}) = { [figure: r(ng, ng); d; d]}.

In the first step, the abstract unification returns the pair (r(g(X), g(X)), ∅) only. A ground dependence is detected between the first and the second argument and on the other way round by α-apply. Since the argument of α-apply is a set of pairs including only one element, the resulting dependences are labelled as deterministic.

T_{r}^{♯^{2}}(∅) = α-apply({(r(g(X), g(X)), ∅), (r(f(X), g(Y)), [figure: (X/ng, Y/ng); d; d] )} = { [figure: r(ng, ng); ?; d]}.

In the second step, α-apply considers two pairs: the one returned by the previous step and the one produced by the abstract unification of the abstract atom returned by the previous step with the concrete atom in the body of the non-unit clause of r. Since the second arguments of the concrete atoms in the pairs unify, this step returns a single deterministic dependence from the first argument to the second one.

T_{r}^{♯^{3}}(∅) = α-apply({(r(g(X), g(X)), ∅), (r(f(X), g(Y)), [figure: (X/ng, Y/ng); d; ?] )} = { [figure: r(ng, ng); ?; ?]}.

The third step (fixpoint) detects that the dependence between the first and the second argument is a non-deterministic one. As in the previous steps, the first two arguments do not unify, but, since no deterministic dependence exists between the abstract terms associated with the variables X and Y, no deterministic dependence is returned. Let us consider the program

sumlist([], 0) : −.
sumlist([X|Xs], S) : −sumlist(Xs, Ss), plus(X, Ss, S).
select(X, [X|Xs], Xs) : −.
select(X, [Y |Y s], [Y |Zs]) : −select(X, Y s, Zs).
check(X, Y) : −select(Y, X, R), sumlist(X, Y).

The predicate sumlist(X, Y) is such that Y is the sum of the elements of the list X. The predicate plus is assumed to be a predefined one. The dependences of plus relevant for the analysis are a deterministic one from the first and the second argument to the third one and a non-deterministic one from the third argument to the first and the second, respectively. The list X includes relative numbers. The predicate select(X, L_{1}, L_{2}) is such that L_{2} is the list L_{1} where exactly one occurrence of X has been removed. The predicate check(X, Y) is such that Y is an element E of the list X and E is equal to the sum of the elements of X. The dependences detected by the analysis of sumlist and of select may be easily deduced from the declarative meaning of the predicates (only some dependences of sumlist and select are shown):

[figure: sumlist(ng, ng); ?; d] [figure: select(ng, ng, ng); ?; ?; ?] .

The dependences of sumlist and select are propagated, through abstract unification, to the body of check. In the hypergraph built by abstract unification, the variable Y is the target of two paths. Both of them have the variable X as source node, but only one is labelled by d. In this case, a deterministic dependence between the variables X and Y is returned. Therefore, there exists a deterministic dependence between the first and the second argument of check. As a matter of fact, since the sum of the elements in the list is uniquely determined, all the elements selected from the list are equivalent, hence the dependence may be considered as a deterministic one. The analysis infers deterministic dependences among arguments rather than determinacy of whole predicates. Let us consider the following modified version of predicate check:

check(X, Y, R) : −select(Y, X, R), sumlist(X, Y).

In this case also a non-deterministic dependence is detected between the first argument and the third one. As a matter of fact, if a list includes several elements equal to its sum, distinct lists are returned even by removing the same element.

[figure: check(ng, ng); d; ?] , [figure: check(ng, ng, ng); d; ?; ?; ?] .

The two former examples show that our analysis can return deterministic dependences not detected by previous analyses. In particular, the last example shows the importance of defining deterministic dependences among arguments rather than for the whole predicate.

Let us finally consider the classical example:

append([], X, X) : −.

append([X|Xs], Y, [X|Y s]) : −append(Xs, Y, Y s).

The analysis detects the following dependences: [figure: append(ng, ng, ng); ?; ?; d; d] (see Example 3.8 and 3.9).

5 Conclusions

Our analysis of determinate computations extends previous proposals in several directions. The ground dependence notion, introduced in the database framework [11], has been extended in order to handle recursive clauses. Hence, the analysis returns significative results not only in the case of database programming, but also in other cases, such as programs manipulating recursive data structures. We recall that determinacy is inferred with respect to arguments rather than to whole predicates. This means that a ground instance of a set of arguments may uniquely determine another set of arguments of a predicate, while producing multiple bindings for other arguments. With respect to [14], our proposal can detect both ground and ground deterministic dependences in a single step, and requires no knowledge of the types of the predicates nor of the activating modes of a predicate. Our abstract interpretation can be easily integrated with further analyses, such as depth-k [13], type and general functional ones. By pairing our analysis with a term structure one (e.g. depth-k), dependences among subterms may be detected. Furthermore, it is possible to relax the ground dependences condition in order to obtain a more general analysis of functional dependences.

References

[1] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semantics-based Bottomup Abstract Interpretation of Logic Programs. Technical Report TR 12/91, Dipartimento di Informatica, Università di Pisa, 1991. To appear in ACM Transactions on Programming Languages and Systems.

[2] C. Berge. Graphs and Hypergraphs. North-Holland, 1973.

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

[4] S. Debray and D.S. Warren. Functional Computations in Logic Programs. ACM Transactions on Programming Languages and Systems, 11-3:451–481, 1989.

[5] B. Demoen, P. VanRoy, and Y.D. Willems. Improving the Execution Speed of Compiled Prolog with Modes, Clause Selection and Determinism. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proc. TAPSOFT 1987, volume 250 of Lecture Notes in Computer Science, pages 111–125. Springer-Verlag, Berlin, 1987.

[6] P. Deransart and J. Maluszynski. Relating Logic Programs and Attribute Grammars. Journal of Logic Programming, 2:119–156, 1985.

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

[8] R. Giacobazzi and L. Ricci. Pipeline Optimizations in AND-Parallelism by Abstract Interpretation. In D. H. D. Warren and P. Szeredi, editors, Proc. Seventh Int’l Conf. on Logic Programming, pages 291–305. The MIT Press, Cambridge, Mass., 1990.

[9] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

[10] M.J. Maher and R. Ramakrishnan. Dèjà Vu in Fixpoints of Logic Programs. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming’89, pages 963–980. The MIT Press, Cambridge, Mass., 1989.

[11] A.O. Mendelzon. Functional Dependencies in Logic Programs. In Proc. of the Eleventh International Conference on Very Large Data Bases, pages 324–330, 1985.

[12] L. Ricci. Compilation of Logic Programs for Massively Parallel Systems. PhD thesis, Universitá di Pisa, Feb. 1990. T.D. 3-90.

[13] T. Sato and H. Tamaki. Enumeration of Success Patterns in Logic Programs. Theoretical Computer Science, 34:227–240, 1984.

[14] J. Zobel and P. Dart. On Logic Programs, Functional Dependencies, and Types. Technical report, University of Melbourne, 1990.