arXiv:cs/0102030v1 [cs.PL] 27 Feb 2001

To appear on Theory and Practice of Logic Programming

1

Soundness, Idempotence and Commutativity
of Set-Sharing
PATRICIA M. HILL∗
School of Computer Studies, University of Leeds, Leeds, U.K.

(e-mail: hill@scs.leeds.ac.uk)
ROBERTO BAGNARA, ENEA ZAFFANELLA†
Department of Mathematics, University of Parma, Italy

(e-mail: {bagnara,zaffanella}@cs.unipr.it)

Abstract
It is important that practical data-flow analyzers 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 soundness of Sharing assume the occurs-check. This paper provides a
generalization of the abstraction function for Sharing that can be applied to any language,
with or without the occurs-check. Results for soundness, idempotence and commutativity
for abstract unification using this abstraction function are proven.

Keywords: Abstract Interpretation; Logic Programming; Occurs-Check; Rational
Trees; Set-Sharing.

1 Introduction
In abstract interpretation, the concrete semantics of a program is approximated
by an abstract semantics; that is, the concrete domain is replaced by an abstract
domain and each elementary operation on the concrete domain is replaced by a
corresponding abstract operation on the abstract domain. Assuming the global
abstract procedure mimics the concrete execution procedure, each basic operation
on the elements of the abstract domain must produce a safe approximation of the
corresponding operation on corresponding elements of the concrete domain. For
logic programming, the key elementary operation is unification that computes a
solution to a set of equations. This solution can be represented by means of a
∗ This work was partly supported by EPSRC under grant GR/M05645.
† The work of the second and third authors has been partly supported by MURST project “Certificazione automatica di programmi mediante interpretazione astratta.”

2

P. M. Hill, R. Bagnara and E. Zaffanella

mapping (called a substitution) from variables to first-order terms in the language.
For global soundness of the abstract semantics, there needs to be, therefore, a
corresponding abstract operation, aunify, that is sound with respect to unification.
For parallelization and several other program optimizations, it is important to
know before execution which variables may be bound to terms that share a common variable. Jacobs and Langen developed the abstract domain Sharing (Jacobs
and Langen 1989, Jacobs and Langen 1992) for representing and propagating the
sharing behavior of variables and this is now a standard choice for sharing analysis.
Subsequent research then concentrated mainly on extending the domain to incorporate additional properties such as linearity, freeness and depth-k abstractions
(Langen 1990, Bruynooghe and Codish 1993, Codish, Dams, Filé and Bruynooghe
1996, King 1994, King and Soper 1994, Muthukumar and Hermenegildo 1992) or in
reducing its complexity (Bagnara, Hill and Zaffanella 1997, Bagnara, Hill and Zaffanella 2001). Key properties such as commutativity and soundness of this domain
and its associated abstract operations such as abstract unification were normally
assumed to hold. One reason for this was that (Jacobs and Langen 1992) includes a
proof of the soundness and refers to the Ph.D. thesis of Langen (Langen 1990) for
the proofs of commutativity and idempotence.1 We discuss below why these results
are inadequate.

1.1 Soundness of aunify
An important step in standard unification algorithms based on that of Robinson (Robinson 1965) (such as the Martelli-Montanari algorithm (Martelli and Montanari 1982)) is the occurs-check, which avoids the generation of infinite (or cyclic)
data structures. With such algorithms, the resulting solution is both unique and
idempotent. However, in computational terms, the occurs-check is expensive and the
vast majority of Prolog implementations omit this test, although some Prolog implementations do offer unification with the occurs-check as a separate built-in predicate (in ISO Prolog (ISO/IEC 1995) the predicate is unify with occurs check/2).
In addition, if the unification algorithm is based on the Martelli-Montanari algorithm but without the occurs-check step, then the resulting solution may be nonidempotent. 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 the Martelli-Montanari

1

Even though the thesis of Langen has been published as a technical report of the University of
Southern California, an extensive survey of the literature on Sharing indicates that the thesis
has not been widely circulated even among researchers in the field. For instance, Langen is
rarely credited as being the first person to integrate Sharing with linearity information, despite
the fact that this is described in the thesis.

3

Soundness, Idempotence and Commutativity of Set-Sharing
procedure but without the occurs-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)

4

x = z, y = y

5

y=y

∅

z 7→ f (z, y)

z 7→ f (z, y)

6

∅



z→
7 f (z, y), x 7→ z

z→
7 f (z, y), x 7→ z

Then σ = z 7→ f (z, y), x 7→ z is the computed substitution; it is not idempotent
since, for example, xσ = z and xσσ = f (z, y).
Non-standard equality theories and unification procedures are also available and
used in many logic programming systems. In particular, there are theoretically coherent languages, such as Prolog III (Colmerauer 1982), that employ an equality
theory and unification algorithm based on a theory of rational trees (possibly infinite trees with a finite number of subtrees). As remarked in (Colmerauer 1982),
complete (i.e., always terminating) unification with the omission of the occurs-check
solves equations over rational trees. Complete unification is made available by several Prolog implementations. The substitutions computed by such systems are in
rational solved form and therefore not necessarily idempotent. As an example, the
substitution {x 7→ f (x)}, which is clearly non-idempotent, is in rational solved form
and could itself be computed by the above algorithms.
It is therefore important that theoretical work in data-flow analysis makes no
assumption that the computed solutions are idempotent. In spite of this, most theoretical work on data-flow analysis of logic programming and of Prolog assume the
occurs-check is performed, thus allowing idempotent substitutions only. In particular, (Jacobs and Langen 1992), (Langen 1990), and, more recently, (Cortesi and Filé
1999) make this assumption in their proofs of soundness. As a consequence, their results do not apply to the analysis of all Prolog programs. A recent exception to this
is (King 2000) where a soundness result is proved for a domain representing just the
pair-sharing and linearity information. In this work it is assumed that a separate
groundness analysis is performed and its results are used to recover from the precision losses incurred by the proposed domain. However, the problem of specifying a
sound and precise groundness analysis when dealing with possibly non-idempotent
substitutions is completely disregarded, so that the overall solution is incomplete.
Moreover, the proposed abstraction function is based on a limit operation that, in
the general case, is not finitely computable.
We have therefore addressed the problem of defining a sound and precise approximation of the sharing information contained in a substitution in rational solved
form.
In particular, we observed that the Sharing domain is concerned with the set
of variables occurring in a term, rather than with the term structure. We have

4

P. M. Hill, R. Bagnara and E. Zaffanella

therefore generalized the notion of idempotence to variable-idempotence. That is, if
σ is a variable-idempotent substitution and t is any term, then any variable which
is not in the domain of σ and occurs in tσσ also occurs in tσ. Clearly, as illustrated
by the above example, substitutions generated by unification algorithms without
the occurs-check may not even be variable-idempotent. To resolve this, we have
devised an algorithm that transforms any substitution in rational solved form to an
equivalent (with respect to any equality theory) variable-idempotent
substitution.

For instance, in the example, it would transform σ to z 7→ f (z, y), x 7→ f (z, y) .
By suitably exploiting the properties enjoyed by variable-idempotent substitutions, we show that, for the domain Sharing, the abstract unification algorithm
aunify is sound with respect to the actually implemented unification procedures
for all logic programming languages. Moreover, we define a new abstraction function mapping any set of substitutions in rational solved form into the corresponding
abstract descriptions so that there is no need for the analyser to compute the equivalent set of variable-idempotent substitutions. We note that this new abstraction
function is carefully chosen so as to avoid any precision loss due to the possible
non-idempotence of the substitution.
Note that both the notion of variable-idempotent substitution and the proven
results relating it to arbitrary substitutions in rational solved form do not depend
on the particular abstract domain considered. Indeed, we believe that this concept,
perhaps with minor adjustments, can be usefully applied to other abstract domains
when extending the soundness proofs devised for idempotent substitutions to the
more general case of substitutions in rational solved form.
1.2 Commutativity and Idempotence of aunify
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 unification. 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 also useful if the global
abstract procedure can proceed in a different order with respect to the concrete one
without affecting the accuracy of the analysis results. On the other hand, as sharing
is normally combined with linearity and freeness domains that are not idempotent
or commutative (Langen 1990, Bruynooghe and Codish 1993, King 1994), it may be
asked why these properties are still important for sharing analysis. In answer to this,
we observe that the order and multiplicity in which the bindings in a substitution
are analyzed affects the accuracy of the linearity and freeness information. It is
therefore a real advantage to be able to ignore these aspects as far as the sharing
domain is concerned. Specifically, the order in which the bindings are analyzed can
be chosen so as to improve the accuracy of linearity and freeness. We thus conclude
that it is extremely desirable that aunify is also commutative and idempotent.
We found that there was no satisfactory proof of commutativity. In addition, for
idempotence the only previous result was given in (Langen 1990, Theorem 32) of

Soundness, Idempotence and Commutativity of Set-Sharing

5

the thesis of Langen. However, his definition of abstract unification 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. We therefore
provide here the first published proofs of these properties.
In summary, this paper, which is an extended and improved version of (Hill, Bagnara and Zaffanella 1998), provides a generalization of the abstraction function for
Sharing that can be applied to any logic programming language dealing with syntactic term structures. The results for soundness, idempotence and commutativity
for abstract unification using this abstraction function are proved.
The paper is organised as follows. In the next section, the notation and definitions needed for equality and substitutions in the concrete domain are given.
In Section 3, we recall the definition of the domain Sharing and of the classical
abstraction function defined for idempotent substitutions. We also show why this
abstraction function cannot be applied, as is, to non-idempotent substitutions. In
Section 4, we introduce variable-idempotence and provide a transformation that
may be used to map any substitution in rational solved form to an equivalent,
variable-idempontent one. In Section 5, we define a new abstraction function relating the Sharing domain to the domain of arbitrary substitutions in rational solved
form. In Section 6, we recall the definition of the abstract unification for Sharing
and state our main results. Section 7 concludes. For the convenience of the reader,
throughout the paper all the proofs (apart from the simpler ones) of the stated
results are appended to the end of the corresponding section.

2 Equations and Substitutions
In this section we introduce the notation and some terminology concerning equality
and substitutions that will be used in the rest of the paper.

2.1 Notation
For a set 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
TVars denotes the set of first-order terms over Vars for some given set of function
symbols. It is assumed that there are at least two distinct function symbols, one
of which is a constant (i.e., of zero arity), in the given set. The set of variables
occurring in a syntactic object o is denoted by vars(o). To simplify the expressions
in the paper, any variable in a formula that is not in the scope of a quantifier is
assumed to be universally quantified. To prove the results in the paper, it is useful
to assume a total ordering, denoted with ‘≤’, on Vars.

6

P. M. Hill, R. Bagnara and E. Zaffanella
2.2 Substitutions

A substitution is a total function σ : Vars → TVars that is the identity almost
everywhere; in other words, the domain of σ,
def 
dom(σ) = x ∈ Vars σ(x) 6= x ,

is finite. Given a substitution σ : Vars → TVars we overload the symbol ‘σ’ so as
to denote also the function σ : TVars → TVars defined as follows, for each term
t ∈ TVars :


if t is a constant symbol;

t,
def
σ(t) = σ(t),
if t ∈ Vars;


f σ(t ), . . . , σ(t ), if t = f (t , . . . , t ).
1

n

1

n

If t ∈ TVars , we write tσ to denote σ(t) and t[x/s] to denote t{x 7→ s}.
If x ∈ Vars and s ∈ TVars \ {x}, then x 7→ s is called a binding. The set of all
bindings is denoted by Bind . Substitutions are syntactically denoted by the set of
their bindings, thus a substitution σ is identified with the (finite) set

x 7→ σ(x) x ∈ dom(σ) .

Thus, vars(σ) is the set of variables occurring in the bindings of σ and we also
define the set of parameter variables of a substitution σ as
def

param(σ) = vars(σ) \ dom(σ).
A substitution is said to be circular if, for n > 1, it has the form
{x1 7→ x2 , . . . , xn−1 7→ xn , xn 7→ x1 },
where x1 , . . . , xn are distinct variables. 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 RSubst. A substitution σ is idempotent if, for all t ∈ TVars , we have tσσ = tσ.
The set of all idempotent substitutions is denoted by ISubst and ISubst ⊂ RSubst.
Example 1
The following hold:

x 7→ y, y →
7 a ∈ RSubst \ ISubst,

x 7→ a, y →
7 a ∈ ISubst,




x 7→ y, y 7→ g(y) ∈ RSubst \ ISubst,

x 7→ y, y 7→ g(x) ∈ RSubst \ ISubst,

x 7→ y, y 7→ x ∈
/ RSubst,

x 7→ y, y 7→ x, z 7→ a ∈
/ RSubst.

We have assumed that there is a total ordering ‘≤’ for Vars. We say that σ ∈
RSubst is ordered (with respect to this ordering) if, for each binding (v 7→ w) ∈ σ
such that w ∈ param(σ), we have w < v.

Soundness, Idempotence and Commutativity of Set-Sharing

7

The composition of substitutions is defined in the usual way. Thus τ ◦ σ is the
substitution such that, for all terms t ∈ TVars ,

(τ ◦ σ)(t) = τ σ(t)
and has the formulation

τ ◦ σ = x 7→ xστ x ∈ dom(σ), x 6= xστ


∪ x 7→ xτ

x ∈ dom(τ ) \ dom(σ) .
(1)

As usual, σ 0 denotes the identity function (i.e., the empty substitution) and, when
i > 0, σ i denotes the substitution (σ ◦ σ i−1 ).
2.3 Equations
An equation is of the form s = t where s, t ∈ TVars . Eqs denotes the set of all
equations.
 A substitution σ may be regarded as a finite set of equations, that is, as
the set x = t (x 7→ t) ∈ σ . We say that a set of equations e is in rational solved
form if s 7→ t (s = t) ∈ e ∈ RSubst. In the rest of the paper, we will often
write a substitution σ ∈ RSubst to denote a set of equations in rational solved form
(and vice versa).
We assume that any equality theory T over TVars includes the congruence axioms
denoted by the following schemata:
s = s,

(2)

s = t ↔ t = s,

(3)

r = s ∧ s = t → r = t,

(4)

s1 = t1 ∧ · · · ∧ sn = tn → f (s1 , . . . , sn ) = f (t1 , . . . , tn ).

(5)

In logic programming and most implementations of Prolog it is usual to assume an
equality theory based on syntactic identity. This consists of the congruence axioms
together with the identity axioms denoted by the following schemata, where f and
g are distinct function symbols or n 6= m:
f (s1 , . . . , sn ) = f (t1 , . . . , tn ) → s1 = t1 ∧ · · · ∧ sn = tn ,

¬ f (s1 , . . . , sn ) = g(t1 , . . . , tm ) .

(6)

∀z ∈ Vars : ∀t ∈ (TVars \ Vars) : z ∈ vars(t) → ¬(z = t).

(8)

(7)

The axioms characterized by schemata (6) and (7) ensure the equality theory depends only on the syntax. The equality theory for a non-syntactic domain replaces
these axioms by ones that depend instead on the semantics of the domain and, in
particular, on the interpretation given to functor symbols.
The equality theory of Clark (Clark 1978) on which pure logic programming
is based, usually called the Herbrand equality theory, is given by the congruence
axioms, the identity axioms, and the axiom schema

Axioms characterized by the schema (8) are called the occurs-check axioms and are
an essential part of the standard unification procedure in SLD-resolution.

8

P. M. Hill, R. Bagnara and E. Zaffanella

An alternative approach used in some implementations of Prolog, does not require the occurs-check axioms. This approach is based on the theory of rational
trees (Colmerauer 1982, Colmerauer 1984). It assumes the congruence axioms and
the identity axioms together with a uniqueness axiom for each substitution in rational solved form. Informally speaking these state that, after assigning a ground
rational tree to each parameter variable, the substitution uniquely defines a ground
rational tree for each of its domain variables. Note that being in rational solved form
is a very weak property. Indeed, unification algorithms returning a set of equations
in rational solved form are allowed to be much more “lazy” than one would usually expect (e.g., see the first substitution in Example 1). We refer the interested
reader to (Jaffar, Lassez and Maher 1987, Keisu 1994, Maher 1988) for details on
the subject.
In the sequel we will use the expression “equality theory” to denote any consistent, decidable theory T satisfying the congruence axioms. We will also use the
expression “syntactic equality theory” to denote any equality theory T also satisfying the identity axioms.2 When the equality theory T is clear from the context,
it is convenient to adopt the notations σ =⇒ τ and σ ⇐⇒ τ , where σ, τ are sets
of equations, to denote T ⊢ ∀(σ → τ ) and T ⊢ ∀(σ ↔ τ ), respectively.
Given an equality theory T , and a set of equations in rational solved form σ, we
say that σ is satisfiable in T if T ⊢ ∀Vars \ dom(σ) : ∃ dom(σ) . σ. If T is a syntactic
equality theory that also includes the occurs-check axioms, and σ is satisfiable in
T , then we say that σ is Herbrand.
Given a satisfiable set of equations e ∈ ℘f (Eqs) in an equality theory T , then a
substitution σ ∈ RSubst is called a solution for e in T if σ is satisfiable in T and
T ⊢ ∀(σ → e). If vars(σ) ⊆ vars(e), then σ is said to be a relevant solution for e.
In addition, σ is a most general solution for e in T if T ⊢ ∀(σ ↔ e). In this paper,
a most general solution is always a relevant solution of e.
Observe that, given an equality theory T , a set of equations in rational solved
form may not be satisfiable in T . For example, ∃x : x = f (x) is false in the Clark
equality theory.
Lemma 1
Suppose T is an equality theory, σ ∈ RSubst is satisfiable in T , x ∈ Vars \ dom(σ),
def

and a ∈ T∅ . Then, σ ′ = σ ∪ {x 7→ a} ∈ RSubst and σ ′ is satisfiable in T .
Proof
As x ∈
/ dom(σ) and σ ∈ RSubst and a ∈ T∅ , it follows that σ ′ = σ ∪ {x 7→ a} ∈
RSubst.
Since σ is satisfiable in T ,
T ⊢ ∀Vars \ dom(σ) : ∃ dom(σ) . σ.

2

Note that, as a consequence of axiom (7) and the assumption that there are at least two distinct
function symbols in the language, one of which is a constant, there exist two terms a1 , a2 ∈ T∅
such that, for any syntactic equality theory T , we have T ⊢ a1 6= a2 .

Soundness, Idempotence and Commutativity of Set-Sharing

9

Moreover, by the congruence axiom (2),
T ⊢ ∀Vars \ {x} : ∃x . {x = a}.
Hence,


T ⊢ ∀Vars \ dom(σ) ∪ {x} : ∃ dom(σ) ∪ {x} . σ ∪ {x = a}.

Thus σ ′ = σ ∪ {x 7→ a} is satisfiable in T .

Syntactically we have shown that any substitution in RSubst may be regarded
as a set of equations in rational solved form and vice versa. The next lemma shows
the semantic relationship between them.
Lemma 2
If T is an equality theory and σ ∈ RSubst, then, for each t ∈ TVars ,

T ⊢ ∀ σ → (t = tσ) .

Proof
We assume the congruence axioms hold and prove that, for any t ∈ TVars , we have
σ =⇒ {t = tσ}. The proof is by induction on the depth of t.
Suppose, first that the depth of t is one. If t is a variable not in dom(σ) or a
constant, then tσ = t and the result follows from axiom (2). If t ∈ dom(σ), then,
for some r ∈ TVars , (t 7→ r) ∈ σ. Thus σ =⇒ {t = tσ}.
If the depth of t is greater than one, then t has the form f (s1 , . . . , sn ) where
s1 , . . . , sn ∈ TVars have depth less than the depth of t. By the inductive hypothesis,
for each i = 1, . . . , n, we have σ =⇒ {si = si σ}. Therefore, applying axiom (5),
we have σ =⇒ {t = tσ}.
As is common in papers involving equality, we overload the symbol ‘=’ and use
it to denote both equality and to represent syntactic identity. The context makes
it clear what is intended.

3 The Set-Sharing Domain
In this section, we first recall the definition of the Sharing domain and present the
(classical) abstraction function used for dealing with idempotent substitutions. We
will then give evidence for the problems arising when applying this abstraction
function to the more general case of substitutions in rational solved form.

3.1 The Sharing Domain
The Sharing domain is due to Jacobs and Langen (Jacobs and Langen 1989). However, we use the definition as presented in (Bagnara et al. 1997) where the set of
variables of interest is given explicitly.

10

P. M. Hill, R. Bagnara and E. Zaffanella

Definition 1
(The set-sharing lattice.) Let
def

SG = ℘f (Vars) \ {∅}
and let
def

SH = ℘(SG).
The set-sharing lattice is given by the set
def

SS =



(sh, U ) sh ∈ SH , U ∈ ℘f (Vars), ∀S ∈ sh : S ⊆ U

∪ {⊥, ⊤},

which is ordered by ‘SS ’ defined as follows, for each d, (sh 1 , U1 ), (sh 2 , U2 ) ∈ SS :
⊥ SS d,
d SS ⊤,
(sh 1 , U1 ) SS (sh 2 , U2 )

⇐⇒

(U1 = U2 ) ∧ (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.3 The lub operator over SS will be
denoted by ‘⊔’.
3.2 The Classical Abstraction Function for ISubst
An element sh of SH encodes the sharing information contained in an idempotent
substitution σ. Namely, two variables x and y must be in the same set in sh if some
variable occurs in both xσ and yσ.
Definition 2
(Classical sg and abstraction functions.) sg : ISubst × Vars → ℘f (Vars), called
sharing group function, is defined, for each σ ∈ ISubst and each v ∈ Vars, by
def 
sg(σ, v) = y ∈ Vars v ∈ vars(yσ) .

The concrete domain ℘(ISubst) is related to SS by means of the abstraction function
αI : ℘(ISubst) × ℘f (Vars) → SS . For each Σ ∈ ℘(ISubst) and each U ∈ ℘f (Vars),
G
def
αI (Σ, U ) =
αI (σ, U ),
σ∈Σ

where αI : ISubst × ℘f (Vars) → SS is defined, for each substitution σ ∈ ISubst and
each U ∈ ℘f (Vars), by


def 
αI (σ, U ) =
sg(σ, v) ∩ U v ∈ Vars \ {∅}, U .
3

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

Soundness, Idempotence and Commutativity of Set-Sharing

11

The sharing group function sg was first defined by Jacobs and Langen (Jacobs and
Langen 1989) and used in their definition of a concretisation function for SH . The
function αI corresponds closely to the abstract counterpart of this concretisation
function, but explicitly includes the set of variables of interest as a separate argument. It is identical to the abstraction function for Sharing defined by Cortesi and
Filé (Cortesi and Filé 1999).
In order to provide an intuitive reading of the sharing information encoded into
an abstract element, we should stress that the analysis aims at capturing possible sharing. The corresponding definite information (e.g., definite groundness or
independence) can be extracted by observing which sharing groups are not in the
abstract element. As an example, if we observe that there is no sharing group containing a particular variable of U , then we can safely conclude that this variable is
definitely ground (namely, it is bound to a term containing no variables). Similarly,
if we observe that two variables never occur together in the same sharing group,
then we can safely conclude that they are independent (namely, they are bound
to terms that do not share a common variable). For a more detailed description of
the information contained in an element of SS , we refer the interested reader to
(Bagnara et al. 1997, Bagnara et al. 2001).

Example 2
Assume U = {x1 , x2 , x3 , x4 } and let

σ = x1 7→ f (x2 , x3 ), x4 7→ a ,
so that its abstraction is given by
αI (σ, U ) =




{x1 , x2 }, {x1 , x3 } , U .

From this abstraction we can safely conclude that variable x4 is ground and variables
x2 and x3 are independent.

3.3 Towards an Abstraction Function for RSubst
To help motivate the approach we have taken in adapting the classical abstraction
function to non-idempotent substitutions, we now explain some of the problems
that arise if we apply αI , as it is defined on ISubst, to the non-idempotent substitutions in RSubst. Note that these problems are only partially due to allowing
for non-Herbrand substitutions (that is substitutions that are not satisfiable in a
syntactic equality theory containing the occurs-check axioms). They are also due to
the presence of non-idempotent but Herbrand substitutions that may arise because
of the potential “laziness” of unification procedures based on the rational solved
form.
We use the following substitutions to illustrate the problems, where it is assumed

12

P. M. Hill, R. Bagnara and E. Zaffanella

that the set of variables of interest is U = {x1 , x2 , x3 , x4 }. Let

σ1 = x1 7→ f (x1 ) ,

σ2 = x3 7→ x4 ,

σ3 = x1 7→ x2 , x2 7→ x3 , x3 7→ x4 ,

σ4 = x1 7→ x4 , x2 7→ x4 , x3 7→ x4

so that we have



{x1 }, {x2 }, {x3 }, {x4 } , U ,


αI (σ2 , U ) = αI (σ3 , U ) = {x1 }, {x2 }, {x3 , x4 } , U ,


αI (σ4 , U ) = {x1 , x2 , x3 , x4 } , U .
αI (∅, U ) = αI (σ1 , U ) =

The first problem is that the concrete equivalence classes induced by the classical
abstraction function on RSubst are much coarser than one would expect and hence
we have an unwanted loss of precision. For example, in all the sets of rational
trees that are solutions for σ1 , the variable x1 is ground. However, the computed
abstract element fails to distinguish this situation from that resulting from the
empty substitution, where all the variables are free and un-aliased. Similarly, we
have the same abstract element for both σ2 and σ3 although, x1 , x2 and x3 are
independent in σ2 only.
The second problem is quite the opposite from the first in that the abstraction
function distinguishes between substitutions that are equivalent (with respect to
any equality theory). For example, σ3 and σ4 are equivalent although the abstract
elements are distinct. Note that the two problems described here are completely
orthogonal although they can interact and produce more complex situations.

4 Variable-Idempotence
In this section we define a new class of substitutions based on the concept of
variable-idempotence. Variable-idempotent substitutions are then related to substitutions in rational solved form by means of an equivalence preserving rewriting
relation.

4.1 Variable-Idempotent Substitutions
Recall that, for substitutions, the definition of idempotence requires that repeated
applications of a substitution do not change the syntactic structure of a term.
However, a sharing abstraction such as αI is only interested in the variables and
not in the structure that contains them. Thus, an obvious way to relax the definition
of idempotence to allow for a non-Herbrand substitution is to ignore the structure
and just require that its repeated application leaves the set of free variables in a
term invariant.

Soundness, Idempotence and Commutativity of Set-Sharing

13

Definition 3
(Variable-Idempotence.) A substitution σ is said to be variable-idempotent if
σ ∈ RSubst and, for each t ∈ TVars ,
vars(tσσ) \ dom(σ) = vars(tσ) \ dom(σ).
The set of all variable-idempotent substitutions is denoted by VSubst.
Note that, as the condition vars(tσ) \ dom(σ) ⊆ vars(tσσ) is trivial and holds for
all substitutions, we have σ ∈ VSubst if and only if σ ∈ RSubst and
vars(tσσ) \ dom(σ) ⊆ vars(tσ).

(9)

Also note that any idempotent substitution is also variable-idempotent, so that
ISubst ⊂ VSubst ⊂ RSubst.
Example 3
Consider the following substitutions which are all in RSubst.

σ1 = x 7→ f (x)
∈ VSubst \ ISubst,

σ2 = x 7→ f (y), y 7→ z
∈
/ VSubst,

σ3 = x 7→ f (z), y 7→ z
∈ ISubst,

σ4 = x 7→ z, y 7→ f (x, y) ∈
/ VSubst,

σ5 = x 7→ z, y 7→ f (z, y) ∈ VSubst \ ISubst.

Note that σ2 is equivalent (with respect to any equality theory) to the idempotent
substitution σ3 ; and σ4 is equivalent (with respect to any equality theory) to the
substitution σ5 which is variable-idempotent but not idempotent.
The next result provides an alternative characterization of variable-idempotence.

Lemma 3
Suppose that σ ∈ RSubst. Then σ ∈ VSubst if and only if, for all (x 7→ r) ∈ σ,
vars(rσ) \ dom(σ) = vars(r) \ dom(σ).
Proof
Suppose first that σ ∈ VSubst and that (x 7→ r) ∈ σ. Then
vars(xσσ) \ dom(σ) = vars(xσ) \ dom(σ)
and hence, vars(rσ) \ dom(σ) = vars(r) \ dom(σ).
Next, suppose that for all (x 7→ r) ∈ σ, vars(rσ) \ dom(σ) = vars(r) \ dom(σ).
Let t ∈ TVars . We will show that vars(tσσ) \ dom(σ) = vars(tσ) \ dom(σ) by
induction on the depth of t. If t is a constant or t ∈ Vars \ dom(σ), then the
result follows from the fact that tσ = t. If t ∈ dom(σ), then the result follows
from the hypothesis. Finally, if t = f (t1 , . . . , tn ), then, by the inductive hypothesis,
vars(ti σσ) \ dom(σ) = vars(ti σ) \ dom(σ) for i = 1, . . . , n. Therefore we have
vars(tσσ) \ dom(σ) = vars(tσ) \ dom(σ). Thus, by Definition (3), as σ ∈ RSubst,
σ ∈ VSubst.

14

P. M. Hill, R. Bagnara and E. Zaffanella

Note that, as a consequence of Lemma 3, any substitution consisting of a single
binding is variable-idempotent. Note though that we cannot assume that every
subset of a variable-idempotent substitution is variable-idempotent.
Example 4
Let
σ1 = {x1 7→ x2 , x2 7→ g(x3 ), x3 7→ f (x3 )},
σ2 = {x3 7→ f (x3 )},
σ3 = σ1 \ σ2 = {x1 7→ x2 , x2 7→ g(x3 )}.
It can be observed that σ1 , σ2 ∈ VSubst. Also note that σ3 ∈
/ VSubst, because we
have x3 ∈ vars(x1 σ3 σ3 ) \ dom(σ3 ) but x3 ∈
/ vars(x1 σ3 ) \ dom(σ3 ).
On the other hand, a variable-idempotent substitution does enjoy the following
useful property with respect to its subsets.
Lemma 4
If σ ∈ VSubst and t ∈ TVars , then, for all σ ′ ⊆ σ,
vars(tσσ ′ ) \ dom(σ) = vars(tσ) \ dom(σ).
Proof
Observe that, since σ ′ ⊆ σ, the relation vars(tσ) \ dom(σ) ⊆ vars(tσσ ′ ) is trivial.
To prove the opposite relation, suppose that y ∈ vars(tσσ ′ ) \ dom(σ). Then there
exists x ∈ vars(tσ) such that y ∈ vars(xσ ′ ). Now, if x ∈
/ dom(σ ′ ), then x = y
′
and y ∈ vars(tσ). On the other hand, if x ∈ dom(σ ), then xσ ′ = xσ so that
y ∈ vars(tσσ) \ dom(σ) and hence, as σ ∈ VSubst, y ∈ vars(tσ).
We note that this result depends on the definition of variable-idempotence ignoring
the domain elements of the substitution.
Example 5
Let

Then σ ∈ VSubst but


σ = x 7→ f (x, y), y 7→ a .
vars(xσ) = {x, y},
vars(xσσ) = {x, y},

vars xσ{y 7→ a} = {x}.

We now state two technical results that will be needed later in the paper. Note
that, when proving these results at the end of this section, we require that the equality theory also satisfies the identity axioms. They show that equivalent, ordered,
variable-idempotent substitutions have the same domain and bind the domain variables to terms with the same set of parameter variables.
Lemma 5
Suppose that T is a syntactic equality theory, τ, σ ∈ VSubst are ordered and satisfiable in T and T ⊢ ∀(τ → σ). Then dom(σ) ⊆ dom(τ ).

Soundness, Idempotence and Commutativity of Set-Sharing

15

Lemma 6
Suppose that T is a syntactic equality theory, τ, σ ∈ VSubst are satisfiable in T and

T ⊢ ∀(τ → σ). In addition, suppose s, t ∈ TVars are such that T ⊢ ∀ τ → (s = t) .
Then, if v ∈ vars(s) \ dom(τ ), there exists a variable z ∈ vars(tσ) \ dom(σ) such
that v ∈ vars(zτ ).
4.2 S-transformations
A useful property of variable-idempotent substitutions is that any substitution can
be transformed to an equivalent (with respect to any equality theory) variableidempotent one.
Definition 4
S

(S-transformation.) The relation 7−→ ⊆ RSubst ×RSubst, called S-step, is defined
by
(x 7→ t) ∈ σ

(y 7→ s) ∈ σ
x 6= y
.

σ−
7 → σ \ {y 7→ s} ∪ {y 7→ s[x/t]}
S

S

S

If we have a finite sequence of S-steps σ1 7−→ · · · 7−→ σn mapping σ1 to σn , then
S
we write σ1 7−→∗ σn and say that σ1 can be rewritten, by S-transformation, to σn .
Example 6
Let

σ0 = x1 7→ f (x2 ), x2 7→ g(x3 , x4 ), x3 7→ x1 .

Observe that σ0 is not variable-idempotent since vars(x1 σ0 ) \ {x1 , x2 , x3 } = ∅ but
vars(x1 σ0 σ0 ) \ {x1 , x2 , x3 } = {x4 }. By considering all the bindings of the substitution, one at a time, and applying the corresponding S-step to all the other bindings,
we produce a new substitution σ3 .

σ0 = x1 7→ f (x2 ), x2 7→ g(x3 , x4 ), x3 7→ x1

σ1 = x1 7→ f (x2 ), x2 7→ g(x3 , x4 ), x3 7→ f (x2 ) ,

σ2 = x1 7→ f (g(x3 , x4 )), x2 7→ g(x3 , x4 ), x3 7→ f (g(x3 , x4 )) ,

σ3 = x1 7→ f (g(f (g(x3 , x4 )), x4 )),
x2 7→ g(f (g(x3 , x4 )), x4 ), x3 7→ f (g(x3 , x4 )) .

Then
S

S

S

σ0 7−→∗ σ1 7−→∗ σ2 7−→∗ σ3 .
Note that σ0 ⇐⇒ σ3 and, for any τ ⊆ σ3 , the substitution τ is variable-idempotent.
In particular, σ3 is variable-idempotent.
The next two theorems, which are proved at the end of this section, show that
we need only consider variable-idempotent substitutions.

16

P. M. Hill, R. Bagnara and E. Zaffanella

Theorem 1
S
Suppose σ ∈ RSubst and σ 7−→∗ σ ′ . Then σ ′ ∈ RSubst, dom(σ) = dom(σ ′ ),
vars(σ) = vars(σ ′ ) and, if T is any equality theory, then T ⊢ ∀(σ ↔ σ ′ ).
Theorem 2
S
Suppose σ ∈ RSubst. Then there exists σ ′ ∈ VSubst such that σ 7−→∗ σ ′ and, for
′
all τ ⊆ σ , τ ∈ VSubst.
As a consequence of Theorem 2, we can transform any substitution in rational solved
form to a substitution for which it and all its subsets are variable-idempotent. Thus,
substitutions such as σ1 in Example 4 can be disregarded. The proof of this theorem
formalizes the rewriting process informally described in Example 6.
The following result concerning composition of substitutions will be needed later.
Lemma 7
Let τ, σ ∈ VSubst, where dom(σ) ∩ vars(τ ) = ∅. Then τ ◦ σ has the following
properties.

1. T ⊢ ∀ (τ ◦ σ) ↔ (τ ∪ σ) , for any equality theory T ;
2. dom(τ ◦ σ) = dom(τ ∪ σ);
3. τ ◦ σ ∈ VSubst.
4.3 The Abstraction Function for VSubst
With these results, it can be seen that we need to consider variable-idempotent
substitutions only. Moreover, in this case, one of the causes of the problems outlined in Section 3.3, due to the possible “laziness” of the unification algorithm, is no
longer present. As a consequence, it is now sufficient to address the potential loss
in precision due to the non-Herbrand substitutions. The simple solution is to define
a new abstraction function for VSubst which is the same as that in Definition 2
but where any sharing group generated by a variable in the domain of the substitution is disregarded. This new abstraction function works for variable-idempotent
substitutions and no longer suffers the drawbacks outlined in Section 3.3.
Therefore, at least from a theoretical point of view, the problem of defining a
sound and precise abstraction function for arbitrary substitutions in rational solved
form would have been solved. Given a substitution in RSubst, we would proceed in
two steps: we first transform it to an equivalent substitution in VSubst and then
compute the corresponding description by using the modified abstraction function.
However, from a practical point of view, we need to define an abstraction function
that directly computes the description of a substitution in RSubst in a single step,
thus avoiding the expensive computation of the intermediate variable-idempotent
substitution. We present such an abstraction function in Section 5.
4.4 Proofs of Lemmas 5, 6 and 7 and Theorems 1 and 2
To prove Lemmas 5 and 6, it is useful to first establish the following two properties
of variable-idempotent substitutions.

Soundness, Idempotence and Commutativity of Set-Sharing

17

Lemma 8
Suppose that σ ∈ VSubst, r ∈ TVars and, for all i ≥ 0, rσ i ∈ Vars. Then we have
rσ ∈ Vars \ dom(σ).

Proof
As σ has no circular subset and dom(σ) is finite, there exists a j ≥ 1 such that
rσ j = rσ j+1 and hence, rσ j ∈ Vars \ dom(σ). As σ is variable-idempotent, we have
{rσ j } = vars(rσ j ) \ dom(σ)
= vars(rσ) \ dom(σ)
= {rσ} \ dom(σ).
Hence rσ ∈ Vars \ dom(σ).

Lemma 9
Suppose that σ ∈ VSubst and v, r ∈ TVars , where
 v ∈ Vars \ dom(σ) and, for any
syntactic equality theory T , T ⊢ ∀ σ → {v = r} . Then v = rσ.
Proof
We assume that the congruence and identity axioms hold. Let a1 , a2 ∈ T∅ have
distinct outer-most symbols so that, by the identity axioms, T ⊢ a1 6= a2 . By
Lemma 8, either rσ ∈ Vars \ dom(σ) or, for some j ≥ 0, rσ j ∈
/ Vars. We consider
each case separately.
If, for some j ≥ 0, rσ j ∈
/ Vars, then, as a1 and a2 have distinct outer-most
symbols, there exists an i ∈ {1, 2} such that ai and rσ j have distinct outer-most
symbols. Thus, by the identity axioms, ai 6= rσ j . Let σ ′ = σ ∪ {v = ai }. It follows from Lemma 1 that, as v ∈
/ dom(σ) and σ is satisfiable, σ ′ ∈ RSubst and is
satisfiable. By Lemma 2 and the congruence axioms, σ =⇒ {v = rσ j }. However,
σ ′ =⇒ σ, so that σ ′ =⇒ {v = rσ j , v = ai }. Thus, by the congruence axioms, we
have σ ′ =⇒ {ai = rσ j }, which is a contradiction.
Suppose then that rσ ∈ Vars \ dom(σ). If v 6= rσ, then it follows from Lemma 1
that σ ′ = σ ∪ {v = a1 , rσ = a2 } ∈ RSubst and, as σ is satisfiable, σ ′ is satisfiable.
By Lemma 2 and the congruence axioms, σ =⇒ {v = rσ}. However, σ ′ =⇒ σ, so
that σ ′ =⇒ {v = rσ, v = a1 , rσ = a2 }. Thus, by the congruence axioms, we have
σ ′ =⇒ {a1 = a2 }, which is a contradiction. Hence v = rσ as required.

18

P. M. Hill, R. Bagnara and E. Zaffanella

Proof of Lemma 5.
We assume that the congruence and identity axioms hold. To prove the result, we
suppose that there exists v ∈ dom(σ) \ dom(τ ) and derive a contradiction.
By hypothesis, τ =⇒ σ. Thus, using Lemma 2 and the congruence axioms, we
have, for any i ≥ 0, τ =⇒ {v = vσ i }. By Lemma 9, for all i ≥ 0, v = vσ i τ so that
vσ i ∈ Vars. By Lemma 8, vσ ∈
/ dom(σ), so that, as σ is ordered and v ∈ dom(σ),
vσ < v. In particular, vσ 6= v, so that as vστ = v and τ is ordered, we would have
v < vσ, which is a contradiction.
Proof of Lemma 6.
We assume that the congruence and identity axioms hold. Note that, by the hypothesis, τ =⇒ σ and τ =⇒ {s = t} so that, using Lemma 2 and the congruence
axioms, we have τ =⇒ {s = tσ j } and τ =⇒ {tστ k = s}, for all j, k ≥ 0.
Let v ∈ vars(s) \ dom(τ ). We prove, by induction on the depth d of s, that there
exists z ∈ vars(tσ) \ dom(σ) such that v ∈ vars(zτ ). The base case is when d = 1
so that s = v. Now, for each j ≥ 0, τ =⇒ {v = tσ j } and hence, by Lemma 9 (as
v∈
/ dom(τ )), v = tσ j τ . As a consequence, tσ j ∈ Vars for all j ≥ 0 and v = tστ . By
Lemma 8, tσ ∈ Vars \ dom(σ). Thus, we define z = tσ.
For the inductive step, we assume that d > 1 so that, for some n ≥ 1, we have
s = f (s1 , . . . , sn ) and, for some i ∈ {1, . . . , n}, v ∈ vars(si ) and si has depth
d − 1. By Lemma 8, either tσ ∈ Vars \ dom(σ) or there exists a j ≥ 0 such that
tσ j ∈
/ Vars.
First, suppose that tσ ∈ Vars \ dom(σ). Now, τ =⇒ {tστ = s} so that, as
sτ ∈
/ Vars, by Lemma 9, we have tστ ∈
/ Vars \ dom(τ ). Thus, by Lemma 8, there
exists k > 1 such that tστ k ∈
/ Vars. Then, using the identity axioms, we have
tστ k = f (r1 , . . . , rn ) and τ =⇒ {si = ri }. By the inductive hypothesis (letting σ
be the empty substitution), we have v ∈ vars(ri τ ). However, vars(ri ) ⊆ vars(tστ k )
so that v ∈ vars(tστ k+1 ). As τ ∈ VSubst and v ∈
/ dom(τ ), v ∈ vars(tστ ). Thus, in
this case, let z = tσ.
Secondly, suppose that there exists a j ≥ 0 such that tσ j ∈
/ Vars. Then, as
τ =⇒ {s = tσ j }, it follows from the identity axioms that tσ j = f (t1 , . . . , tn ) and
τ =⇒ {si = ti }. By the inductive hypothesis, there exists z ∈ vars(ti σ) \ dom(σ)
such that v ∈ vars(zτ ). However, vars(ti σ) ⊆ vars(tσ j+1 ) so that we must have
z ∈ vars(tσ j+1 ) \ dom(σ). As σ ∈ VSubst, z ∈ vars(tσ) \ dom(σ) as required.
To prove Theorem 1, we need to show that the result holds for a single S-step.
Lemma 10
S
Let T be an equality theory and suppose that σ ∈ RSubst and σ 7−→ σ ′ . Then
σ ′ ∈ RSubst, dom(σ) = dom(σ ′ ), vars(σ) = vars(σ ′ ), and T ⊢ ∀(σ ↔ σ ′ ).
Proof
S
Since σ 7−→ σ ′ , there exists
 x,
 y ∈ dom(σ) with x 6= y such that (x′ 7→ t), (y 7→ s) ∈ σ
′
and σ = σ \ {y 7→ s} ∪ y 7→ s[x/t] . If x ∈
/ vars(s), σ = σ and the result is
trivial. Suppose now that x ∈ vars(s). We define
def

σ0 = σ \ {x = t, y = s}.

Soundness, Idempotence and Commutativity of Set-Sharing

19

Hence, as it is assumed that x 6= y,
σ = σ0 ∪ {x 7→ t, y 7→ s},
′

σ = σ0 ∪ {x 7→ t, y 7→ s[x/t]}.

(10)
(11)

We first show that σ ′ ∈ RSubst and dom(σ) = dom(σ ′ ). If s ∈
/ Vars, then
s[x/t] ∈
/ Vars so that dom(σ) = dom(σ ′ ). Also, as σ has no circular subset, σ ′ has
no circular subset and σ ′ ∈ RSubst. If s ∈ Vars, then s = x and s[x/t] = t. Thus, as
σ = σ0 ∪ {x 7→ t, y 7→ x} has no circular subset, t 6= y so that dom(σ) = dom(σ ′ ).
Moreover, neither σ0 ∪ {x 7→ t} nor σ0 ∪ {y 7→ t} have circular subsets. Hence σ ′
has no circular subset. Thus σ ′ ∈ RSubst.
Now, since


vars(s) ∪ vars(t) \ dom(σ) = vars s[x/t] ∪ vars(t) \ dom(σ),

it follows that vars(σ) = vars(σ ′ ).
Therefore, it remains to show that, for any equality theory T , T ⊢ ∀(σ ↔ σ ′ ). To
do this, we assume that the congruence axioms hold, and show that σ ⇐⇒ σ ′ . By
Lemma 2, we have
{x = t} =⇒ {s = s[x/t]}.
Thus, using the congruence axiom (4), we have

{x = t, y = s} =⇒ x = t, y = s, s = s[x/t]

=⇒ x = t, y = s[x/t] .

Similarly, using congruence axioms (3) and (4), we have


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

Thus
{x = t, y = s} ⇐⇒



x = t, y = s[x/t] .

It therefore follows from (10) and (11) that σ ⇐⇒ σ ′ .
The
 condition x 6= y in the
 proof of Lemma 10 is necessary. For example, suppose
σ = x 7→ f (x) and σ ′ = x 7→ f (f (x)) . Then we do not have σ ′ =⇒ σ. Note
however that this implication will hold as soon as we enrich the equality theory T
with either the occurs-check axioms or the uniqueness axioms of the rational trees’
theory.
Proof of Theorem 1.
The proof is by induction on the length of the sequence of S-steps transforming σ
to σ ′ . The base case is the empty sequence. For the inductive step, the sequence
S
S
S
has length n > 0 and there exists σ1 such that σ 7−→ σ1 7−→∗ σ ′ and σ1 7−→∗ σ ′ has
length n − 1. By Lemma 10, σ1 ∈ RSubst, dom(σ) = dom(σ1 ), vars(σ) = vars(σ1 )
and T ⊢ ∀(σ ↔ σ1 ). By the inductive hypothesis, σ ′ ∈ RSubst, dom(σ1 ) = dom(σ ′ ),

20

P. M. Hill, R. Bagnara and E. Zaffanella

vars(σ1 ) = vars(σ ′ ) and T ⊢ ∀(σ1 ↔ σ ′ ). Hence we have dom(σ) = dom(σ ′ ),
vars(σ) = vars(σ ′ ), and T ⊢ ∀(σ ↔ σ ′ ).
Proof of Theorem 2.
To prove the theorem, we construct an S-transformation and show that the resulting
substitution has the required properties.
Suppose that {x1 , . . . , xn } = dom(σ), σ0 = σ and, for each j = 0, . . . , n,
σj = {x1 7→ t1,j , . . . , xn 7→ tn,j },
where, if j > 0, tj,j = tj,j−1 and, for each i = 1, . . . , n with i 6= j, we have
ti,j = ti,j−1 [xj /tj,j ].
It follows from the definition of σj that, for j = 1, . . . , n , σj can be obtained
from σj−1 by two sequences of S-steps of lengths j − 1 and n − j + 1:
S

S

S

S

j−1
j
n
0
= σj ,
7−→ · · · 7−→ σj−1
7−→ · · · 7−→ σj−1
= σj−1
σj−1 = σj−1

where, for i = 1, . . . , n with i 6= j,
 
i−1
i
σj−1
= σj−1
\ {xi 7→ ti,j−1 } ∪ xi 7→ ti,j−1 [xj /tj,j ]

= {x1 7→ t1,j , . . . , xi 7→ ti,j , xi+1 7→ ti+1,j−1 , . . . , xn 7→ tn,j−1 }.

Hence, by Theorem 1, σ1 , . . . , σn ∈ RSubst.
We next show, by induction on j, with 0 ≤ j ≤ n, that, for
 each i = 1, . . . , n
and each h = 1, . . . , j, we have vars(ti,j ) = vars ti,j [xh /th,j ] .
For the base case when j = 0 there is nothing to prove. Suppose, therefore, that
1 ≤ j ≤ n and that, for each i = 1, . . . , n and h = 1, . . . , j − 1,

vars(ti,j−1 ) = vars ti,j−1 [xh /th,j−1 ] .
Now by the definition of tk,j where 1 ≤ k ≤ n, k 6= j, we have

vars(tk,j ) = vars tk,j−1 [xj /tj,j ] .

(12)

Also, since a substitution consisting of a single binding is variable-idempotent,
vars(tj,j ) = vars tj,j [xj /tj,j ]



so that, as tj,j = tj,j−1 ,

vars(tj,j ) = vars tj,j−1 [xj /tj,j ] .

(13)

Thus, by (12) and (13), for all k such that 1 ≤ k ≤ n, we have

vars(tk,j ) = vars tk,j−1 [xj /tj,j ] .

(14)

Therefore, for each i = 1, . . . , n and h = 1, . . . , j, using (14) and the inductive

Soundness, Idempotence and Commutativity of Set-Sharing

21

hypothesis, we have




vars ti,j [xh /th,j ] = vars ti,j−1 [xj /tj,j ] xh /th,j−1 [xj /tj,j ]

= vars ti,j−1 [xh /th,j−1 ][xj /tj,j ]

= vars ti,j−1 [xj /tj,j ]
= vars(ti,j ).

Letting j = n we obtain, for each i, h = 1, . . . , n,

vars ti,n [xh /th,n ] = vars(ti,n ).
Therefore, for all τ ⊆ σn and each i = 1, . . . , n,
vars(ti,n τ ) = vars(ti,n ).
Thus, by Lemma 3, for all τ ⊆ σn , τ ∈ VSubst. The result follows by taking σ ′ = σn .

Proof of Lemma 7.
Since τ , σ ∈ VSubst and dom(σ) ∩ vars(τ ) = ∅, we have that (τ ∪ σ) ∈ RSubst.
It follows from Eq. (1) that τ ◦ σ can be obtained from (τ ∪ σ) by a sequence of
S-steps so that, by Theorem 1, we have Properties 1 and 2.
To prove Property 3, we suppose that, for some v ∈ dom(τ ◦ σ), there exist
w ∈ vars(vσ), x ∈ vars(wτ ) and y ∈ vars(xσ) such that z ∈ vars(yτ ) \ dom(τ ◦ σ).
We need to prove that z ∈ vars(vστ ).
It follows from Property 2, that z ∈
/ dom(σ) and z ∈
/ dom(τ ). Suppose first that
x ∈
/ dom(σ). Then y = x and hence z ∈ vars(vστ τ ). Therefore, as τ ∈ VSubst
and z ∈
/ dom(τ ), we can conclude z ∈ vars(vστ ). Thus, we now assume that
x ∈ dom(σ). As dom(σ) ∩ vars(τ ) = ∅, we have x ∈
/ vars(τ ), so that x = w and
hence, y ∈ vars(vσσ). If y ∈
/ dom(τ ) we have y = z, so that y ∈
/ dom(σ). On the
other hand, if y ∈ dom(τ ) then, by the hypothesis, y ∈
/ dom(σ). Thus, in both
cases, as σ ∈ VSubst, we obtain y ∈ vars(vσ) and hence z ∈ vars(vστ ). It follows,
using Eq. (9), that Property 3 holds.

5 The Abstraction Function for RSubst
In this section we define a new abstraction function mapping arbitrary substitutions
in rational solved form into their abstract descriptions. This abstraction function
is based on a new definition for the notion of occurrence. The new occurrence operator occ is defined on RSubst so that it does not require the explicit computation
of intermediate variable-idempotent substitutions. To this end, it is given as the
fixed point of a sequence of occurrence functions. The occ operator generalises the
sg operator, defined for ISubst, coinciding with it when applied to idempotent substitutions.

22

P. M. Hill, R. Bagnara and E. Zaffanella

Definition 5
(Occurrence functions.) For each n ∈ N, occn : RSubst × Vars → ℘f (Vars),
called occurrence function, is defined, for each σ ∈ RSubst and each v ∈ Vars, by
def

occ0 (σ, v) = {v} \ dom(σ)
and, for n > 0, by
def

occn (σ, v) =



y ∈ Vars vars(yσ) ∩ occn−1 (σ, v) 6= ∅ .

The following monotonicity property for occn is proved at the end of this section.
Lemma 11
If n > 0, then, for each σ ∈ RSubst and each v ∈ Vars,
occn−1 (σ, v) ⊆ occn (σ, v).
Note that, by considering the substitution {u 7→ v, v 7→ w}, it can be seen that,
if we had not excluded the domain variables in the definition of occ0 , then this
monotonicity property would not have held.
For any n, the set occn (σ, v) is restricted to the set {v} ∪ vars(σ). Thus, it follows
from Lemma 11, that there is an ℓ = ℓ(σ, v) ∈ N such that occℓ (σ, v) = occn (σ, v)
for all n ≥ ℓ.
Definition 6
(Occurrence operator.) For each σ ∈ RSubst and v ∈ Vars, the occurrence
operator occ : RSubst × Vars → ℘f (Vars) is given by
def

occ(σ, v) = occℓ (σ, v)
where ℓ ∈ N is such that occℓ (σ, v) = occn (σ, v) for all n ≥ ℓ.
Note that, by combining Definitions 5 and 6, we obtain

occ(σ, v) = y ∈ Vars vars(yσ) ∩ occ(σ, v) 6= ∅ .

(15)

The following simpler characterisations for occ can be used when the variable is
in the domain of the substitution, the substitution is variable-idempotent or the
substitution is idempotent.
Lemma 12
If σ ∈ RSubst and v ∈ dom(σ), then occ(σ, v) = ∅.
Lemma 13
If σ ∈ VSubst then, for each v ∈ Vars,
occ(σ, v) = occ1 (σ, v)

= y ∈ Vars v ∈ vars(yσ) \ dom(σ) .

Lemma 14
If σ ∈ ISubst and v ∈ Vars then occ(σ, v) = sg(σ, v).
These results are proved at the end of this section.

Soundness, Idempotence and Commutativity of Set-Sharing

23

Example 7
Consider again Example 6. Then, for all i ≥ 0, dom(σi ) = {x1 , x2 , x3 } so that
occ(σi , x1 ) = occ(σi , x2 ) = occ(σi , x3 ) = ∅.
However,
occ0 (σ0 , x4 ) = {x4 },
occ1 (σ0 , x4 ) = {x2 , x4 },
occ2 (σ0 , x4 ) = {x1 , x2 , x4 },
occ3 (σ0 , x4 ) = {x1 , x2 , x3 , x4 } = occ(σ0 , x4 ).
Also, note that
occ1 (σ3 , x4 ) = {x1 , x2 , x3 , x4 } = occ(σ3 , x4 ).
The definition of abstraction is based on the occurrence operator, occ.
Definition 7
(Abstraction.) The concrete domain ℘(RSubst) is related to SS by means of the
abstraction function α : ℘(RSubst) × ℘f (Vars) → SS . For each Σ ∈ ℘(RSubst) and
each U ∈ ℘f (Vars),
G
def
α(Σ, U ) =
α(σ, U )
σ∈Σ

where α : RSubst × ℘f (Vars) → SS is defined, for each substitution σ ∈ RSubst and
each U ∈ ℘f (Vars), by


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

Example 8
Let us consider Examples 6 and 7 once more. Then, assuming U = {x1 , x2 , x3 , x4 },

 

α(σ0 , U ) = occ(σ0 , x4 ) , U = {x1 , x2 , x3 , x4 } , U .
As a second example, consider the substitution

σ = x1 7→ f (x1 ), x2 7→ x1 , x3 7→ x1 , x4 7→ x2 .

Then

occ(σ, x1 ) = occ(σ, x2 ) = occ(σ, x3 ) = occ(σ, x4 ) = ∅
so that, if we again assume U = {x1 , x2 , x3 , x4 },


α σ, U = ∅, U .

Any substitution in rational solved form is equivalent, with respect to any equality
theory, to a variable-idempotent substitution having the same abstraction.

24

P. M. Hill, R. Bagnara and E. Zaffanella

Theorem 3
If T is an equality theory and σ ∈ RSubst is satisfiable in T , then there exists a
substitution σ ′ ∈ VSubst such that τ ∈ VSubst, for all τ ⊆ σ ′ , T ⊢ ∀(σ ↔ σ ′ ),
vars(σ) = vars(σ ′ ) and α(σ, U ) = α(σ ′ , U ), for any U ∈ ℘f (Vars).
Equivalent substitutions in rational solved form have the same abstraction. We
note that this property is essential for the implementation of the SS domain.
Theorem 4
If T is a syntactic equality theory and σ, σ ′ ∈ RSubst are satisfiable in T and such
that T ⊢ ∀(σ ↔ σ ′ ), then α(σ, U ) = α(σ ′ , U ), for any U ∈ ℘f (Vars).
5.1 Proofs of Lemmas 11, 12, 13 and 14 and Theorems 3 and 4
Proof of Lemma 11.
The proof is by induction on n. For the base case (when n = 1), if occ0 (σ, v) 6= ∅,
then v ∈
/ dom(σ) and occ0 (σ, v) = {v}. Thus, v = vσ so that, by Definition 5,
v ∈ occ1 (σ, v). Suppose n > 1. Then, if y ∈ occn−1 (σ, v), we have, by Definition 5,
vars(yσ) ∩ occn−2 (σ, v) 6= ∅. By the induction hypothesis,
occn−2 (σ, v) ⊆ occn−1 (σ, v)
so that vars(yσ) ∩ occn−1 (σ, v) 6= ∅ and thus y ∈ occn (σ, v).
Proof of Lemma 12.
By Definition 5, occ0 (σ, v) = ∅ and, for all n > 0, we have occn (σ, v) = ∅ if
occn−1 (σ, v) = ∅. Thus, occn (σ, v) = ∅, for all n ≥ 0, so that, by Definition 6,
occ(σ, v) = ∅.
Proof of Lemma 13.
Suppose first that v ∈ dom(σ). Then

y ∈ Vars v ∈ vars(yσ) \ dom(σ)

= ∅.

Also, by Lemma 12, occ1 (σ, v) = occ(σ, v) = ∅.
Suppose next that v ∈
/ dom(σ). It follows from Definition 5, that

and

occ0 (σ, v) = {v},

occ1 (σ, v) = y ∈ Vars vars(yσ) ∩ {v} 6= ∅

= y ∈ Vars v ∈ vars(yσ) ,
occ2 (σ, v) =
=

n



y ∈ Vars vars(yσ) ∩ y1 ∈ Vars | v ∈ vars(y1 σ)

y ∈ Vars v ∈ vars(yσ 2 ) .

6= ∅

o

However, as σ ∈ VSubst, we have vars(yσ) \ dom(σ) = vars(yσ 2 ) \ dom(σ). Thus,
as v ∈
/ dom(σ), occ1 (σ, v) = occ2 (σ, v) and hence, by Definition 5, we have also
occn (σ, v) = occ1 (σ, v), for all n ≥ 1. Therefore, by Definition 6,

occ(σ, v) = occ1 (σ, v) = y ∈ Vars v ∈ vars(yσ) .

Soundness, Idempotence and Commutativity of Set-Sharing

25

Proof of Lemma 14.
As σ ∈ ISubst we have, for all y ∈ Vars, vars(yσ) \ dom(σ) = vars(yσ). Also, as
σ ∈ VSubst, we can apply Lemma 13 so that

occ(σ, v) = y ∈ Vars v ∈ vars(yσ) \ dom(σ)

= y ∈ Vars v ∈ vars(yσ)
= sg(σ, v).

To prove Theorem 3, we need to show that the abstraction function α is invariant
with respect to S-transformation.
Lemma 15
S
Let σ, σ ′ ∈ RSubst where σ 7−→∗ σ ′ and U ∈ ℘f (Vars). Then α(σ, U ) = α(σ ′ , U ).
Proof
S
Suppose first that σ 7−→ σ ′ . Thus we assume that (x 7→ t), (y 7→ s) ∈ σ , where
x 6= y, and that
 
σ ′ = σ \ {y 7→ s} ∪ y 7→ s[x/t] .
(16)

Suppose v ∈ Vars. Then we show that occ(σ, v) = occ(σ ′ , v).
If x ∈
/ vars(s), then σ ′ = σ and there is nothing to prove. Also, if v ∈ dom(σ)
then, by Theorem 1, v ∈ dom(σ ′ ) so that by Lemma 12, occ(σ, v) = occ(σ ′ , v) = ∅.
We now assume that x ∈ vars(s) and v = vσ = vσ ′ . We first prove that, for each
m ≥ 0,
occm (σ, v) ⊆ occ(σ ′ , v).

(17)

The proof is by induction on m. By Definition 5, we have that
occ0 (σ, v) = occ0 (σ ′ , v) = {v},
so that (17) holds for m = 0. Suppose then that m > 0 and that vm ∈ occm (σ, v).
Then, to prove (17), we must show that vm ∈ occ(σ ′ , v). By Definition 5, there
exists
vm−1 ∈ vars(vm σ) ∩ occm−1 (σ, v).

(18)

Hence, by the inductive hypothesis, vm−1 ∈ occ(σ ′ , v). If vm−1 ∈ vars(vm σ ′ ), then,
by Eq. (15), vm ∈ occ(σ ′ , v). Suppose now that vm−1 ∈
/ vars(vm σ ′ ). Since, by (18),
we have that vm−1 ∈ vars(vm σ), it follows, using (16), that vm = y and vm−1 =
x. However, by assumption, v ∈
/ dom(σ), so that x 6= v and m > 1. Thus, by
Definition 5, there exists
vm−2 ∈ vars(xσ) ∩ occm−2 (σ, v).

(19)

However, xσ = t and x ∈ vars(s)
 so ′that, by (19), we have vm−2 ∈ ′vars s[x/t] .
Since, by Eq. (16), y 7→ s[x/t] ∈ σ , we have also vm−2 ∈ vars(yσ ). Moreover,
by (19), vm−2 ∈ occm−2 (σ, v) so that, by the inductive hypothesis, we have that
vm−2 ∈ occ(σ ′ , v). Thus, by Eq. (15), as vm = y, vm ∈ occ(σ ′ , v).

26

P. M. Hill, R. Bagnara and E. Zaffanella

Conversely, we now prove that, for all m ≥ 0,
occm (σ ′ , v) ⊆ occ(σ, v).

(20)

The proof is again by induction on m. As before, occ0 (σ ′ , v) = occ0 (σ, v) = {v} so
that (20) holds for m = 0. Suppose then that m > 0 and vm ∈ occm (σ ′ , v). Then,
to prove (20), we must show that vm ∈ occ(σ, v). By Definition 5, there exists
vm−1 ∈ vars(vm σ ′ ) ∩ occm−1 (σ ′ , v).

(21)

Hence, by the inductive hypothesis, vm−1 ∈ occ(σ, v). If vm−1 ∈ vars(vm σ) then,
by Eq. (15), we have vm ∈ occ(σ, v). Suppose now that vm−1 ∈
/ vars(vm σ). Since,
by (21), we have vm−1 ∈ vars(vm σ ′ ), it follows, using Eq. (16), that vm = y and
vm−1 ∈ vars(t) = vars(xσ). Hence, since vm−1 ∈ occ(σ, v), by Eq. (15), we have
also x ∈ occ(σ, v). Furthermore, x ∈ vars(yσ) so again, by Eq. (15), as vm = y,
vm ∈ occ(σ, v).
Combining (17) and (20) we obtain the result that, if σ ′ is obtained from σ
by a single S-step, then occ(σ, v) = occ(σ ′ , v). Thus, as v ∈ Vars was arbitrary,
α(σ, U ) = α(σ ′ , U ).
S
S
Suppose now that σ = σ1 7−→ · · · 7−→ σn = σ ′ . If n = 1, then σ = σ ′ . If n > 1, we
have by the first part of the proof that, for each i = 2, . . . , n, α(σi−1 , U ) = α(σi , U ),
and hence the required result.
Proof of Theorem 3.
S
By Theorem 2, there exists σ ′ ∈ VSubst such that σ 7−→∗ σ ′ and, for any τ ⊆ σ ′ ,
τ ∈ VSubst. Moreover, by Theorem 1, vars(σ) = vars(σ ′ ) and T ⊢ ∀(σ ↔ σ ′ ).
Thus, by Lemma 15, α(σ, U ) = α(σ ′ , U ).
To prove Theorem 4, we need to show that the abstraction function α is invariant
when we exchange equivalent variables to obtain an ordered substitution.
Lemma 16
Suppose σ ∈ VSubst, v, w ∈ Vars and (v 7→ w) ∈ σ. Let ρ = {v 7→ w, w 7→ v} be a
(circular) substitution and define σ ′ = ρ ◦ σ = { xρ 7→ tρ | x 7→ t ∈ σ }. Then
1.
2.
3.
4.

σ ′ ∈ VSubst,
vars(σ) = vars(σ ′ ),
α(σ, U ) = α(σ ′ , U ), for all U ∈ ℘f (Vars), and
T ⊢ ∀(σ ↔ σ ′ ), for any equality theory T .

Proof
Since σ ′ is obtained from σ by renaming variables and σ ∈ VSubst, we have also
that σ ′ ∈ VSubst. In addition, vars(σ) \ {v, w} = vars(σ ′ ) \ {v, w} so that, since
(v 7→ w) ∈ σ and (w 7→ v) ∈ σ ′ , we have vars(σ) = vars(σ ′ ).
To prove property 3, we have to show that, if
def

α(σ, U ) = (sh, U )

and

def

α(σ ′ , U ) = (sh ′ , U ),

then sh = sh ′ . By the hypothesis, for all y ∈ Vars we have x ∈ vars(yσ) if and only if
xρ ∈ vars(yσ ′ ). As σ, σ ′ ∈ VSubst, we can use the alternative characterisation of occ

Soundness, Idempotence and Commutativity of Set-Sharing

27

given by Lemma 13 and conclude that, for each x ∈ Vars, occ(σ, x) = occ(σ ′ , xρ).
Therefore sh ⊆ sh ′ . The reverse inclusion follows by symmetry so that sh = sh ′ .
To prove property 4, we first show by induction on the depth of r ∈ TVars that

T ⊢ ∀ (v = w) → (r = rρ) .
(22)

For the base case, r has depth 1. If r is a constant or a variable other than v
or w, then r = rρ. If r = v, then rρ = w and T ⊢ ∀ (v = w) → (v = w) .
Finally, if r = w, then rρ =
 v and we have, using the congruence axioms, that
T ⊢ ∀ (v = w) → (w = v) . For the inductive step, let r = f (r1 , . . . , rn ). Then
rρ = f (r1 ρ, . . . , rn ρ). Thus,using the inductive hypothesis, for each i = 1, . . . , n,
T ⊢ ∀ (v = w) → (ri = ri ρ) . Hence, by the congruence axioms, (22) holds.
Note that (v 7→ w) ∈ σ. Thus, it follows
from (22) that, for each (x 7→ t) ∈ σ,

T ⊢ ∀ σ → {x = t, x = xρ, t = tρ} and hence, using the congruence axioms,
T ⊢ ∀ σ → {xρ = tρ} . Thus, T ⊢ ∀(σ → σ ′ ). Since (w 7→ v) ∈ σ ′ , the reverse
implication follows by symmetry so that T ⊢ ∀(σ ′ ↔ σ).
Lemma 17
Suppose σ ∈ VSubst. Then there exists σ ′ ∈ VSubst that is ordered such that
vars(σ) = vars(σ ′ ), α(σ, U ) = α(σ ′ , U ), for all U ∈ ℘f (Vars), and T ⊢ ∀(σ ↔ σ ′ ),
for any equality theory T .
Proof
The proof is by induction on the number b ≥ 0 of the bindings (v 7→ w) ∈ σ such
that w ∈ param(σ) and w > v (the number of unordered bindings). For the base
case, when b = 0, σ is ordered and the result holds by taking σ ′ = σ.
For the inductive case, when b > 0, let (v 7→ w) ∈ σ be an unordered binding
and define ρ = {v 7→ w, w 7→ v}. Then, by Lemma 16, we have ρ ◦ σ ∈ VSubst,
vars(σ) = vars(ρ ◦ σ), α(σ, U ) = α(ρ ◦ σ, U ), for all U ∈ ℘f (Vars), and, finally,
T ⊢ ∀(σ ↔ ρ ◦ σ), for any equality theory T . In order to apply the inductive
hypothesis to ρ ◦ σ, we must show that the number of unordered bindings in ρ ◦ σ is
less than b. To this end, roughly speaking, we start showing that any ordered binding
in σ is mapped by ρ into another ordered binding in ρ◦σ, therefore proving that the
number of unordered bindings is not increasing. There are three cases. First, any
ordered binding (y 7→ t) ∈ σ such that t ∈
/ Vars is mapped by ρ into the binding
(yρ 7→ tρ) ∈ (ρ ◦ σ) which is clearly ordered, since tρ ∈
/ Vars. Second, consider any
ordered binding (y 7→ z) ∈ σ such that z ∈ dom(σ). Since w ∈ param(σ), we have
z 6= w. If also z 6= v then we have zρ = z and z ∈ dom(ρ ◦ σ); otherwise z = v so
that zρ = w and, as (w 7→ v) ∈ (ρ ◦ σ), zρ ∈ dom(ρ ◦ σ). Thus, in either case, such
a binding is mapped by ρ into the binding (yρ 7→ zρ) ∈ (ρ ◦ σ) which is ordered
since zρ ∈ dom(ρ ◦ σ). Third, consider any ordered binding (y 7→ z) ∈ σ such that
z ∈ param(σ) and z < y. The ordering relation implies y 6= v and we also have
y 6= w, since w ∈ param(σ). Hence, we obtain yρ = y. Now, as z ∈ param(σ), z 6= v.
If z 6= w, then zρ = z. On the other hand, if z = w, then zρ = v so that zρ < z.
Thus, in both cases, as z < y, zρ < y. and hence, (yρ 7→ zρ) ∈ (ρ ◦ σ) is ordered.
Finally, to show that the number of unordered bindings is strictly decreasing, we

28

P. M. Hill, R. Bagnara and E. Zaffanella

note that the unordered binding (v 7→ w) ∈ σ is mapped by ρ into the binding
(w 7→ v) ∈ (ρ ◦ σ), which is ordered.
Therefore, by applying the inductive hypothesis, there exists a substitution σ ′
such that σ ′ ∈ VSubst is ordered, vars(ρ ◦ σ) = vars(σ ′ ), α(ρ ◦ σ, U ) = α(σ ′ , U ),
for all U ∈ ℘f (Vars), and T ⊢ ∀(ρ ◦ σ ↔ σ ′ ), for any equality theory T . Then the
required result follows by transitivity.
Proof of Theorem 4.
By Theorem 3, we can assume that σ, σ ′ ∈ VSubst, T ⊢ ∀(σ ↔ σ ′ ) and, for any
U ∈ ℘f (Vars), α(σ, U ) = α(σ ′ , U ). By Lemma 17, we can assume that σ, σ ′ are also
ordered substitutions so that, by Lemma 5, dom(σ ′ ) = dom(σ).
To prove the result we need to show that, for all v ∈ Vars, we have both
occ(σ, v) ⊆ occ(σ ′ , v) and occ(σ ′ , v) ⊆ occ(σ, v). We just prove the first of these
as the other case is symmetric.
Suppose that w ∈ Vars and that v ∈ vars(wσ) \ dom(σ). Then, using the alternative characterisation of occ for variable-idempotent substitutions given by
Lemma 13, we just have to show that v ∈ vars(wσ ′ ) \ dom(σ ′ ).
By Lemma 6 (replacing τ by σ, σ by σ ′ and s = t by w = w), we have that there
exists z ∈ vars(wσ ′ ) \ dom(σ ′ ) such that v ∈ vars(zσ). Thus as dom(σ ′ ) = dom(σ),
z∈
/ dom(σ), and hence, v = z so that v ∈ vars(wσ ′ ) \ dom(σ ′ ), as required.

6 Abstract Unification
The operations of abstract unification together with statements of the main results
are presented here in three stages. In the first two stages, we consider substitutions
containing just a single binding. For the first, it is assumed that the set of variables
of interest is fixed so that the definition is based on the SH domain. Then, in the
second, using the SS domain, the definition is extended to allow for the introduction
of new variables in the binding. The final stage extends this definition further to
deal with arbitrary substitutions.
6.1 Abstract Operations for Sharing Sets
The abstract unifier amgu abstracts the effect of a single binding on an element of
the SH domain. For this we need some ancillary definitions.
Definition 8
(Auxiliary functions.) The closure under union function (also called star-union),
(·)⋆ : SH → SH , is given, for each sh ∈ SH , by
def 
sh ⋆ = S ∈ SG ∃n ≥ 1 . ∃S1 , . . . , Sn ∈ sh . S = S1 ∪ · · · ∪ Sn .
For each sh ∈ SH and each V ∈ ℘f (Vars), the extraction of the relevant component
of sh with respect to V is encoded by rel : ℘f (Vars) × SH → SH defined as
def

rel(V, sh) = { S ∈ sh | S ∩ V 6= ∅ }.

Soundness, Idempotence and Commutativity of Set-Sharing

29

For each sh 1 , sh 2 ∈ SH , the binary union function bin : SH × SH → SH is given
by
def

bin(sh 1 , sh 2 ) = { S1 ∪ S2 | S1 ∈ sh 1 , S2 ∈ sh 2 }.
Definition 9
(amgu.) The function amgu : SH × Bind → SH captures the effects of a binding
on an SH element. Suppose x ∈ Vars, r ∈ TVars , and sh ∈ SH . Let

def
A = rel {x}, sh ,

def
B = rel vars(r), sh .

Then


def
amgu(sh, x 7→ r) = sh \ (A ∪ B) ∪ bin(A⋆ , B ⋆ ).

The following soundness result for amgu is proved in Section 6.4.

Theorem 5
Let T be a syntactic equality theory, (sh, U ) ∈ SS an abstract description and
{x 7→ r}, σ ∈ RSubst such that vars(x 7→ r) ∪ vars(σ)
⊆ U . Suppose that there

exists a most general solution µ for {x = r} ∪ σ in T . Then

α(σ, U ) SS (sh, U ) =⇒ α(µ, U ) SS amgu(sh, x 7→ r), U .
The following theorems, proved in Section 6.4, show that amgu is idempotent
and commutative.
Theorem 6
Let sh ∈ SH and (x 7→ r) ∈ Bind . Then

amgu(sh, x 7→ r) = amgu amgu(sh, x 7→ r), x 7→ r .

Theorem 7
Let sh ∈ SH and (x 7→ r), (y 7→ t) ∈ Bind . Then


amgu amgu(sh, x 7→ r), y 7→ t = amgu amgu(sh, y 7→ t), x 7→ r .
6.2 Abstract Operations for Sharing Domains
The definitions and results of Section 6.1 can be lifted to apply to the proper setsharing domain.
Definition 10
(Amgu.) The operation Amgu : SS × Bind → 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. Formally:
def

U ′ = vars(x 7→ r) \ U,




 def

′
′
Amgu (sh, U ), x 7→ r = amgu sh ∪ {u} u ∈ U , x 7→ r , U ∪ U .

The results for amgu can easily be extended to apply to Amgu giving us the
following corollaries.

30

P. M. Hill, R. Bagnara and E. Zaffanella

Corollary 1
Let T be a syntactic equality theory, (sh, U ) ∈ SS and {x 7→ r}, σ ∈ RSubst such
that vars(σ) ⊆ U . Suppose there exists a most general solution µ for {x = r} ∪ σ
in T . Then


α(σ, U ) SS (sh, U ) =⇒ α µ, U ∪ vars(x 7→ r) SS Amgu (sh, U ), x 7→ r .
Corollary 2
Let sh ∈ SH and (x 7→ r) ∈ Bind . Then




Amgu (sh, U ), x 7→ r = Amgu Amgu (sh, U ), x 7→ r , x 7→ r .

Corollary 3
Let sh ∈ SH and (x 7→ r), (y 7→ t) ∈ Bind . Then



Amgu Amgu (sh, U ), x 7→ r , y 7→ t



= Amgu Amgu (sh, U ), y 7→ t , x 7→ r .
6.3 Abstract Unifiers for Sharing
We now extend the above definitions and results for a single binding to any substitution.
Definition 11
(aunify.) The function aunify : SS × RSubst → SS generalizes Amgu to any substitution µ ∈ RSubst in the context of some syntactic equality theory T : If we have
(sh, U ) ∈ SS , then
 def
aunify (sh, U ), ∅ = (sh, U );
if µ is satisfiable in T and (x 7→ r) ∈ µ,


 def

aunify (sh, U ), µ = aunify Amgu(sh, U ), x 7→ r , µ \ {x 7→ r} ;

and, if µ is not satisfiable in T ,
 def
aunify (sh, U ), µ = ⊥.

For the distinguished elements ⊥ and ⊤ of SS ,
def

aunify(⊥, µ) = ⊥,
def

aunify(⊤, µ) = ⊤.
As a result of Corollary 3, Amgu and aunify commute.
Lemma 18
Let (sh, U ) ∈ SS , ν ∈ RSubst and (y 7→ t) ∈ Bind . Then



 

aunify Amgu (sh, U ), y 7→ t , ν = Amgu aunify (sh, U ), ν , y 7→ t .

Soundness, Idempotence and Commutativity of Set-Sharing

31

As a consequence of this and Corollaries 1, 2 and 3, we have the following soundness,
idempotence and commutativity results required for aunify to be sound and welldefined.
Theorem 8
Let T be a syntactic equality theory, (sh, U ) ∈ SS and σ, ν ∈ RSubst such that
vars(σ) ⊆ U . Suppose also that there exists a most general solution µ for (ν ∪ σ)
in T . Then


α(σ, U ) SS (sh, U ) =⇒ α µ, U ∪ vars(ν) SS aunify (sh, U ), µ .

This theorem shows also that it is safe for the analyzer to perform part or all of
the concrete unification algorithm before computing aunify.
Theorem 9
Let (sh, U ) ∈ SS and ν ∈ RSubst. Then


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

Theorem 10
Let (sh, U ) ∈ SS and ν1 , ν2 ∈ RSubst. Then


 
 
aunify aunify (sh, U ), ν1 , ν2 = aunify aunify (sh, U ), ν2 , ν1 .
The proofs of all these results are in Section 6.5.

6.4 Proofs of Results for Sharing-Sets
In the proofs we use the fact that (·)⋆ and rel are monotonic so that
sh 1 ⊆ sh 2 =⇒ sh ⋆1 ⊆ sh ⋆2 ,

(23)

sh 1 ⊆ sh 2 =⇒ rel(sh 1 , U ) ⊆ rel(sh 2 , U ).

(24)

We will also use the fact that (·)⋆ is idempotent.
Let t1 , . . . , tn be terms. For the sake of brevity we will use the notation vt1 ···tn to
S
denote ni=1 vars(ti ). In particular, if x and y are variables, and r and t are terms,
we will use the following definitions:
def

def

vy = {y},

def

vt = vars(t),

def

vyt = vy ∪ vt .

vx = {x},

def

vr = vars(r),

def

vxr = vx ∪ vr ,
Definition 12
(rel.) Suppose V ∈ ℘f (Vars) and sh ∈ SH . Then
def

rel(V, sh) = sh \ rel(V, sh).
Notice that if S ∈ rel(V, sh) then S ∩V = ∅. Conversely, if S ∈ sh and S ∩V = ∅
then S ∈ rel(V, sh). The following definition of amgu is clearly equivalent to the
one given in Definition 9: for each variable x, each term r, and each sh ∈ SH ,

def
(25)
amgu(sh, x 7→ r) = rel(vxr , sh) ∪ bin rel(vx , sh)⋆ , rel(vr , sh)⋆ .

32

P. M. Hill, R. Bagnara and E. Zaffanella

Proof of Theorem 5.
We first prove the result under the assumption that α(σ, U ) = (sh, U ). We do this
in two parts. In the first, we partition σ into two substitutions one of which, called
σ − , is the same as σ when σ and µ are idempotent. We construct a new substitution
ν which, in the case that σ and µ are idempotent, is a most general solution for
xσ = rσ. Finally we compose ν with σ − to define a substitution that has the same
abstraction as µ but with a number of useful properties including that of variableidempotence. In the second part, we use this composed substitution in place of µ
to prove the result.
Part 1. By Theorem 3, we can assume that
σ ∈ VSubst

(26)

and that all subsets of σ are in VSubst. Let σ ◦ , σ − ∈ RSubst be defined such that
σ − ∪ σ ◦ = σ,

(27)

◦

dom(σ ) = dom(σ) ∩

[

i

i

vars(xσ = rσ ),

(28)

i≥1

dom(σ − ) ∩ dom(σ ◦ ) = ∅.

(29)

Then, it follows from the above assumption on subsets of σ that
σ − ∈ VSubst,

σ ◦ ∈ VSubst.

(30)

Now, suppose z ∈ vars(σ ◦ ) \ dom(σ ◦ ). Then z ∈ vars(yσ ◦ ) for some y ∈ dom(σ ◦ ).
Thus, by (28), for some j ≥ 2, z ∈ vars(xσ j = rσ j ) \ dom(σ ◦ ) and, again by (28),
z∈
/ dom(σ) so that, by (26), z ∈ vars(xσ = rσ). Therefore, as z was an arbitrary
variable in vars(σ ◦ ) \ dom(σ ◦ ),

vars(σ ◦ ) ⊆ vars(xσ = rσ) ∪ dom(σ ◦ ) .
(31)

It follows from (28) that dom(σ) ∩ vars(xσ = rσ) ⊆ dom(σ ◦ ) so that, by (29)
dom(σ − ) ∩ vars(xσ = rσ) = ∅.

(32)

Hence, by (29) and (31), we have
dom(σ − ) ∩ vars(σ ◦ ) = ∅.

(33)

Let ν ∈ RSubst be a most general solution for {xσ = rσ} ∪ σ ◦ in T so that

(34)
T ⊢ ∀ ν ↔ {xσ = rσ} ∪ σ ◦ ,

◦
vars(ν) ⊆ vars(xσ = rσ) ∪ vars(σ ) .
(35)

By Theorem 3, we can assume that

ν ∈ VSubst.

(36)

dom(σ − ) ∩ vars(ν) = ∅.

(37)

By (32), (33), and (35), we have

Soundness, Idempotence and Commutativity of Set-Sharing

33

Therefore, as σ − , ν ∈ VSubst (by (30) and (36)), we can use Lemma 7 to obtain
the following properties for ν ◦ σ − .

T ⊢ ∀ (ν ◦ σ − ) ↔ (ν ∪ σ − ) ,
(38)
dom(ν ◦ σ − ) = dom(ν ∪ σ − ),
−

ν ◦ σ ∈ VSubst.

(39)
(40)

Now we have
T ⊢ ∀ µ ↔ {x = r} ∪ σ
[by hypothesis]



T ⊢ ∀ µ ↔ {xσ = rσ} ∪ σ



[by Lemma 2 and the congruence axioms]

T ⊢ ∀ µ ↔ ν ∪ σ−
[by (27) and (34)]

T ⊢ ∀ µ ↔ ν ◦ σ−

(41)

[by (38)].

Therefore, by Theorem 4,
α(µ, U ) = α(ν ◦ σ − , U ).

(42)

Part 2. To prove the result under the assumption that α(σ, U ) = (sh, U ), we
define sh ′ ∈ SH so that
α(µ, U ) = (sh ′ , U ).

(43)

Then, by (42), α(ν ◦ σ − , U ) = (sh ′ , U ). We show that sh ′ ⊆ amgu(sh, x 7→ r). If
sh ′ = ∅, there is nothing to prove. Therefore, we assume that there exists S ∈ sh ′
so that S 6= ∅ and, for some v ∈ Vars,
v∈
/ dom(ν ◦ σ − ),
def

S = occ(ν ◦ σ − , v).

(44)
(45)

Note that (39) and (44) imply that
v∈
/ dom(ν),

v∈
/ dom(σ − ).

(46)

Let
def

S′ =
We show that

[

occ(σ, y) y ∈ occ(ν, v) .

S = S ′.

(47)

(48)

By (26), (36) and (40), σ, ν, ν ◦ σ − ∈ VSubst and, by (44) and (46), v ∈
/ dom(ν ◦ σ − )
and v ∈
/ dom(ν). Thus, it follows from Lemma 13 with (45) and (47), that it
suffices to show that, for each w ∈ Vars, v ∈ vars(wσ − ν) if and only if there exists
z ∈ vars(wσ) \ dom(σ) such that v ∈ vars(zν).

34

P. M. Hill, R. Bagnara and E. Zaffanella

First, we suppose that v ∈ vars(wσ − ν). Thus, there exists y ∈ vars(wσ − ) such
◦
that v ∈ vars(yν). Since σ ◦ , ν ∈ VSubst (by (30) and (36)),
 T ⊢ ∀(ν → σ )
(by (34)), v ∈
/ dom(ν) (by (46)) and T ⊢ ∀ ν → (yν = y) (using Lemma 2),
we can apply Lemma 6 (replacing τ by ν, σ by σ ◦ and s = t by yν = y) so
that there exists z ∈ vars(yσ ◦ ) \ dom(σ ◦ ) such that v ∈ vars(zν). We want to
show that z ∈ vars(wσ) \ dom(σ). Now either z ∈ dom(ν) or z = v so that, by
(37) (if z ∈ dom(ν)) or (46) (if z = v), z ∈
/ dom(σ − ). However, z ∈
/ dom(σ ◦ ), so
that, by (27), z ∈
/ dom(σ). Thus, it remains to prove that z ∈ vars(wσ). Now, as
y ∈ vars(wσ − ) and z ∈ vars(yσ ◦ ), we have z ∈ vars(wσ − σ ◦ ). So we must show
that vars(wσ − σ ◦ ) \ dom(σ) ⊆ vars(wσ). To see this note that, if w ∈
/ dom(σ − ),
−
◦
− ◦
then wσ = w and, by (27), wσ = wσ so that wσ σ = wσ. On the other
hand, if w ∈ dom(σ − ), then, by (27), wσ − = wσ so that wσ − σ ◦ = wσσ ◦ Now,
as σ ∈ VSubst and σ ◦ ⊆ σ (by (26) and (27)), we can apply Lemma 4 so that
vars(wσσ ◦ ) \ dom(σ) ⊆ vars(wσ). Hence, vars(wσ − σ ◦ ) \ dom(σ) ⊆ vars(wσ).
Secondly, suppose there exists z ∈ vars(wσ) \ dom(σ) such that v ∈ vars(zν).
Then v ∈ vars(wσν). We need to show that v ∈ vars(wσ − ν). By Eq. (27), if
w ∈ dom(σ − ), then wσ − ν = wσν so that v ∈ vars(wσ − ν). On the other hand, if
w∈
/ dom(σ − ), then again, by (27), v ∈ vars(wσ ◦ ν). Moreover, w = wσ − so that,

by (34) and Lemma 2 with the congruence axioms, T ⊢ ∀ ν → (wσ ◦ ν = wσ − ) .
Hence, since ν ∈ VSubst (by (36)) and v ∈
/ dom(ν) (by (46)), we can apply Lemma 6
(replacing τ by ν, σ by the empty substitution and s = t by wσ ◦ ν = wσ − ) and
obtain v ∈ vars(wσ − ν).
Therefore, as a consequence of the previous two paragraphs, for each w ∈ Vars,
we have v ∈ vars(wσ − ν) if and only if there exists z ∈ vars(wσ) \ dom(σ) such that
v ∈ vars(zν). It therefore follows that Eq. (48) holds.
Let

[
def
occ(σ, y) y ∈ occ(ν, v) ∩ rel(vx , sh) ,
(49)
Sx =


[ 
def
occ(σ, y) y ∈ occ(ν, v) ∩ rel(vr , sh) ,
(50)
Sr =


[
def
(51)
occ(σ, y) y ∈ occ(ν, v) ∩ rel(vxr , sh) .
S0 =
Note that by (47), (48) and the fact that

we have


rel(vxr , sh) = sh \ rel(vx , sh) ∪ rel(vr , sh) ,
S0 = S \ (Sx ∪ Sr ).

(52)

We now consider the two cases S0 6= ∅ and S0 = ∅ separately.
Consider first the case when S0 6= ∅. Then, by (51), for some y ∈ Vars,
y ∈ occ(ν, v),
occ(σ, y) ∈ rel(vxr , sh).

(53)
(54)

Thus, by Lemma 12, y ∈
/ dom(σ) and hence, by (27), y ∈
/ dom(σ ◦ ). Also, by (54),
occ(σ, y) ∩ vxr = ∅. Thus as σ ∈ VSubst (by (26)) we can use Lemma 13 to see

Soundness, Idempotence and Commutativity of Set-Sharing

35

that, for each w ∈ vxr , y ∈
/ vars(wσ) and hence, y ∈
/ vars(xσ = rσ). Therefore,
by (31) and (35), y ∈
/ vars(ν). As ν ∈ VSubst (by (36)), we can apply Lemma 13
to both occ(ν, y) and occ(ν, v). Thus, as y ∈
/ vars(ν), occ(ν, y) = {y} and also
(using (53)) v = y so that occ(ν, v) = {v}. It therefore follows from (47) and (48)
that S = occ(σ, v) and hence from (54), that
S ∈ rel(vxr , sh).

(55)

Now consider the case when S0 = ∅. By (52), and the assumption that S 6= ∅,
S = Sx ∪ Sr 6= ∅.

(56)

As a consequence of (49) and (50),
Sx ∈ rel(vx , sh)⋆ ∪ ∅,
⋆

Sr ∈ rel(vr , sh) ∪ ∅.

(57)
(58)

Now, by (56) either Sx 6= ∅ or Sr 6= ∅. We will show that both Sx 6= ∅ and
Sr 6= ∅. Suppose first that Sx 6= ∅. Then, by (57), x ∈ Sx . Hence, by (56), x ∈ S.
By (45), x ∈ occ(ν ◦σ − , v). However, ν ◦σ − ∈ VSubst (by (40)) so that we can apply
−
Lemma 13 to occ(ν ◦ σ − , v) and obtain that v ∈ vars(xσ
ν). By the definition of µ

−
in the hypothesis and (41), T ⊢ ∀ ν ◦ σ → (x = r) and
 hence, by Lemma 2 with
the congruence axioms, T ⊢ ∀ ν ◦ σ − → (xσ − ν = r) . Thus, as ν ◦ σ − ∈ VSubst
(by (40)) and v ∈
/ dom(ν ◦ σ − ) (by (44)), we have, by Lemma 6 (replacing τ by
−
ν ◦ σ , σ by the empty substitution and s = t by xσ − ν = r), v ∈ vars(rσ − ν). By
re-applying Lemma 13 to occ(ν ◦σ − , v), it can be seen that, as v ∈
/ dom(ν) (by (44)),
−
vr ∩ occ(ν ◦ σ , v) 6= ∅. Hence, by (45), S ∩ vr 6= ∅. Thus, by (47) and (48), there
exists a y ∈ occ(ν, v) such that occ(σ, y) ∩ vr 6= ∅. Therefore, by (50), Sr ∩ vr 6= ∅
and so Sr 6= ∅. Secondly, by a similar argument, if Sr 6= ∅ then we have Sx 6= ∅.
Hence Sx 6= ∅ and Sr 6= ∅. So that, by (57) and (58), Sx ∈ rel(vx , sh)⋆ and
Sr ∈ rel(vr , sh)⋆ . Therefore, we have, by (56),

(59)
S ∈ bin rel(vx , sh)⋆ , rel(vr , sh)⋆ .
Combining (55) when S0 6= ∅ and (59) when S0 = ∅ we obtain

S ∈ rel(vxr , sh) ∪ bin rel(vx , sh)⋆ , rel(vr , sh)⋆

and therefore, by (25),

S ∈ amgu(sh, x 7→ r).
As a consequence, since S was any set in sh ′ , we have sh ′ ⊆ amgu(sh, x 7→ r) and
hence, by (43),

(60)
α(µ, U ) SS amgu(sh, x 7→ r), U .
We now drop the assumption that α(σ, U ) = (sh, U ) and just assume the hypothesis of the theorem that α(σ, U ) SS (sh, U ). Suppose α(σ, U ) = (sh 1 , U ).
Then sh 1 ⊆ sh. It follows from Definition 9 that amgu is monotonic on its first

36

P. M. Hill, R. Bagnara and E. Zaffanella

argument so that
amgu(sh 1 , x 7→ r) ⊆ amgu(sh, x 7→ r).
Thus, by (60) (replacing sh by sh 1 ), we obtain the required result

α(µ, U ) SS amgu(sh, x 7→ r), U .

Lemma 19

For each sh 1 , sh 2 ∈ SH , we have
bin(sh 1 , sh 2 )⋆ = bin(sh ⋆1 , sh ⋆2 ).
Proof
Suppose S ∈ SG. Then S ∈ bin(sh 1 , sh 2 )⋆ means that, for some n ∈ N, there exist
sets R1 , . . . , Rn ∈ sh 1 and T1 , . . . , Tn ∈ sh 2 such that S = (R1 ∪T1 )∪· · ·∪(Rn ∪Tn ).
Thus S = (R1 ∪ · · · ∪ Rn ) ∪ (T1 ∪ · · · ∪ Tn ). However R1 ∪ · · · ∪ Rn ∈ sh ⋆1 and
T1 ∪ · · · ∪ Tn ∈ sh ⋆2 . Thus S ∈ bin(sh ⋆1 , sh ⋆2 ).
On the other hand, S ∈ bin(sh ⋆1 , sh ⋆2 ) means that S = R ∪ T where, for some
k, l ∈ N, R1 , . . . , Rk ∈ sh 1 , and T1 , . . . , Tl ∈ sh 2 , we have R = R1 ∪ · · · ∪ Rk and
T = T1 ∪· · ·∪Tl . Let n be the maximum of {k, l} and suppose that, for each i, j ∈ N
def

def

where k + 1 ≤ i ≤ n and l + 1 ≤ j ≤ n, we define Ri = Rk and Tj = Tl . Then,
S = (R1 ∪ T1 ) ∪ · · · ∪ (Rn ∪ Tn ). However, for 1 ≤ i ≤ n, Ri ∪ Ti ∈ bin(sh 1 , sh 2 ).
Thus S ∈ bin(sh 1 , sh 2 )⋆ .
Proof of Theorem 6.
Let
def

sh − = rel(vxr , sh),

Then, by Lemma 19,


def
sh xr = bin rel(vx , sh)⋆ , rel(vr , sh)⋆ .
sh ⋆xr = sh xr ,

bin(sh xr , sh xr ) = sh xr .

Moreover,
rel(vx , sh xr ) = sh xr ,

rel(vx , sh − ) = ∅,

rel(vr , sh xr ) = sh xr ,

rel(vr , sh − ) = ∅,

rel(vxr , sh xr ) = ∅,

rel(vxr , sh − ) = sh − .

Hence, we have
rel(vx , sh − ∪ sh xr ) = sh xr ,
rel(vr , sh − ∪ sh xr ) = sh xr ,
rel(vxr , sh − ∪ sh xr ) = sh − .

37

Soundness, Idempotence and Commutativity of Set-Sharing
Now, by (25),
amgu amgu(sh, x 7→ r), x 7→ r



= rel(vxr , sh − ∪ sh xr ) ∪ bin rel(vx , sh − ∪ sh xr )⋆ , rel(vr , sh − ∪ sh xr )⋆
= sh − ∪ sh xr



= amgu(sh, x 7→ r).
For the proof of commutativity, we require the following auxiliary results.
Lemma 20
For each V ∈ ℘f (Vars) and sh ∈ SH we have
rel(V, sh ⋆ ) = rel(V, sh)⋆ .
Proof
Let S ∈ SG. Then S ∈ rel(V, sh ⋆ ) means S ∈ sh ⋆ and S ∩ V = ∅. In other words,
Sn
there exist S1 , . . . , Sn ∈ sh such that S = i=1 Si and, for each i = 1, . . . , n, we
have Si ∩ V = ∅. This amounts to saying that there exist S1 , . . . , Sn ∈ rel(V, sh)
S
such that S = ni=1 Si , which is equivalent to S ∈ rel(V, sh)⋆ .
The auxiliary function rel possesses a weaker property.

Lemma 21
For each V ∈ ℘f (Vars) and sh ∈ SH we have
rel(V, sh ⋆ ) ⊇ rel(V, sh)⋆ .
Proof
Let S ∈ SG. Then S ∈ rel(V, sh)⋆ means that there exist S1 , . . . , Sn ∈ sh such
Sn
that Si ∩ V 6= ∅, for each i = 1, . . . , n, and S = i=1 Si . Thus S ∩ V 6= ∅ and
S ∈ rel(V, sh ⋆ ). Hence, rel(V, sh ⋆ ) ⊇ rel(V, sh)⋆ .
Lemma 22
For each V ∈ ℘f (Vars), sh 1 , sh 2 ∈ SH , and S ∈ ℘f (Vars) we have
S ∈ rel(V, sh 1 ∪ sh 2 )⋆ ∪ {∅}
⇐⇒ ∃S1 ∈ rel(V, sh 1 )⋆ ∪ {∅} . ∃S2 ∈ rel(V, sh 2 )⋆ ∪ {∅} . S = S1 ∪ S2 .
Proof
If S = ∅ the statement is trivial.
Suppose S ∈ rel(V, sh 1 ∪ sh 2 )⋆ . Then, for some n ∈ N, there exists n sets
R1 , . . . , Rn ∈ (sh 1 ∪ sh 2 ) such that Ri ∩ V 6= ∅ for each i = 1, . . . , n, and
Sn
S
S = i=1 Ri . Suppose Sj = { Ri ∈ sh j | 1 ≤ i ≤ n } for j = 1, 2. Thus we have
S1 ∈ rel(V, sh 1 )⋆ ∪ {∅}, S2 ∈ rel(V, sh 2 )⋆ ∪ {∅}, and S = S1 ∪ S2 .
Suppose
∃S1 ∈ rel(V, sh 1 )⋆ ∪ {∅} . ∃S2 ∈ rel(V, sh 2 )⋆ ∪ {∅} . S = S1 ∪ S2 ,
with S1 and S2 not both empty. Then, for some m ≥ 0 and n ≥ 0, there exist

38

P. M. Hill, R. Bagnara and E. Zaffanella

R1 , . . . , Rm ∈ rel(V, sh 1 ) and T1 , . . . , Tn ∈ rel(V, sh 2 ) such that S1 =
Sn
S2 = i=1 Ti . Then R1 , . . . , Rm , T1 , . . . , Tn ∈ rel(V, sh 1 ∪ sh 2 ) and
S=

m
[

i=1

Sm

i=1

Ri and

n

 [
Ti .
Ri ∪
i=1

Thus S ∈ rel(V, sh 1 ∪ sh 2 )⋆ .
Lemma 23
For each V1 , V2 ∈ ℘f (Vars) and sh ∈ SH we have


rel V1 , rel(V2 , sh) = rel V2 , rel(V1 , sh) .

Proof

Suppose S ∈ SG. Then S ∈ rel V1 , rel(V2 , sh) means S ∩ V1 6= ∅ and S ∩ V2 = ∅.
Similarly, S ∈ rel V2 , rel(V1 , sh) means that S ∩ V2 = ∅ and S ∩ V1 6= ∅.

Proof of Theorem 7.
We let R, S, T , and U (possibly subscripted) denote elements of sh ⋆ . The subscripts
reflect certain properties of the sets. In particular, subscripts x, r, xr, y, t, yt indicate
sets of variables that definitely have a variable in common with the subscripted set.
For example, Rx is a set in sh ⋆ that has a common element with vx and Txt is a
set in sh ⋆ that has common elements with vx and vt . In contrast, the subscript ‘−’
indicates that the subscripted set does not share with one of the sets vxr or vyt . Of
course, in the proof, each set is formally defined as needed.
Suppose that

S ∈ amgu amgu(sh, x 7→ r), y 7→ t .
We will show that


S ∈ amgu amgu(sh, y 7→ t), x 7→ r .

The converse then holds by simply exchanging x and y, and r and t.
There are two cases due to the two components of the definition of amgu in
Eq. (25).
Case 1. Assume

S ∈ rel vyt , amgu(sh, x 7→ r) .

Then S ∈ amgu(sh, x 7→ r) and S ∩ vyt = ∅. Again there are two possibilities.
Subcase 1a. Suppose first that
S ∈ rel(vxr , sh).
Thus S ∈ sh, and, since in this case we have S ∩ vyt = ∅,
S ∈ rel(vyt , sh).

Soundness, Idempotence and Commutativity of Set-Sharing

39

The alternative definition of amgu, (25), implies rel(vyt , sh) ⊆ amgu(sh, y 7→ t) and
thus we have also
S ∈ amgu(sh, y 7→ t).
Now, since the hypothesis of this subcase implies S ∩ vxr = ∅, we obtain

S ∈ rel vxr , amgu(sh, y 7→ t) .
Hence, again by (25), we can conclude that


S ∈ amgu amgu(sh, y 7→ t), x 7→ r .
Subcase 1b. Suppose now that

S ∈ bin rel(vx , sh)⋆ , rel(vr , sh)⋆ .

Then, there exist Sx , Sr ∈ SG such that S = Sx ∪ Sr , where
Sx ∈ rel(vx , sh)⋆ ,

Sr ∈ rel(vr , sh)⋆ .

By the hypothesis for this case we have S ∩ vyt = ∅ and thus Sx ∩ vyt = ∅ and
Sr ∩ vyt = ∅. This allows to state that


Sr ∈ rel vyt , rel(vr , sh)⋆ ,
Sx ∈ rel vyt , rel(vx , sh)⋆ ,
and hence, by Lemma 20,

⋆
Sx ∈ rel vyt , rel(vx , sh) ,

⋆
Sr ∈ rel vyt , rel(vr , sh) ,

⋆
Sx ∈ rel vx , rel(vyt , sh) ,

⋆
Sr ∈ rel vr , rel(vyt , sh) ,

⋆
Sx ∈ rel vx , amgu(sh, y 7→ t) ,

⋆
Sr ∈ rel vr , amgu(sh, y 7→ t) .

Thus, by Lemma 23,

so that, by (23), (24), and (25),

Therefore,


⋆
⋆ 
Sx ∪ Sr ∈ bin rel vx , amgu(sh, y 7→ t) , rel vr , amgu(sh, y 7→ t)
so that, as Sx ∪ Sr = S, it follows from (25) that

S ∈ amgu amgu(sh, y 7→ t), x 7→ r .
Case 2. Assume

⋆
⋆ 
S ∈ bin rel vy , amgu(sh, x 7→ r) , rel vt , amgu(sh, x 7→ r)
.

Then there exist Sy , St ∈ SG such that
S = Sy ∪ St

(61)

40

P. M. Hill, R. Bagnara and E. Zaffanella

where

Then, by Lemma 21,

⋆
Sy ∈ rel vy , amgu(sh, x 7→ r) ,
⋆
St ∈ rel vt , amgu(sh, x 7→ r) .
Sy ∩ vy 6= ∅,

St ∩ vt 6= ∅.

(62)

(63)

By (25) and Lemma 22, there exist R− , Rxr , T− , and Txr such that
Sy = R− ∪ Rxr ,

St = T− ∪ Txr

(64)

where
⋆
R− ∈ rel vy , rel(vxr , sh) ∪ {∅},

⋆
∪ {∅},
Rxr ∈ rel vy , bin rel(vx , sh)⋆ , rel(vr , sh)⋆
⋆
T− ∈ rel vt , rel(vxr , sh) ∪ {∅},

⋆
Txr ∈ rel vt , bin rel(vx , sh)⋆ , rel(vr , sh)⋆
∪ {∅}.

(65)

Then, by Lemmas 23 and 20,

R− ∈ rel vxr , rel(vy , sh)⋆ ∪ {∅},

T− ∈ rel vxr , rel(vt , sh)⋆ ∪ {∅}.

Also, using Lemmas 21, 19, and then the idempotence of (·)⋆ ,


Rxr ∈ rel vy , bin rel(vx , sh)⋆ , rel(vr , sh)⋆ ∪ {∅},


Txr ∈ rel vt , bin rel(vx , sh)⋆ , rel(vr , sh)⋆ ∪ {∅}.

(66)

(67)

Subcase 2a. Suppose Rxr = Txr = ∅. Then, by (64),
Sy = R− ,

St = T − .

By (63), R− , T− 6= ∅ and hence, using (66),

so that, by (25),


R− ∪ T− ∈ bin rel(vy , sh)⋆ , rel(vt , sh)⋆ ,
R− ∪ T− ∈ amgu(sh, y 7→ t).

Also, it follows from (66) that R− ∩ vxr = ∅ and T− ∩ vxr = ∅, so that

R− ∪ T− ∈ rel vxr , amgu(sh, y 7→ t) .
However, by (61) and (68), S = R− ∪ T− so that, by (25),

S ∈ amgu amgu(sh, y 7→ t), x 7→ r .

(68)

Soundness, Idempotence and Commutativity of Set-Sharing

41

Subcase 2b. Suppose Rxr ∪ Txr 6= ∅. Then, by (67),
(Rxr ∪ Txr ) ∩ vyt 6= ∅.

(69)

The proof of this subcase is in two parts. In the first part we divide Rxr and Txr
into a number of subsets. In the second part, these subsets will be reassembled so
as to prove the required result.
First, by (67), there exist Rx , Rr , Tx , Tr ∈ ℘f (Vars) such that
Rxr = Rx ∪ Rr ,

Txr = Tx ∪ Tr ,

(70)

where either Rx = Rr = ∅ or
Rx ∈ rel(vx , sh)⋆ ,

Rr ∈ rel(vr , sh)⋆ ,

and either Tx = Tr = ∅ or
Tx ∈ rel(vx , sh)⋆ ,

Tr ∈ rel(vr , sh)⋆ .

Thus, if either Rx ∪ Tx = ∅ or Rr ∪ Tr = ∅, it follows that
Rxr ∪ Txr = (Rx ∪ Rr ) ∪ (Tx ∪ Tr ) = ∅.
However, by (69), Rxr ∪ Txr 6= ∅, so that we have
Rx ∪ Tx 6= ∅,

Rr ∪ Tr 6= ∅.

(71)

We now subdivide the sets Rx , Tx , Rr , and Tr further. First note that

sh = rel(vyt , sh) ∪ rel(vy , sh) ∪ rel vy , rel(vt , sh) ,

sh = rel(vyt , sh) ∪ rel vt , rel(vy , sh) ∪ rel(vt , sh).

Hence, by Lemma 22, sets Rx− , Rxy , Rxt , Rr− , Rry , Rrt , Tx− , Txy , Txt , Tr− , Try ,
Trt ∈ ℘f (Vars) exist such that
Rx = Rx− ∪ Rxy ∪ Rxt ,

Tx = Tx− ∪ Txy ∪ Txt ,

Rr = Rr− ∪ Rry ∪ Rrt ,

Tr = Tr− ∪ Try ∪ Trt ,

(72)

where

and

and also

⋆
Rx− , Tx− ∈ rel vx , rel(vyt , sh) ∪ {∅},
⋆
Rr− , Tr− ∈ rel vr , rel(vyt , sh) ∪ {∅},
⋆
Rxy , Txy ∈ rel vx , rel(vy , sh) ∪ {∅},
⋆
Rry , Try ∈ rel vr , rel(vy , sh) ∪ {∅},
⋆
Rxt , Txt ∈ rel vx , rel(vt , sh) ∪ {∅},
⋆
Rrt , Trt ∈ rel vr , rel(vt , sh) ∪ {∅},
(Rx \ Rxy ) ∩ vy = ∅,

(Tx \ Txt ) ∩ vt = ∅,

(Rr \ Rry ) ∩ vy = ∅,

(Tr \ Trt ) ∩ vt = ∅.

(73)

(74)

(75)

42

P. M. Hill, R. Bagnara and E. Zaffanella

We note a few simple but useful consequences of these definitions. First, it follows
from (73) using (23), (24), and (25), that
⋆
Rx− , Tx− ∈ rel vx , amgu(sh, y 7→ t) ∪ {∅},
(76)
⋆
Rr− , Tr− ∈ rel vr , amgu(sh, y 7→ t) ∪ {∅}.

Secondly, using (73) with Lemma 21, we have

Rx− , Tx− , Rr− , Tr− ∈ rel(vyt , sh)⋆ ∪ {∅},

(77)

and then, using this with (69), (70), and (72), it follows that
Rxy ∪ Txy ∪ Rry ∪ Try ∪ Rxt ∪ Txt ∪ Rrt ∪ Trt 6= ∅.

(78)

In the second part of the proof for this subcase, the component subsets of S are
reassembled in an order that proves the required result. First, let
def

Uy = R− ∪ Rxy ∪ Rry ∪ Txy ∪ Try ,
def

(79)

Ut = T− ∪ Rxt ∪ Rrt ∪ Txt ∪ Trt ,
and
def

U = Uy ∪ Ut .

(80)

By relations (65) and (74) (with Lemma 21), each component set in the definition
of Uy is in rel(vy , sh)⋆ ∪ {∅} and each component set in the definition of Ut is in
rel(vt , sh)⋆ ∪ {∅}. Thus, by the definition of (·)⋆ ,
Uy ∈ rel(vy , sh)⋆ ∪ {∅},
Ut ∈ rel(vt , sh)⋆ ∪ {∅}.

(81)

By (70) and (75) we have

Rxr \ (Rxy ∪ Rry ) ∩ vy = ∅

and hence, by (64), we have also that


Sy \ (Rxy ∪ Rry ∪ R− ) ∩ vy = ∅.

By (63), Sy ∩ vy 6= ∅. Thus, Rxy ∪ Rry ∪ R− 6= ∅ and, as a consequence of (79),
Uy 6= ∅. For similar reasons, Ut 6= ∅. Hence, by (80),

U ∈ bin rel(vy , sh)⋆ , rel(vt , sh)⋆ ,
and therefore, using (25), it follows that

U ∈ amgu(sh, y 7→ t).

(82)

Now, by (78), at least one of the following two inequalities holds:
Rxy ∪ Txy ∪ Rxt ∪ Txt 6= ∅,
Rry ∪ Try ∪ Rrt ∪ Trt 6= ∅.

(83)

Soundness, Idempotence and Commutativity of Set-Sharing

43

Assume first that Rxy ∪ Txy ∪ Rxt ∪ Txt = ∅ and Rry ∪ Try ∪ Rrt ∪ Trt 6= ∅. Then,
using (71) and (72) with the first of these,
Rx− ∪ Tx− 6= ∅.
Also, using (74) with the second, we have (Rry ∪ Rrt ∪ Try ∪ Trt ) ∩ vr 6= ∅ and
therefore it follows from (79) and (80), that
U ∩ vr 6= ∅.
Hence, by (76) and (82),
⋆
Rx− ∪ Tx− ∈ rel vx , amgu(sh, y 7→ t) ,
⋆
U ∪ Rr− ∪ Tr− ∈ rel vr , amgu(sh, y 7→ t) .

(84)

Similarly, assuming Rxy ∪ Txy ∪ Rxt ∪ Txt 6= ∅ and Rry ∪ Try ∪ Rrt ∪ Trt = ∅ it
follows that
⋆
Rr− ∪ Tr− ∈ rel vr , amgu(sh, y 7→ t) ,
(85)
⋆
Rx− ∪ Tx− ∪ U ∈ rel vx , amgu(sh, y 7→ t) .
Finally, assuming Rxy ∪ Txy ∪ Rxt ∪ Txt =
6 ∅ and Rry ∪ Try ∪ Rrt ∪ Trt 6= ∅ it follows
from (74) that U ∩ vx 6= ∅ and U ∩ vr =
6 ∅, and hence
⋆
Rx− ∪ Tx− ∪ U ∈ rel vx , amgu(sh, y 7→ t) ,
(86)
⋆
U ∪ Rr− ∪ Tr− ∈ rel vr , amgu(sh, y 7→ t) .

Thus, as one of the inequalities in (83) holds, one of (84), (85) or (86) holds so that
Rx− ∪ Tx− ∪ U ∪ Rr− ∪ Tr−

⋆
⋆ 
.
∈ bin rel vx , amgu(sh, y 7→ t) , rel vr , amgu(sh, y 7→ t)

However, since

S = Rx− ∪ Tx− ∪ U ∪ Rr− ∪ Tr− ,
we have

⋆ 
⋆
S ∈ bin rel vx , amgu(sh, y 7→ t) , rel vr , amgu(sh, y 7→ t)
.
Hence, by (25),

S ∈ amgu amgu(sh, y 7→ t), x 7→ r .
6.5 Proofs of Results for Sharing Domains
We prove all the results in this section by induction on the cardinality of a substitution ν. For each result, the proof is obvious if ν is empty or does not unify. Thus,
in the following proofs, we assume that ν unifies and is non-empty. We suppose
def
that (x 7→ r) ∈ ν and let ν ′ = ν \ {x 7→ r}.

44

P. M. Hill, R. Bagnara and E. Zaffanella

Proof of Lemma 18.
We have

 
aunify Amgu (sh, U ), y 7→ t , ν


 

= aunify Amgu Amgu (sh, U ), y 7→ t , x 7→ r , ν ′


 

= aunify Amgu Amgu (sh, U ), x 7→ r , y 7→ t , ν ′



 ′
= Amgu aunify Amgu (sh, U ), x 7→ r , ν , y 7→ t



= Amgu aunify (sh, U ), ν , y 7→ t

[Def. 11]
[Cor. 3]
[induction]
[Def. 11].

Proof of Theorem 8.
Let µ′ be a most general solution for (ν ′ ∪ σ). Then
α(σ, U ) SS (sh, U )

=⇒ α µ′ , U ∪ vars(ν ′ )


SS aunify (sh, U ), ν ′

=⇒ α µ, U ∪ vars(ν)



SS Amgu aunify (sh, U ), ν ′ , x 7→ r

=⇒ α µ, U ∪ vars(ν)

 
SS aunify Amgu (sh, U ), x 7→ r , ν ′

=⇒ α µ, U ∪ vars(ν)

SS aunify (sh, U ), ν

[induction]

[Cor. 1]

[Lem. 18]

[Def. 11].

Proof of Theorem 9.
We have


 
aunify aunify (sh, U ), ν , ν


 

′
= aunify Amgu aunify Amgu((sh, U ), x 7→ r), ν , x 7→ r , ν ′



 ′ ′
= aunify aunify Amgu Amgu((sh, U ), x 7→ r), x 7→ r , ν , ν

 
= aunify Amgu Amgu((sh, U ), x 7→ r), x 7→ r , ν ′

 
= aunify Amgu (sh, U ), x 7→ r , ν ′

= aunify (sh, U ), ν

[Def. 11]
[Lem. 18]
[induction]
[Cor. 2]
[Def. 11].

Proof of Theorem 10.

The induction is on the set of equations ν1 . The comments at the start of this
def
section apply therefore to ν1 instead of ν and thus we let ν1′ = ν1 \ {x 7→ r} so

Soundness, Idempotence and Commutativity of Set-Sharing
that we have

 
aunify aunify (sh, U ), ν1 , ν2



 ′
= aunify aunify Amgu (sh, U ), x 7→ r , ν1 , ν2



  ′
= aunify aunify Amgu (sh, U ), x 7→ r , ν2 , ν1

 


= aunify Amgu aunify (sh, U ), ν2 , x 7→ r , ν1′

 
= aunify aunify (sh, U ), ν2 , ν1

45

[Def. 11]
[induction]
[Lem. 18]
[Def. 11].

7 Conclusion
The Sharing domain, which was defined in (Jacobs and Langen 1989, Langen 1990),
is considered to be the principal abstract domain for sharing analysis of logic programs in both practical work and theoretical study. For many years, this domain
was accepted and implemented as it was. However, in (Bagnara et al. 1997), we
proved that Sharing is, in fact, redundant for pair-sharing and we identified the
weakest abstraction of Sharing that can capture pair-sharing with the same degree
of precision. One notable advantage of this abstraction is that the costly star-union
operator is no longer necessary. The question of whether the abstract operations
for Sharing were complete or optimal was studied by Cortesi and Filé (Cortesi and
Filé 1999). Here it is proved that although the ‘⊔’ and projection operations are
complete (and hence, optimal), aunify is optimal but not complete. The problem
of scalability of Sharing, still retaining as much precision as possible, was tackled in
(Zaffanella, Bagnara and Hill 1999a), where a family of widenings is presented that
allow the desired goal to be achieved. In (Zaffanella, Hill and Bagnara 1999b, Zaffanella, Hill and Bagnara 2001), the decomposition of Sharing and its non-redundant
counterpart via complementation is studied. This shows the close relationship between these domains and PS (the usual domain for pair-sharing) and Def (the
domain of definite Boolean functions). Many sharing analysis techniques and/or
enhancements have been advocated to have potential for improving the precision
of the sharing information over and above that obtainable using the classical combination of Sharing with the usual domains for linearity and freeness. Moreover,
these enhancements had been circulating for years without an adequate supporting experimental evaluation. Thus we investigated these techniques to see if and
by how much they could improve precision. Using the China analyzer (Bagnara
1997) for the experimental part of the work, we discovered that, apart from the
enhancement that upgrades Sharing with structural information, these techniques
had little impact on precision (Bagnara, Zaffanella and Hill 2000).
In this paper, we have defined a new abstraction function mapping a set of substitutions in rational solved form into their corresponding sharing abstraction. The
new function is a generalisation of the classical abstraction function of (Jacobs and
Langen 1989), which was defined for idempotent substitutions only. Using our new

46

P. M. Hill, R. Bagnara and E. Zaffanella

abstraction function, we have proved the soundness of the classical abstract unification operator aunify. Other contributions of our work are the formal proofs of
the commutativity and idempotence of the aunify operator on the Sharing domain.
Even if commutativity was a known property, the corresponding proof in (Langen
1990) was not satisfactory. As far as idempotence is concerned, our result differs
from that given in (Langen 1990), which was based on a composite abstract unification operator performing also the renaming of variables. It is our opinion that our
main result, the soundness of the aunify operator, is really valuable as it allows for
the safe application of sharing analysis based on Sharing to any constraint logic language supporting syntactic term structures, based on either finite trees or rational
trees. This happens because our result does not rely on the presence (or even the
absence) of the occurs-check in the concrete unification procedure implemented by
the analysed language. Furthermore, as the groundness domain Def is included in
Sharing, our main soundness result also shows that Def is sound for non-idempotent
substitutions.
From a technical point of view, we have introduced a new class of concrete substitutions based on the notion of variable-idempotence, generalizing the classical
concept of idempotence. We have shown that any substitution is equivalent to a
variable-idempotent one, providing a finite sequence of transformations for its construction. This result assumes an arbitrary equality theory and is therefore applicable to the study of any abstract property which is preserved by logical equivalence.
Our application of this idea to the study of the soundness of abstract unification
for Sharing has shown that it is particularly suitable for data-flow analyzers where
the corresponding abstraction function only depends on the set of variables occurring in a term. However, we believe that this concept can be usefully exploited
in a more general context. Possible applications include the proofs of optimality
and completeness of abstract operators with respect to the corresponding concrete
operators defined on a domain of substitutions in rational solved form.
References
Bagnara, R. (1997). Data-Flow Analysis for Constraint Logic-Based Languages, PhD thesis,
Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56125 Pisa, Italy.
Printed as Report TD-1/97.
Bagnara, R., Hill, P. M. and Zaffanella, E. (1997). Set-sharing is redundant for pairsharing, in P. Van Hentenryck (ed.), Static Analysis: Proceedings of the 4th International
Symposium, Vol. 1302 of Lecture Notes in Computer Science, Springer-Verlag, Berlin,
Paris, France, pp. 53–67.
Bagnara, R., Hill, P. M. and Zaffanella, E. (2001). Set-sharing is redundant for pair-sharing,
Theoretical Computer Science. To appear.
Bagnara, R., Zaffanella, E. and Hill, P. M. (2000). Enhanced sharing analysis techniques:
A comprehensive evaluation, in M. Gabbrielli and F. Pfenning (eds), Proceedings of the
2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative
Programming, Association for Computing Machinery, Montreal, Canada, pp. 103–114.
Bruynooghe, M. and Codish, M. (1993). Freeness, sharing, linearity and correctness — All at
once, in P. Cousot, M. Falaschi, G. Filé and A. Rauzy (eds), Static Analysis, Proceedings
of the Third International Workshop, Vol. 724 of Lecture Notes in Computer Science,

Soundness, Idempotence and Commutativity of Set-Sharing

47

Springer-Verlag, Berlin, Padova, Italy, pp. 153–164. An extended version is available as
Technical Report CW 179, Department of Computer Science, K.U. Leuven, September
1993.
Clark, K. L. (1978). Negation as failure, in H. Gallaire and J. Minker (eds), Logic and
Databases, Plenum Press, Toulouse, France, pp. 293–322.
Codish, M., Dams, D., Filé, G. and Bruynooghe, M. (1996). On the design of a correct
freeness analysis for logic programs, Journal of Logic Programming 28(3): 181–206.
Colmerauer, A. (1982). Prolog and infinite trees, in K. L. Clark and S. Å. Tärnlund (eds),
Logic Programming, APIC Studies in Data Processing, Vol. 16, Academic Press, New
York, pp. 231–251.
Colmerauer, A. (1984). Equations and inequations on finite and infinite trees, Proceedings
of the International Conference on Fifth Generation Computer Systems (FGCS’84),
ICOT, Tokyo, Japan, pp. 85–99.
Cortesi, A. and Filé, G. (1999).
38(3): 371–386.

Sharing is optimal, Journal of Logic Programming

Hill, P. M., Bagnara, R. and Zaffanella, E. (1998). The correctness of set-sharing, in G. Levi
(ed.), Static Analysis: Proceedings of the 5th International Symposium, Vol. 1503 of
Lecture Notes in Computer Science, Springer-Verlag, Berlin, Pisa, Italy, pp. 99–114.
ISO/IEC (1995). ISO/IEC 13211-1: 1995 Information technology — Programming languages — Prolog — Part 1: General core, International Standard Organization.
Jacobs, D. and Langen, A. (1989). Accurate and efficient approximation of variable aliasing
in logic programs, in E. L. Lusk and R. A. Overbeek (eds), Logic Programming: Proceedings of the North American Conference, MIT Press Series in Logic Programming,
The MIT Press, Cleveland, Ohio, USA, pp. 154–165.
Jacobs, D. and Langen, A. (1992). Static analysis of logic programs for independent AND
parallelism, Journal of Logic Programming 13(2&3): 291–314.
Jaffar, J., Lassez, J.-L. and Maher, M. J. (1987). Prolog-II as an instance of the logic programming scheme, in M. Wirsing (ed.), Formal Descriptions of Programming Concepts
III, North-Holland, pp. 275–299.
Keisu, T. (1994). Tree Constraints, PhD thesis, The Royal Institute of Technology, Stockholm, Sweden. Also available in the SICS Dissertation Series: SICS/D–16–SE.
King, A. (1994). A synergistic analysis for sharing and groundness which traces linearity, in
D. Sannella (ed.), Proceedings of the Fifth European Symposium on Programming, Vol.
788 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Edinburgh, UK,
pp. 363–378.
King, A. (2000). Pair-sharing over rational trees, Journal of Logic Programming 46(1–
2): 139–155.
King, A. and Soper, P. (1994). Depth-k sharing and freeness, in P. Van Hentenryck (ed.),
Logic Programming: Proceedings of the Eleventh International Conference on Logic Programming, MIT Press Series in Logic Programming, The MIT Press, Santa Margherita
Ligure, Italy, pp. 553–568.
Langen, A. (1990). Advanced Techniques for Approximating Variable Aliasing in Logic Programs, PhD thesis, Computer Science Department, University of Southern California.
Printed as Report TR 91-05.
Maher, M. J. (1988). Complete axiomatizations of the algebras of finite, rational and
infinite trees, Proceedings, Third Annual Symposium on Logic in Computer Science,
IEEE Computer Society, Edinburgh, Scotland, pp. 348–357.
Martelli, A. and Montanari, U. (1982). An efficient unification algorithm, ACM Transactions on Programming Languages and Systems 4(2): 258–282.

48

P. M. Hill, R. Bagnara and E. Zaffanella

Muthukumar, K. and Hermenegildo, M. (1992). Compile-time derivation of variable dependency using abstract interpretation, Journal of Logic Programming 13(2&3): 315–347.
Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle, Journal
of the ACM 12(1): 23–41.
Zaffanella, E., Bagnara, R. and Hill, P. M. (1999a). Widening Sharing, in G. Nadathur
(ed.), Principles and Practice of Declarative Programming, Vol. 1702 of Lecture Notes
in Computer Science, Springer-Verlag, Berlin, Paris, France, pp. 414–431.
Zaffanella, E., Hill, P. M. and Bagnara, R. (1999b). Decomposing non-redundant sharing
by complementation, in A. Cortesi and G. Filé (eds), Static Analysis: Proceedings of the
6th International Symposium, Vol. 1694 of Lecture Notes in Computer Science, SpringerVerlag, Berlin, Venice, Italy, pp. 69–84.
Zaffanella, E., Hill, P. M. and Bagnara, R. (2001). Decomposing non-redundant sharing by
complementation, Theory and Practice of Logic Programming. To appear.

