The Correctness of Set-Sharing

Patricia M. Hill^{1}, Roberto Bagnara^{2}^{⋆}, and Enea Zaffanella^{3}

1 School of Computer Studies, University of Leeds, Leeds, LS2 9JT, United Kingdom

                     hill@scs.leeds.ac.uk

2 Dipartimento di Matematica, Università degli Studi di Parma, Italy.

                 bagnara@prmat.math.unipr.it

3 Servizio IX Automazione, Università degli Studi di Modena, Italy.

               zaffanella@elektra.casa.unimo.it

Abstract. It is important that practical data flow analysers are backed by reliably proven theoretical results. Abstract interpretation provides a sound mathematical framework and necessary generic properties for an abstract domain to be well-defined and sound with respect to the concrete semantics. In logic programming, the abstract domain Sharing is a standard choice for sharing analysis for both practical work and further theoretical study. In spite of this, we found that there were no satisfactory proofs for the key properties of commutativity and idempotence that are essential for Sharing to be well-defined and that published statements of the safeness property assumed the occur-check. This paper provides a generalisation of the abstraction function for Sharing that can be applied to any language, with or without the occur-check. The results for safeness, idempotence and commutativity for abstract unification using this abstraction function are given. Keywords: abstract interpretation, logic programming, occur-check, rational trees, set-sharing.

1 Introduction

Today, talking about sharing analysis for logic programs is almost the same as talking about the set-sharing domain Sharing of Jacobs and Langen [8, 9]. Researchers are primarily concerned with extending the domain with linearity, freeness, depth-k abstract substitutions and so on [2, 4, 12, 13, 16]. Key properties such as commutativity and soundness of this domain and its associated abstract operations are normally assumed to hold. The main reason for this is that [9] not only includes a proof of the soundness but also refers the reader to the thesis of Langen [14] for proofs of commutativity and idempotence.

In abstract interpretation, the concrete semantics of a program is approximated by an abstract semantics. In particular, the concrete domain is replaced

⋆ Much of this work was supported by EPSRC grant GR/L19515.

by an abstract domain and each elementary operation on the concrete domain is replaced by a corresponding abstract operation on the abstract domain. Thus, assuming the global abstract procedure mimics the concrete execution procedure, each operation on elements in the abstract domain must produce an approximation of the corresponding operation on corresponding elements in the concrete domain. The key operation in a logic programming derivation is unification (unify) and the corresponding operation for an abstract domain is aunify.

An important step in standard unification algorithms is the occur-check that avoids the generation of infinite data structures. However, in computational terms, it is expensive and it is well known that Prolog implementations by default omit this check. Although standard unification algorithms that include the occur-check produce a substitution that is idempotent, the resulting substitution when the occur-check is omitted, may not be idempotent. In spite of this, most theoretical work on data-flow analysis of logic programming assume the result of unify is always idempotent. In particular both [9] and [14] assume in their proofs of soundness that the concrete substitutions are idempotent. Thus their results do not apply to the analysis of all Prolog programs.

If two terms in the concrete domain are unifiable, then unify computes the most general unifier (mgu). Up to renaming of variables, an mgu is unique. Moreover a substitution is defined as a set of bindings or equations between variables and other terms. Thus, for the concrete domain, the order and multiplicity of elements are irrelevant in both the computation and semantics of unify. It is therefore useful that the abstraction of the unification procedure should be unaffected by the order and multiplicity in which it abstracts the bindings that are present in the substitution. Furthermore, from a practical perspective, it is useful if the global abstract procedure can proceed in a different order to the concrete one without affecting the accuracy of the analysis results. Hence, it is extremely desirable that aunify is also commutative and idempotent. However, as discussed later in this paper, only a weak form of idempotence has ever been proved while the only previous proof of commutativity [14] is seriously flawed.

As sharing is normally combined with linearity and freeness domains that are not idempotent or commutative, [2, 12] it may be asked why these properties are important for sharing. In answer to this, we observe that the order and multiplicity in which the bindings in a substitution are analysed affects the accuracy of the linearity and freeness domains. It is therefore a real advantage to be able to ignore these aspects as far as the sharing domain is concerned.

This paper provides a generalisation of the abstraction function for Sharing that can be applied to any language, with or without the occur-check. The results for safeness, idempotence and commutativity for abstract unification using this abstraction function are given. Detailed proofs of the results stated in this paper are available in [7].

In the next section, the notation and definitions needed for equality and substitutions in the concrete domain are given. In Section 3, we introduce a new concept called variable-idempotence that generalises idempotence to allow for rational trees. In Section 4, we recall the definition of Sharing and define its abstraction function, generalised to allow for non-idempotent substitutions. We conclude in Section 5.

2 Equations and Substitutions

2.1 Notation

For a set S, # S is the cardinality of S, ℘(S) is the powerset of S, whereas ℘_{f}(S) is the set of all the finite subsets of S. The symbol Vars denotes a denumerable set of variables, whereas T_{Vars} denotes the set of first-order terms over Vars for some given set of function symbols. The set of variables occurring in a syntactic object o is denoted by vars(o).

2.2 Substitutions

If x ∈ Vars and s ∈ T_{Vars}, then x ↦ s is called a binding. A substitution is a total function σ: Vars → T_{Vars} that is the identity almost everywhere; in other words, the domain of σ,

dom(σ) =^{def} { x ∈ Vars | σ(x) ≠ x }

is finite. If t ∈ T_{Vars}, we write tσ to denote σ(t).

Substitutions are denoted by the set of their bindings, thus σ is identified with the set { x ↦ σ(x) | x ∈ dom(σ) }. The composition of substitutions is defined in the usual way. Thus τ ∘ σ is the substitution such that, for all terms t, (τ ∘ σ)(t) = τ(σ(t)). A substitution is said circular if it has the form {x_{1} ↦ x_{2}, …, x_{n−1} ↦ x_{n}, x_{n} ↦ x_{1}}. A substitution is in rational solved form if it has no circular subset. The set of all substitutions in rational solved form is denoted by Subst.

2.3 Equations

An equation is of the form s = t where s, t ∈ T_{Vars}. Eqs denotes the set of all equations.

We are concerned in this paper to keep the results on sharing as general as possible. In particular, we do not want to restrict ourselves to a specific equality theory. Thus we allow for any equality theory T over T_{Vars} that includes the basic axioms denoted by the following schemata.

s = s,  (1)
s = t ⟺ t = s,  (2)
r = s ∧ s = t ⟹ r = t,  (3)
f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}) ⟺ s_{1} = t_{1}, …, s_{n} = t_{n}.  (4)

Of course, T can include other axioms. For example, it is usual in logic programming and most implementations of Prolog to assume an equality theory based on syntactic identity and characterised by the axiom schemata given by Clark [3]. This consists of the basic axioms together with the following:

¬f(s_{1}, …, s_{n}) = g(t_{1}, …, t_{m})  (5)
∀z ∈ Vars ∀t ∈ (T_{Vars} \ Vars) : z ∈ vars(t) ⟹ ¬(z = t).  (6)

The identity axioms characterised by the schemata 5 ensure the equality theory is Herbrand and depends only on the syntax. Equality theory for a non-Herbrand domain replaces these axioms by ones that depend instead on the semantics of the domain. Axioms characterised by the schemata 6 are called the occur-check axioms and are an essential part of the standard unification procedure in SLDresolution.

An alternative approach used in some implementations of Prolog, does not require the occur-check axioms. This approach is based on the theory of rational trees [5, 6]. It assumes the basic axioms and the identity axioms together with a set of uniqueness axioms [10, 11]. These state that each equation in rational solved form uniquely defines a set of trees. Thus, an equation z = t where z ∈ vars(t) and t ∈ (T_{Vars} \ Vars) denotes the axiom (expressed in terms of the usual first-order quantifiers [15]):

∀x ∈ Vars : (z = t ∧ (x = t{z ↦ x} ⟹ z = x)).

The basic axioms defined by schemata 1, 2, 3, and 4, which are all that are required for the results in this paper, are included in both these theories.

A substitution σ may be regarded as a set of equations { x = t | x ↦ t ∈ σ }. A set of equations e ∈ ℘_{f}(Eqs) is unifiable if there is σ ∈ Subst such that T ⊢ (σ ⟹ e). σ is called a unifier for e. σ is said to be a relevant unifier of e if vars(σ) ⊆ vars(e). That is, σ does not introduce any new variables. σ is a most general unifier for e if, for every unifier σ′ of e, T ⊢ (σ′ ⟹ σ). An mgu, if it exists, is unique up to the renaming of variables. In this paper, mgu(e) always denotes a relevant unifier of e.

3 Variable-Idempotence

It is usual in papers on sharing analysis to assume that all the substitutions are idempotent. Note that a substitution σ is idempotent if, for all t ∈ T_{Vars}, tσσ = tσ. However, the sharing domain is just concerned with the variables. So, to allow for substitutions representing rational trees, we generalise idempotence to variable-idempotence.

Definition 1. A substitution σ is variable-idempotent if

∀t ∈ T_{Vars} : vars(tσσ) = vars(tσ).

The set of all variable-idempotent substitutions is denoted by VSubst.

It is convenient to use the following alternative characterisation of variableidempotence: A substitution σ is variable-idempotent if and only if,

∀(x ↦ t) ∈ σ : vars(tσ) = vars(t).

Thus any substitution consisting of a single binding is variable-idempotent. Moreover, all idempotent substitutions are also variable-idempotent.

Example 1. The substitution {x ↦ f(x)} is not idempotent but is variableidempotent. Also, {x ↦ f(y), y ↦ z} is not idempotent or variable-idempotent but is equivalent (with respect to some equality theory T) to {x ↦ f(z), y ↦ z}, which is idempotent.

We define the transformation ⟼^{S} ⊆ Subst × Subst, called S-transformation, as follows:

\frac{(x ↦ t) ∈ σ  (y ↦ s) ∈ σ  x ≠ y}{σ ⟼^{S} (σ \ \{y ↦ s\}) ∪ \{y ↦ s[x/t]\}}

Any substitution σ can be transformed to a variable-idempotent substitution σ′ for σ by a finite sequence of S-transformations. Furthermore, if the substitutions σ and σ′ are regarded as equations, then they are equivalent with respect to any equality theory that includes the basic equality axioms. These two statements are direct consequences of Lemmas 1 and 2, respectively.

Lemma 1. Let T be an equality theory that satisfies the basic equality axioms. Suppose that σ and σ′ are substitutions such that σ ⟼^{S} σ′. Then, regarding σ and σ′ as sets of equations, T ⊢ (σ ⟺ σ′).

Proof. Suppose that (x ↦ t), (y ↦ s) ∈ σ where x ≠ y and suppose also σ′ = (σ \ {y ↦ s}) ∪ {y ↦ s[x/t]}. We first show by induction on the depth of the term s that

x = t ⟹ s = s[x/t].

Suppose s has depth 1. If s is x, then s[x/t] = t and the result is trivial. If s is a variable distinct from x or a constant, then s[x/t] = s and the result follows from equality Axiom 1. Suppose now that s = f(s_{1}, …, s_{n}) and the result holds for all terms of depth less than that of s. Then, by the inductive hypothesis, for each i = 1, …, n,

x = t ⟹ s_{i} = s_{i}[x/t].

Hence, by Axiom 4,

x = t ⟹ f(s_{1}, …, s_{n}) = f(s_{1}[x/t], …, s_{n}[x/t])

and hence

x = t ⟹ f(s_{1}, …, s_{n}) = f(s_{1}, …, s_{n})[x/t].

Thus, combining this result with Axiom 3, we have

{x = t, y = s} ⟹ {x = t, y = s, s = s[x/t]}
⟹ {x = t, y = s[x/t]}.

Similarly, combining this result with Axioms 2 and 3,

{x = t, y = s[x/t]} ⟹ {x = t, y = s[x/t], s = s[x/t]}
⟹ {x = t, y = s}.
⊓ ⊔

Note that the condition x ≠ y in Lemma1 is necessary. For example, suppose σ = {x ↦ f(x)} and σ′ = {x ↦ f(f(x))}. Then we do not have σ′ ⟹ σ.

Lemma 2. Suppose that, for each j = 0, …, n:

σ_{j} = {x_{1} ↦ t_{1,j}, …, x_{n} ↦ t_{n,j}},

where t_{j,j} = t_{j,j−1} and if j > 0, for each i = 1, …, n, where i ≠ j, t_{i,j} = t_{i,j−1}[x_{j}/t_{j,j−1}]. Then, for each j = 0, …, n,

ν_{j} = {x_{1} ↦ t_{1,j}, …, x_{j} ↦ t_{j,j}}

is variable-idempotent and, if j > 0, σ_{j} can be obtained from σ_{j−1} by a sequence of S-transformations.

Proof. The proof is by induction on j. Since ν_{0} is empty, the base case when j = 0 is trivial. Suppose, therefore that 1 ≤ j ≤ n and the hypothesis holds for ν_{j−1} and σ_{j−1}. By the definition of ν_{j}, we have ν_{j} = {x_{j} ↦ t_{j,j−1}} ∘ ν_{j−1}. Consider an arbitrary i, 1 ≤ i ≤ j. We will show that vars(t_{i,j}ν_{j}) = vars(t_{i,j}).

Suppose first that i = j. Then since t_{j,j} = t_{j,j−1}, t_{j,j−1} = t_{j,0}ν_{j−1} and, by the inductive hypothesis, vars(t_{j,0}ν_{j−1}ν_{j−1}) = vars(t_{j,0}ν_{j−1}), we have

vars(t_{j,j}ν_{j}) = vars(t_{j,0}ν_{j−1}ν_{j−1}{x_{j} ↦ t_{j,j}})
= vars(t_{j,0}ν_{j−1}{x_{j} ↦ t_{j,j}})
= vars(t_{j,j}{x_{j} ↦ t_{j,j}})
= vars(t_{j,j}).

Suppose now that i ≠ j. Then,

vars(t_{i,j}) = vars(t_{i,j−1}{x_{j} ↦ t_{j,j−1}}).

and, by the inductive hypothesis, vars(t_{i,j−1}ν_{j−1}) = vars(t_{i,j−1}).

If x_{j} ∉ vars(t_{i,j−1}), then

vars(t_{i,j}ν_{j−1}) = vars(t_{i,j−1}{x_{j} ↦ t_{j,j−1}}ν_{j−1})
= vars(t_{i,j−1}ν_{j−1})
= vars(t_{i,j}).

On the other hand, if x_{j} ∈ vars(t_{i,j−1}), then

vars(t_{i,j}ν_{j−1}) = vars(t_{i,j−1}{x_{j} ↦ t_{j,j−1}}ν_{j−1})
= vars(t_{i,j−1}ν_{j−1}) \ {x_{j}} ∪ vars(t_{j,j−1}ν_{j−1})
= vars(t_{i,j−1}) \ {x_{j}} ∪ vars(t_{j,j−1})
= vars(t_{i,j−1}{x_{j} ↦ t_{j,j−1}})
= vars(t_{i,j}).

Thus, in both cases,

vars(t_{i,j}ν_{j}) = vars(t_{i,j}ν_{j−1}{x_{j} ↦ t_{j,j−1}})
= vars(t_{i,j}{x_{j} ↦ t_{j,j−1}})
= vars(t_{i,j−1}{x_{j} ↦ t_{j,j−1}}{x_{j} ↦ t_{j,j−1}}).

However, a substitution consisting of a single binding is variable-idempotent. Thus

vars(t_{i,j}ν_{j}) = vars(t_{i,j−1}{x_{j} ↦ t_{j,j−1}})
= vars(t_{i,j}).

Therefore, for each i = 1, …, j, vars(t_{i,j}ν_{j}) = vars(t_{i,j}). It then follows (using the alternative characterisation of variable-idempotence) that ν_{j} is variableidempotent. ⊓ ⊔

Example 2. Let

σ_{0} ={x_{1} ↦ f(x_{2}), x_{2} ↦ g(x_{3}, x_{4}), x_{3} ↦ x_{1}}.

Then

σ_{1} ={x_{1} ↦ f(x_{2}), x_{2} ↦ g(x_{3}, x_{4}), x_{3} ↦ f(x_{2})},
σ_{2} ={x_{1} ↦ f(g(x_{3}, x_{4})), x_{2} ↦ g(x_{3}, x_{4}), x_{3} ↦ f(g(x_{3}, x_{4}))},
σ_{3} ={x_{1} ↦ f(g(f(g(x_{3}, x_{4})), x_{4})), x_{2} ↦ g(f(g(x_{3}, x_{4})), x_{4}), x_{3} ↦ f(g(x_{3}, x_{4}))}.

Note that σ_{3} is variable-idempotent and that T ⊢ σ_{0} ⟺ σ_{3}.

4 Set-Sharing

4.1 The Sharing Domain

The Sharing domain is due to Jacobs and Langen [8]. However, we use the definition as presented in [1].

Definition 2. (The set-sharing lattice.) Let

SG =^{def} { S ∈ ℘_{f}(Vars) | S ≠ ∅ }

and let SH =^{def} ℘(SG). The set-sharing lattice is given by the set

SS =^{def} { (sh, U) | sh ∈ SH , U ∈ ℘_{f}(Vars), ∀S ∈ sh : S ⊆ U } ∪ {⊥, ⊤}

ordered by ⪯_{SS} defined as follows, for each d, (sh_{1}, U_{1}), (sh_{2}, U_{2}) ∈ SS:

⊥ ⪯_{SS} d,
d ⪯_{SS} ⊤,
(sh_{1}, U_{1}) ⪯_{SS} (sh_{2}, U_{2}) ⟺ (U_{1} = U_{2}) ∧ (sh_{1} ⊆ sh_{2}).

It is straightforward to see that every subset of SS has a least upper bound with respect to ⪯_{SS}. Hence SS is a complete lattice.^{1}

An element sh of SH abstracts the property of sharing in a substitution σ. That is, if σ is idempotent, two variables x, y must be in the same set in sh if some variable, say v occurs in both xσ and yσ. In fact, this is also true for variable-idempotent substitutions although it is shown below that this needs to be generalised for substitutions that are not variable-idempotent. Thus, the definition of the abstraction function α for sharing, requires an ancillary definition for the notion of occurrence.

Definition 3. (Occurrence.) For each n ∈ ℕ, occ_{i}: Subst × Vars → ℘_{f}(Vars) is defined for each σ ∈ Subst and each v ∈ Vars:

occ_{0}(σ, v) =^{def} {v},  if v = vσ;
occ_{0}(σ, v) =^{def} ∅,  if v ≠ vσ;
occ_{n}(σ, v) =^{def} { y ∈ Vars | x ∈ vars(yσ) ∩ occ_{n−1}(σ, v) },  if n > 0.

It follows that, for fixed values of σ and v, occ_{n}(σ, v) is monotonic and extensive with respect to the index n. Hence, as the range of occ_{n}(σ, v) is restricted to the finite set of variables in σ, there is an ℓ = ℓ(σ, v) ∈ ℕ such that occ_{ℓ}(σ, v) = occ_{n}(σ, v)) for all n ≥ ℓ. Let

occ!(σ, v) =^{def} occ_{ℓ}(σ, v).

Note that if σ is variable-idempotent, then occ!(σ, v) = occ_{1}(σ, v). Note also that if v ≠ vσ, then occ!(σ, v) = ∅. Previous definitions for an occurrence operator such as that for sg in [8] have all been for idempotent substitutions. However, when σ is an idempotent substitution, occ!(σ, v) and sg(σ, v) are the same for all v ∈ Vars.

We base the definition of abstraction on the occurrence operator, occ!.

1 Notice that the only reason we have ⊤ ∈ SS is in order to turn SS into a lattice rather than a CPO.

Definition 4. (Abstraction.) The concrete domain Subst is related to SS by means of the abstraction function α: ℘(Subst) × ℘_{f}(Vars) → SS. For each Σ ∈ ℘(Subst) and each U ∈ ℘_{f}(Vars),

α(Σ, U) =^{def} ⨆_{σ∈Σ} α(σ, U),

where α: Subst × ℘_{f}(Vars) → SS is defined, for each σ ∈ Subst and each U ∈ ℘_{f}(Vars), by

α(σ, U) =^{def} ({ occ!(σ, v) ∩ U | v ∈ Vars } \ {∅}, U).

The following result states that the abstraction for a substitution σ is the same as the abstraction for a variable-idempotent substitution for σ.

Lemma 3. Let σ be a substitution, σ′ a substitution obtained from σ by a sequence of S-transformations, U a set of variables and v ∈ Vars. Then

v = vσ ⟺ v = vσ′, occ!(σ, v) = occ!(σ′, v), and α(σ, U) = α(σ′, U).

Proof. Suppose first that σ′ is obtained from σ by a single S-transformation. Thus we can assume that x ↦ t and y ↦ s are in σ where x ∈ vars(s) and that

σ′ = (σ \ {y ↦ s}) ∪ {y ↦ s[x/t]}.

It follows that, since σ is in rational solved form, σ has no circular subset and hence v = vσ ⟺ v = vσ′. Thus, if v ≠ vσ, then we have v ≠ vσ′ and occ!(σ, v) = occ!(σ′, v) = ∅.

We now assume that v = vσ = vσ′ and prove that

occ_{m}(σ, v) ⊆ occ!(σ′, v).

The proof is by induction on m. By Definition 3, occ_{0}(σ, v) = occ_{0}(σ′, v) = {v}, so that the result holds for m = 0. Suppose then that m > 0 and that v_{m} ∈ occ_{m}(σ, v). By Definition 3, there exists v_{m−1} ∈ vars(v_{m}σ) where v_{m−1} ∈ occ_{m−1}(σ, v). Hence, by the inductive hypothesis, v_{m−1} ∈ occ!(σ′, v). If v_{m−1} ∈ vars(v_{m}σ′), then, by Definition 3, v_{m} ∈ occ!(σ′, v)). On the other hand, if v_{m−1} ∉ vars(v_{m}σ′), then v_{m} = y, v_{m−1} = x, and x ∈ vars(s) (so that vars(t) ⊆ vars(s[x/t])). However, by hypothesis, v = vσ, so that x ≠ v and m > 1. Thus, by Definition 3, there exists v_{m−2} ∈ vars(t) such that v_{m−2} ∈ occ_{m−2}(σ, v). By the inductive hypothesis, v_{m−2} ∈ occ!(σ′, v). Since y ↦ s[x/t] ∈ σ′, and v_{m−2} ∈ vars(s[x/t]), v_{m−2} ∈ vars(yσ′). Thus, by Definition 3, y ∈ occ!(σ′, v).

Conversely, we now prove that, for all m,

occ_{m}(σ′, v) ⊆ occ!(σ, v).

The proof is again by induction on m. As in the previous case, occ_{0}(σ′, v) = occ_{0}(σ, v) = {v}, so that the result holds for m = 0. Suppose then that m > 0 and that v_{m} ∈ occ_{m}(σ′, v). By Definition 3, there exists v_{m−1} ∈ vars(v_{m}σ′) where v_{m−1} ∈ occ_{m−1}(σ′, v). Hence, by the inductive hypothesis, v_{m−1} ∈ occ!(σ, v). If v_{m} ∈ occ(σ, v_{m−1}), then, by Definition 3, v_{m} ∈ occ!(σ, v). On the other hand, if v_{m−1} ∉ vars(v_{m}σ), then v_{m} = y, v_{m−1} ∈ vars(t) and x ∈ vars(s). Thus, as y ↦ s ∈ σ, y ∈ vars(xσ). However, since x ↦ t ∈ σ, v_{m−1} ∈ vars(xσ) so that, by Definition 3, x ∈ occ!(σ, v). Thus, again by Definition 3, y ∈ occ!(σ, v).

Thus, if σ′ is obtained from σ by a single S-transformation, we have the required results: v = vσ ⟺ v = vσ′, occ!(σ, v) = occ!(σ′, v), and α(σ, U) = α(σ′, U).

Suppose now that there is a sequence σ = σ_{1}, …, σ_{n} = σ′ such that, for i = 2, …, n, σ_{i} is obtained from σ_{i−1} by a single S-step. If n = 1, then σ = σ′. If n > 1, we have by the first part of the proof that, for each i = 2, …, n, v = vσ_{i−1} ⟺ v = vσ_{i}, occ!(σ_{i−1}, v) = occ!(σ_{i}, v), and α(σ_{i−1}, U) = α(σ_{i}, U), and hence the required results. ⊓ ⊔

Example 3. Consider again Example 2. Then

occ_{1}(σ_{0}, x_{4}) = {x_{2}, x_{4}},
occ_{2}(σ_{0}, x_{4}) = {x_{1}, x_{2}, x_{4}},
occ_{3}(σ_{0}, x_{4}) = {x_{1}, x_{2}, x_{3}, x_{4}} = occ!(σ_{0}, x_{4}),

and

occ_{1}(σ_{3}, x_{4}) = {x_{1}, x_{2}, x_{3}, x_{4}} = occ!(σ_{3}, x_{4}).

Thus, if V = {x_{1}, x_{2}, x_{3}, x_{4}},

α(σ_{0}, V) = α(σ_{3}, V) = {{x_{1}, x_{2}, x_{3}, x_{4}}}.

4.2 Abstract Operations for Sharing Sets

We are concerned in this paper in establishing results for the abstract operation aunify which is defined for arbitrary sets of equations. However, by building the definition of aunify in three steps via the definitions of amgu (for sharing sets) and Amgu (for sharing domains) and stating corresponding results for each of them, we provide an outline for the overall method of proof for the aunify results. Details of all proofs are available in [7].

In order to define the abstract operation amgu we need some ancillary definitions.

Definition 5. (Auxiliary functions.) The closure under union function (also called star-union), (·)^{⋆}: SH → SH , is, for each sh ∈ SH ,

sh^{⋆} =^{def} { S ∈ SG | ∃n ≥ 1 . ∃T_{1}, …, T_{n} ∈ sh . S = T_{1} ∪ ⋯ ∪ T_{n} }.

For each sh ∈ SH and each T ∈ ℘_{f}(Vars), the extraction of the relevant component of sh with respect to T is encoded by the function rel: ℘_{f}(Vars)×SH → SH defined as

rel(T, sh) =^{def} { S ∈ sh | S ∩ T ≠ ∅ }.

For each sh_{1}, sh_{2} ∈ SH , the binary union function bin: SH ×SH → SH is given by

bin(sh_{1}, sh_{2}) =^{def} { S_{1} ∪ S_{2} | S_{1} ∈ sh_{1}, S_{2} ∈ sh_{2} }.

The function proj: SH × ℘_{f}(Vars) → SH projects an element of SH onto a set of variables of interest: if sh ∈ SH and V ∈ ℘_{f}(Vars), then

proj(sh, V) =^{def} { S ∩ V | S ∈ sh, S ∩ V ≠ ∅ }.

Definition 6. (amgu.) The function amgu captures the effects of a binding x ↦ t on an SH element. Let x be a variable and t a term. Let also sh ∈ SH and

A =^{def} rel({x}, sh),
B =^{def} rel(vars(t), sh).

Then

amgu(sh, x ↦ t) =^{def} (sh \ (A ∪ B)) ∪ bin(A^{⋆}, B^{⋆}).

Then we have the following soundness result for amgu.

Lemma 4. Let (sh, U) ∈ SS and {x ↦ t}, σ, ν ∈ Subst such that ν is a relevant unifier of {xσ = tσ} and vars(x), vars(t), vars(σ) ⊆ U. Then

α(σ, U) ⪯_{SS} (sh, U) ⟹ α(ν ∘ σ, U) ⪯_{SS} (amgu(sh, x ↦ t), U).

To prove this, observe that, by Lemma 2, if σ is not variable-idempotent, it can be transformed to a variable-idempotent substitution σ′. Hence, by Lemma 3, α(σ, U) = α(σ′, U). Therefore, the proof, which is given in [7], deals primarily with the case when σ is variable-idempotent.

Since a relevant unifier of e is a relevant unifier of any other set e′ equivalent to e wrt to the equality theory T, this lemma shows that it is safe for the analyser to perform part or all of the concrete unification algorithm before computing amgu.

The following lemmas, proved in [7], show that amgu is commutative and idempotent.

Lemma 5. Let sh ∈ SH and {x ↦ r} ∈ Subst. Then

amgu(sh, x ↦ r) = amgu(amgu(sh, x ↦ r), x ↦ r).

Lemma 6. Let sh ∈ SH and {x ↦ r}, {y ↦ t} ∈ Subst. Then

amgu(amgu(sh, x ↦ r), y ↦ t) = amgu(amgu(sh, y ↦ t), x ↦ r).

4.3 Abstract Operations for Sharing Domains

The definitions and results of Subsection 4.2 can be lifted to apply to sharing domains.

Definition 7. (Amgu.) The operation Amgu: SS × Subst → SS extends the SS description it takes as an argument, to the set of variables occurring in the binding it is given as the second argument. Then it applies amgu:

Amgu((sh, U), x ↦ t)

=^{def} (amgu(sh ∪ { {u} | u ∈ vars(x ↦ t) \ U }, x ↦ t), U ∪ vars(x ↦ t)).

The results for amgu can easily be extended to apply to Amgu.

Definition 8. (aunify.) The function aunify: SS ×Eqs → SS generalises Amgu to a set of equations e: If (sh, U) ∈ SS, x is a variable, r is a term, s = f(s_{1}, …, s_{n}) and t = f(t_{1}, …, t_{n}) are non-variable terms, and \overline{s} = \overline{t} denote the set of equations {s_{1} = t_{1}, …, s_{n} = t_{n}}, then

aunify((sh, U), ∅) =^{def} (sh, U),

if e ∈ ℘_{f}(Eqs) is unifiable,

aunify((sh, U), e ∪ {x = r}) =^{def} aunify(Amgu(sh, U), x ↦ r), e \ {x = r}),
aunify((sh, U), e ∪ {s = x}) =^{def} aunify((sh, U), (e \ {s = x}) ∪ {x = s}),
aunify((sh, U), e ∪ \{s = t\}) =^{def} aunify((sh, U), (e \ \{s = t\}) ∪ \overline{s} = \overline{t}),

and, if e is not unifiable,

aunify((sh, U), e) =^{def} ⊥.

For the distinguished elements ⊥ and ⊤ of SS

aunify(⊥, e) =^{def} ⊥, aunify(⊤, e) =^{def} ⊤.

As a consequence of this and the generalisation of Lemmas 4, 5 and 6 to Amgu, we have the following soundness, commutativity and idempotence results required for aunify to be sound and well-defined. As before, the proofs of these results are in [7].

Theorem 1. Let (sh, U) ∈ SS, σ, ν ∈ Subst, and e ∈ ℘_{f}(Eqs) be such that vars(σ) ⊆ U and ν is a relevant unifier of e. Then

α(σ, U) ⪯_{SS} (sh, U) ⟹ α(ν ∘ σ, U) ⪯_{SS} aunify((sh, U), e).

Theorem 2. Let (sh, U) ∈ SS and e ∈ ℘_{f}(Eqs). Then

aunify((sh, U), e) = aunify(aunify((sh, U), e), e).

Theorem 3. Let (sh, U) ∈ SS and e_{1}, e_{2} ∈ ℘_{f}(Eqs). Then

aunify(aunify((sh, U), e_{1}), e_{2}) = aunify(aunify((sh, U), e_{2}), e_{1}).

5 Discussion

The SS domain which was first defined by Langen [14] and published by Jacobs and Langen [8] is an important domain for sharing analysis. In this paper, we have provided a framework for analysing non-idempotent substitutions and presented results for soundness, idempotence and commutativity of aunify. In fact, most researchers concerned with analysing sharing and related properties using the SS domain, assume these properties hold. Why therefore are the results in this paper necessary? Let us consider each of the above properties one at a time.

5.1 Soundness

We have shown that, for any substitution σ over a set of variables U, the abstraction α(σ, U) = (sh, U) is unique (Lemma 3) and the aunify operation is sound (Theorem 1). Note that, in Theorem 1, there are no restrictions on σ; it can be non-idempotent, possibly including cyclic bindings (that is, bindings where the domain variable occurs in its co-domain). Thus this result is widely applicable.

Previous results on sharing have assumed that substitutions are idempotent. This is true if equality is syntactic identity and the implementation uses a unification algorithm based on that of Robinson [17] which includes the occur-check. With such algorithms, the resulting unifier is both unique and idempotent. Unfortunately, this is not what is implemented by most Prolog systems.

In particular, if the algorithm is as described in [11] and used in Prolog III [5], then the resulting unifier is in rational solved form. This algorithm does not generate idempotent or even variable-idempotent substitutions even when the occur-check would never have succeeded. However, it has been shown that the substitution obtained in this way uniquely defines a system of rational trees [5]. Thus our results show that its abstraction using α, as defined in this paper, is also unique and that aunify is sound.

Alternatively, if, as in most commercial Prolog systems, the unification algorithm is based on the Martelli-Montanari algorithm, but omits the occur check step, then the resulting substitution may not be idempotent. Consider the following example.

Suppose we are given as input the equation p(z, f(x, y)) = p(f(z, y), z) with an initial substitution that is empty. We apply the steps in Martelli-Montanari procedure but without the occur-check:

equations  substitution
1 p(z, f(x, y)) = p(f(z, y), z) ∅
2 z = f(z, y), f(x, y) = z  ∅
3 f(x, y) = f(z, y)  {z ↦ f(z, y)}
4 x = z, y = y  {z ↦ f(z, y)}
5 y = y  {z ↦ f(z, y), x ↦ z}
6 ∅  {z ↦ f(z, y), x ↦ z}

Note that we have used three kinds of steps here. In lines 1 and 3, neither argument of the selected equation is a variable. In this case, the outer nonvariable symbols (when, as in this example, they are the same) are removed and new equations are formed between the corresponding arguments. In lines 2 and 4, the selected equation has the form v = t, where v is a variable and t is not identical to v, then every occurrence of v is replaced by t in all the remaining equations and the range of the substitution. v ↦ t is then added to the substitution. In line 5, the identity is removed.

Let σ = {z ↦ f(z, y), x ↦ z}, be the computed substitution. Then, we have

vars(xσ) = vars(z) = {z},
vars(xσ^{2}) = vars(f(z, y)) = {y, z}.

Hence σ is not variable-idempotent.

We conjecture that the resulting substitution is still unique (up to variable renaming). In this case our results can be applied so that its abstraction using α, as defined in this paper, is also unique and aunify is sound.

5.2 Idempotence

Definition 8 defines aunify inductively over a set of equations, so that it is important for this definition that aunify is both idempotent and commutative.

The only previous result concerning the idempotence of aunify is given in thesis of Langen [14, Theorem 32]. However, the definition of aunify in [14] includes the renaming and projection operations and, in this case, only a weak form of idempotence holds. In fact, for the basic aunify operation as defined here and without projection and renaming, idempotence has never before been proven.

5.3 Commutativity

In the thesis of Langen the “proof” of commutativity of amguhas a number of omissions and errors [14, Lemma 30]. We highlight here, one error which we were unable to correct in the context of the given proof.

To make it easier to compare, we adapt our notation and, define amge only in the case that a is a variable:

amge(a, b, sh) =^{def} amgu(sh, a ↦ b).

To prove the lemma, it has to show that:

amge(a_{2}, b_{2} amge(a_{1}, b_{1}, sh)) = amge(a_{1}, b_{1}, amge(a_{2}, b_{2}, sh)).

holds when a_{1} and a_{2} are variables. This corresponds to “the second base case” of the proof. We use Langen’s terminology:

– A set of variables X is at a term t iff var(t) ∩ X ≠ ∅.

– A set of variables X is at i iff X is at a_{i} or b_{i}.

– A union X ∪_{i} Y is of Type i iff X is at a_{i} and Y is at b_{i}.

Let lhs =^{def} amge(a_{2}, b_{2}, amge(a_{1}, b_{1}, S)), and rhs =^{def} amge(a_{1}, b_{1}, amge(a_{2}, b_{2}, S)). Let also Z ∈ lhs and T =^{def} aunify(a_{1}, b_{1}, S). Consider the case when

Z = X ∪_{2} Y where X ∈ rel(a_{2}, T), Y ∈ rel(b_{2}, T),
X = U ∪_{1} V where U ∈ rel(a_{1}, sh), V ∈ rel(b_{1}, sh)

and U ∩ (vars(a_{2}) ∪ vars(b_{2})) = ∅ (that is, U is not at 2). Then the following quote [14, page 53, line 23] applies:

In this case (U ∪_{1} V)∪_{2} Y = U ∪_{1} (V ∪_{2} Y). By the inductive assumption V ∪_{2} Y is in the rhs and therefore so is Z.

We give a counter-example to the statement “V ∪_{2} Y is in the rhs”.

Suppose a_{1}, b_{1}, a_{2}, b_{2} are variables. We let each of a_{1}, b_{1}, a_{2}, b_{2} denote both the actual variable and the singleton set containing that variable. Suppose sh = {a_{1}, b_{1}a_{2}, b_{2}}. Then, from the definition of amge,

lhs = {a_{1}b_{1}a_{2}b_{2}},  rhs = {a_{1}b_{1}a_{2}b_{2}},  T = {a_{1}b_{1}a_{2}, b_{2}}.

Let Z = a_{1}b_{1}a_{2}b_{2}, X = a_{1}b_{1}a_{2}, Y = b_{2}, U = a_{1}, V = b_{1}a_{2}. All the above conditions. However V ∪_{2} Y = b_{1}a_{2}b_{2} and this is not in {a_{1}b_{1}a_{2}b_{2}}.

References

1. R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. In P. Van Hentenryck, editor, Static Analysis: Proceedings of the 4th International Symposium, volume 1302 of Lecture Notes in Computer Science, pages 53–67, Paris, France, 1997. Springer-Verlag, Berlin.

2. M. Bruynooghe and M. Codish. Freeness, sharing, linearity and correctness — All at once. In P. Cousot, M. Falaschi, G. Filé, and A. Rauzy, editors, Static Analysis, Proceedings of the Third International Workshop, volume 724 of Lecture Notes in Computer Science, pages 153–164, Padova, Italy, 1993. Springer-Verlag, Berlin. An extended version is available as Technical Report CW 179, Department of Computer Science, K.U. Leuven, September 1993.

3. K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Databases, pages 293–322, Toulouse, France, 1978. Plenum Press.

4. M. Codish, D. Dams, G. Filé, and M. Bruynooghe. Freeness analysis for logic programs-and correctness? In D. S. Warren, editor, Logic Programming: Proceedings of the Tenth International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 116–131, Budapest, Hungary, 1993. The MIT Press. An extended version is available as Technical Report CW 161, Department of Computer Science, K.U. Leuven, December 1992.

5. A. Colmerauer. Prolog and Infinite Trees. In K. L. Clark and S. Å. Tärnlund, editors, Logic Programming, APIC Studies in Data Processing, volume 16, pages 231–251. Academic Press, New York, 1982.

6. A. Colmerauer. Equations and inequations on finite and infinite trees. In Proceedings of the International Conference on Fifth Generation Computer Systems (FGCS’84), pages 85–99, Tokyo, Japan, 1984. ICOT.

7. P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. Technical Report 98.03, School of Computer Studies, University of Leeds, 1998.

8. D. Jacobs and A. Langen. Accurate and efficient approximation of variable aliasing in logic programs. In E. L. Lusk and R. A. Overbeek, editors, Logic Programming: Proceedings of the North American Conference, MIT Press Series in Logic Programming, pages 154–165, Cleveland, Ohio, USA, 1989. The MIT Press.

9. D. Jacobs and A. Langen. Static analysis of logic programs for independent AND parallelism. Journal of Logic Programming, 13(2&3):291–314, 1992.

10. J. Jaffar, J-L. Lassez, and M. J. Maher. Prolog-II as an instance of the logic programming scheme. In M. Wirsing, editor, Formal Descriptions of Programming Concepts III, pages 275–299. North Holland, 1987.

11. T. Keisu. Tree Constraints. PhD thesis, The Royal Institute of Technology, Stockholm, Sweden, May 1994. Also available in the SICS Dissertation Series: SICS/D– 16–SE.

12. A. King. A synergistic analysis for sharing and groundness which traces linearity. In D. Sannella, editor, Proceedings of the Fifth European Symposium on Programming, volume 788 of Lecture Notes in Computer Science, pages 363–378, Edinburgh, UK, 1994. Springer-Verlag, Berlin.

13. A. King and P. Soper. Depth-k sharing and freeness. In P. Van Hentenryck, editor, Logic Programming: Proceedings of the Eleventh International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 553–568, Santa Margherita Ligure, Italy, 1994. The MIT Press.

14. A. Langen. Static Analysis for Independent And-Parallelism in Logic Programs. PhD thesis, Computer Science Department, University of Southern California, 1990. Printed as Report TR 91-05.

15. M. J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 348–357, Edinburgh, Scotland, 1988. IEEE Computer Society.

16. K. Muthukumar and M. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming, 13(2&3):315– 347, 1992.

17. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.