Under consideration for publication in Theory and Practice of Logic Programming

1

On the interaction between sharing and linearity

arXiv:0710.0528v2 [] 28 Jul 2009

GIANLUCA AMATO and FRANCESCA SCOZZARI
Dipartimento di Science, Università “G. d’Annunzio” di Chieti-Pescara, Pescara, Italy.
(e-mail: amato@sci.unich.it, scozzari@sci.unich.it)
submitted 26 March 2008; revised 3 July 2008, 15 July 2009; accepted 27 July 2009

Abstract
In the analysis of logic programs, abstract domains for detecting sharing and linearity
information are widely used. Devising abstract unification algorithms for such domains
has proved to be rather hard. At the moment, the available algorithms are correct but not
optimal, i.e., they cannot fully exploit the information conveyed by the abstract domains.
In this paper, we define a new (infinite) domain ShLinω which can be thought of as a
general framework from which other domains can be easily derived by abstraction. ShLinω
makes the interaction between sharing and linearity explicit. We provide a constructive
characterization of the optimal abstract unification operator on ShLinω and we lift it to
two well-known abstractions of ShLinω . Namely, to the classical Sharing × Lin abstract
domain and to the more precise ShLin2 abstract domain by Andy King. In the case of
single binding substitutions, we obtain optimal abstract unification algorithms for such
domains.
KEYWORDS: Static analysis, abstract interpretation, sharing, linearity, unification.

1 Introduction
In the analysis of logic programs, the theory of abstract interpretation (Cousot
and Cousot 1979; Cousot and Cousot 1992a) has been widely used to design new
analyses and to improve existing ones. Given a concrete semantics working over a
concrete domain, an abstract interpretation formalizes an analysis by providing an
abstract domain and an abstract semantics (working on the abstract domain), and
relating them to their concrete counterparts. An abstract domain is a collection of
abstract objects which encode the property to analyze. The concrete and abstract
domains are related by means of abstraction and concretization maps, which allow
each concrete object to be abstracted into an abstract object which describes it.
The abstract semantics, in most cases, is given by a set of abstract operators on
the abstract domain, which are the counterparts of the concrete ones. For example, in the case of logic programs, one can individuate in the concrete semantics
the main operations (unification, projection, union), and an abstract semantics can
be specified by giving the abstract unification, abstract projection and abstract
union operations. The theory of abstract interpretation assures us that, for any
concrete operator, there exists a best abstract operator, called the optimal operator. It computes the most precise result among all possible correct operators, on a

2

G. Amato and F. Scozzari

given abstract domain. Designing the optimal abstract counterpart of each concrete
operator is often a very difficult task. In fact, even if the definition of the optimal
operator for any abstract domain is known from the theory of abstract interpretation (as a composition of the concrete operator and the abstraction map), the
hard task is to provide an explicit definition of the abstract operators and to devise
algorithms on the abstract domain which compute them.
1.0.1 The context
The property of sharing has been the subject of many papers (Jacobs and Langen
1992; Hans and Winkler 1992; Muthukumar and Hermenegildo 1992; Codish et al.
1999; Bagnara et al. 2002), from the both theoretical and practical point of view.
Typical applications of sharing analysis are in the fields of optimization of unification (Søndergaard 1986) and parallelization of logic programs (Hermenegildo and
Rossi 1995). The goal of (set) sharing analysis is to detect sets of variables which
share a common variable in the answer substitutions. For instance, consider the
substitution {x/f (u, v), y/g(u, u, u), z/v}. We say that x and y share the variable
u, while x and z share the variable v, and no single variable is shared by x, y and
z. Many domains concerning sharing properties also consider linearity in order to
improve the precision of the analysis. We say that a term is linear if it does not contain multiple occurrences of the same variable. For instance, the term f (x, f (y, z))
is linear, while f (x, f (y, x)) is not, since x occurs twice.
1.0.2 The problem
It is now widely recognized that the original domain proposed for sharing analysis, namely, Sharing (Langen 1990; Jacobs and Langen 1992), is not very precise,
so that it is often combined with other domains for handling freeness, linearity,
groundness or structural information (see Bagnara et al. 2005 for a comparative
evaluation). In particular, adding some kind of linearity information seems to be
very profitable, both for the gain in precision and speed which can be obtained, and
for the fact that it can be easily and elegantly embedded inside the sharing groups
(see King 1994). In the literature, many authors have proposed abstract unification operators (e.g. Codish et al. 1991; Hans and Winkler 1992; Muthukumar and
Hermenegildo 1992; King 1994) for domains of sharing properties, encoding different amounts of linearity information. However, optimal operators for combined
analysis of sharing and linearity have never been devised, neither for the domain
ShLin2 (King 1994), nor for the more broadly adopted Sharing × Lin (Hans and
Winkler 1992; Muthukumar and Hermenegildo 1992).
With the lack of optimal operators, the analysis loses precision and might even
be slower. The latter is typical of sharing analysis, where abstract domains are
usually defined in such a way that, the less information we have, the more complex
the abstract objects are. This is not the case for other kinds of analyses, such as
groundness analysis, where the complexity of abstract objects may grow accordingly
to the amount of groundness information they encode.

On the interaction between sharing and linearity

3

The lack of optimal operators is due to the fact that the role played by linearity
in the unification process has never been fully clarified. The traditional domains
which combine sharing and linearity information are too abstract to capture in a
clean way the effect of repeated occurrences of a variable in a term and most of the
effects of (non-)linearity are obscured by the abstraction process.

1.0.3 The solution
We propose an abstract domain ShLinω which is able to encode the amount of nonlinearity, i.e., which keeps track of the exact number of occurrences of the same variable in a term. Consider again the substitution θ = {x/f (u, v), y/g(u, u, u), z/v}.
Intuitively, to each variable w in the range of the substitution, we associate the
multiset of domain variables which are bound to a term where w occurs, and call
it an ω-sharing group. For instance, we associate, to the variable u, the ω-sharing
group {x, y, y, y}, to denote that u appears once in θ(x) and three times in θ(y). To
the variable v, we associate the ω-sharing group {x, z}, to denote that v appears
once in θ(x) and once in θ(z). Then we consider the collection of all the multisets
so obtained {{x, y, y, y}, {x, z}}, which describes both the sharing property and
the exact amount of non-linearity in the given substitution. The domain we obtain
is conceptually simple, but cannot be directly used for static analysis, without a
widening operator (Cousot and Cousot 1992c), since it contains infinite ascending
chains. However, in this domain the role played by (non-)linearity is manifest, and
we can provide a constructive characterization of the optimal abstract unification
operator. The cornerstone of the abstract unification is the concept of sharing graph
which plays the same role as alternating paths (Søndergaard 1986; King 2000) for
pair-sharing analysis. We use sharing graphs to combine different ω-sharing groups
during unification. The use of sharing graphs offers a new perspective for looking
at variables in the process of unification, and simplifies the proofs of correctness
and optimality of the abstract operators.
We prove that sharing graphs yield an optimal abstract unification operator for
single binding substitutions. We also provide a purely algebraic characterization
of the unification process, which should help in implementing the domain through
widening operators and in devising abstract operators for further abstractions of
ShLinω .

1.0.4 The applications
We consider two well-known domains for sharing properties, namely, the reduced
product (Cousot and Cousot 1979) Sharing × Lin and the more precise domain
ShLin2 by Andy King, and show that they can be immediately obtained as abstractions of ShLinω . By exploiting the unification operator on ShLinω , we provide the
optimal abstract unification operators, in the case of single binding substitutions,
for both domains. We show that we gain in precision w.r.t. any previous attempt
to design an abstract unification operator on these domains. This is the first time

4

G. Amato and F. Scozzari

that abstract unification has been provided optimal for a domain including sharing
and linearity information.
Surprisingly, the optimal abstract operators are able to improve not only aliasing
and linearity information, but also groundness. We show that, in certain cases, we
improve over Pos (Armstrong et al. 1994). This is mainly due to the fact that our
operators exploits the occur-check condition. As far as we know, there is no abstract
unification operator in the literature, for a domain dealing with sharing, freeness
and linearity, which is more precise than Def for groundness.
Unification for multi-binding substitutions is usually computed by considering
one binding at a time. For instance, the unification of a substitution θ with {x1 /t1 ,
x2 /t2 , . . . , xn /tn } is performed by first computing the unification of θ with {x1 /t1 },
and then unifying the result with {x2 /t2 , . . . , xn /tn }. Actually, computing abstract
unification one binding at a time is optimal in ShLinω (Amato and Scozzari 2005).
We show that this is not the case for ShLin2 and Sharing × Lin. This means that
the classical schema of computing unification iteratively on the number of bindings
cannot be used when looking for optimality with multi-binding substitutions, at
least with these two domains.
1.0.5 Structure of the article
In Section 2 we recall some basic notions and the notations about substitutions,
multisets and abstract interpretation. In Section 3 we briefly recall the domain of
existential substitutions and its operators, which will be used throughout the article.
In Section 4 we define the domain ShLinω , together with the unification operator,
we show the optimality result and give an alternative algebraic characterization of
the unification operator. In Section 5 we exploit our results to devise the optimal
unification operators for ShLin2 and Sharing × Lin, in the case of single binding
substitutions. Section 6 gives some evidence that there are practical advantages in
using the optimal unification operators for ShLin2 and Sharing × Lin. In Section
7 we compare our domains and operators with those known in the literature. We
conclude with some open questions for future work. The proofs of the main results
of the paper are in Appendix A, and the proofs of the results in Section 5 are in
Appendix B.
The paper is a substantial expansion of (Amato and Scozzari 2003), which introduces preliminary results of optimality for domains involving sharing and linearity
properties.
2 Notation
Given a set A, let ℘(A) be the powerset of A and ℘f (A) be the set of finite subsets
of A. Given two posets (A, ≤A ) and (B, ≤B ), we denote by A → B the poset of
monotonic functions from A to B ordered pointwise. We use ≤A→B to denote the
order relation over A → B. When an order for A or B is not specified, we assume
the least informative order (x ≤ y ⇐⇒ x = y). We also use A ⊎ B to denote
disjoint union and |A| for the cardinality of the set A.

On the interaction between sharing and linearity

5

2.1 Terms and substitutions
In the following, we fix a first order signature and a denumerable set of variables V.
Given a term or other syntactic object o, we denote by vars(o) the set of variables
occurring in o and by occ(v, o) the number of occurrences of v in o. When it does
not cause ambiguities, we abuse the notation and prefer to use o itself in the place
of vars(o). For example, if t is a term and x ∈ V, then x ∈ t should be read as
x ∈ vars(t).
We denote by ǫ the empty substitution, by {x1 /t1 , . . . , xn /tn } a substitution
θ with θ(xi ) = ti 6= xi , by dom(θ) = {x ∈ V | θ(x) 6= x} and rng(θ) =
∪x∈dom(θ) vars(θ(x)) the domain and range of θ respectively. Let vars(θ) be the
set dom(θ) ∪ rng(θ) and, given U ∈ ℘f (V), let θ|U be the projection of θ over U ,
i.e., the unique substitution such that θ|U (x) = θ(x) if x ∈ U and θ|U (x) = x
otherwise. Given θ1 and θ2 two substitutions with disjoint domains, we denote by
θ1 ⊎ θ2 the substitution θ such that dom(θ) = dom(θ1 ) ∪ dom(θ2 ) and θ(x) = θi (x)
if x ∈ dom(θi ), for each i ∈ {1, 2}. The application of a substitution θ to a term t is
written as tθ or θ(t). Given two substitutions θ and δ, their composition, denoted
by θ ◦ δ, is given by (θ ◦ δ)(x) = θ(δ(x)). A substitution θ is idempotent when
θ ◦ θ = θ or, equivalently, when dom(θ) ∩ rng(θ) = ∅. A substitution ρ is called
renaming if it is a bijection from V to V (this is equivalent to saying that there
exists a substitution ρ−1 such that ρ ◦ ρ−1 = ρ−1 ◦ ρ = ǫ). Instantiation induces
a preorder on substitutions: θ is more general than δ, denoted by δ ≤ θ, if there
exists σ such that σ ◦ θ = δ. If ≈ is the equivalence relation induced by ≤, we
say that σ and θ are equal up to renaming when σ ≈ θ. The sets of substitutions,
idempotent substitutions and renamings are denoted by Subst, ISubst and Ren respectively. Given a set of equations E, we write σ = mgu(E) to denote that σ is a
most general unifier of E. Any idempotent substitution σ is a most general unifier
of the corresponding set of equations Eq(σ) = {x = σ(x) | x ∈ dom(σ)}. In the following, we will abuse the notation and denote by mgu(σ1 , . . . , σn ) the substitution
mgu(Eq(σ1 ) ∪ . . . ∪ Eq(σn )), when it exists. In spite of a single binding substitution
{x/t} we often use just the binding x/t. In the rest of the paper we assume that a
binding x/t is idempotent, namely,that x ∈
/ vars(t).
A position is a sequence of positive natural numbers. We denote with Ξ the set
of all positions and with N+ the set of all positive natural numbers. Given a term
t and a position ξ, we define t(ξ) inductively as follows:
t(ǫ) = t
(

t(i · ξ ′ ) =

(where ǫ denotes the empty sequence)
ti (ξ ′ )

if t ≡ f (t1 , . . . , tn ) and i ≤ n;

undefined otherwise.

For any variable x, an occurrence of x in t is a position ξ such that t(ξ) = x.
In the rest of the paper, we use: U , V , W to denote finite sets of variables;
h, k, u, v, w, x, y, z for variables; t for terms; f, r, s for term symbols; a, b for constants; η, θ, σ, δ for substitutions; ρ for renamings.

6

G. Amato and F. Scozzari
2.2 Multisets

A multiset is a set where repetitions are allowed. We denote by {{x1 , . . . , xm }} a
multiset, where x1 , . . . , xm is a sequence with (possible) repetitions. We denote by
{{}} the empty multiset. We will often use the polynomial notation v1i1 . . . vnin , where
v1 , . . . , vn is a sequence without repetitions, to denote a multiset A whose element
vj appears ij times. The set {vj | ij > 0} is called the support of A and is denoted
by TAU. We also use the functional notation A : {v1 , . . . , vn } → N, where A(vj ) = ij .
In this paper, we only consider multisets whose support is finite. We denote with
℘m (X) the set of all the multisets whose support is any finite subset of X. For
example, both a2 c4 and a1 b2 c3 are elements of ℘m ({a, b, c}). The cardinality of a
P
multiset is |A| = v∈TAU A(v).
The new fundamental operation for multisets is the sum, defined as
A ⊎ B = λv ∈ TAU ∪ TBU.A(v) + B(v) .
Multiset sum is associative, commutative and {{}} is the neutral element. Note that
we also use ⊎ to denote disjoint union for standard sets. The context will allow us
to identify the proper semantics of ⊎.
Given a multiset A and X ⊆ TAU, the restriction of A over X, denoted by A|X ,
is the only multiset B such that TBU = X and B(v) = A(v) for each v ∈ X. Finally,
if A ∈ ℘m (X), E[x] is an integer expression and x ∈ X, we define
X
X
A(x) · E[x] .
E[x] =
x∈A

x∈TAU

For example, given a multiset A = {{5, 5, 6, 8, 8, 8}} then
3 ∗ 82 = 278.

P

2
x∈A x

= 2 ∗ 52 + 62 +

2.3 Abstract interpretation
Given two sets C and A of concrete and abstract objects respectively, an abstract
interpretation (Cousot and Cousot 1992b) is given by an approximation relation
3 ⊆ A × C. When a 3 c holds, this means that a is a correct abstraction of c. In
particular, we are interested in the case when (A, ≤A ) is a poset and a ≤A a′ means
that a is more precise than a′ . In this case we require that, if a 3 c and a ≤A a′ ,
then a′ 3 c, too. In more detail, we require what Cousot and Cousot (1992b) call the
existence of a best abstract approximation assumption, i.e., the existence of a map
α : C → A such that for all a ∈ A, c ∈ C, it holds that a 3 c ⇐⇒ α(c) ≤A a. The
map α is called the abstraction function and maps each c to its best approximation
in A.
Given a (possibly partial) function f : C → C, we say that f˜ : A → A is a correct
abstraction of f , and write f˜ 3 f , whenever
a 3 c ⇒ f˜(a) 3 f (c) ,
assuming that f˜(a) 3 f (c) is true whenever f (c) is not defined. We say that f˜ :
A → A is the optimal abstraction of f when it is the best correct approximation of

On the interaction between sharing and linearity

7

f , i.e., when f˜ 3 f and
∀f ′ : A → A. f ′ 3 f ⇒ f˜ ≤A→A f ′ .
In some cases, we prefer to deal with a stronger framework, in which the domain
C is also endowed with a partial order ≤C and α : C → A is a left adjoint to
γ : A → C, i.e.,
∀c ∈ C.∀a ∈ A.α(c) ≤A a ⇐⇒ c ≤C γ(a) .
The pair hα, γi is called a Galois connection. In particular, we will only consider
the case of Galois insertions, which are Galois connections such that α ◦ γ is the
identity map. If hα, γi is a Galois insertion and f : C → C is a monotone map, the
optimal abstraction f˜ always exists and it is definable as f˜ = α ◦ f ◦ γ.
3 The domain of existential substitutions
The choice of the concrete domain depends on the observable properties we want
to analyze. Most of the semantics suited for the analysis of logic programs are
based on computed answer substitutions, and most of the domains are expressed
as abstractions of sets of substitutions. In general, we are not really interested
in the substitutions, but in their quotient-set w.r.t. an appropriate equivalence
relation. Let us consider a one-clause program p(x, x), the goal p(x, y), and the
following answer substitutions: θ1 = {y/x}, θ2 = {x/y}, θ3 = {x/u, y/u} and
θ4 = {x/v, y/v}. Although θ1 and θ2 are equal up to renaming, the same does
not hold for θ3 and θ4 . Nonetheless, they essentially represent the same answer,
since u and v are just two different variables we chose when renaming apart the
clause p(x, x) from the goal p(x, y), and therefore are not relevant to the user.
On the other hand, if θ3 and θ4 are answer substitutions for the goal q(x, y, u),
then they correspond to computed answers q(u, u, u) and q(v, v, u) and therefore
are fundamentally different. As a consequence, the equivalence relation we need
to consider must be coarser then renaming, and must take into account the set
of variables of interest, i.e., the set of variables which appear in the goal. For
these reasons, we think that the best solution is to use a domain of equivalence
classes of substitutions. Among the various domains proposed in the literature (e.g.
Jacobs and Langen 1992; Marriott et al. 1994; Levi and Spoto 2003), we adopt the
domain of existential substitutions (Amato and Scozzari 2009), since it is explicitly
defined as a quotient of a set of substitutions, w.r.t. a suitable equivalence relation.
Moreover, the domain is equipped with all the necessary operators for defining a
denotational semantics, namely, projection, renaming and unification. We briefly
recall the basic definitions of the domain and the unification operator.
Given θ1 , θ2 ∈ Subst and U ∈ ℘f (V), the preorder U is defined as follows:
θ1 U θ2 ⇐⇒ ∃δ ∈ Subst.∀x ∈ U. θ1 (x) = δ(θ2 (x)) .
The notation θ1 U θ2 states that θ1 is an instance of θ2 w.r.t. the variables in
U . The equivalence relation induced by the preorder U is given by:
θ1 ∼U θ2 ⇐⇒ ∃ρ ∈ Ren.∀x ∈ U. θ1 (x) = ρ(θ2 (x)) .

8

G. Amato and F. Scozzari

This relation precisely captures the extended notion of renaming which is needed
to work with computed answer substitutions.
Example 3.1
It is easy to check that {x/w, y/u} ∼{x,y} ǫ by choosing the renaming ρ = {x/w,
w/x, y/u, u/y}. Note that ∼U is coarser than the standard equivalence relation ≈:
there is no renaming ρ such that ǫ = ρ ◦ {x/w, y/u}. As it happens for , if we
enlarge the set of variables of interest, not all equivalences between substitutions
are preserved: for instance, {x/w, y/u} 6∼{w,x,y} ǫ.
Let ISubst ∼U be the quotient set of ISubst w.r.t. ∼U . The domain ISubst ∼ of
existential substitutions is defined as the disjoint union of all the ISubst ∼U for
U ∈ ℘f (V), namely:
]
ISubst ∼U .
ISubst ∼ =
U∈℘f (V)

In the following we write [θ]U for the equivalence class of θ w.r.t. ∼U . The partial
order  over ISubst ∼ is given by:
[θ]U  [θ′ ]V ⇐⇒ U ⊇ V ∧ θ V θ′ .

Intuitively, [θ]U  [θ′ ]V means that θ is an instance of θ′ w.r.t. the variables in V ,
provided that they are all variables of interest of θ.
To ease notation, we often omit braces from the sets of variables of interest when
they are given extensionally. So we write [θ]x,y instead of [θ]{x,y} and ∼x,y,z instead
of ∼{x,y,z}. When the set of variables of interest is clear from the context or when
it is not relevant, it will be omitted. Finally, we omit the braces which enclose the
bindings of a substitution when the latter occurs inside an equivalence class, i.e.,
we write [x/y]U instead of [{x/y}]U .
3.0.1 Unification
Given U, V ∈ ℘f (V), [θ1 ]U , [θ2 ]V ∈ ISubst ∼ , the most general unifier between these
two classes is defined as the mgu of suitably chosen representatives, where variables
not of interest are renamed apart. In formulas:
mgu([θ1 ]U , [θ2 ]V ) = [mgu(θ1′ , θ2′ )]U∪V ,

(1)

where θ1 ∼U θ1′ ∈ ISubst, θ2 ∼V θ2′ ∈ ISubst and (U ∪ vars(θ1′ )) ∩ (V ∪ vars(θ2′ )) ⊆
U ∩ V . The last condition is needed to avoid variable clashes between the chosen
representatives θ1′ and θ2′ . Moreover, mgu is the greatest lower bound of ISubst ∼
ordered by .
Example 3.2
Let θ1 = {x/a, y/r(v1 , v1 , v2 )} and θ2 = {y/r(a, v2 , v1 ), z/b}. Then
mgu([θ1 ]x,y , [θ2 ]y,z ) = [x/a, y/r(a, a, v), z/b]x,y,z ,
by choosing θ1′ = θ1 and θ2′ = {y/r(a, w, v), z/b}. In this case we have

9

On the interaction between sharing and linearity
{x/a, y/r(a, a, v), z/b} ∼x,y,z
mgu(θ1′ , θ2′ ) = {x/a, y/r(a, a, v), z/b, v1/a, w/a, v2 /v} .

A different version of unification is obtained when one of the two arguments is
an existential substitution, and the other one is a standard substitution. In this
case, the latter argument may be viewed as an existential substitution where all
the variables are of interest:
mgu([θ]U , δ) = mgu([θ]U , [δ]vars(δ) ) .

(2)

Note that deriving the general unification in (1) from the special case in (2) is not
possible. This is because there are elements in ISubst ∼ which cannot be obtained
as [δ]vars(δ) for any δ ∈ ISubst (see Example 4.10).
This is the form of unification which is better suited for analysis of logic programs, where existential substitutions are the denotations of programs while standard substitutions are the result of unification between goals and heads of clauses.
Therefore, the rest of the paper will be concerned with the problem of devising optimal abstract operators corresponding to (2), for three different abstract domains.
Of course, unification is not the only operator needed to give semantics to logic
programs: we also need projection, renaming and union. However, providing optimal abstract counterparts for these operators is generally a trivial task, and will
not be considered here.
We want to conclude the section with a small remark about our choice of the concrete domain. By adopting existential substitutions and the corresponding notion of
unification, we greatly simplify all the semantic definitions which are heavily based
on renaming variables apart. This is because all the details concerning renamings
are shifted towards the inner level of the semantic domain, where they are more
easily managed (Jacobs and Langen 1992; Amato and Scozzari 2009).

4 The abstract domain ShLinω
The domain Sharing × Lin is one of the best known domains in the literature
which combine sharing and linearity information. The domain Sharing records the
information of variable aliasing, by abstracting the substitution θ = {x/f (u, v),
y/g(u, u, u), z/v} into the set {uxy, vxz}. The object uxy, called a sharing group,
states that θ(u), θ(x) and θ(y) do share some variable (the variable u in this case).
Analogously, the sharing group vxz states that θ(v), θ(x) and θ(z) do share (in this
case the variable v). One of the simplest way of adding linearity information is to
record, in a separate object, the set of variables w such that θ(w) is a linear term. In
our example, only θ(y) is not linear. Thus the substitution is abstracted into the pair
({uxy, vxz}, {u, v, x, z}). Another known domain in the literature is ASub whose
main difference w.r.t. Sharing × Lin is that it only records sharing information
between pairs of variables. Thus, in ASub, each sharing group has at most two
elements. Developing optimal unification operators for such abstract domains is a
difficult task. In our opinion, this is because the gap between the substitutions and

10

G. Amato and F. Scozzari

Sharing×Lin (or ASub) is too wide and the combined effect of aliasing and linearity
is difficult to grasp.
We solve this problem by defining a new abstract domain ShLinω which can be
used to approximate ISubst ∼ . Since ShLinω has infinite ascending chains, in most
cases it cannot be directly used for the analysis. It should be thought of as a general
framework from which other domains can be easily derived by abstraction. In this
sense, ShLinω closes the gap between the concrete domain of substitutions and
the abstractions like Sharing × Lin or ASub. The structure of ShLinω has made it
possible to develop clean and optimal abstract unification operators. From these,
optimal operators for the simpler domains are easy to obtain, at least for single
binding substitutions.
The idea underlying ShLinω is to count the exact number of occurrences of the
same variable in a term. It extends the standard domain Sharing by recording, for
each v ∈ V and θ ∈ ISubst, not only the set {w ∈ V | v ∈ θ(w)} but the multiset
λw ∈ V.occ(v, θ(w)).
Definition 4.1 (ω-Sharing Group)
An ω-sharing group is a multiset of variables, i.e., an element of ℘m (V).
Example 4.2
Given variables u, v, w, x, y ∈ V, examples of ω-sharing groups are u2 v 3 x19 , xyz
and u23 vwx2 y 3 .
Definition 4.3
Given a substitution θ and a variable v ∈ V, we define
θ−1 (v) = λw. occ(v, θ(w)) .
Intuitively, θ−1 (v) is an ω-sharing group which maps each variable w to the number
of occurrences of v in θ(w).
Example 4.4
Given θ = {x/f (u, u, u), y/g(u, v), z/f (u, v, v)}, we have that θ−1 (u) = ux3 yz,
θ−1 (v) = vyz 2 , θ−1 (w) = w, and θ−1 (x) = {{}}.
Definition 4.5 (Correct Approximation)
Given a set of variables U and a set of ω-sharing groups S (i.e., S ⊆ ℘m (U )), we
say that the pair (S, U ) correctly approximates a substitution [θ]W if U = W and
for each v ∈ V, θ−1 (v)|W ∈ S. In the following we denote by [S]U the pair (S, U )
and write [S]U 3 [θ]W to mean that [S]U correctly approximates [θ]W .
Therefore, [S]U correctly approximates [θ]U when S contains at least all the ωsharing groups which may arise in θ, restricted to the variables U . Note that [θ]U
is an equivalence class of substitutions, as defined in Section 3, while [S]U is just a
symbol to denote the pair of objects (S, U ). We prefer this notation for the sake of
uniformity with substitutions.

On the interaction between sharing and linearity

11

Theorem 4.6
The relation 3 is well defined.
We can now define the domain ShLinω of ω-sharing groups.
Definition 4.7 (ShLinω )
The domain ShLinω is defined as
ShLinω = {[S]U | U ∈ ℘f (V), S ⊆ ℘m (U ), S 6= ∅ ⇒ {{}} ∈ S} ,
and ordered by [S1 ]U1 ≤ω [S2 ]U2 iff U1 = U2 and S1 ⊆ S2 .
The order relation corresponds to the approximation ordering, since bigger (w.r.t
≤ω ) elements correctly approximate a larger number of substitutions than smaller
elements. The existence of the empty multiset, when S is not empty, is required
in order to obtain a Galois insertion, instead of a Galois connection. In order to
simplify the notation, in the following we write an object [{{{}}, B1 , . . . , Bn }]U ∈
ShLinω as [B1 , . . . , Bn ]U by omitting the braces and the empty multiset. Moreover,
if X ∈ ShLinω , we write B ∈ X in place of X = [S]U ∧ B ∈ S.
Definition 4.8 (Abstraction for ShLinω )
We define the abstraction for a substitution [θ]U as
αω ([θ]U ) = [{θ−1 (v)|U | v ∈ V}]U .
This is the least element of ShLinω which correctly approximates [θ]U . Note that
by the proof of Theorem 4.6 it immediately follows that αω is well defined, i.e., it
does not depend from the choice of the representative for [θ]U .
Example 4.9
Given θ = {x/r(y, u, u), z/y, v/u} and U = {w, x, y, z}, we have θ−1 (u) = x2 vu,
θ−1 (y) = xyz, θ−1 (z) = θ−1 (v) = θ−1 (x) = {{}} and θ−1 (s) = s for all the other
variables (included w). Projecting over U we obtain αω ([θ]U ) = [x2 , xyz, w]U .
Example 4.10
As we have said in Section 3, we show an element of ISubst ∼ , namely the existential
substitution [x/r(v, v)]x , which cannot be obtained as [δ]vars(δ) for any substitution δ. In fact, consider any ω-sharing group B = δ −1 (u)|vars(δ) ∈ αω ([δ]vars(δ) ).
Then either u ∈
/ rng(δ) and B = {{}} or u ∈ rng(δ) and B(u) = 1. However,
α([x/r(v, v)]x ) = [x2 ]x and x2 does not contain any variable with multiplicity one.

4.1 Multigraphs
In order to define an abstract unification operator over ShLinω , we need to introduce
the concept of multigraph. We call (directed) multigraph a graph where multiple
distinguished edges are allowed between nodes. We use the definition of multigraph
which is customary in category theory (Mac Lane 1988).

12

G. Amato and F. Scozzari

Definition 4.11 (Multigraph)
A multigraph G is a tuple hNG , EG , srcG , tgtG i where NG 6= ∅ and EG are the sets
of nodes and edges respectively, srcG : EG → NG is the source function which maps
each edge to its start node, and tgtG : EG → NG is the target function which maps
each edge to its end node.
A labeled multigraph G is a multigraph equipped with a labelling function lG :
NG → LG which maps each node to its label in the given set LG .
We write e : n1 → n2 ∈ G to denote the edge e ∈ EG such that srcG (e) = n1
and tgtG (e) = n2 . We also write n1 → n2 ∈ G to denote any edge e ∈ EG such
that srcG (e) = n1 and tgtG (e) = n2 . Moreover, with |n1 → n2 ∈ G| we denote
the cardinality of the set {e ∈ EG | srcG (e) = n1 ∧ tgtG (e) = n2 }. In the notation
above, we omit “∈ G” whenever the multigraph G is clear from the context.
We call in-degree (respectively out-degree) of a node n the cardinality of the set
{e ∈ EG | tgt(e) = n} (respectively {e ∈ EG | src(e) = n}).
Given a multigraph G, a path π is a non-empty sequence of nodes n1 . . . nk such
that, for each i ∈ {1, . . . , k − 1}, there is either an edge ni → ni+1 ∈ G or an edge
ni+1 → ni ∈ G. Nodes n1 and nk are the endpoints of π, and we say that π connects
n1 and nk . A multigraph is connected when all pairs of nodes are connected by at
least one path.
4.2 Abstract unification
We need to find the abstract counterpart of mgu over ShLinω , i.e., an operation
mguω such that, if [S]U 3 [θ]U , then
mguω ([S]U , δ) 3 mgu([θ]U , δ)

(3)

for each δ ∈ ISubst. Note that we are looking for an abstract counterpart to the
mixed unification in (2), where one of the two arguments is a plain substitution. In
particular, we would like to find an operator which is the minimum element that
satisfies the condition in (3), i.e., the optimal abstract counterpart of mgu. Observe
that, for a fixed U , the set of all the elements [S]U ∈ ShLinω is a complete lattice
w.r.t. ≤ω with the top element given by [℘m (U )]U and the meet operator given by

T
V
i∈I Si U ,
ω {[Si ]U | i ∈ I} =

for any family {[Si ]U | i ∈ I} of elements of ShLinω . Moreover, the relation 3 is
V
meet-preserving on the left, since if [Si ]U 3 [θ]U for each i ∈ I, then ω {[Si ]U | i ∈
I} 3 [θ]U . Therefore, we may define the abstract mgu as follows
^ 
mguω ([S]U , δ) =
[S ′ ]U ′ | ∀θ.[S]U 3 [θ]U ⇒ [S ′ ]U ′ 3 mgu([θ]U , δ) ,
ω

where the definitions of 3 and mgu force U ′ to be U ∪ vars(δ). Note that this is just
a translation of the general definition of optimal operator in (Cousot and Cousot
1992b) and it satisfies (3).
This definition is completely non-constructive. The rest of this section is devoted
to providing a constructive characterization for mguω ([S]U , δ). We begin to characterize the operation of abstract unification by means of graph theoretic notions.

On the interaction between sharing and linearity

13

Definition 4.12 (Multiplicity of ω-sharing groups)
The multiplicity of an ω-sharing group B in a term t is defined as:
X
X
B(v) · occ(v, t) .
χ(B, t) =
occ(v, t) =
v∈B

v∈TBU

For instance, χ(x3 yz 4 , r(x, y, f (x, y, z))) = 3 · 2 + 1 · 2 + 4 · 1 = 12. The meaning of
the map χ is made clear by the following proposition.
Proposition 4.13
Given a substitution θ, a variable v and a term t, we have that χ(θ−1 (v), t) =
occ(v, θ(t)). Moreover, given a set of variables U , when vars(t) ⊆ U , it holds that
χ(θ−1 (v)|U , t) = occ(v, θ(t)).
Example 4.14
Let B = xy 2 z 3 and θ = {y/r(x, x), z/r(x, x, x)}, so that θ−1 (x) = {xy 2 z 3 }. Given
t ≡ s(x, z) we have
occ(x, θ(t)) = occ(x, s(x, r(x, x, x))) = 4 ,
and
χ(B, t) = B(x)occ(x, t) + B(z)occ(z, t) = 1 · 1 + 3 · 1 = 4 .
If [S]U 3 [θ]U and we unify [θ]U with δ, some of the ω-sharing groups in S may
be glued together to obtain a bigger resultant group. It happens that the gluing of
the sharing groups during the unification of [θ]U with a single binding substitution
{x/t} may be represented by special labelled multigraphs which we call sharing
graphs.
Example 4.15
Let S = {x3 , y} and U = {x, y}. We look for a representation of the unification
process between any substitution θ approximated by S and the binding x/r(y). We
show that multigraphs can be easily used for this purpose. For instance, the substitution θ = {x/r(g(u, u, u))} is approximated by S. By unifying θ with {x/r(y)}
we obtain δ = {x/r(g(u, u, u)), y/g(u, u, u)}. Note that any approximation of δ on
the variables {x, y} must include the sharing group x3 y 3 generated by the variable
u. Thus, any correct approximation of the unification must also contain x3 y 3 .
We want to associate to any ω-sharing group B in δ a special multigraph which
represents the way the ω-sharing groups in S have been merged in order to obtain
B. The nodes of this multigraph are the ω-sharing groups in S (possibly repeated
any number of times). The following is a sharing graph for x/r(y) and S:
☎
✞
1
y
✝
✆
;
0
ww
ww
w
w
ww
☎
☎
✞
✞
0
1
/ y
x3
✝
✆
✝
✆
3GG
0
GG
GG
GG
#
✞
☎
1
y
✝
✆
0

14

G. Amato and F. Scozzari

where pedices and apices on a sharing group B are respectively the values of χ(B, x)
and χ(B, r(y)). For instance, since χ(x3 , x) = 3, then we put the pedice 3 on the
node x3 to mean that x is bound to a term containing 3 occurrences of the same
variable. Symmetrically, since χ(x3 , r(y)) = 0, then we put the apice 0 on the node
x3 . The in-degree and the out-degree of the nodes reflect the values of apices and
pedices. In this case, we have 3 out-going edges from x3 and no in-going edges.
Moreover, the multigraph must be connected, in order to guarantee that we can
use a single variable to form the sharing group x3 y 3 .
By summing the labels of all the nodes, namely, x3 ⊎ y ⊎ y ⊎ y, we obtain the
ω-sharing group x3 y 3 which must appear in any correct approximation of the unification.
Given any labelled multigraph G, in the rest of the paper we assume that the
codomain of the labelling function lG is ℘m (V), the set of ω-sharing groups.
Definition 4.16 (Sharing Graph)
A sharing graph for the binding x/t and a set of ω-sharing groups S is a labelled
multigraph G such that
1. G is connected;
2. for each node n ∈ NG , lG (n) ∈ S;
3. for each node n ∈ NG , the out-degree of n is equal to χ(lG (n), x) and the
in-degree of n is equal to χ(lG (n), t).
The resultant ω-sharing group of G is
res(G) =

]

lG (n) .

n∈NG

Example 4.17
Let S = {ux2 , xy, vz, wz, xyz}. The following is a sharing graph for x/r(y, z) and
S:
✞
✞
☎
☎
✞
☎
0
1
1
/
/
2
xy
vz
ux
✝
✆
✝
✆
✝
✆
2GG
0
1
GG
GG
GG
#
✞
☎
☎
✞
1
1
/ wz
xy
✝
✆
✝
✆
0
1
where pedices and apices on a sharing group B are respectively the value of χ(B, x)
and χ(B, r(y, z)). Therefore the resultant sharing group is uvwx4 y 2 z 2 .
It is worth noting that, given any set of ω-sharing groups S and binding x/t,
there exist many different sharing graphs for x/t and S. Each sharing graph yields
a resultant sharing group which must be included in the result of the abstract
unification operator. Of course, different sharing graphs may give the same resultant
sharing group. The abstract unification operator is defined by collecting all the
resultant sharing groups.

On the interaction between sharing and linearity

15

Definition 4.18 (Single binding unification)
Let U ∈ ℘f (V), S be a set of ω-sharing groups with [S]U ∈ ShLinω , x/t be a
binding, and vars(x/t) ⊆ U . The set of resultant ω-sharing groups for x/t and S is
mguω (S, x/t) = {res(G) | G is a sharing graph for S and x/t} .
We lift mguω to an operation over ShLinω .
mguω ([S]U , x/t) = [mgu(S, x/t)]U .
This is a particular case of the abstract unification operator, for single binding
substitutions and vars(x/t) ⊆ U .
Example 4.19
Let S be as in Example 4.17. The following is
S:
✞
☎
0
,✞
2
ux
2 xyz
✝
✆
✝
2

a sharing graph for x/r(y, y, z) and
☎
3
_
✆
1

where pedices and apices on a sharing group B are respectively the value of χ(B, x)
and χ(B, r(y, y, z)). Therefore ux3 yz ∈ mguω (S, x/r(y, y, z)). Note that this sharing
group can actually be generated by the substitution θ = {x/r(v1 , v1 , v2 ), y/v2 , z/v2 ,
u/v1 , v/a, w/a} where a is a ground term. Let U = {u, v, w, x, y, z}. It is the case
that [S]U 3[θ]U and mgu([θ]U , {x/r(y, y, z)}) performs exactly the variable aliasings
depicted by the sharing graph. Actually mgu([θ]U , {x/r(y, y, z)}) = [x/r(v1 , v1 , v1 ),
y/v1 , u/v1 , v/a, w/a]U = [η]U and η −1 (v1 )|U = ux3 yz.
We give here an intuition of the way sharing graphs work. Assume given a set of
ω-sharing groups [S]U and a binding x/t with vars(x/t) ⊆ U . We want to compute
[mguω (S, x/t)]U . To this aim, for any substitution θ approximated by [S]U , that is,
[S]U 3 [θ]U , we compute αω (mgu([θ]U , {x/t})).
For any B1 , B2 ∈ S, assume that there exist v1 , v2 ∈ V such that B1 = θ−1 (v1 )|U
and B2 = θ−1 (v2 )|U . When unifying θ with the binding x/t, we use the fact that
mgu(Eq(θ) ∪ {x = t}) = mgu({θ(x) = θ(t)}) ◦ θ. By Prop. 4.13, θ(x) contains
χ(B1 , x) instances of v1 and χ(B2 , x) instances of v2 . Symmetrically, θ(t) contains
χ(B1 , t) instances of v1 and χ(B2 , t) instances of v2 .
Assume that θ(x) and θ(t) only differ for the variables occurring in them (and
not for the structure of terms). Then, an arrow from the sharing group B1 to B2
represents the fact that, in mgu({θ(x) = θ(t)}), one of the copies of v1 is aliased
to one of the copies of v2 , i.e., that there are corresponding positions in θ(x) and
θ(t) where the two terms contain the variables v1 and v2 respectively. The third
condition for sharing graphs implies that each occurrence of v1 and v2 is aliased
to some other variable. The first condition (the sharing graph must be connected)
ensures that all the variables corresponding to the ω-sharing groups involved in the
sharing graph are aliased to each other. In other words, given any two such variables,
they are aliased. Although here we are only considering the case when θ(x) and θ(t)
differ for the variables occurring in them, we will show that it is enough to reach
correctness and optimality. The next example applies this intuition to a concrete
case.

16

G. Amato and F. Scozzari

Example 4.20
Consider Example 4.19, where θ = {x/r(v1 , v1 , v2 ), y/v2 , z/v2 , u/v1 , v/a, w/a} and
U = {u, v, w, x, y, z}. Let B1 = ux2 and B2 = xyz, thus B1 = θ−1 (v1 )|U and
B2 = θ−1 (v2 )|U . When unifying θ with the binding x/r(y, y, z) we have that θ(x) =
r(v1 , v1 , v2 ) and θ(r(y, y, z)) = r(v2 , v2 , v2 ).
Note that θ(x) contains χ(ux2 , x) = 2 instances of v1 and χ(xyz, x) = 1 instance
of v2 . Symmetrically, θ(r(y, y, z)) contains χ(ux2 , r(y, y, z)) = 0 instances of v1 and
χ(xyz, r(y, y, z)) = 3 instances of v2 . Moreover, θ(x) and θ(r(y, y, z)) only differ
for the variables occurring in them. Thus, the three edges in the sharing graph of
Example 4.19 correspond to the following aliasings:
θ(r(y, y, z))=r(vO2 , vO 2 , vO 2 )
θ(x)

=r(v1 , v1 , v2 )

In particular, the last arrow from v2 to itsself, corresponds to the self-loop in the
sharing graph.
The unification operator mguω ([S]U , x/t) can be extended to the case vars(x/t) *
U . The idea is to enlarge S by including all the singletons in vars(x/t) \ U .
Definition 4.21 (Single binding unification with extension)
Let U ∈ ℘f (V), S be a set of ω-sharing groups with [S]U ∈ ShLinω and x/t be a
binding.
mguω ([S]U , x/t) = mguω ([S ∪ {{{v}} | v ∈ vars(x/t) \ U }]U∪vars(x/t) , x/t) .
Note that, for a generic abstract domain, the method of extending the abstract
object to include all the variables in the concrete substitution δ may result in a
non-optimal abstract unification. For example, this is what happens in the case of
the domain Sharing, as shown in (Amato and Scozzari 2009). However, we will
prove that, in the case of ShLinω , the abstract mgu in Definition 4.21 is optimal.
This operator can be extended to multi-binding substitutions in the obvious way,
namely by iterating the single binding operator.
Definition 4.22 (Multi-binding unification)
We define mguω ([S]U , δ) with δ ∈ ISubst and [S]U ∈ ShLinω by induction on the
number of bindings:
mguω ([S]U , ǫ) = [S]U ,
mguω ([S]U , {x/t} ⊎ δ) = mguω (mguω ([S]U , x/t), δ) .
It is possible to prove that mguω ([S]U , δ) is optimal for multi-binding substitutions
(Amato and Scozzari 2005). Since optimality of iterative multi-binding unification
is not inherited by the abstractions of ShLinω (as we show in Section 5.3), we
will focus on single binding unification. In the rest of the paper, we only consider
bindings x/t which are idempotent, namely, such that x ∈
/ vars(t).

On the interaction between sharing and linearity

17

4.3 Correctness of abstract unification
We now show that mguω ([S]U , δ) is correct w.r.t. concrete unification. We show
correctness for multi-binding substitutions, since it is a trivial extension of the
single binding case. In fact, composition of correct operators is still correct.
First of all, we extend the definition of θ−1 to the case when it is applied to a
sharing group B.
Definition 4.23
Given θ ∈ ISubst and B an ω-sharing group, we define
θ−1 (B) = λv ∈ V.χ(B, θ(v)) .
In order to prove the correctness of abstract unification, we need the following
auxiliary property.
Proposition 4.24
Given substitutions θ, η ∈ ISubst and an ω-sharing group B, we have
(η ◦ θ)−1 (B) = θ−1 (η −1 (B)) .
Theorem 4.25 (Correctness of mguω )
The operation mguω is correct w.r.t. mgu, i.e.,
∀[S]U ∈ ShLinω , δ ∈ ISubst. [S]U 3 [θ]U =⇒ mguω ([S]U , δ) 3 mgu([θ]U , δ) .
Example 4.26
Let θ = {x/r(s(u, u, u), v, w), y/v ′ , z/w′ }, δ = {x/r(y, y, z)} and U = {x, y, z}.
Therefore αω ([θ]U ) = [x3 , x, y, z]U . If we proceed with the concrete unification
of [θ]U with δ, we have mgu([θ]U , δ) = [θ′ ]U with θ′ = mgu(θ, δ) = η ◦ θ and
η = mgu(θ(x) = θ(r(y, y, z))). This gives the following results:
η = {v ′ /s(u, u, u), v/s(u, u, u), w′/w} ,
θ′ = {x/r(s(u, u, u), s(u, u, u), w), y/s(u, u, u), z/w, v ′/s(u, u, u), w′ /w} ,
with [θ′ ]U = [θ]U . Now, let η ′ be obtained from η by replacing each occurrence of a
variable in rng(η) with a different fresh variable, β = η ′ ◦ θ and ρ be a substitution
mapping variables to variables such that ρ(β(x)) = θ′ (x) for each x ∈ U . Note that
ρ is not a renaming, since it is not bijective. We have:
η = {v/s(u1 , u2 , u3 ), v ′ /s(u4 , u5 , u6 ), w′ /u7 } ,
β = {x/r(s(u, u, u), s(u1 , u2 , u3 ), w), y/s(u4 , u5 , u6 ), z/u7 , v ′ /s(u4 , u5 , u6 ), w′ /u7 } ,
ρ = {u1 /u, u2 /u, u3 /u, u4/u, u5 /u, u6 /u, u7/w} .
Following the
✞
x3 (u)
✝

proof, we build a multigraph G as follows:
✞
☎
☎
☎
✞
✞
0
0
0
x(u
)
x(u
)
x(u3 )
1
2
✆
✆
✝
✆
✝
3FSSSS ✝
1
1
FF SxSxSS
x
x
FFxx SSSS
xx
xx
x FF
xx
SSS xxx
x
x
S
F
#

{xx
{xx SSSS
{xx
☎
☎
☎
)✞
✞
✞
✞
2
2
2
y(u4 )
y(u5 )
y(u6 )
z(u7 )
✝
✆
✝
✆
✝
✆
✝
0
0
0

☎
0

☎
✞
0
x(w)
✆
✝
✆
1
1
x
x
x
x
xx
{xx
☎
1
✆
0

18

G. Amato and F. Scozzari

Note that we have chosen to annotate every sharing group with the corresponding
variable in vars(β(U )). This is not a sharing graph since it is not connected, but if
we take Y = Tρ−1 (u)U = {u, u1 , u2 , u3 , u4 , u5 , u6 }, the restriction of G to the nodes
annotated with a variable in Y is a sharing graph whose resultant ω-sharing group
is x6 y 3 .
4.4 Optimality of Abstract Unification
We now prove that mguω is not only correct, but also optimal for a single binding
substitution, i.e., it is the least correct abstraction. This means proving that, given
a set of ω-sharing groups [S]U ∈ ShLinω , a binding x/t, and an ω-sharing group
B ∈ mguω ([S]U , x/t), there exists a substitution [δ]U such that [S]U 3 [δ]U and
B ∈ αω (mgu([δ]U , {x/t})). First of all, we prove optimality of mguω ([S]U , x/t) in
the special case of vars(x/t) ⊆ U . Next, we extend this result to the general case.
Example 4.27
Consider S = {xu, xv, y} and the binding x/s(y, y). The following is a sharing graph
for x/s(y, y) and S whose resultant ω-sharing group is x2 uvy.
☎
✞
0
xu
✝
✆
1D
DD
DD
DD
D"
✞
✝

y

☎
✞
0
xv
✝
✆
1
zz
z
z
zz
|zz
☎
2
✆
0

We show how to find a substitution [δ]U such that the ω-sharing group x2 uvy ∈
αω (mgu([δ]U , {x/s(y, y)})). Let U = {u, v, x, y}. For each node n of the sharing
graph, we consider a different fresh variable wn . Assume that the node labelled
with xu in the upper-left corner is node 1, and proceed clockwise to number the
other nodes.
For each variable z ∈ U \ {x}, we associate to δ(z) a term containing all the
variables wi such that the label of the i-th node contains the variable z. Thus, we
define δ(u) = r(w1 ) where w1 correspond to the node containing u. Analogously,
we define δ(v) = r(w2 ) and δ(y) = r(w3 ).
We now define δ(x) in a different way, namely by replacing in s(y, y) each occurrence of the variable y with a term similar to δ(y), with the difference that w3
is replaced with the variables w1 and w2 . The choice of w1 and w2 is obvious by
looking at the sharing graph, since the first and second node are the sources of the
two edges targeted at the node three. Therefore we obtain δ(x) = s(r(w1 ), r(w2 )).
Summing up, we have:
δ = {u/r(w1 ), v/r(w2 ), x/s(r(w1 ), r(w2 )), y/r(w3 )} .
It is easy to check that [S]U 3 [δ]U and
mgu(δ, {x/s(y, y)}) =
{u/r(w1 ), v/r(w1 ), x/s(r(w1 ), r(w1 )), y/r(w1 ), w2 /w1 , w3 /w1 } ,

On the interaction between sharing and linearity

19

hence αω ([mgu(δ, {x/s(y, y)})]U ) = [x2 uvy]U .
In the above example we have shown how to find a special substitution such that
its fresh variables are unified according to the arrows in a sharing graph. The same
idea is exploited in the next theorem for proving the optimality of the abstract unification operator mguω . For any ω-sharing group X ∈ mguω ([S]U , x/t), we provide
a substitution δ obtained as in Example 4.27, such that [S]U approximates [δ]U and
X ∈ αω (mgu([δ]U , {x/t)}).
Theorem 4.28 (Optimality of mguω )
The single binding unification mguω ([S]U , x/t) is optimal w.r.t. mgu, under the
assumption that vars(x/t) ⊆ U , i.e., :
∀B ∈ mguω ([S]U , x/t) ∃δ ∈ ISubst. [S]U 3 [δ]U and B ∈ αω (mgu([δ]U , {x/t})) .
The previous proof requires that vars(x/t) ⊆ U . However, the same construction
also works when this condition does not hold.
Example 4.29
Given U = {x, y} and S = {x2 , x2 y}, we want to compute mguω ([S]U , x/s(y, z)). By
extending the domain of the variables of interests, we obtain [S ′ ]V = [x2 , x2 y, z]x,y,z .
One of the sharing graphs for x/s(y, z) and [S ′ ]V is
☎
0
2
x
✝
✆
2
✞

✞
✝


z

☎
1
✆
0

✞
☎
1
/ x2 y
✝
✆
2D
DD
DD
DD
D"

✞
✞
☎
1
z
z
✝
✆
✝
0

☎
1
✆
0

Following the proof of the previous theorem, we obtain the substitution
δ ′ = {x/s(r(w1 ), r(w1 , w2 , w2 )), y/r(w2 ), z/r(w3 , w4 , w5 )} ,
where [S ′ ]V 3[δ ′ ]V and x4 yz 3 ∈ αω (mgu([δ ′ ]V , {x/s(y, z)})). However we are looking
for a substitution δ such that [S]U 3 [δ]U and x4 yz 3 ∈ αω (mgu([δ]U , {x/s(y, z)})).
Nonetheless, we may choose δ = δ ′ (or, if we prefer, δ = δ ′ |x,y ) to get the required
substitution.
This is not a fortuitous coincidence. We may show that it consistently happens
every time we apply Theorem 4.28 to an abstract unification where vars(x/t) * U .
Therefore, we can prove the main result of the paper.
Theorem 4.30 (Optimality of mguω with extension)
The single binding unification mguω with extension is optimal w.r.t. mgu.
4.5 A characterization for resultant sharing groups
The domain ShLinω has not been designed to be directly implemented, but some
of its abstractions could. Providing a simpler definition for the set of resultant ωsharing groups could help in developing the abstract operators for its abstractions.

20

G. Amato and F. Scozzari

We show that given a set S of ω-sharing groups and a binding x/t, the set of
resultant ω-sharing groups has an elegant algebraic characterization.
By definition of sharing graph, a set of nodes N labelled with ω-sharing groups
of S can be turned into a sharing graph for S and x/t if and only if the condition on
the out-degree and in-degree is satisfied and the obtained graph is connected. The
condition on the degrees says that for each node s labelled with the sharing group
Bs , the out-degree of s must be equal to χ(Bs , x). Symmetrically, the in-degree
must be equal to χ(Bs , t). As a consequence, the sum of the out-degrees of all the
P
nodes s∈N χ(Bs , x) must be equal to the sum of the in-degrees of all the nodes
P
s∈N χ(Bs , t). This is because each edge has a source and a target node. Moreover,
in order to be connected, any graph needs at least |N | − 1 edges. Since the number
of edges is equal to the sum of in-degrees of all the nodes, it turns out that such
a sum must be equal to or greater than |N | − 1. Surprisingly, this is enough to
construct a sharing graph from N .
Theorem 4.31
Let S be a set of ω-sharing groups and x/t be a binding. Then B ∈ mguω (S, x/t)
iff there exist n ∈ N+ , B1 , . . . , Bn ∈ S which satisfy the following conditions:
1. B = ⊎1≤i≤n Bi ;
P
P
2.
1≤i≤n χ(Bi , t) ≥ n − 1;
1≤i≤n χ(Bi , x) =
3. either n = 1 or ∀1 ≤ i ≤ n. χ(Bi , x) + χ(Bi , t) > 0.
Following the above theorem, we can give an algebraic characterization of the
abstract unification operator as follows.
Corollary 4.32 (Algebraic characterization of mguω )
Given a set of ω-sharing groups S and a binding x/t, we have that
mguω (S, x/t) = (S \ rel (S, x, t))∪
(

⊎R | R ∈ ℘m (rel (S, x, t)),

X

B∈R

χ(B, x) =

X

)

χ(B, t) ≥ |R| − 1 ,

B∈R

where
rel (S, x, t) = {B ∈ S. χ(B, x) + χ(B, t) > 0}
= {B ∈ S. TBU ∩ vars(x/t) 6= ∅} .
Example 4.33
Consider S = {xa, xb, z 2 , zc} and the equation x = z. Then if we choose R =
P
P
{{xa, xb, z 2 }}, we have B∈R χ(B, x) = 2 = B∈R χ(B, z) ≥ |R| − 1. Therefore
P
x2 z 2 ab ∈ mguω (S, x/z). If we take R = {{xa, xb, zc, zc}}, although B∈R χ(B, x) =
P
2 = B∈R χ(B, z), we have |R| − 1 = 3. This only proves that z 2 c2 x2 ab cannot be
obtained by the multiset R. If we check for every possible multiset over S, we have
that z 2 c2 x2 ab ∈
/ mguω (S, x/z).
This characterization of the abstract mgu will be the key point for devising the
optimal abstract unification operators on the abstractions of ShLinω . Let α be the
abstraction function from ISubst ∼ to an abstract domain A. If we are able to factor

On the interaction between sharing and linearity

21

α through a Galois connection hα′ : ShLinω → A, γ ′ : A → ShLinω i as α = α′ ◦ αω ,
then the optimal abstract unification for α is exactly α′ (mguω (γ ′ (·), ·)). However,
this expression is helpful when it may be simplified in order to use only objects in
A. Our algebraic characterization makes the simplification feasible, as we show in
the following section.
5 Practical domains for program analysis
We consider two domains for sharing analysis with linearity information, namely,
the domain proposed in (King 1994) and the classical reduced product Sharing ×
Lin. They are defined as abstractions of ShLinω through Galois insertions. This
allows us to design optimal abstract operators for both of them, by exploiting the
results introduced so far. By composing each Galois insertion with αω , we get the
corresponding abstraction function for substitutions (Cousot and Cousot 1992a,
Sect. 4.2.3.1).
5.1 King’s domain for linearity and aliasing
We first consider the domain for combined analysis of sharing and linearity in (King
1994). The idea is to enhance the domain Sharing by annotating each sharing
group with linearity information on each variable. For instance, the object xy ∞ z
represents the sharing group xyz and the information that y may be non-linear
(while x and z are definitely linear). The objects in this domain can be easily
viewed as abstraction of ω-sharing groups. Intuitively, in order to abstract an ωsharing groups, one simply needs to replace each exponent equal to or greater than
2 with ∞. Let us now formalize the domain as an abstraction of ShLinω .
An ω-sharing group (which is a multiset V → N whose support is finite) is abstracted into a map o : V →{0, 1, ∞} such that its support ToU = {v ∈ V | o(v) 6= 0}
is finite. We call such a map the 2-sharing group. We use a polynomial notation
for 2-sharing groups as for ω-sharing groups. For instance, o = xy ∞ z denotes the
2-sharing group whose support is ToU = {x, y, z}, such that o(x) = o(z) = 1 and
o(y) = ∞. We denote with ∅ the 2-sharing group with empty support. Note that in
(King 1994) the number 2 is used as an exponent instead of ∞, but we prefer this
notation to be coherent with ω-sharing groups.
We denote min{o(x), 2} by om (x), where the ordering on N is extended in the
obvious way, i.e., for all n ∈ N we have that n < ∞. A 2-sharing group o represents
the sets γ2 (o) of ω-sharing group given by:
γ2 (o) = {B ∈ ℘m (V) | ToU = TBU ∧ ∀x ∈ ToU.om (x) ≤ B(x) ≤ o(x)} .
For instance, the 2-sharing group xy ∞ z represents the set of ω-sharing groups
{xy 2 z, xy 3 z, xy 4 z, xy 5 z, . . .}. The idea is to use 2-sharing groups to keep track of
linearity: if o(x) = ∞, it means that the variable x is not linear in the 2-sharing
group o. In the rest of this section, we use the term “sharing group” as a short form
of 2-sharing group, when this does not cause ambiguity.
An ω-sharing group B may be abstracted into the 2-sharing group α2 (B) given

22

G. Amato and F. Scozzari

by:
α2 (B) = λv ∈ TBU.

(

1 if B(x) = 1,
∞ otherwise.

The next proposition shows two useful properties of the maps α2 and γ2 .
Proposition 5.1
The following properties hold:
U
U
1. α2 ( R) = α2 (R).
2. rel (γ2 (S), x, t)) = γ2 (rel (S, x, t)).
Since we do not want to represent definite non-linearity, we introduce an order
relation over sharing groups as follows:
o ≤ o′ ⇐⇒ ToU = To′ U ∧ ∀x ∈ ToU. o(x) ≤ o′ (x) ,
and we restrict our attention to downward closed sets of sharing groups. We denote
by Sg 2 (V ) the set of 2-sharing groups whose support is a subset of V . The domain
we are interested in is the following:

ShLin2 = [S]U | S ∈ ℘↓ (Sg 2 (U )), U ∈ ℘f (V), S 6= ∅ ⇒ ∅ ∈ S ,

where ℘↓ (Sg 2 (U )) is the powerset of downward closed subsets of Sg 2 (U ) according to ≤ and [S1 ]U1 ≤2 [S2 ]U2 iff U1 = U2 and S1 ⊆ S2 . For instance, the set
{xy ∞ z} is not downward closed, while {xyz, xy ∞ z} is downward closed. There
is a Galois insertion of ShLin2 into ShLinω given by the pair of adjoint maps
γ2 : ShLin2 → ShLinω and α2 : ShLinω → ShLin2 :
h[
i
γ2 ([S]U ) =
{γ2 (o) | o ∈ S}
,
U

α2 ([S]U ) = [↓{α2 (B) | B ∈ S}]U .

With an abuse of notation, we also apply γ2 and α2 to subsets of ω-sharing groups
and 2-sharing groups respectively, by ignoring the set of variables of interest. For
instance, γ2 ({xyz, xy ∞ z}) = {xyz, xy 2 z, xy 3 z, xy 4 z, xy 5 z, . . .}.
Theorem 5.2
The pair hα2 , γ2 i is a Galois insertion.
Now we may define the optimal mgu for ShLin2 and single binding substitutions
as follows:
Definition 5.3 (Unification for ShLin2 )
Given [S]U ∈ ShLin2 and the binding x/t, we define
mgu2 ([S]U , x/t) = α2 (mguω (γ2 ([S]U ), x/t)) .
By construction, mgu2 is the optimal abstraction of mguω , hence also of mgu. In
the case where vars(x/t) ⊆ U , by using additivity of α2 we get:
h
mgu2 ([S]U , x/t) = α2 (γ2 (S) \ rel (γ2 (S), x, t))∪

On the interaction between sharing and linearity

α2 {⊎R | R ∈ ℘m (rel (γ2 (S), x, t)),
i
X
X
χ(B, x) =
χ(B, t) ≥ |R| − 1}
B∈R

U

B∈R

23

. (4)

Now we want to simplify Eq. 4. In particular we would like to get rid of the
abstraction and concretization maps and to express the result using only objects
and operators in ShLin2 . Therefore, we need to define operations in ShLin2 which
correspond to ⊎ and χ in ShLinω .
The operation on 2-sharing groups which corresponds to multiset union on ωsharing groups, is given by
o ⊎ o′ = λv ∈ V.o(v) ⊕ o′ (v) ,
U
where 0⊕x = x⊕0 = x and ∞⊕x = x⊕∞ = 1⊕1 = ∞. We will use {{o1 , . . . , on }}
for o1 ⊎· · ·⊎on . Given a sharing group o, we also define the delinearization operator:
o2 = o ⊎ o .

(5)

Note that o2 = λx ∈ ToU.∞. The operator is extended pointwise to sets and
multisets.
A fundamental role is played by the notion of multiplicity of a sharing group in
a term. While the multiplicity of an ω-sharing group in a term is a single natural
number, every object in ShLin2 represents a set of ω-sharing groups, hence its
multiplicity should be a set of natural numbers. Actually, it is enough to consider
intervals. We define the minimum χm and maximum χM multiplicity of o in t as
follows:
X
X
o(v) · occ(v, t) .
om (v) · occ(v, t)
χM (o, t) =
χm (o, t) =
v∈ToU

v∈ToU

Sum and product on integers are lifted in the obvious way, namely, the sum is ∞ if
and only if at least one of the addenda is ∞ and n · ∞ = ∞ · n = ∞ for any n ∈ N+ ,
while 0 · ∞ = ∞ · 0 = 0. The maximum multiplicity χM (o, t) either is equal to the
minimum multiplicity χm (o, t) or it is infinite. Note that, if B is an ω-sharing group
represented by o, i.e., B ∈ γ2 (o), then χm (o, t) ≤ χ(B, t) ≤ χM (o, t). Actually, not
all the values between χm (o, t) and χM (o, t) may be assumed by χ(B, t).
Example 5.4
Let o = x∞ and t = f (x, x). According, to our definition, χ(o, t) = [4, ∞). However,
it is obvious that if B ∈ γ2 (o), then χ(B, t) is an even number.
According to the above definitions, we define the multiplicity of a multiset of
sharing groups as
n
o
X
X
χ(Y, t) = n ∈ N |
χm (o, t) ≤ n ≤
χM (o, t) .
o∈Y

o∈Y

Even if this is a superset of all the possible values which can be obtained by combining the multiplicities of all the sharing groups in Y , this definition is sufficiently
accurate to allow us to design the optimal abstract unification.

24

G. Amato and F. Scozzari

We extend in the obvious way the definition of rel (see Corollary 4.32) from
ω-sharing groups to 2-sharing groups, i.e.,
rel (S, x, t) = {o ∈ S | ToU ∩ vars(x/t) 6= ∅} ,
and we prove the following
Theorem 5.5 (Characterization of abstract unification for ShLin2 )
Given [S]U ∈ ShLinω and the binding x/t with vars(x/t) ⊆ U , we have that
mgu2 ([S]U , x/t) = [(S \ S ′ )∪
]
↓
Y | Y ∈ ℘m (S ′ ), n ∈ χ(Y, x) ∩ χ(Y, t). n ≥ |Y | − 1 ]U ,

where S ′ = rel (S, x, t).

Example 5.6
Let S = ↓{∅, ux∞ , vx∞ , x∞ y, z ∞ } and Y = {{ux∞ , vx∞ , xy, z ∞ }}. We have that
χ(Y, x) = {n | n ≥ 5} and χ(Y, f (z, z)) = {n | n ≥ 4}. Since f (z, z) contains
two occurrences of z, the “actual” multiplicity of the sharing group z ∞ in f (z, z)
should be a multiple of 2. But we do not need to check this condition and can
safely approximate this set with {n | n ≥ 4}. This works because we can always
choose a number which is contained in both χ(Y, x) and χ(Y, t) and which is an
“actual” multiplicity. For instance, we can take n = 6 ∈ χ(Y, x) ∩ χ(Y, f (z, z)) and
U
since we have 6 ≥ 3 = |Y | − 1, we get that the sharing group Y = uvx∞ yz ∞
belongs to mgu2 ([S]U , x/f (z, z)). This sharing group can be generated by the substitution {x/f (f (u, u, y), f (v, v, y)), z/f (w, w, w)} when the variables of interest are
{u, v, x, y, z}.
Theorem 5.5 gives a characterization of the abstract unification over ShLin2 .
However, it cannot be directly implemented, since one needs to check a certain
condition for each element of ℘m (rel (S, x, t)), which is an infinite set. Nonetheless,
this is an important starting point to prove correctness and completeness of the
abstract unification algorithm which we are going to introduce.
The characterization in Theorem 5.5 may be used even when vars(x/t) * U , if
we first enlarge the set of variables of interest in order to include all vars(x/t).
Theorem 5.7 (Characterization of abstract unification with extension for ShLin2 )
Given [S]U in ShLin2 and the binding x/t, let V = {v1 , . . . , vn } be vars(x/t) \ U .
Then,
mgu2 ([S]U , x/t) = mgu2 ([S ∪ {v1 , . . . , vn }]U∪V , x/t) .
The previous theorem states that enlarging the set of variables of interest preserves
optimality.
5.2 An algorithm for abstract unification in ShLin2
In order to obtain an algorithm from the characterization in Theorem 5.5 we need
to avoid the use of ℘m (rel (S, x, t)) and to develop a procedure able to compute

On the interaction between sharing and linearity

25

the resultant sharing groups by inspecting subsets (not multisets!) of rel (S, x, t). In
general, any X ⊆ rel (S, x, t) yields more than one sharing group, since every element
in X may be considered more than once. However, since ShLin2 is downward closed,
it is enough to compute the maximal resultant sharing groups.
Given X ⊆ rel (S, x, t) and the binding x/t, assume that we are only interested
U
in those sharing groups whose support is T XU. By joining (multiple copies of)
U
U
the sharing groups in X, any resultant sharing group o is between X and X 2 ,
U
U 2
i.e., X ≤ o ≤ X , where X 2 is the pointwise extension of the delinearization
operator (see Eq. 5). Note that, if X is badly chosen, it is possible that we are
not able to generate any sharing group with this support. In this computation, the
notion of multiplicity of a sharing group in a term plays a major role.
U
For example, given the binding x/t, if χM (o, x) ≤ 1 for each o ∈ X, then X is
a resultant sharing group only if there is a unique sharing group o ∈ X such that
vars(t)∩ToU 6= ∅. If there are o1 , o2 ∈ X such that χM (o1 , x) > 1 and χM (o2 , t) > 1
U
then X is a resultant sharing group. Moreover, we may join two copies of each
U
sharing group in X, and therefore also X 2 is a resultant sharing group.
Now we can define the notions of linearity and non-linearity on the abstract
domain. In addition, we also introduce a new notion of strong non-linearity. Given
X ⊆ rel (S, x, t), we partition X in three subsets Xx = {o ∈ X | χM (o, t) = 0},
Xt = {o ∈ X | χM (o, x) = 0} and Xxt = X \ (Xx ∪ Xt ).
Definition 5.8
Given a set S of sharing groups and X ⊆ rel(S, x, t), we say that X is:
• linear for the term t if for all o ∈ X it holds that χM (o, t) ≤ 1;
• non-linear for the term t if there exists o ∈ X such that χM (o, t) > 1;
• strongly non-linear for the term t if there exists o ∈ X such that χM (o, t) = ∞
or there exists o ∈ Xxt such that χM (o, t) > 1.
Analogously, we define linearity and non-linearity of X for the variable x.
Note that, if t is a variable, the non-linear and strongly non-linear cases coincide.
We now present the algorithm for computing the abstract unification in ShLin2 .
Theorem 5.9 (Abstract unification algorithm for ShLin2 )
Given [S]U ∈ ShLin2 and the binding x/t with vars(x/t) ⊆ U , we have
[
mgu2 ([S]U , x/t) = [(S \ S ′ ) ∪ ↓
res(X, x, t)]U ,
X⊆S ′

where S ′ = rel (S, x, t) and res(X, x, t) is defined as follows:
U
1. if X is non-linear for x and t, then res(X, x, t) = { X 2 };
2. if X is non-linear for x and linear for t, |Xx | ≤ 1 and |Xt | ≥ 1, then we have
U
U 2
U
res(X, x, t) = {( Xx ) ⊎ ( Xxt
) ⊎ ( Xt2 )};
3. if X is linear for x and strongly non-linear for t, |Xx | ≥ 1 and |Xt | ≤ 1, then
U
U 2
U
we have res(X, x, t) = {( Xx2 ) ⊎ ( Xxt
) ⊎ ( Xt )};

26

G. Amato and F. Scozzari
4. if X is linear for x and not strongly non-linear for t, |Xt | ≤ 1, then we have
]
]
]
2
res(X, x, t) = {( Z) ⊎ ( Xxt
) ⊎ ( Xt ) | Z ∈ ℘m (Xx ),

|Z| = χM (Xt , t) = χm (Xt , t),

TZU = Xx } ;
5. otherwise res(X, x, t) = ∅.

Example 5.10
Let U = {u, v, x, y} and consider the set of 2-sharing groups S = {∅, xu, x∞ , xy, yv}
and consider the binding x/r(y, y). Note that S ′ = {xu, x∞ , xy, yv}. Let us compute
res(X, x, r(y, y)) for some X’s, subsets of S ′ .

• X = {x∞ , yv}. In this case, χM (x∞ , x) = ∞ and χM (yv, r(y, y) = 2, hence
X is non-linear for x and r(y, y). From the first case of Theorem 5.9, we have
U
U
that res(X, x, r(y, y)) = { X 2 } = { {x∞ , y ∞ v ∞ } = {x∞ y ∞ v ∞ };

• X = {xu, xy, yv}. Then X is linear for x and strongly non-linear for r(y, y),
since xy ∈ Xxt and χM (xy, r(y, y)) = 2. From the third case, it follows that
U
U
U
res(X, x, t) = {( {xu}2 ) ⊎ ( {xy}2 ) ⊎ ( {yv})} = {x∞ y ∞ u∞ v};

• X = {xu, yv}. Then X is linear for x and not strongly non-linear for r(y, y)
(note that χM (yv, r(y, y)) = 2 > 1 and yv ∈ Xt , hence X is non-linear for
r(y, y) but it is not strongly non-linear). Since χM (Xt , r(y, y)) = 2, we only
need to consider those Z ∈ ℘m (Xx ) such that |Z| = 2. There is only one such
U
set, which is Z = {{xu, xu}}. Therefore res(X, x, r(y, y)) = {( {{xu, xu}}) ⊎
U 2
U
( {} ) ⊎ ( {yv})} = {x∞ yu∞ v}.
Note that, given X ⊆ S ′ , if x does not appear in any sharing group of S, then
res(X, x, t) ⊆ {∅}. In fact, we can only apply the fourth or fifth case. In the fourth
case, we have that Xx = Xxt = ∅, and thus the only Z ∈ ℘m (Xx ) is the empty
multiset. Thus, |Z| = 0, which implies that Xt = ∅, and res(X, x, t) = {∅}. In
the fifth case, the result is trivially the emptyset. Symmetrically, when none of the
variables of t appears in S, again we can apply only the fourth or fifth case, and
res(X, x, t) ⊆ {∅}.

Example 5.11
Consider S and U as in Example 5.10. We compute mgu2 ([S]U , x/r(y, y)). We show
the value of res(X, x, r(y, y)) for every X ⊆ S ′ = rel (S, x, r(y, y)) which contains

On the interaction between sharing and linearity

27

both the variables x and y:
X

res(S, x, r(y, y))

case in Theorem 5.9

x∞ , xy
x∞ , yv
x∞ , xy, yv
x∞ , xu, xy
x∞ , xu, yv
x∞ , xu, xy, yv
xu, xy
xu, yv
xu, xy, yv

x∞ y ∞
x∞ y ∞ v ∞
x∞ y ∞ v ∞
x∞ y ∞ u∞
x∞ y ∞ u∞ v ∞
x∞ y ∞ u∞ v ∞
x∞ y ∞ u∞
x∞ yu∞ v
x∞ y ∞ u∞ v

1
1
1
1
1
1
3
4
3

Hence
mgu2 ([S]U , x/r(y, y)) =
↓{∅, x∞ y ∞ , x∞ y ∞ v ∞ , x∞ y ∞ u∞ , x∞ y ∞ u∞ v ∞ , x∞ yu∞ v, x∞ y ∞ u∞ v}
The main difference between the algorithm in Theorem 5.9 and the characterization in Theorem 5.5 is that in the former X is a subset of S ′ while, in Theorem 5.5, Y
is a multiset over S ′ . Since the number of subsets of S ′ is finite, the characterization
in Theorem 5.9 is an algorithm.
Obviously, a direct implementation of mgu2 would be very slow, so that appropriate data structures and procedures should be developed for a real implementation.
Although this is mostly out of the scope of this paper, we show here that the
definition of mgu2 ([S]U , x/t) may be modified to consider only maximal subsets
of rel (S, x, t). This should help in reducing the computational complexity of the
abstract operator.
Given [A]U ∈ ShLin2 , let max A be the set of maximal elements of A, i.e.,
max A = {a ∈ A | ∄b ∈ A.b >2 a}. Given a sharing group o, we define the linearized version of o, denoted by l(o), as
(
1 if v ∈ ToU ,
l(o)(v) =
0 otherwise .
The linearization operator l is extended pointwise to sets of sharing groups. We
show that instead of choosing X as a subset of S ′ in the definition of mgu2 , we may
only consider those X’s which are subsets of max S ′ .
Theorem 5.12
Given [S]U ∈ ShLin2 and the binding x/t with vars(x/t) ⊆ U , we have
[
mgu2 ([S]U , x/t) = [(S \ S ′ ) ∪ ↓
(res(X, x, t) ∪ res ′ (X, x, t))]U ,
X⊆max S ′

where S ′ = rel (S, x, t) and
( U
{ X 2}
res ′ (X, x, t) =
∅

if X = Xxt and l(X) is linear for t ,
otherwise .

28

G. Amato and F. Scozzari

The next examples compare our optimal abstract unification operator to the
original one and show the increase in precision.
Example 5.13
Let U = {u, v, w, x, y}. Consider the set of 2-sharing groups S = {∅, xu, xv, xw, y}.
We compute mgu2 ([S]U , x/r(y, y)). Since rel(S, x, r(y, y)) = S, we need to consider any X ⊆ S. If y ∈
/ X then clearly res(X, x, r(y, y)) = ∅. If y ∈ X, since
χM (y, r(y, y)) = 2, it follows that X is linear for x and not strongly non-linear for
r(y, y). Thus
mgu2 ([S]U , x/r(y, y)) = [↓{∅, x∞ u∞ y, x∞ uvy, x2 uwy, x∞ v ∞ y, x∞ vwy, x∞ w∞ y}]U
On the other hand, computing with the unification algorithm given in (King 1994),
the result is
↓{∅, x∞ u∞ y, x∞ u∞ v ∞ y, x∞ u∞ w∞ y,
x∞ v ∞ y, x∞ v ∞ w∞ y, x∞ w∞ y, x∞ u∞ v ∞ w∞ y} .
The old algorithm is not able to infer the linearity which arises when combining two
distinct sharing groups from {xu, xv, xw} with {y}. Moreover, it does not assert
that the variables u, v, w cannot share a common variable.
Example 5.14
Let U = {u, x, y, z} and S = {∅, xu, xy, yz}. By computing mgu2 ([S]U , x/r(y))
we obtain ↓{∅, x∞ y ∞ , x∞ uy ∞ z}, which shows that u and z are linear after the
unification. This is not the case when computing with the unification algorithm in
(King 1994), since we obtain ↓{∅, x∞ y ∞ , x∞ u∞ y ∞ z ∞ , x∞ u∞ y ∞ , x∞ y ∞ z ∞ }. Note
that, we also improve the groundness information. In fact, in our result, groundness
of u implies groundness of z.
Both examples show the increased precision w.r.t. King’s algorithm. In the first
example, we obtain optimality thanks to the introduction of the notion of (non-)
strong non-linearity. In the second example, we improve the result since we do
not need to consider independence between x and t, in order to exploit linearity
information.
5.3 Unification for multi-binding substitutions
The unification operator on ShLin2 has been defined for single binding substitutions. It is possible to extend this operator to multi-binding substitutions in the
obvious way, namely by iterating the single binding operators.
mgu2 ([S]U , {x/t} ⊎ θ) = mgu2 (mgu2 ([S]U , x/t), θ) .
However, defined in such a way, mgu2 is not optimal. Consider, for example, S =
{∅, xz, yw}, U = {x, y, z, w}, and the substitution θ = {x/r(y, y), z/w}. We have
that mgu2 ([S]U , x/r(y, y)) = [↓ {∅, x∞ z ∞ yw}]U . Since x∞ zyw ≤2 x∞ z ∞ yw, by
applying the third case of mgu2 to Y = {x∞ zyw} we get
mgu2 ([↓ {∅, z ∞ x∞ yw}]U , z/w) = [↓ {∅, x∞ y ∞ z ∞ w∞ }]U .

On the interaction between sharing and linearity

29

However,
α2 (mguω (γ2 ([{∅, xz, yw}]U , θ)))
= α2 (mguω ([{xz, yw}]U , θ))
= α2 (mguω ([{wx2 yz 2 }]U , {z/w}))
= α2 ([{{}}]U ) = [∅]U ,
which shows that mgu2 is not optimal. Note that, we do not use optimality of mguω
to prove this result, since correctness is enough.
The problem is that, to be able to conclude that the unification of S with θ is
ground, we need to keep track of the fact that, after the first binding, w is linear
and z is definitively non-linear. Since ShLin2 is downward closed, we are not able
to state this property. Note that, in the case we have presented here, by changing
the order of the bindings we get an optimal result in ShLin2 , but this happens just
by accident.
Now, consider the substitution θ = {x/r(y, ...., y), z/s(y, ..., y), u/v} with S =
{∅, xu, zv, y} and U = {u, v, x, y, z}. Assume that r(y, ...., y) is an n-ary term,
s(y, ..., y) is an m-ary term with n 6= m and n, m ≥ 2. We have that:
mgu2 ([S]U , x/r(y, ...., y)) = [↓{∅, x∞ u∞ y, zv}]U ,
mgu2 ([↓{∅, x∞ u∞ y, zv}]U , z/s(y, ..., y)) = [↓{∅, x∞ u∞ z ∞ v ∞ y}]U ,
mgu2 ([↓{∅, x∞ u∞ z ∞ v ∞ y}]U , u/v) = [↓{∅, x∞ u∞ z ∞ v ∞ y}]U .
On the other hand, we have that:
α2 (mguω (γ2 ([{∅, xu, zv, y}]U , θ)))
= α2 (mguω ([{xu, zv, y}]U , θ))
= α2 (mguω ([{xn un y, zv}]U , {z/s(y, ..., y), u/v}))
= α2 (mguω ([{xn un yz m v m }]U , {u/v}))
= α2 ([{{}}]U ) = [∅]U .
However, if n = m, we have:
α2 (mguω (γ2 ([{∅, xu, zv, y}]U , θ)))
= α2 ([{{{}}} ∪ {xkn ukn y k z kn v kn | k ∈ N}]U )
= [↓{∅, x∞ u∞ z ∞ v ∞ y}]U .
In this case, keeping track of the variables which are definitively non-linear does
not help. It seems that, in order to compute abstract unification one binding at
a time, we need to work in a domain which is able to keep track of the exact
multiplicity of variables in a sharing group. Actually, this is how ShLinω works.
Obviously, we could try to develop a different algorithm for unification in ShLin2
which directly works with multi-binding substitutions. However, since the algorithm
for single binding substitutions is already quite complex, we think this is not worth
the effort.

30

G. Amato and F. Scozzari
5.4 The domain Sharing × Lin

The reduced product ShLin = Sharing × Lin has been used for a long time in the
analysis of aliasing properties, since it was recognized that the precision of these
analyses could be greatly improved by keeping track of the linear variables. Among
the papers which consider the domain ShLin, we refer to (Hans and Winkler 1992)
and (Hill et al. 2004). Actually, these papers also deal with freeness properties,
which we do not consider here, to further improve precision. Although the domain
ShLin has been used for many years, the optimal unification operator is as yet
unknown, even for a single binding substitution. We provide here a new abstract
operator for ShLin, designed from the abstract unification for ShLin2 , and we prove
that it is optimal for single binding substitutions.
The domain ShLin keeps track of linearity by recording, for each object of
Sharing, the set of linear variables. Each element is now a triple: the first component is an object of Sharing, the second component is an object of Lin, that is, the
set of variables which are linear in all the sharing groups of the first component,
and the third component is the set of variables of interest. It is immediate that
ShLin is an abstraction of ShLin2 (and thus of ShLinω ). In the following, we briefly
recall the definition of the abstract domain and provide the abstraction function
from ShLin2 .
ShLin = {[S, L, U ] | S ⊆ ℘(U ), (S 6= ∅ ⇒ ∅ ∈ S), L ⊇ U \ vars(S), U ∈ ℘f (V)} ,
with the approximation relation ≤sl defined as [S, L, U ] ≤sl [S ′ , L′ , U ′ ] iff U = U ′ ,
S ⊆ S ′ , L ⊇ L′ . There is a Galois insertion of ShLin into ShLin2 given by the pair
of maps:
αsl ([S]U ) = [{ToU | o ∈ S}, {x ∈ U | ∀o ∈ S. o(x) ≤ 1}, U ] ,
γsl ([S, L, U ]) = [{BL | B ∈ S}]U ,
where BL is the 2-sharing group which has the same support of B, with linear
variables dictated by the set L. In formula:


∞ if B ∈ U \ L,

BL = λv ∈ V. 1
if B ∈ L,


0
otherwise.

The functional composition of αω , α2 and αsl gives the standard abstraction
map from substitutions to ShLin. We still use the polynomial notation to represent
sharing groups, but now all the exponents are fixed to one. Note that the last
component U in [S, L, U ] is redundant since it can be retrieved as L ∪ vars(S). This
is because the set L contains all the ground variables.
5.5 Abstract unification for Sharing × Lin
In order to obtain a correct and optimal abstract unification over ShLin, the trivial
way is to directly compute αsl (mgu2 (γsl ([S, L, U ]), x/t)). However, we prefer to give

On the interaction between sharing and linearity

31

an unification operator similar to the other operators for ShLin in the literature
(Howe and King 2003; Bagnara et al. 2005; Hill et al. 2004). As for the domain
ShLin2 , we now provide the notions of multiplicity and linearity over ShLin.
Given a set L of linear variables, we define the maximum multiplicity of a sharing
group o in a term t as follows:
(P
v∈o occ(v, t) if o ∩ vars(t) ⊆ L
χL
M (o, t) =
∞
otherwise
According to the similar definition for 2-sharing groups, given [S, L, U ] ∈ ShLin, we
say that (S, L) is linear for a term t when for all o ∈ S it holds that χL
M (o, t) ≤ 1.
Note that, when t is a variable, the definition boils down to check whether t ∈ L.
Given X ⊆ rel (S, x, t), we fix the set L of linear variables and partition X in
L
three subsets Xx = {o ∈ X | χL
M (o, t) = 0}, Xt = {o ∈ X | χM (o, x) = 0} and
Xxt = X \ (Xx ∪ Xt ). Moreover, we need to define the following subsets of X:
Xt=∞
Xt=1
=1
Xxt

= {B ∈ Xt | χL
M (B, t) = ∞},
= {B ∈ Xt | χL
M (B, t) = 1},
= {B ∈ Xxt | χL
M (B, t) = 1},

Xt∈N
Xt>1
>1
Xxt

= {B ∈ Xt | χL
M (B, t) ∈ N},
= {B ∈ Xt | χL
M (B, t) > 1},
L
= {Xxt | χM (B, t) > 1}.

Since we do not deal with definite linearity, we need to take into account the sharing
groups which can be obtained by linearizing variables. This may be accomplished
U
by using the set U instead of L when computing the multiplicity. We denote by Xxt
the set
U
Xxt
= {B ∈ Xxt | χU
M (B, t) = 1} ,

which corresponds to the linearizable sharing groups.
Moreover, given sets A1 , . . . , An with n ≥ 2 we denote by bin(A1 , . . . , An ) the
S
S
set { {a1 , . . . , an } | a1 ∈ A1 , . . . , an ∈ An }, by A∗ the set { B | B ⊆ A} and by
S
A+ the set { B | B ⊆ A, B 6= ∅}. This notation slightly deviates from most of
other literature on Sharing, where A∗ does not include the empty set. We prefer
to adopt a double notation, namely, A∗ and A+ , which is more standard in the rest
of the research community.

Definition 5.15 (Abstract unification algorithm for ShLin)
Given [S, L, U ] ∈ ShLin and the binding x/t such that vars(x/t) ⊆ U , we define
mgusl ([S, L, U ], x/t) = [(S \ X) ∪ K, U ′ ∪ L′ , U ] ,
where X = rel (S, x, t) = {B ∈ S | B∩vars(x/t) 6= ∅} and U ′ = U \vars((S\X)∪K).
Here, K is the set of new sharing groups created by the unification process and U ′
is the set of variables which do not appear in any sharing group of the result, i.e.
the set of ground variables. K is defined as follows:

32

G. Amato and F. Scozzari

• If x ∈ L:
∗
K = bin(Xt=∞ , Xx+ , Xxt
)∪
>1
∗
bin(Xt ∪ {∅}, Xxt
, Xx+ , Xxt
)∪
=1 ∗
bin({{o} ∪ (∪Z) | o ∈ Xt∈N , Z ⊆ Xx , 1 ≤ |Z| ≤ χL
M (o, t)}, (Xxt ) )∪

(6)

U +
(Xxt
) .

• If x ∈
/ L:
>1
K = bin(Xt>1 ∪ Xxt
, Xx ∪ Xxt , X ∗ )∪
=1
=1 ∗
bin((Xt=1 )+ , Xx ∪ Xxt
, (Xxt
) )∪
=1 +
(Xxt
)

(7)

.

Finally, the set L′ of linear variables which are not ground is


L \ (vars(Xx ∪ Xxt ) ∩ vars(Xt ∪ Xxt )) if (S, L) is linear for x and t,



L \ vars(X ∪ X )
otherwise, if (S, L) is linear for x,
x
xt
L′ =
(8)

otherwise, if (S, L) is linear for t,
L \ vars(Xt ∪ Xxt )



L \ vars(X)
otherwise.

Theorem 5.16 (Optimality of mgusl )
The operator mgusl in Definition 5.15 is correct and optimal w.r.t. mgu, when
vars(x/t) ⊆ U .

Example 5.17
Let S = {∅, xv, xy, zw}, L = {v, w, x, y}, U = {v, w, x, y, z} and consider the binding x/f (y, z). It is easy to check that (S, L) is linear for x but not for t. Applying our operator, we obtain mgusl ([S, L, U ], x/f (y, z)) = [S ′ , L′ , U ] with S ′ =
{∅, xy, vwxyz, vwxz} and L′ = {w}. This is more precise that the operators for
Sharing × Lin in (Hans and Winkler 1992). Actually, even using the optimizations
proposed in (Howe and King 2003; Hill et al. 2004), one obtains as result the object
[{vxy, vwxz, xy, wxyz, vwxyz}, {w}, U ] .
The optimization proposed in (Bagnara et al. 2005) is not applicable as it is, since it
requires vars(rel (S, x)) and vars(rel (S, f (y, z))) to be disjoint. Even assuming that
this test for independence may be removed as unnecessary, the final result would
be the same as above. In both cases, our operator is able to prove that vxy and
wxyz are not possible sharing groups.
Note that, in a domain for rational trees, the sharing group vxy is needed for
correctness, since the unification of {x/f (f (v, y), c), z/w} with the binding x/f (y, z)
succeeds with {x/f (f (v, y), c), z/c, w/c, y/f (v, y)}. This means that we are able to
exploit the occur-check of the unification in finite trees. As a consequence, our
abstract unification operator is not correct w.r.t. a concrete domain of rational
substitutions (King 2000).

On the interaction between sharing and linearity

33

An alternative would be to compute the abstract unification following Theorem
5.9 with χM and ⊎ replaced by χL
M and ∪ respectively (we can obviously ignore the
delinearization operator ( )2 since B ∪ B = B). However, we do not pursue further
this approach.
In the case vars(x/t) * U , we may proceed as for ShLinω and ShLin2 : enlarge the
set of variables of interest in order to include all vars(x/t) and compute unification
with mgusl .
Definition 5.18 (Abstract unification algorithm with extension in ShLin)
Given [S, L, U ] ∈ ShLin and the binding x/t, let V = {v1 , . . . , vn } be vars(x/t) \ U .
We define:
mgusl ([S, L, U ], x/t) = mgusl ([S ∪ {v1 , . . . , vn }, L ∪ V, U ∪ V ], x/t) .
Theorem 5.19 (Optimality of mgusl with extension)
The operator mgusl in Definition 5.18 is the optimal abstraction of mgu.
Although the abstract operator mgusl is optimal for the unification with a single
binding, the optimal operator for a multi-binding substitution cannot be obtained
by considering one binding at a time. This is a consequence of the fact that the
corresponding operator for single binding unification on ShLin2 cannot be extended
to an optimal multi-binding operator by simply considering one binding at a time.
In fact, all the counterexamples in Section 5.3 are also counterexamples for mgusl ,
since it is the case that [S]U = γsl (αsl ([S]U )).
6 Optimal unification in practice
In this section, we give some evidence that there are practical advantages in using
the optimal unification operators for ShLin. It is far beyond the scope of this paper to provide an experimental evaluation of the new algorithms, but the results
in (Bagnara et al. 2005) give some hints on its possible outcome. Bagnara et al.
(2005) introduce an improvement for Sharing × Lin × Free exploiting some ideas
from King’s unification operator for the domain ShLin2 . In this way, they improve
precision in a few cases and show that efficiency of the analysis is more likely to be
increased than decreased. In fact, even if the final result of the analysis does not
change, a more precise operator may reduce the number of sharing groups in the
intermediate steps, which helps performance. Hence, we expect the optimal unification for ShLin to further improve the analysis, both in efficiency and precision. This
is more evident if we consider that Bagnara et al. (2005) measure precision in terms
of the number of independent pairs (as well as definitively ground, free and linear
variables) and do not consider set-sharing. However, Bueno and Garcı́a de la Banda
(2004) show that set-sharing information may be useful in several application of the
analysis, such as parallelization of logic programs. Hence, a greater improvement in
precision is to be expected if we consider the full set-sharing property.
We now provide a concrete example of a simple program where our abstract
operators give better results than the operators known in the literature.

34

G. Amato and F. Scozzari
6.1 An example: difference lists

We work with difference lists, an alternative data structure to lists for representing
a sequence of elements. A difference list is a term of the kind A \ B where A and
B are lists, which represents the list obtained by removing B from the tail of A.
For example, using PROLOG notation for lists, [1, 2, 3, 4] \ [3, 4] represents the list
[1, 2], while [1, 2, 3|x] \ x and [1, 2, 3] \ [] represent the list [1, 2, 3]. The difference
lists whose tail is a variable (such as [1, 2, 3|x] \ x) are mostly useful, since they can
be concatenated in constant time. An overview of difference lists may be found in
(Sterling and Shapiro 1994).
We define the predicate difflist /3, which translates lists to difference lists and
vice-versa. The goal ← difflist (l, h, t) succeeds when the difference list h\t represents
the standard list l. For example, difflist ([], x, x) and difflist ([1, 2, 3], [1, 2, 3|x], x)
succeed without any further instantiation of variables. In order to improve the precision of the analysis, we keep head and tail of difference lists in separate predicate
arguments. The code for difflist /3, in head normal form, is the following.
difflist (l, h, t) ← l = [], h = t.
difflist (l, h, t) ← l = [x|l′ ], h = [x|h′ ], difflist (l′ , h′ , t).
where l, l′ (list), h, h′ (head), t (tail) and x are variables. We informally compute
the goal-independent analysis of difflist on the domain ShLin, which gives:
Jdifflist K0 =[{∅}, {l, h, t}, {l, h, t}] ,
Jdifflist K1 =[{∅, ht, hl}, {l, h, t}, {l, h, t}] ,
Jdifflist K2 =Jdifflist K1 .
The result of the analysis is not affected by our improved unification operator:
the standard mgu for ShLin, as given in (Hans and Winkler 1992), yields exactly
the same result. Now, suppose we want to analyze the goal ← difflist (l, h, h). This
corresponds to the goal ← difflist (l, h, t), h = t in head normal form. Its semantics
may be computed, using our operators, as
mgusl ([{∅, ht, hl}, {l, h, t}, {l, h, t}], h/t) = [{∅, ht}, {l}, {l, h, t}] .
By projecting over l and h, we get [{∅, h}, {l}, {l, h}]. Hence, the analysis is able to
infer that, upon exiting the goal ← difflist (l, h, h), the variable l is ground.
By using the standard mgu for ShLin in (Hans and Winkler 1992), we get
[{∅, ht, htl}, {l}, {l, h, t}] ,

(9)

hence l is detected to be linear but not ground. The optimizations introduced
in (Howe and King 2003; Hill et al. 2004; Bagnara et al. 2005) do not improve
this result. This is a consequence of the fact that these optimizations have been
developed to be correct also for rational trees. In this case, you cannot infer that
l is ground after ← difflist (l, h, h) since the substitution in rational solved form
{l/[v], h/[v|h]} is a correct answer for the same goal.
If we perform the analysis in ShLin2 , using our operators we have Jdifflist K =
[{∅, hl, ht}]lht and the result for the goal ← difflist (l, h, h) is [{∅, h}]lh . However,

On the interaction between sharing and linearity

35

by using the original operator in (King 1994), the semantics of difflist does not
change, but the result for the goal ← difflist (l, h, h) is [{∅, h∞ , h∞ l∞ }]lh thus l is
not proven to be either ground or linear.
The fact that optimal operators improve groundness information is somehow
surprising. Generally, one expects that groundness affects aliasing analysis, but not
vice-versa. In fact, it is well known that Sharing is a refinement (Cortesi et al.
1997) of the domain Def. However, as far as groundness is concerned, the precision
of Sharing and Def is the same, i.e., the other objects included in Sharing do
not improve groundness analysis (Cortesi et al. 1998). As far as we know, there is
no abstract unification operator in the literature, for a domain dealing with sharing, freeness and linearity, which is more precise that Def for groundness. On the
contrary, the example above shows that ShLin, endowed with the optimal unification, improves over Def. Amazingly, in this example ShLin is even better than Pos
(Armstrong et al. 1994). In the latter, the abstract semantics of difflist is h ↔ (l∧t),
i.e., h is ground iff both l and t are ground. The result of the analysis for the goal
← difflist (l, h, h) is ∃t (h ↔ (l ∧ t) ∧ h ↔ t). This is equivalent to h → l which does
not imply groundness of l. Actually, h → l is the groundness information which
may be inferred by (9).
6.2 Another example for ShLin2
As far as we know, there is no implementation or experimental evaluation of the
domain ShLin2 . We think it would be worthwhile to give such an implementation
and that there is some evidence that ShLin2 improves over ShLin also in practice.
For instance, we show a simple program where King’s domain is more precise than
ShLin with optimal operators.
We provide a variant of the predicate difflist /3, which we call difflist ′ /2, with
only two arguments: head and tail of the difference list are encoded in the second
argument as the term head \ tail .
difflist ′ (l, d) ← l = [], d = h \ h.
difflist ′ (l, d) ← l = [x|l′ ], d = [x|h] \ t, d′ = h \ t, difflist ′ (l′ , d′ ).
We informally compute the goal-independent analysis of difflist ′ on the domain
ShLin, which gives:
Jdifflist ′ K0 =[{∅}, {d, l}, {d, l}] ,
Jdifflist ′ K1 =[{∅, dl, d}, {l}, {d, l}] ,
Jdifflist ′ K2 =Jdifflist ′ K1 .
The same analysis, computed over ShLin2 , gives
Jdifflist ′ K0 =[{∅}]dl ,
Jdifflist ′ K1 =[{∅, dl, d, d∞ }]dl ,
Jdifflist ′ K2 =Jdifflist ′ K1 .
Now, suppose we want to analyze the goal ← difflist ′ (l, d), d = [x1 , x2 |h] \ t,

36

G. Amato and F. Scozzari

which extracts the first two elements from the difference list d. In ShLin we have
the following
mgusl ([{∅, dl, d}, {l}, {d, l}], d/[x1, x2 |h] \ t) =
[{∅} ∪ bin({dl, d}, {x1 , x2 , h, t}∗ ), {l}, {d, l, x1, x2 , h, t}] .
Note that the sharing group dlx1 x2 is part of the result. If we repeat the analysis
in ShLin2 , we have

mgu2 ([{∅, dl, d, d∞ }]dl , d/[x1 , x2 |h] \ t) = {∅, dlx1 , dlx2 , dlh, dlt} ∪
]

∞ ∞ ∞ ∞ ∞ ∞
↓
X | X ∈ ℘({d∞ x∞
1 , d x2 , d h , d t }) dlx1 x2 ht .

This result does not contain the sharing group dlx1 x2 .
Generally speaking, it is easier to analyze the predicate difflist /3 than difflist ′ /2.
Codish et al. (2000) propose a method named untupling which is able to automatically recover difflist /3 from difflist ′ /2.
7 Related work

In this paper, we work with a concrete domain of substitutions on finite trees. In
the literature, some authors deal with rational trees.
Since any correct operator for rational trees is also correct for finite trees, we can
compare the unification operators for rational trees with ours (of course, this is not
entirely fair as far as the precision is concerned). The opposite is not true, since an
abstract unification operator for finite trees may be able to exploit the occur-check
condition. We have shown in Example 5.17 that our optimal operator can exploit
the occur-check condition, and thus it is not correct for rational trees.
7.1 Sharing
It is well-known that the abstract unification operator of the domain Sharing alone
(i.e., without any freeness or linearity information) is optimal. Cortesi and Filé
(1999) give a formal proof of optimality, considering a slightly different unification operator with two abstract objects and a concrete substitution. Since the two
abstract objects are renamed apart, it is equivalent to consider a single abstract
object. The basic idea underlying the proof is to exhibit, for each sharing group in
the result of the unification, a pair of concrete substitutions generating the resulting
sharing group. We follow the same constructive schema in the proof of optimality
for ShLinω (but we look for a single substitution, due to the different concrete operator). Instead, to prove optimality for ShLin and ShLin2 , we use a direct approach
and show that the abstract unification operator corresponds to the best correct
abstraction (i.e., α ◦ mguω ◦ γ) of the unification on ShLinω with simple (although
tedious) algebraic manipulations.
A different unification operator has been proposed in (Amato and Scozzari 2002;
Amato and Scozzari 2009) for goal-dependent analysis of Sharing. In this paper,
the standard unification operator is splitted into two different operators for forward

On the interaction between sharing and linearity

37

and backward unification. Both operators are proved to be optimal and the overall
analysis is strictly more precise than the analysis performed on Sharing equipped
with the standard operator.
As far as we know, these are the only optimality results for domains encoding
aliasing properties.
7.2 Sharing × Lin
In most of the work combining sharing and linearity, freeness information is included
in the abstract domain. In fact, freeness may improve the precision of the aliasing
component and it is also interesting by itself, for example in the parallelization
of logic programs (Hermenegildo and Rossi 1995). In this comparison, we do not
consider the freeness component.
The first work which combines set-sharing with linearity is (Langen 1990), followed by (Hans and Winkler 1992). The initial unification algorithm has been
improved by Howe and King (2003) and Hill et al. (2004) by removing an independence test. This increases the number of cases when linearity information may
be exploited. Bagnara et al. (2005) propose a different improvement, adopting an
idea by King (1994) for the domain ShLin2 , which simplifies the unification of a
linear term with a non-linear one. Example 5.17 shows that, even adopting all these
improvements, we still obtain a strictly more precise operator. Since our operator
is optimal, any further improvement is now impossible.
Bagnara et al. (2002) show that, if we are only interested in pair-sharing information, Sharing is redundant. They propose a new domain SS ρ which is obtained by
discharging redundant sharing groups. A sharing group B in a set S is redundant
if |B| > 2 and ∀x, y ∈ B. ∃C ∈ S. {x, y} ⊆ C ⊂ B. Analyses performed with SS ρ
are shown to be as precise as those performed with Sharing, if only pair-sharing
information is required. Hill et al. (2004) introduce the domain SS ρ × Lin × Free.
Example 5.17 shows that our operator is still more precise (of course, without considering the freeness component), because of the sharing group vxy which does not
appear in S ′ and is not redundant for SS ρ . In any case, Bueno and Garcı́a de la
Banda (2004) have shown that classical applications of sharing analyses, such as
parallelization of logic programs, are able to exploit information which is encoded
in Sharing × Free but not in SS ρ × Free.
An alternative presentation of Sharing × Lin, based on set logic programs, has
been introduced by Codish et al. (2000). However, the proposed operators are not
optimal, as shown in Hill et al. 2004.
The domain ShLin2 is introduced by King (1994), which provides correct operators for abstract unification. However, these operators are not optimal, as Examples
5.13 and 5.14 show.
7.3 ASub
An alternative approach to aliasing analysis is to only record sharing between pairs
of variables (and possibly linearity and groundness information). The best known

38

G. Amato and F. Scozzari

domain of this category is ASub, introduced by Søndergaard (1986) and formalized
by Codish et al. (1991). The domain ASub is the reduced product of pair-sharing, Lin
and Con (Jones and Søndergaard 1987), which is the simplest domain for definite
groundness. Recently, King (2000) reformulated the proofs in order to work with
rational trees. Moreover, King’s algorithms are parametric w.r.t. the groundness
domain, allowing to replace Con with more precise domains such as Def and Pos.
The domain Sharing × Lin is strictly more precise than ASub, since it embeds
more groundness information (equivalent to Def) and set-sharing information. Since
our operator for Sharing × Lin is optimal, we are sure that the analyses performed
in Sharing × Lin are strictly more precise than those in ASub.
The following is a counterexample to the optimality of the abstract unification
in (King 2000), in the case of finite trees, when pair sharing is equipped with Def
or Pos.
Example 7.1
Consider the object κ = (x ↔ y, {xy}) where the first component is a formula of Def
and Pos and {xy} is the set of pairs of variables which may possibly share. In this
domain, linearity information is embedded in the second component in the following
way: if v is not linear, then vv must be included in the second component. Thus, both
x, y and z are linear in (x ↔ y, {xy}). We want to unify κ with x/f (y, z). By using
the algorithm (King 2000), we obtain (y ↔ x∧x → z, {xy, xz, yz, xx, yy}). However,
in Sharing × Lin we may represent κ with [S, L, U ] = [{xy, z}, {x, y, z}, {x, y, z}]
and mgusl ([S, L, U ], x/f (y, z)) = [{xy}, {z}, {x, y, z}] which proves that z is ground.
Actually, King (2000) does not state explicitly how to compute the groundness
component of the result, although he says that it must be computed before the
linearity and pair-sharing components, in order to improve precision. However, it
seems safe to assume that the author’s intention was to compute the groundness
component using the abstract operators already known, and therefore independently from the pair sharing component. This is what makes our operator more
precise, since linearity information may help in tracking ground variables when
working over finite trees.
7.3.1 Alternating paths
The domain ASub and its derivatives (King 2000) use the concept of alternating
path. Alternating paths may seem the counterparts, for pair-sharing, of sharing
graphs. We now investigate this idea, and show to what extent this correspondence
is faithful.
We call carrier graph a special graph defined by a set of equations E. Each
distinct occurrence of a variable in E is a node. Edges in the carrier graphs can be
of two types:
• edges of type one between two variable occurrences if the occurrences are on
opposite sides of a single equation in E,

39

On the interaction between sharing and linearity
• edges of type two linking two (distinct) occurrences of the same variable.

An alternating path is a sequence of edges of alternating type over the carrier graph.
Alternating paths in ASub (and derivatives) are used to prove correctness of
the abstract unification operators. For example, they are used to prove Prop. 3.1
in (King 2000). Sharing graphs are used in this paper to prove Theorem 4.31,
which is the starting point to prove correctness and optimality of the unification
algorithms for ShLin2 and ShLin. However, sharing graphs are also used to compute
the abstract unification in ShLinω . Even if alternating paths are not used, in the
literature, for computing abstract unification, they could. For any object of pairsharing o, which is a set of pairs of variables, consider any substitution θ in the
concretization of o. Then, the object o is an abstraction of the set of alternating
paths in θ. More precisely, it represents all the paths which start and end with edges
of type one, which we call admissible paths. They are abstracted by considering only
the start and end variables. In order to unify o with the binding x/t, we build a
carrier graph with all the occurrences of variables in o and x/t. For each pair of
variables in o, we add an edge of type one. We add edges of type one and two for
the binding x/t, as explained above. Finally, we add all the type two edges between
any occurrence in x/t and any occurrence of the same variable in o. We consider
all the admissible paths over the graph so obtained. It is not difficult to check that
the result of the unification algorithm for pair-sharing in (King 2000), without any
additional groundness domain, is the set of all the start and end variables for all
these admissible paths.
Example 7.2
Let S = {xv} be the set of pairs of variables which share, and consider the binding
x/r(y, y). We obtain the carrier graph:
y





x?
??
??1
??
1

1

v

x

2

2

y

which gives origin to several alternating paths. Among them, there is an admissible
path from v to v, which proves that v is not linear after the unification.
The first difference between alternating paths and sharing graphs is that all the
alternating paths are subgraphs of the same carrier graph, while each sharing graph
has a different structure, with a different set of nodes. The second difference is that
the information coming from the abstract object and the binding is encoded in a
different way. For instance, consider the set S = {xy} and the binding x/z. We
obtain a carrier graph with 4 nodes x, y, x, z, two edges x
2

1

y and x

1

z

x of type two. Therefore, the sharing information
of type one, and an edge x
coming from the initial pair-sharing and the binding is treated symmetrically, and

40

G. Amato and F. Scozzari

is entirely encoded on the edges. Performing unification on the carrier graph boils
down to devising the alternating paths on the graph. On the contrary, each sharing
graph has a set of nodes labelled by xy, x and z, with suitable multiplicities. The
labels of the nodes encode the initial pair-sharing information, while the binding
affects the multiplicity of nodes. The process of unification consists of adding the
necessary arrows to get a sharing graph.
If we consider a single alternating path in a carrier graph and the sharing graph
for the same pair-sharing information and the same binding, they are obviously
related, although not in a straightforward manner. Consider an admissible path
and delete all type two edges, collapsing in a single node their start and end nodes
(type two edges are used in the carrier graph to avoid the creation of invalid paths,
but in a single alternating path they do not add information). Then, each type one
edge coming from the initial pair-sharing information corresponds to a node in the
sharing graph, while a type one edge coming from the binding becomes an arrow
in the sharing graph.
Example 7.3
Consider Example 7.2. We depict the (admissible) alternating path from v to v, its
collapsed version and the corresponding sharing graph.
v

v

1

2

x
1

x

x

✞
☎
0
xv
✝
✆
1

1

y

2

1

y

1

1

y

/

✞
✝

y

x

☎
2
o
✆
0

2

x

1

v

x

1

v

✞
☎
0
xv
✝
✆
1

Note that, while in the carrier graph, non-linearity of the variable x is handled by
duplicating the variable y which occurs twice, in alternating paths without type
two nodes, the duplicated variables are x and v, which are connected to y. The
same holds in the sharing graph, where we have only one node labeled by y and
two nodes labelled by xv.
In sharing graphs we also require the multiplicities of a node to be equal to
its in- and out-degrees. This makes possible to handle groundness at the same
level of sharing and linearity, without requiring a separate domain. Remember that
a sharing group S with multiplicity n corresponds, in the concrete domain, to
a variable u such that θ−1 (u) = S. If the degree of the node labeled with this
sharing group is not n, this means that one of the occurrences of u is bound to a
ground term. This would make ground the entire connected component containing
S. Hence, in order to correctly and precisely propagate groundness, we just forbid
this kind of sharing graphs. On the contrary, the pair-sharing algorithm in (King
2000), which focus on a single path in the carrier graph, is not able to extract
groundness information without the help of an auxiliary domain.

On the interaction between sharing and linearity

41

7.4 Lagoon and Stuckey’s domain
Lagoon and Stuckey (2002) have recently proposed a different approach to pairsharing analysis. The authors use multigraphs, called relation graphs, to represent
sharing and linearity information. The nodes of the multigraph are variables, and
two of them may share only if there is a traversable path from one variable to the
other. Intuitively, each binding generates edges of different types. The definition of
traversable paths is very similar to that of alternating paths. A traversable path is
a sequence of edges, such that contiguous edges are always of different types.
This domain should be coupled with a groundness domain, and operators are
parametric w.r.t. the latter one. The authors show that relation graphs, when coupled with the Def groundness domain, are more precise than Sharing and ASub.
However, this is not the case for Sharing × Lin, at least in the case of finite trees,
since the operators in (Lagoon and Stuckey 2002) are not able to use linearity to
improve the precision of the groundness component.
Example 7.4
As shown in Example 7.1, if we unify [S, L, U ] = [{xy, z}, {x, y, z}, {x, y, z}] with
the binding x/f (y, z), we obtain mgusl ([S, L, U ], x/f (y, z)) = [{xy}, {z}, {x, y, z}],
proving that z is ground after the unification. In the domains ΩDef and ΩPos of
(Lagoon and Stuckey 2002), the abstract object corresponding to [S, L, U ] is

y ,x ↔ y .
µ1 = x

Intuitively, the first element of µ1 encodes the sharing information, namely, that x
and y may share (while z does not share neither with x nor with y). The second
element of µ1 is an element of Pos (and also of Def) and denotes the groundness
information that x is ground if and only if y is ground.
The unification of µ1 with x/f (y, z) in ΩPos is realized by abstracting the substitution and composing the two abstract object. The abstraction of x/f (y, z) is


y







 



µ2 =  x @
, x ↔ (y ∧ z) ,
 @@



@@


@@
z

The first element says that x shares with both y and z, while y and z do not share.
The second element says that x is ground if and only if both y and z are ground.
The abstract conjunction is


y








, (x ↔ y) ∧ (x → z) ,
µ1 f µ2 =  x @

 @@


@@


@@
z

42

G. Amato and F. Scozzari

where edges drawn in different styles are compatible, namely, that they come from
different bindings. From this result, it is not possible to infer that z is ground after
the unification.
In the actual implementation, Lagoon and Stuckey (2002) use another representation for their domain. Each pair of variables is annotated with a formula denoting
the groundness models under which the corresponding pair-sharing may occur. For
example, a pair uv annotated with the formula ū ∧ v̄ ∧ w̄ ∧ z̄ means that u and
v may share only if none of u, v, w, z is ground. We conjecture that this domain
may be embedded in King’s ShLin2 . The next example shows how to perform this
embedding.
Example 7.5
We consider the example in Figure 4 in (Lagoon and Stuckey 2002). The variables
of interest are u, v, w, z.
uw
vz
uv
wz

:
:
:
:

ū ∧ w̄
v̄ ∧ z̄
ū ∧ v̄ ∧ w̄ ∧ z̄
w̄ ∧ z̄

uz
uu
vv
vw

:
:
:
:

ū ∧ z̄
ū ∧ w̄ ∧ z̄
v̄ ∧ w̄ ∧ z̄
v̄ ∧ w̄

For instance, uv : ū ∧ v̄ ∧ w̄ ∧ z̄ means that u and v may share only if u, v, w, z are
not ground, while uu : ū ∧ w̄ ∧ z̄ means that u is (possibly) not linear only if u, w, z
are not ground. Each of these formulas may be viewed as a condition over 2-sharing
groups. For example uv : ū ∧ v̄ ∧ w̄ ∧ z̄ means that every 2-sharing group which
contains u and v should also contain w and z, while uu : ū ∧ w̄ ∧ z̄ means that each
2-sharing group where u is non-linear should also contain w and z. In order to find
the object of ShLin2 which corresponds to this example, it is enough to collect all
the 2-sharing groups which satisfy all the conditions enforced by the formulas. In
this case, we get ↓{u∞ v ∞ wz, u∞ wz, v ∞ wz, uw, vz, wz, uz, vw, u, v, w, z}.
7.4.1 Traversable paths
The idea behind traversable paths is very similar to the concept of alternating path
and relation graphs are quite similar to carrier graphs. From a carrier graph, we
can obtain a relation graph by removing type two edges and introducing a different
type of edge for each binding. This works because the use of non-linear terms is
forbidden: a binding like x/r(y, y) has to be replaced by two bindings x/r(y, z) and
y/z. However, the main difference w.r.t. traditional pair-sharing (and also ShLinω )
is that Lagoon and Stuckey (2002) do not abstract traversable paths to set of pairs
of variables, but they keep in the abstract object the set of all the edges generated
during the unification process. In this way, they are able to record that, in order
for two variables x and y to share, the only possible path touches another variable
z. Hence, if z is ground, x and y cannot share: in this way they recover pair sharing
dependence information which would be lost otherwise.
We could follow the same approach and use multilayer sharing graphs (namely,
sets of sharing graphs over the same set of nodes, where each layer represents the

On the interaction between sharing and linearity

43

unification with a single binding) as abstract objects, without collapsing them to
sharing groups. We do not think this would improve precision of the domain very
much, since a sharing group is already a much more concrete abstraction of a graph
w.r.t. the set of all the connected pairs of variables. In fact, already Sharing can
encode the information that, grounding a certain variable z, two variables x and
y become independent. Moreover, in the Example 7.5 we have shown that relation
graphs may be encoded into ShLin2 .
7.5 Rational trees
In the recent years, many authors have studied the behavior of logic programs on
rational trees (King 2000; Hill et al. 2004), which formalize the standard implementations of logic languages. We have shown that our operators, which are optimal for
finite trees, are not correct for rational trees, since they exploit the occur-check to
reduce the sharing groups generated by the abstract unification (see Example 5.17).
It would be interesting to adapt our framework to work with rational trees, in order
to obtain optimal operators also in this case. Since a rational tree may contain infinite occurrences of a variable, the notion of ω-sharing group needs to be extended in
order to allow infinite exponents. Also, we need to consider infinite sharing graphs
(or, at least, a representation of them) and find suitable regularity conditions for
them, analogously to the regularity conditions on rational trees.
Example 7.6
Consider the set of ω-sharing groups S = {xy, z} and the binding x/r(z, y). On
rational trees, unifying δ = {x/y} (such that [S]xyz 3 [δ]xyz ) with x/r(z, y) would
get the substitution {x/r(z, x), y/r(z, y)} in rational solved form. This, intuitively,
corresponds to the sharing group xω y ω z where the exponent ω denotes an infinite
number of occurrences. A possible (infinite) sharing graph generating this sharing
group is the following:
☎
✞
☎
✞
☎
✞
☎
✞
1
1
1
1
/ xy
/ xy
/ z
/ xy
···
✝
✆
✝
✆
✝
✆
✝
✆
0
1
1
1

Although the structure of abstract objects and operators for adapting ShLinω to
work with rational trees is more complex, we expect the optimal abstract operators
for rational trees on ShLin2 and Sharing × Lin to be simpler than those presented
here for finite trees. This is because we do not need to worry about the occur-check
condition (embedded in our unification operator) and infinite multiplicities.

8 Conclusion and Future Works
We summarize the main results of this paper:
• We define a new domain ShLinω as a general framework for investigating
sharing and linearity properties and provide the optimal unification operator.

44

G. Amato and F. Scozzari
• We show that ShLinω is a useful starting point for studying further abstractions. We obtain the optimal operators for single binding abstract unification
in Sharing×Lin and ShLin2 , and we show that these are strictly more precise
than all the other operators in the literature for the same domains.
• We show, for the first time, an optimality result for a domain which combines
aliasing and linearity information.

Moreover, as a negative result, we prove that the standard schema of the iterative
unification algorithm (one binding at a time) does not lead to optimal operators
for the domains ShLin2 and Sharing × Lin. As a side result, we show that ShLin
and ShLin2 with optimal operators may be more precise than Pos for groundness
analysis.
Several things remain to be explored: first of all, we need to study the impact on
the precision and performance obtained by adopting the new optimal operators and
domains. We plan to implement the operators on ShLin2 and Sharing× Lin within
the CiaoPP static analyzer (Bueno et al. 1997). Moreover, we plan to analyze the
domain SS ρ × Lin (Bagnara et al. 2002) in our framework and, possibly, to devise
a variant of ShLin2 which enjoys a similar closure property for redundant sharing
groups. This could be of great impact on the efficiency of the analysis. Last but not
least, we plan to translate our framework to the case of unification over rational
trees.
A Proofs of Section 4
In this section we give the proofs of the main results of the paper.
Theorem 4.6
The relation 3 is well defined.
Proof
It is enough to prove that {θ1 −1 (v)|U | v ∈ V} = {θ2 −1 (v)|U | v ∈ V} when
θ1 ∼U θ2 . Assume that θ1 ∼U θ2 , then by definition of ∼U there exists a renaming
ρ such that ρ(θ1 (u)) = θ2 (u) for each u ∈ U . Given S = θ1−1 (v)|U , if w = ρ(v) we
have θ2−1 (w)|U = θ1−1 (v)|U = S. This concludes the proof.
Proposition 4.13
Given a substitution θ, a variable v and a term t, we have that χ(θ−1 (v), t) =
occ(v, θ(t)). Moreover, given a set of variables U , when vars(t) ⊆ U , it holds that
χ(θ−1 (v)|U , t) = occ(v, θ(t)).
Proof
Let B = θ−1 (v). The proof is by induction on the structure of the term t. If
t ≡ a is a constant, then occ(v, θ(a)) = occ(v, a) = 0 which is equal to χ(B, a)
since occ(w, a) = 0 for each w ∈ V. If t ≡ w is a variable, then occ(v, θ(w)) =
θ−1 (v)(w) = B(w). At the same time, χ(B, t) = B(w) since occ(w, w) = 1 and

45

On the interaction between sharing and linearity

occ(y, w) = 0 for y 6≡ w. For the inductive case, if t ≡ f (t1 , . . . , tn ), we have
Pn
Pn
occ(v, t) = i=1 occ(v, ti ) = i=1 χ(B, ti ) by inductive hypothesis. Moreover
χ(B, t) =

X

(B(v) ·

n
X

occ(v, ti )) =

B(v) · occ(v, ti ) =

n
X

χ(B, ti ) .

i=1

i=1 v∈TBU

i=1

v∈TBU

n
X
X

Let U be a set of variables with vars(t) ⊆ U . By definition, χ(θ−1 (v)|U , t) =
P
/ U it holds that occ(w, t) = 0,
w∈θ −1 (v)|U occ(w, t). Since vars(t) ⊆ U , for any w ∈
and thus χ(θ−1 (v)|U , t) = χ(θ−1 (v), t).
Proposition 4.24
Given substitutions θ, η ∈ ISubst and an ω-sharing group B, we have
(η ◦ θ)−1 (B) = θ−1 (η −1 (B)) .
Proof
Using the definitions and simple algebraic manipulations, we have
θ−1 (η −1 (B))
=
=


λw.χ λv.χ(B, η(v)), θ(w)
X
λw.
χ(B, η(y)) · occ(y, θ(w))
y

=

λw.

X X
y

=

λw.

X

B(x) · occ(x, η(y))

x

B(x) ·

x

=

λw.

X
x

=

λw.

X

!

X

· occ(y, θ(w))

occ(x, η(y)) · occ(y, θ(w))

y

B(x) ·

X

η −1 (x)(y) · occ(y, θ(w))

y

B(x) · χ(η −1 (x), θ(w)) .

x

By Prop. 4.13, we have that χ(η −1 (x), θ(w)) = occ(x, η(θ(w)) and therefore
θ−1 (η −1 (B)) = (η ◦ θ)−1 (B) .
Theorem 4.25 (Correctness of mguω )
The operation mguω is correct w.r.t. mgu, i.e.,
∀[S]U ∈ ShLinω , δ ∈ ISubst. [S]U 3 [θ]U =⇒ mguω ([S]U , δ) 3 mgu([θ]U , δ) .
Proof
Given [S]U 3[θ]U and δ ∈ ISubst, we need to prove that mguω ([S]U , δ)3mgu([θ]U , δ)
or the equivalent property αω (mgu([θ]U , δ)) ≤ω mguω ([S]U , δ).
Since mguω is defined inductively on the number of bindings in δ, it is enough to
prove that mguω ([S]U , x/t) 3 mgu([θ]U , {x/t}) for a single binding x/t. Since composition of correct operators is still correct, it follows that multi-binding unification
is correct.

46

G. Amato and F. Scozzari

Moreover, when vars(x/t) 6⊆ U , we exploit the identity mgu([θ]U , {x/t}) =
mgu(mgu([θ]U , [ǫ]vars(x/t) ), {x/t}). When computing mgu([θ]U , [ǫ]vars(x/t) ) all the
variables in vars(x/t) \ U occurring in θ are renamed apart from x/t itself. Therefore each v ∈ vars(x/t) \ U is free (hence linear) in mgu([θ]U , [ǫ]vars(x/t) ), i.e.,
αω (mgu([θ]U , [ǫ]vars(x/t) )) = [S ∪ {{{v}} | v ∈ vars(x/t) \ U }]U∪vars(x/t) .
Therefore, it is enough to prove that mguω ([S]U , x/t) 3 mgu([θ]U , {x/t}) when
vars(x/t) ⊆ U . Let B be a sharing group in αω (mgu([θ]U , {x/t})), we prove that
B ∈ mguω ([S]U , x/t).
If B = {{}}, we consider a multigraph G with only one node labelled by {{}} and
no edges. It is easy to check that G is a sharing graph for S (since {{}} ∈ S) and
x/t, and that res(G) = {{}}. Therefore, in the following we consider only the case
B 6= {{}}.
The proof is composed of three parts: first, we look for a (special) substitution β
obtained by renaming some variables in θ and such that β is still approximated by
S; second, we define a multigraph G exploiting the variables of β; third, we show
that we can restrict G to a smaller sharing graph whose resultant ω-sharing group
is exactly B.
First part. Without loss of generality, we assume that dom(θ) = U (this is
always possible since, in any class [θ]U , there exists a substitution whose domain
is exactly U ). Let θ′ = mgu(θ, {x/t}) = η ◦ θ with η = mgu({θ(x) = θ(t)}) and
we have [θ′ ]U = mgu([θ]U , [x/t]U ). Since dom(θ) = U , we have vars(η) ∩ U = ∅.
Consider η ′ obtained from η by replacing each occurrence of a variable in rng(η)
with a different fresh variable. This means that there exists ρ ∈ Subst mapping
variables to variables such that ρ(η ′ (x)) = η(x) for each x ∈ dom(η). Namely, we
have
ρ = {v1 /v2 | ∃x ∈ dom(η), ξ ∈ Ξ s.t. η ′ (x)(ξ) = v1 ∧ η(x)(ξ) = v2 } .
Note that ρ is not a renaming, since it is not bijective. We now show that β = η ′ ◦ θ
has the property that [S]U 3 [β]U . For any C ∈ α([β]U ), we may distinguish three
cases:
• C = {{}}. In this case C ∈ S by definition of ShLinω ;
• C = β −1 (w)|U for w ∈ rng(θ) \ dom(η). In this case occ(w, (η ′ ◦ θ)(v)) =
occ(w, θ(v)) for each v ∈ V, therefore β −1 (w)|U = θ−1 (w)|U ∈ S;
• C = β −1 (w)|U for w ∈ rng(η ′ ). Hence there exists v ∈ rng(θ) such that
occ(w, η ′ (v)) = 1 and occ(w, η ′ (v ′ )) = 0 for each v ′ ∈
/ {v ′ , w}. Hence, for
each u ∈ U , occ(w, η ′ (θ(u))) = n iff occ(v, θ(u)) = n and this implies C =
θ−1 (v)|U ∈ S.
Moreover ρ(β(u)) = θ′ (u) for each u ∈ U , therefore θ′ ∼U ρ ◦ β.
Second part. Consider the labelled multigraph G such that NG = {v | v ∈
vars(β(U ))}, lG (v) = β −1 (v)|U ∈ S and EG = {ξ | β(x)(ξ) ∈ V}. Note that if
β(x)(ξ) ∈ V, then β(t)(ξ) ∈ V, too. Each position ξ in EG is an arrow such that
srcG (ξ) = β(x)(ξ) and tgtG (ξ) = β(t)(ξ). Observe that the second condition in the
definition of sharing graph for S and x/t is satisfied, since [S]U 3 [β]U .

On the interaction between sharing and linearity

47

Let us check the third condition. For each node v ∈ NG , if χ(β −1 (v)|U , x) = n by
Prop. 4.13 we have occ(v, β(x)) = n, i.e., there are n positions in β(x) corresponding
to v. Therefore the outdegree of v is n. In the same way, we have that χ(β −1 (v)|U , t)
is the in-degree of v.
Third part. Given B = θ′−1 (u)|U , by Prop. 4.24 we have B = β −1 (ρ−1 (u))|U .
Since θ′ U β U θ, then [θ′ ]U = mgu([β]U , {x/t}) = [mgu(β, {x/t})]U . Therefore
ρ ◦ β ′ ∼U θ′ = mgu(θ, {x/t}) ∼U mgu(β, {x/t}) = mgu(β(x) = β(t)) ◦ β. We call δ
the result of mgu(β(x) = β(t)), and note that β(x) = β(t) is equivalent to the set of
equations X = {v1 = v2 | there is a position ξ such that β(x)(ξ) = v1 ∧ β(t)(ξ) =
v2 }. The relation ρ ◦ β ∼U δ ◦ β means that, if w1 , w2 ∈ β(U ) and ρ(w1 ) = ρ(w2 )
then δ(w1 ) = δ(w2 ). The latter implies that there are in X equations of the kind
x1 = x2 , x2 = x3 , . . . , xn−1 = xn with x1 = w1 and xn = w2 , i.e., that w1 and w2
are connected in the graph G.
Therefore, let Y = {w | ρ(w) = u} = Tρ−1 (u)U. This is not empty, since B 6= {{}}.
If ξ is an edge such that srcG (ξ) ∈ Y , then tgtG (ξ) ∈ Y , since β(x)(ξ) = β(t)(ξ) ∈
X. The converse also holds. Hence, if we restrict the graph G to the set of nodes Y ,
U
we obtain a sharing graph whose resultant ω-sharing group is w∈Y β −1 (w)|U =
β −1 (ρ−1 (u))|U = B.
Theorem 4.28 (Optimality of mguω )
The single binding unification mguω ([S]U , x/t) is optimal w.r.t. mgu, under the
assumption that vars(x/t) ⊆ U , i.e., :
∀B ∈ mguω ([S]U , x/t) ∃δ ∈ ISubst. [S]U 3 [δ]U and B ∈ αω (mgu([δ]U , {x/t})) .
Proof
Let X ∈ mguω (S, x/t). By definition of mguω , there exists a sharing graph G such
that X ∈ res(G). Let NG = {n1 , . . . , nk }. We want to define a substitution δ such
that [S]U 3 [δ]U and X ∈ αω (mgu([δ]U , {x/t})). If X = {{}} this is trivial, hence
we assume that X 6= {{}}. The structure of the proof is as follows: first, we define a
substitution δ which unifies with x/t; second, we show that δ is approximated by
[S]U , namely, [S]U 3 [δ]U ; third, we show that X ∈ αω (mgu([δ]U , {x/t})).
First part. We now define a substitution δ which unifies with x/t. For each node
n ∈ NG we consider a fresh variable wn and we denote by W the set of all these
new variables.
P
For any y ∈ U \ {x} we define a term ty of arity n∈NG lG (n)(y) as follows:
ty = r(wn1 , . . . , wn1 , wn2 , . . . , wn2 , . . . , wnk , . . . , wnk )
{z
} |
{z
}
|
|
{z
}
lG (n1 )(y) times lG (n2 )(y) times

lG (nk )(y) times

We know that there exists a map f : EG → V such that, for each variable y
and node n, the set of edges targeted at n and labelled with y by f is exactly
lG (n)(y) · occ(y, t). Namely, we require
|{e ∈ EG | f (e) = y ∧ tgtG (e) = n}| = lG (n)(y) · occ(y, t) .
The idea is that each edge targeted at the node n is actually targeted at one of

48

G. Amato and F. Scozzari

the specific variables in lG (n). In particular, each variable y ∈ TlG (n)U should have
exactly lG (n)(y) · occ(y, t) edges targeted at it, so that the total number of edges
P
pointing n is y∈U lG (n)(y) · occ(y, t) = χ(lG (n), t), i.e., the in-degree of n. The
map f chooses, for each edge targeted at n, a variable in lG (n) according to the
previous idea.
Now, for each node n and variable y ∈ U , we denote by Mn,y the set of edges
pointing at y in n, i.e., Mn,y = {e ∈ EG | tgtG (e) = n ∧ f (e) = y}. Thus Mn,y may
be partitioned in occ(y, t) sets of lG (n)(y) elements, denoted by Mn,y,ξ such that
∪{Mn,y,ξ | t(ξ) = y} = Mn,y .
We may define some variations of the terms ty by replacing the variables occurring
in them with those in the set Mn,y,l . In particular, for y ∈ U \{x} and any occurrence
P
ξ of a variable y in t, we define the term tyξ of arity n∈NG lG (n)(y) as
tyξ = r(w(Mn1 ,y,ξ ), w(Mn2 ,y,ξ ), . . . , w(Mnk ,y,ξ )) ,

where, if M = {e1 , . . . , eq }, we define w(M ) as the sequence wn′1 , . . . , wn′q where
n′j = srcEG (ej ).
Note that ty and tyξ have, in corresponding positions, variables related to nodes
which are connected through edges. We are now ready to define the substitution δ
in the following way:
• δ(x) is the same as t with the difference that each occurrence ξ of a variable
y ∈ t is replaced by the term tyξ ;
• for y ∈ U \ {x} then δ(y) = ty ;
• in all the other cases, i.e v ∈
/ U , δ(v) = v.
Second part. Now we show that [S]U 3[δ]U . We need to consider all the variables
v ∈ V and check that δ −1 (v)|U ∈ S. We distinguish several cases.
• If we choose the variable wn for some n ∈ N , by construction occ(wn , ty ) =
lG (n)(y). Moreover, since G is a sharing graph, there are lG (n)(x) edges in E
departing from n and targeted to nodes m such that χ(lG (m), t) 6= 0. Thus
P
y∈vars(t),m∈NG |{e ∈ Mm,y |srcEG (e) = n}| = lG (n)(x) and occ(δ(x), wn ) =
lG (n)(x). Since for each v ∈ U we have that occ(δ(v), wn ) = lG (n)(v), we
obtain the required result which is δ −1 (wn )|U = lG (n) ∈ S.
• If we choose a variable v ∈ U then v ∈ dom(δ) and δ −1 (v) = {{}} ∈ S.
• Finally, if v ∈
/ U ∪ W , then δ −1 (v) = {{v}} and δ −1 (v)|U = {{}} ∈ S.
Third part. We now show that X ∈ αω (mgu([δ]U , {x/t})). By definition of mgu
over ISubst ∼ , we have that mgu([δ]U , {x/t}) = [mgu(δ, {x/t})]U . We obtain:
η =mgu(δ, {x/t}) =

{x/t} ◦ mgu {y = ty | y ∈ U \ {x}} ∪ {y = tyξ | t(ξ) = y} =

{x/t} ◦ {y/ty | y ∈ U \ {x}} ◦ mgu{ty =

tyξ

(A1)

| t(ξ) = y} .

Let F be the set of equations {ty = tyj | t(j) = y}. We show that, for any edge
n → m ∈ EG , it follows from F that wn = wm . Since n → m ∈ EG , then for some
y ∈ vars(t) it holds that f (n → m) = y. This implies that n → m ∈ Mm,y and

49

On the interaction between sharing and linearity

therefore there exists a position ξ such that n → m ∈ Mm,y,ξ . By definition of tyξ ,
it means that wn ∈ vars(tyξ ), in the same position where wm occurs in ty , hence
wn = wm follows from ty = tyξ ∈ F .
We know that G is connected, hence for any n, m ∈ NG , the set of equations in
F implies wn = wm . We choose a particular node n̄ ∈ NG and, for what we said
before, we have mgu(F ) = {wn /wn̄ | n ∈ NG \ {n̄}}. We show that η −1 (wn̄ )|U = X.
η −1 (wn̄ )|U
= {x/t}−1 ({y/ty | y ∈ U \ {x}}−1 ({{wn1 , . . . , wnk }}))|U
X
= {x/t}−1 ({{wn1 , . . . , wnk }} ⊎ λy ∈ U \ {x}.
lG (n)(y))|U
X

= λy ∈ U \ {x}.

P

lG (n)(y) ⊎ {{x

y∈V

n∈NG
P

occ(y,t)·

n∈NG

lG (n)(y)

}}

n∈NG

X

= λy ∈ U \ {x}.

P

lG (n)(y) ⊎ {{x

n∈NG

χ(lG (n),t)

}} .

n∈NG

Since G is a sharing graph, the total out-degree
P
total in-degree n∈NG χ(lG (n), x). Hence

P

n∈NG

χ(lG (n), t), is equal to the

η −1 (wn̄ )|U

= λy ∈ U \ {x}.

X

P

lG (n)(y) ⊎ {{x

n∈NG

χ(lG (n),x)

}}

n∈NG

= λy ∈ U.

X

lG (n)(y)

n∈NG

= res(G) .
This concludes the proof.
Theorem 4.30 (Optimality of mguω with extension)
The single binding unification mguω with extension is optimal w.r.t. mgu.
Proof
Let S ′ = S ∪ {{{v}} | v ∈ vars(x/t) \ U }, V = U ∪ vars(x/t) and X ∈ mguω (S ′ , x/t).
We want to find [δ]U such that [S]U 3 [δ]U and X ∈ αω (mgu([δ]U , {x/t})).
Following the previous theorem, we find δ such that X ∈ αω (mgu([δ]V , {x/t}))
and [S ′ ]V 3 [δ]V . We want to prove that [S]U 3 [δ]U and αω (mgu([δ]V , {x/t})) ≤ω
αω (mgu([δ]U , {x/t})), so that [δ]U is the existential substitutions we are looking
for.
We first show that [S]U 3 [δ]U . Let v ∈ V. Since [S ′ ]V 3 [δ]V , it follows that
−1
δ (v)|V ∈ S ′ .
• If δ −1 (v)|V ∈ S, then δ −1 (v)|V = δ −1 (v)|U , since vars(S) ⊆ U , and thus
δ −1 (v)|U ∈ S.
• If δ −1 (v)|V ∈
/ S, then δ −1 (v)|V ∈ {{{v}} | v ∈ vars(x/t) \ U }. Then δ −1 (v)|U =
{{}} ∈ S.

50

G. Amato and F. Scozzari

Now we distinguish two cases: either x ∈ U or x ∈
/ U.
If x ∈ U , with the same considerations which led to (A1), we have
mgu({x/t}, δ) = mgu({x = t} ∪ Eq(δ|U ) ∪ Eq(δ|V \U )) =
= mgu({x = t} ∪ Eq(δ|U ) ∪ {y = ty | y ∈ vars(t) \ U }
For each y ∈ vars(t) \ U there exist a position ξy such that t(ξy ) = y and
{x/t} ∪ Eq(δ|U ) ∪ {y = ty } is equivalent to {x/t} ∪ Eq(δ|U ) ∪ {tyξy = ty }. Note that,
since y ∈
/ U , then ty (which is actually δ(y)) is linear and independent from x/t
and the other bindings in δ. Therefore
mgu({x = t} ∪ Eq(δ|U ) ∪ {y = ty | y ∈ vars(t) \ U }
=mgu({x = t} ∪ Eq(δ|U ) ∪ {tyξy = ty | y ∈ vars(t) \ U }
=mgu({x = t} ∪ Eq(δ|U )) ⊎ β ′
where β ′ = mgu({tyξy = ty | y ∈ vars(t) \ U }) and dom(β ′ ) = vars({ty | y ∈
vars(t) \ U }). It follows that
αω ([mgu({x = t} ∪ Eq(δ|U )) ⊎ β ′ ]V )
=αω ([mgu({x = t} ∪ Eq(δ|U ))]V )
=αω (mgu([δ]U , {x/t})) .
If x ∈
/ U , then
mgu({x/t}, δ) = mgu({x = t} ∪ Eq(δ|U ) ∪ Eq(δ|vars(t)\U ) ∪ Eq(δ|{x} )
=mgu({x = t} ∪ Eq(δ|U ) ∪ {y = ty | y ∈ vars(t) \ U }∪
{ty = tyξ | t(ξ) = y}
Note that x appears in S ′ only in the multiset {{x}}. Moreover, if n is a node labelled
by {{x}}, there is only one edge which departs from n and there are no edges which
arrive in n. This means that
• wn does not appear in any ty for y ∈ V \ {x},
• δ(x) is linear since given edges e 6= e′ , we have that srcEG (e) 6= srcEG (e′ ).
As a result, δ(x) is linear and does not share variables with x/t or the other bindings
in δ. The last formula may be rewritten as
mgu({x = t} ∪ Eq(δ|U ) ∪ {y = ty | y ∈ vars(t) \ U }) ⊎ β
where β is a substitution such that dom(β) = vars(δ(x)) ⊆ W . It is obvious that
αω ([mgu({x = t} ∪ Eq(δ|U ) ∪ {y = ty | y ∈ vars(t) \ U }) ⊎ β]V )
= αω ([mgu({x = t} ∪ Eq(δ|U ) ∪ {y = ty | y ∈ vars(t) \ U })]V ) .
since dom(β) ∩ V = ∅.

On the interaction between sharing and linearity

51

Let U1 = vars(t) \ U , then
mgu({x = t} ∪ Eq(δ|U ) ∪ Eq(δ|U1 ))
=δ|U ◦ mgu(δ|U ({x = t} ∪ Eq(δ|U1 )))
=δ|U ◦ mgu({x = δ|U (t)}) ∪ Eq(δ|U1 )))
[since vars(δ|U1 ) ∩ vars(δ|U ) = ∅ and x 6∈ vars(δ|U1 )]
=δ|U ◦ {x/δ|U (t)} ◦ δ|U1
[since {x} ∈
/ vars(δ|U1 )]
Note that δ|U ◦ {x/δ|U (t)} is mgu(δ|U , {x/t}). We call γ = δ|U ◦ {x/δ|U (t)} and we
prove that αω ([γ]V ) ≥ω αω ([γ ◦ δ|U1 ]V ).
Consider a variable v ∈ V. If v ∈
/ vars(δ|U1 ) there is nothing to prove. If
v ∈ rng(δ|U1 ) we know that v does not occur anywhere else in δ|U1 and γ. Then
(γ ◦ δ|U1 )−1 (v) = γ −1 ({{y, v}}) = γ −1 (y) ⊎ {{v}} for the unique y such that v ∈
/ V , the sharing group over V we obtain in
vars(δ|U1 (y)). Therefore, since v ∈
γ ◦ δ|U1 from v may be obtained in γ from the variable y. If v ∈ dom(δ|U1 ) then
(γ ◦ δ|U1 )−1 (v) = {{}} which occurs in every element of ShLinω .
Theorem 4.31
Let S be a set of ω-sharing groups and x/t be a binding. Then B ∈ mguω (S, x/t)
iff there exist n ∈ N+ , B1 , . . . , Bn ∈ S which satisfy the following conditions:
1. B = ⊎1≤i≤n Bi ,
P
P
2.
1≤i≤n χ(Bi , t) ≥ n − 1,
1≤i≤n χ(Bi , x) =
3. either n = 1 or ∀1 ≤ i ≤ n. χ(Bi , x) + χ(Bi , t) > 0.
Proof
We first prove that these conditions are necessary. Assume that B is a resultant
sharing group for S and x/t, obtained by the sharing graph G. We show that there
exist a finite set I and, for each i ∈ I, a multiset Bi ∈ S, which satisfy the above
conditions.
Take I = NG and Bi = lG (i) for each i ∈ I, so that B = ⊎i∈I Bi . Since then
in-degree of each node is χ(Bi , x), the sum of the in-degrees of all the nodes is
P
P
i∈I χ(Bi , t). Both of them must
i∈I χ(Bi , x) and the sum of the out-degree is
be equal to the number of edges in EG . Moreover, each connected graph with |I|
nodes has at least |I| − 1 edges. Finally, if a connected graph has more than one
node, then every node i has an adjacent edge. Therefore, either χ(Bi , x) or χ(Bi , t)
is not zero.
Now we prove that the conditions are sufficient. Let I = {1, . . . , n}. If n = 1 and
χ(Bi , x) + χ(Bi , t) = 0 for the only i ∈ I, simply consider a sharing graph with
a single node labelled with Bi and no edges. Otherwise, we partition the set I in
three parts:
• Nx = {i ∈ I | χ(Bi , x) = 0};
• Nt = {i ∈ I | χ(Bi , t) = 0};
• N = {i ∈ I | χ(Bi , x) 6= 0, χ(Bi , t) 6= 0};

52

G. Amato and F. Scozzari

Note that this is a partition of I since, by hypothesis, ∀i ∈ I. χ(Bi , x)+χ(Bi , t) > 0.
Now we define a connected labelled multigraph G whose sets of nodes is I and whose
labelling function is λi ∈ I.Bi . In order to define the edges, we distinguish two cases.
N 6= ∅: Let N = {b1 , . . . , bm } with m ≥ 1 and consider the set of edges:
{a → b1 | a ∈ Nt } ∪ {b1 → c | c ∈ Nx } ∪ {bi → bi+1 | i ∈ {1, . . . , m − 1}} .
N = ∅: If Nt = ∅, then also Nx = ∅ and there is nothing to prove. We assume that
Nt 6= ∅, and thus Nx 6= ∅. Let ā ∈ Nt , c̄ ∈ Nx and consider the set of edges:
{ā → c | c ∈ Nx } ∪ {a → c̄ | a ∈ Nt \ {ā}} .
Note that, in both cases, we obtain a multigraph with the following properties:
1. it is connected;
2. it has exactly n − 1 edges, i.e. it is a tree (if we do not consider the direction
of edges);
3. there is no edge targeted at a node i with χ(i, t) = 0 and no edge whose source
is a node i with χ(i, x) = 0.
In the rest of the proof, we call pre-sharing graph a multigraph which satisfies the
above properties.
If indeg(i) is the in-degree of a node and outdeg(i) the outdegree, we call unbalancement factor of the graph the value:
X
{outdeg(i) − χ(Bi , x) | i ∈ I, outdeg(i) > χ(Bi , x)}+
X
+
{indeg(i) − χ(Bi , t) | i ∈ I, indeg(i) > χ(Bi , t)} .

We prove that given a pre-sharing graph with unbalancement factor k, we can
build another pre-sharing graph with unbalancement factor strictly less then k. As
a result, there is a pre-sharing graph with unbalancement factor equal to zero.
Assume that the graph has unbalancement factor k. There is at least an unbalanced node. Assume without loss of generality that the unbalanced node is j and
P
that outdeg(j) > χ(Bj , x). Since i∈I χ(Bi , x) ≥ n − 1, there exists a node l such
that outdeg(l) < χ(Bl , x). Let e be the unique edge with source j such that, if we
remove e from the graph, l becomes disconnected from j. Since no edge starts from
a node i with χ(Bi , x) = 0, then χ(Bj , x) > 0. This means that outdeg(j) > 1
and there is at least another edge starting from j. Assume that it is e′ : j → j ′ .
Remove this edge and replace it with an edge l → j ′ . It is obvious that the result
is a pre-sharing graph with a smaller unbalancement factor than the original one.
The case for indeg(j) > χ(Bj , t) is symmetric.
P
P
Once the unbalancement factor is zero, since i∈I χ(Bi , x) = i∈I χ(Bi , t) we
can freely add other edges in such a way to complete the graph w.r.t. the condition
on the degree of nodes. We obtain a sharing graph G such that res(G) = B.
B Proofs of Section 5

In this section we give the proofs of correctness and optimality for the abstract
unification operators mgu2 and mgusl .

On the interaction between sharing and linearity

53

Proposition 5.1
The following properties hold:
U
U
1. α2 ( R) = α2 (R).
2. rel (γ2 (S), x, t)) = γ2 (rel (S, x, t)).
Proof
We begin by proving the first property.
α2 (⊎{{B1 , . . . , Bn }})


[
X
= α2 λv ∈
TBi U.
Bi (v)
1≤i≤n

= λv ∈

[

TBi U.

1≤i≤n

1≤i≤n

(

1 if

P

1≤i≤n

Bi (v) = 1

∞ otherwise

= ⊎ {{o1 , . . . , on }} where oi = λv ∈ TBi U.

(

1 if Bi (v) = 1
∞ otherwise

= ⊎ {{α2 (B1 ), . . . , α2 (Bn )}} .
Now we proceed with the proof of the second property.
rel(γ2 (S), x, t))
[
=
{γ2 (o) | o ∈ S, Tγ2 (o)U ∩ vars(x = t) 6= ∅}
[
=
{γ2 (o) | o ∈ S, ToU ∩ vars(x = t) 6= ∅}
(since ToU = Tγ2 (o)U)
= γ2 (rel (S, x, t))) .

Theorem 5.2
hα2 , γ2 i : ShLin2 ⇌ ShLinω is a Galois insertion.
Proof
It is obvious that α2 and γ2 are monotone functions and that they are both joinmorphisms. Extensionality of γ2 ◦ α2 follows from the fact that, given an ω-sharing
group B, we have B ∈ γ2 (α2 (B)). Finally, given a 2-sharing group o, we have
α2 (γ2 (o)) = {o}. This implies that α2 ◦ γ2 is the identity.
Theorem 5.5
Given [S]U ∈ ShLinω and the binding x/t with vars(x/t) ⊆ U , we have that
mgu2 ([S]U , x/t) = [(S \ S ′ )∪
]
↓
Y | Y ∈ ℘m (S ′ ), n ∈ χ(Y, x) ∩ χ(Y, t). n ≥ |Y | − 1 ]U ,

where S ′ = rel (S, x, t).

54

G. Amato and F. Scozzari

Proof
By using Prop. 5.1 point 2, and since o 6= o′ ⇒ γ2 (o) ∩ γ2 (o′ ) = ∅, we get:
α2 (γ2 (S) \ rel (γ2 (S), x, t))
= α2 (γ2 (S) \ γ2 (rel (S, x, t)))
= α2 (γ2 (S \ rel (S, x, t)))
= S \ rel (S, x, t) .
Therefore, we get the equality
h
mgu2 ([S]U , x/t) = S \ rel(S, x, t)∪

i
X
X
χ(B, x) =
χ(B, t) ≥ |R| − 1}
α2 {⊎R | R ∈ ℘m (rel (γ2 (S), x, t)),
B∈R

U

B∈R

Now, with simple algebraic manipulations, we obtain:
α2 ({⊎R | R ∈ ℘m (rel (γ2 (S), x, t)),

X
X

χ(B, t) ≥ |R| − 1})

B∈R

B∈R

= α2 ({⊎R | R ∈ ℘m (γ2 (rel (S, x, t))),

X

χ(B, x) =

X

χ(B, x) =

χ(B, t) ≥ |R| − 1})

B∈R

B∈R

= α2 ({⊎{{B1 , . . . , Bk }} | k ∈ N,
∀i.Bi ∈ γ2 (rel (S, x, t)),

X

χ(Bi , x) =

X

χ(Bi , t) ≥ k − 1})

1≤i≤k

1≤i≤k

= α2 ({⊎{{B1 , . . . , Bk }} | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel (S, x, t)),
X
X
χ(Bi , t) ≥ k − 1})
χ(Bi , x) =
∀i.Bi ∈ γ2 (oi ),
1≤i≤k

1≤i≤k

= α2 ({⊎{{B1 , . . . , Bk }} | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel (S, x, t)),
X
X
χ(Bi , t) ≥ k − 1})
χ(Bi , x) =
∀i.α2 (Bi ) = oi ,
1≤i≤k

1≤i≤k

(such oi ’s do always exist since rel (S, x, t) is downworld closed)
= ↓{α2 (⊎{{B1 , . . . , Bk }}) | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel(S, x, t)),
X
X
χ(Bi , t) ≥ k − 1}
χ(Bi , x) =
∀i.α2 (Bi ) = oi ,
1≤i≤k

1≤i≤k

= ↓{⊎{{α2 (B1 ), . . . , α2 (Bk )}} | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel (S, x, t)),
X
X
χ(Bi , t) ≥ k − 1}
χ(Bi , x) =
∀i.α2 (Bi ) = oi ,
1≤i≤k

1≤i≤k

(by Prop. 5.1 point 1)
= ↓{⊎{{o1 , . . . , ok }} | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel (S, x, t)),
X
X
χ(Bi , t) ≥ k − 1}}
χ(Bi , x) =
∀i.α2 (Bi ) = oi ,
1≤i≤k

1≤i≤k

= ↓{⊎{{o1 , . . . , ok }} | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel (S, x, t)),
X
X
χ(Bi′ , t) ≥ k − 1}
χ(Bi , x) =
∀i.α2 (Bi ) = oi , ∀i.α2 (Bi′ ) = oi ,
1≤i≤k

1≤i≤k

(we discuss later why this is faithful)
= ↓{⊎{{o1 , . . . , ok }} | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel (S, x, t)), n ≥ k − 1,

.

On the interaction between sharing and linearity
n∈{

X

Bi (x) | ∀i.α2 (Bi ) = oi } ∩ {

X

55

χ(Bi′ , t) | ∀i.α2 (Bi′ ) = oi }}

1≤i≤k

1≤i≤k

= ↓{⊎{{o1 , . . . , ok }} | k ∈ N, {{o1 , . . . , ok }} ∈ ℘m (rel (S, x, t)), n ≥ k − 1
X
X
X
χ(Bi′ , t) | ∀i.α2 (Bi′ ) = oi }} .
oi (x)] ∩ {
oim (x),
n∈[
1≤i≤k

1≤i≤k

1≤i≤k

The move from a single family {Bi }1≤i≤k to different families {Bi }1≤i≤k and
{Bi′ }1≤i≤k is possible since, if
X
X
∀i.α2 (Bi ) = oi and ∀i.α2 (Bi′ ) = oi and
χ(Bi , x) =
χ(Bi′ , t) ≥ k − 1 ,
1≤i≤k

1≤i≤k

we may define a family {Ci }1≤i≤k such that Ci (x) = Bi (x) and Ci (v) = B ′ (v) for
each v 6= x. It is immediate to check that the Ci ’s satisfy the condition
X
X
∀i.α2 (Ci ) = oi and
χ(Ci , x) =
χ(Ci , t) ≥ k − 1 .
1≤i≤k

1≤i≤k

P

If we denote with c({{o1 , . . . , ok }}, t) the set
1≤i≤k χ(Bi , t) | ∀i.α2 (Bi ) = oi ,
what remains to prove is that
]
↓{ X | X ∈ ℘m (rel (S, x, t)), n ∈ χ(X, x) ∩ c(X, t).n ≥ |X| − 1}
]
= ↓{ X | X ∈ ℘m (rel (S, x, t)), n ∈ χ(X, x) ∩ χ(X, t), n ≥ |X| − 1} ,

where the only difference is that we replaced c(X, t) with χ(X, t).
We begin by examining the relationship between c(X, t) and χ(X, t). First of all,
it is obvious that c(X, t) ⊆ χ(X, t), therefore we only need to prove half of the
equality.
If there exists o ∈ X such that χM (o, t) = ∞, then c(X, t) is an infinite set. We
call n its least element. Under the same conditions, χ(X, t) is the interval [n, ∞].
If there is no o ∈ X such that χM (o, t) = ∞, then c(X, t) = χ(X, t) and they are
both singletons.
In the same way, if there exists some o ∈ X such that o(x) = ∞ then χ(X, x)
is an interval of the kind [n, ∞). However, if there is no such o, then χ(X, x) is a
singleton, whose unique element is |{o ∈ X | o(x) = 1}|.
Assume that we have X ∈ ℘m (rel (S, x, t)) such that there exists n ∈ χ(X, x) ∩
χ(X, t) with n ≥ |X| − 1. We want to prove that we may find a multiset Y ∈
℘m (rel (S, x, t)) such that there exists m ≥ |Y | − 1 with m ∈ χ(Y, x) ∩ c(Y, t) and
U
U
X ≤ Y . This is enough to complete the proof of the theorem.
We distinguish several cases.
• χ(X, x) and χ(X, t) are both infinite. In this case, c(X, t) is infinite. Moroever,
since χ(X, x) is an interval, there are infinite natural numbers in χ(X, x) ∩
c(X, t). We may take Y = X.
• χ(X, t) is infinite and χ(X, x) is a singleton {v}, then v = |{o ∈ X | o(x) =
1}| ≤ k. Since it must be v ≥ k − 1, there are only two choices: either v = k
or v = k − 1. We distinguish the two subcases.
— v = k − 1. In this case, there exists o ∈ X such that χm (o, t) = 0 and

56

G. Amato and F. Scozzari
o(x) = 1, otherwise it is not possible that v ≥ χm (X, t). Since χ(X, t)
is infinite, the same holds for c(X, t), hence we may find an n ∈ c(X, t)
such that n ≥ v. Consider Y = X ⊎ (n − v) ∗ {{o}}. We have χ(Y, x) =
{v + (n − v)} = n, c(Y, t) = c(X, t) and |Y | = |X| + n − v = n + 1.
U
Therefore n ∈ c(Y, x) ∩ c(Y, t) and n ≥ |Y | − 1. Y is a valid result,
U
U
and X ≤ Y .
— v = k. If there is an o ∈ X such that χm (o, t) = 0, the proof proceeds
as in the previous case. Otherwise, χm (X, t) ≥ k and since it should be
v = k ≥ χm (X, t), we have χm (X, t) = k. Therefore k ∈ c(X, t) too,
since min c(X, t) = min χ(X, t), and we may take Y = X.
• if χ(X, t) is finite, then χ(X, t) = c(X, t) and we take Y = X.

Theorem 5.7
Given [S]U in ShLin2 and the binding x/t, let V = {v1 , . . . , vn } be vars(x/t) \ U .
Then,
mgu2 ([S]U , x/t) = mgu2 ([S ∪ {v1 , . . . , vn }]U∪V , x/t) .
Proof
First of all, given a finite set of variables V , let us define the extension operator
extV : ShLinω → ShLinω such that extV ([S]U ) = [S ∪ {{{v}} | v ∈ V \ U }]U∪V .
Given V = vars(x/t) \ U = {v1 , . . . , vn }, we have that
mgu2 ([S]U , x/t) = α2 (mguω (γ2 ([S]U ), x/t))
= α2 (mguω (extV (γ2 ([S]U )), x/t)) .
We also know that
mgu2 ([S ∪ {v1 , . . . , vn }]U∪V , x/t) =
α2 (mguω (γ2 ([S ∪ {v1 , . . . , vn }]U∪V ), x/t)) .
Hence, it is enough to prove that
extV (γ2 ([S]U )) = γ2 ([S ∪ {v1 , . . . , vn }]U∪V ) .
By definition of γ2 , we have that
γ2 ([S ∪ {v1 , . . . , vn }]U∪V )
[

=
{γ2 (o) | o ∈ S ∪ {v1 , . . . , vn }} U∪V
[

=
{γ2 (o) | o ∈ S} ∪ {{{v1 }}, . . . , {{vn }}} U∪V
= extV (γ2 ([S]U )) ,

which completes the proof.

[since γ2 (vi ) = {{vi }}]

On the interaction between sharing and linearity

57

Theorem 5.9
Given [S]U ∈ ShLin2 and the binding x/t with vars(x/t) ⊆ U , we have
[
mgu2 ([S]U , x/t) = [(S \ S ′ ) ∪ ↓
res(X, x, t)]U ,
X⊆S ′

where S ′ = rel (S, x, t) and res(X, x, t) is defined as follows:
U
1. if X is non-linear for x and t, then res(X, x, t) = { X 2 };
2. if X is non-linear for x and linear for t, |Xx | ≤ 1 and |Xt | ≥ 1, then we have
U
U 2
U
res(X, x, t) = {( Xx ) ⊎ ( Xxt
) ⊎ ( Xt2 )};
3. if X is linear for x and strongly non-linear for t, |Xx | ≥ 1 and |Xt | ≤ 1, then
U
U 2
U
we have res(X, x, t) = {( Xx2 ) ⊎ ( Xxt
) ⊎ ( Xt )};
4. if X is linear for x and not strongly non-linear for t, |Xt | ≤ 1, then we have
]
]
]
2
) ⊎ ( Xt ) | Z ∈ ℘m (Xx ),
res(X, x, t) = {( Z) ⊎ ( Xxt
|Z| = χM (Xt , t) = χm (Xt , t),

TZU = Xx } ;
5. otherwise res(X, x, t) = ∅.
Proof
By Theorem 5.5, we only need to show that:
[
]
↓
Y | Y ∈ ℘m (S ′ ), n ∈ χ(Y, x) ∩ χ(Y, t). n ≥ |Y | − 1 = ↓
res(X, x, t) ,
X⊆S ′

(B1)
where S ′ = rel (S, x, t). We prove the two different inclusions separately.
Left to Right Inclusion. Let ō ∈ res(X, x, t) for some X ⊆ rel (S, x, t). We
want to prove that there exist Y ∈ ℘m (S ′ ) and n ∈ χ(Y, x) ∩ χ(Y, t) such that
n ≥ |Y | − 1 and ⊎Y = ō. We distinguish several cases:
• if X is non-linear for x and t, it is ⊎X 2 = ō. We distinguish two subcases:
— if χM (X, t) = ∞, it is enough to take Y = X ⊎ X.
— if χM (X, t) is finite, since X is non-linear for t, there exists o′ ∈ X such
that χm (o′ , t) > 1. Since S ′ is downward closed, consider o ∈ S such that
o(x) = min(o′ (x), 1) and o(v) = o′ (v) if v 6= x. We show that there exists
a natural number n such that, for Y = X ⊎X ⊎n{{o}}, we have χm (Y, t) ≥
χm (Y, x) and χm (Y, t) ≥ |Y | − 1. Since χm (Y, x) ≤ 2χm (X, x) + n, we
need to solve the inequalities 2χm (X, t) + nχm (o, t) ≥ 2χm (X, x) + n
and 2χm (X, t) + nχm (o, t) ≥ 2|X| + n. Since χm (o, t) ≥ 2, there always
U
exists a solution for n. Since χM (X, x) = ∞, we have that Y = ō is
in the left hand side of (B1).
• if X is non-linear for x and linear for t. We need to find m such that, if we
take Y = Xx ⊎ 2Xxt ⊎ 2mXt , we have χm (Y, t) ≥ χm (Y, x). In other words,
we need to solve the disequation 2χm (Xxt , t) + 2mχm (Xt , t) ≥ χm (Xx , x) +
2χm (Xxt , x), which is always possible, since |Xt | ≥ 1. Since |Y | ≤ 1 + 2|Xxt |+
2m|Xt | we have χm (X, t) ≥ |Y | − 1.

58

G. Amato and F. Scozzari
• if X is linear for x and strongly non-linear for t, we distinguish two subcases:
— χM (X, t) = ∞. Let n = 2χm (Xxt , t) + χm (Xt , t) and consider any number m such that 2m|Xx | + 2|Xxt | ≥ n (such an m always exists since
|Xx | ≥ 1). Then, consider the multiset Y = 2mXx ⊎ 2Xxt ⊎ Xt , and
we have that χm (Y, x) = χM (Y, x) = 2m|Xx | + 2|Xxt | ≥ χm (Y, t) by
construction. Moreover χM (Y, t) = ∞ and |Y | ≤ 2m|Xx | + 2|Xxt | + 1.
U
Then Y ∈ res(X, x, t) is a valid resultant sharing group.
— χM (X, t) is finite. Let o ∈ Xxt be a sharing group such that χM (o, t) > 1
and o′ be a generic sharing group in Xx . We need to find two natural
numbers n and m such that, if we take Y = 2Xx ⊎ 2Xxt ⊎ Xt ⊎ m{{o}} ⊎
n{{o′ }}, we obtain χm (Y, x) = χm (Y, t) (from this immediately follows
χM (Y, x) = χM (Y, t)) and χm (Y, x) ≥ |Y | − 1. This means we need to
solve the equations:
2|Xx | + 2|Xxt | + m + n = 2χm (Xxt , t) + χm (Xt , t) + mχm (o, t)
2|Xx | + 2|Xxt | + m + n ≥ 2|Xx | + 2|Xxt | + |Xt | + m + n − 1
Since |Xt | ≤ 1, the second equation is always satisfied. A solution for
the first equation always exists, since the greatest common divisor of
χm (o, t) − 1 and 1 is 1.

• if X is linear for x and X is not strongly non-linear for t, consider the multiset
Y = Z ⊎ Xxt ⊎ Xxt ⊎ Xt . Then χm (Y, x) = χM (Y, x) = |Z| + 2|Xxt | and
χm (Y, t) = χM (Y, t) = 2|Xxt | + χm (Xt , t). Since |Z| = χm (Xt , t), we have
that χm (Y, x) = χm (Y, t). Moreover, |Y | = |Z| + 2|Xxt | + |Xt | ≤ χm (Xt , t) +
2|Xxt | + 1 = χm (Y, t) + 1.
U
Right to left inclusion. Let o = X where X ∈ ℘m (S ′ ) and there exists
n ≥ |X| − 1 such that n ∈ χ(X, x) ∩ χ(X, t). We show that there exists Y ⊆ S ′ and
o′ ∈ res(Y, x, t) such that o′ ≥2 o. Let k = |X|. We partition X in three multisets
Xx = X|{o|χM (o,t)=0} , Xt = X|{o|χM (o,x)=0} and X|xt = X|{o|χM (o,t)>0∧χM (o,t)>0} .
Note that Xx , Xt and Xxt here are multisets and not ordinary set as in the definition
of mgu2 . We distinguish several cases:
• if TXU is linear for x and strongly non-linear for t, then χm (X, x) = χM (X, x)
= |Xx | + |Xxt | ≤ k. Since χm (X, x) ≥ k − 1, there are two cases: either
|Xx | + |Xxt | = k − 1 or |Xx | + |Xxt | = k, which implies that |Xt | ≤ 1.
Since TXU is strongly non-linear for t, there exists o′′ ∈ Xt ⊎ Xxt such that
χM (o′′ , t) ≥ 2, and thus χm (X, t) ≥ 2. Therefore χm (X, t) > |Xxt |. Since
χm (X, x) = χM (X, x) ≥ χm (X, t), we have that |Xx | ≥ 1. It follows that
U
U
U
U
o = (Xx ⊎ Xxt ⊎ Xt ) ≤2 ( TXx U)2 ⊎ ( TXxt U)2 ⊎ ( TXt U) ∈ res(TXU, x, t).
• if TXU is linear for x and not strongly non-linear for t, then, as in the previous
case we have |Xt | ≤ 1. Since X is not strongly non-linear for t, χM (X, t) =
χm (X, t) = |Xxt |+χM (Xt , t). Moreover, χM (X, x) = χm (X, x) = |Xx |+|Xxt |.
By the condition n ∈ χ(X, x) ∩ χ(X, t), we get χM (Xt , t) = |Xx |. Therefore
U
U
U
o ≤2 TXx U ⊎ ( TXxt U)2 ⊎ ( Xt ) ∈ res(TXU, x, t).
U
• if TXU is non-linear for x and t, then o ≤2 ( TXU)2 ∈ res(TXU, x, t).

On the interaction between sharing and linearity

59

• if TXU is non-linear for x and linear t, the proof is symmetric to the one of
the first case.
Theorem 5.12
Given [S]U ∈ ShLin2 and the binding x/t with vars(x/t) ⊆ U , we have
[
mgu2 ([S]U , x/t) = [(S \ S ′ ) ∪ ↓
(res(X, x, t) ∪ res ′ (X, x, t))]U ,
X⊆max S ′

where S ′ = rel (S, x, t) and
( U
{ X 2}
′
res (X, x, t) =
∅

if X = Xxt and l(X) is linear for t ,
otherwise .

Proof
It clearly holds that:
mgu2 ([S]U , x/t) ⊇ [(S \ S ′ ) ∪ ↓

[

(res(X, x, t) ∪ res ′ (X, x, t))]U

(B2)

X⊆max S ′

U
since, for each X ⊆ max S ′ , if res ′ (X, x, t) is non-empty then X 2 may be generated by the characterization in Theorem 5.9. It is enough to take X ′ = {l(o) | o ∈
U
U
X}, hence X ′ = X 2 ∈ res(X ′ , x, t) according to the last case of Theorem 5.9.
We prove the opposite inclusion. Let X ⊆ S ′ and assume that X * max S ′ .
There exists X ′ ⊆ max S ′ obtained by replacing each a ∈ X with b ∈ max S ′
such that a ≤2 b. We have that |X ′ | ≤ |X| since two different elements in X may
be replaced with the same maximal element in X ′ . We want to prove that either
res(X, x, t) = ∅, or res(X, x, t) ⊆ ↓res(X ′ , x, t) or res(X, x, t) ⊆ ↓res ′ (X ′ , x, t).
Therefore, we assume that res(X, x, t) 6= ∅ and compare the linearity properties
(linear, non linear, strongly non-linear) of X ′ w.r.t. those of X.
If they coincide, then it follows that res(X, x, t) ⊆ ↓res(X ′ , x, t). This happens
because both res(X, x, t) and res(X ′ , x, t) are obtained by the same case of Theorem
5.9. However, note that X ′ may have less elements than X and therefore some
variable which is non-linear in res(X, x, t) could be linear in res(X ′ , x, t). Actually,
this never happens since the elements in X ′ which are not explicitly delinearized
are either elements of the multiset Z in the third case of Theorem 5.9 (and therefore
may appear multiple times) or elements of Xt (Xx ) subject to the condition |Xt | ≤ 1
(|Xx | ≤ 1).
Assume that the linearity properties of X and X ′ do not coincide. The only
interesting case is when X is linear for x and not strongly non-linear for t. In all
the other cases, it is immediate from the definition that res(X, x, t) ⊆ ↓res(X ′ , x, t).
If X ′ is not linear for x and for t, then it holds res(X, x, t) ⊆ ↓res(X ′ , x, t) by
definition.
If X ′ is linear for x and strongly non-linear for t, then it is immediate from the
definition that res(X, x, t) ⊆ ↓res(X ′ , x, t), provided that |Xx | ≥ 1. Otherwise, it
must be |Xt | = 0 and therefore, in order to be res(X, x, t) 6= ∅, we have X =
Xxt and χM (X, t) = 1, which means l(X ′ ) = X is linear for t. It follows that
U
res(X, x, t) = { X 2 } = res ′ (X ′ , x, t).

60

G. Amato and F. Scozzari

If X ′ is not linear for x and linear for t, we show that |Xx | ≤ 1. Assume, by
contradiction, that |Xx | > 1. Since X ′ is linear for t and |Xt | ≤ 1, then χM (Xt , t) =
χm (Xt , t) ≤ 1, while |TZU| = |Xx | > 1, which is a contradiction. Thus it must be
U
|Xx | ≤ 1. If |Xx | = 0 then |Xt | = 0, hence res(X, x, t) = { X 2 } and res(X, x, t) =
res ′ (X, x, t). If |Xx | = 1, since X ′ is linear for t, it follows that |Z| = 1. Thus
res(X, x, t) ⊆ ↓res(X ′ , x, t).
Theorem 5.16
The operator mgusl in Definition 5.15 is correct and optimal w.r.t. mgu, when
vars(x/t) ⊆ U .
Proof
It is enough to prove that mgusl is correct and optimal w.r.t. mgu2 , namely, that:
mgusl ([S, L, U ]), x/t) = αsl (mgu2 (γsl ([S, L, U ]), x/t)) .
Let γsl ([S, L, U ]) = [T ]U . By Theorem 5.12, it holds that:
αsl (mgu2 (γsl ([S, L, U ]), x/t)
[
= αsl ([(T \ T ′ ) ∪ ↓
(res(Y, x, t) ∪ res ′ (Y, x, t)})]U
Y ⊆max T ′

G

= αsl [T \ T ′ ]U ⊔2

Y ⊆max T ′


([↓res(Y, x, t)]U ⊔2 [↓res ′ (Y, x, t)}]U ) ,

where T ′ = rel (T, x, t) and ⊔2 is the lowest upper bound in ShLin2 . By additivity
of αsl , this is equivalent to
G
αsl ([T \ T ′ ]U ) ⊔sl
(αsl ([res(Y, x, t)]U ) ⊔sl αsl ([res ′ (Y, x, t)]U )) .
(B3)
Y ⊆max T ′

′

′

Let X, L , U and K as in Definition 5.15, we have that mgusl ([S, L, U ], x/t) is
equivalent to
[(S \ X) ∪ K, U ′ ∪ L′ , U ] .

(B4)

We need to prove that equations (B3) and (B4) do coincide. In the rest of the paper,
we assume that the result of (B3) is [S ′′ , L′′ , U ].
Sharing. We first prove that the Sharing components of the two equations are
equal, i.e. that S ′′ = (S \ X) ∪ K. Given B ∈ S ′′ , there are several cases. If B = ToU
with o ∈ T \ T ′ , then B ∈ S \ X.
S
If B = ToU, for o ∈ res ′ (Y, x, t) with Y ⊆ max T ′ , then B = {ToU | o ∈ Y } with
U +
Y = Yxt and l(Y ) is linear for t. If x ∈ L then is generated by (Xxt
) , since l(Y )
is linear for t. If x ∈
/ L there are two cases: if Y is linear for t then it is generated
>1
=1 +
) , otherwise by bin(Xt>1 ∪ Xxt
, Xx ∪ Xxt , X ∗ ). Thus B ∈ K.
by (Xxt
Now, assume that B = ToU with o ∈ res(Y, x, t) and ∅ 6= Y ⊆ max T ′ . Then
S
B = W where W = {ToU | o ∈ Y }. Since Y is made of maximal elements and
[T ]U = γ2 ([S, L, U ]), we have that Y is linear for x iff x ∈ L. For the same reason,
Y is linear for t iff (W, L) is linear for t. As a consequence, if Y is non-linear for t,
then (X, L) is non-linear for t.
We proceed by cases:

On the interaction between sharing and linearity

61

U
Y non-linear for x and t. Then res(Y, x, t) = { Y 2 }. Since (X, L) is non-linear
>1
for x and t, we have Xt>1 ∪ Xxt
6= ∅ and Xx ∪ Xxt 6= ∅. Thus B ∈ bin(Xt>1 ∪
>1
∗
Xxt , Xx ∪ Xxt , X ) ⊆ K.
Y non-linear for x and linear for t. By hypothesis |Yx | ≤ 1 and |Yt | ≥ 1, hence
U
U 2
U
o = ( Yx ) ⊎ ( Yxt
) ⊎ ( Yt2 ) and
=1
=1 ∗
B ∈ bin((Xt=1 )+ , Xx ∪ Xxt
, (Xxt
) )⊆K .

=1 ∗
In particular, B ∈ bin((Xt=1 )+ , Xx , (Xxt
) ) when |Yx | = 1, otherwise B ∈
=1 +
=1
=1 ∗
bin((Xt ) , Xxt , (Xxt ) ).
Y linear for x and strongly non-linear for t. In this case we have that o =
U
U 2
U
( Yx2 ) ⊎ ( Yxt
) ⊎ ( Yt ) with |Yx | ≥ 1 and |Yt | ≤ 1. By definition of strong
non-linearity, we have two cases:

• there exists o ∈ Yxt such that χM (o, t) > 1: in this case
>1
∗
B ∈ bin(Xt ∪ {∅}, Xxt
, Xx+ , Xxt
)⊆K ;

• there exists o ∈ Yt such that χM (o, t) = ∞: in this case
∗
)⊆K .
B ∈ bin(Xt=∞ , Xx+ , Xxt

Y linear for x and non strongly non-linear for t. In this case
]
]
]
2
o = ( Z ′ ) ⊎ ( Yxt
) ⊎ ( Yt ) ,

with |Yt | = 1, for some Z ′ ∈ ℘m (Yx ) such that |Z ′ | = χm (Yt , t) and TZ ′ U = Yx .
It is obvious that
=1 ∗
B ∈ bin({{o} ∪ (∪Z) | o ∈ Xt∈N , Z ⊆ Xx , 1 ≤ |Z| ≤ χL
M (o, t)}, (Xxt ) ) ⊆ K ,

by choosing Z = {ToU | o ∈ Z ′ }.
This proves that if B ∈ S ′′ , then B ∈ (S \ X) ∪ K. Now, we need to prove the
converse implication. If B ∈ S \ X, then B = ToU for some o ∈ T , and it is obvious
that o ∈ T \ T ′ , hence B ∈ S ′′ .
Therefore, assume that B ∈ K, and consider the case when x ∈ L and B ∈
∗
bin(Xt=∞ , Xx+ , Xxt
). We have that B = A ∪ (∪A′ ) ∪ (∪A′′ ) for some A ∈ Xt=∞ , A′
non-empty subset of Xx and A′′ ⊆ Xxt . We may find o′ ∈ max T ′ , Y ′ , Y ′′ ⊆ max T ′
such that To′ U = A, TY ′ U = A′ and TY ′′ U = A′′ . We have that Y ′′′ = {o′ }∪Y ′ ∪Y ′′ is
linear for x and strongly non-linear for t (due to the element o′ ), with |Yx′′′ | ≥ 1 and
|Yt′′′ | ≤ 1. Therefore, we may apply the definition of res to obtain res(Y ′′′ , x, t) =
{o} with ToU = B, hence B ∈ S ′′ .
With similar reasonings, we may prove that for every B ∈ K, we have B ∈ S ′′ .
In particular: the second line of (6) corresponds to the case we choose a Y ′′′ which
′′′
is linear for x and strongly non-linear for t, due to an element o ∈ Yxt
which
′′′
χM (o, t) > 1; the third line of (6) corresponds to the case Y is linear for X and
is not strongly non-linear for t; the first line of (7) corresponds to the case Y ′′′ is
non-linear for both x and t; the second line of (7) corresponds to the case Y ′′′ is
linear for t and non-linear for x.
=1 +
Finally, if x ∈
/ L and B ∈ (Xxt
) , it is possible that B cannot be obtained as

62

G. Amato and F. Scozzari

res(Y ′′′ , x, t) for any Y ′′′ ⊆ max T ′ . However, B may be obtained as res ′ (Y ′′′ , x, t),
U +
choosing Y ′′′ as in the previous cases. The same happens if x ∈ Land B ∈ (Xxt
) .
′′
′
′
Linearity. We want to prove that L = L ∪ U . First of all, let us define L′′g =
U \ vars(mgu2 ([T ]U , x/t)) the set of ground variables in mgu2 ([T ]U , x/t), hence
L′′g ⊆ L′′ . We are going to prove that U ′ = L′′g and L′ \ U ′ = L′′ \ L′′g . The first
equality trivially follows from the fact that the sharing component of mgusl is
optimal, hence a variable occurs in a sharing group of S \ S ∪ K iff it occurs in a
2-sharing group of mgu2 ([T ]U , x/t).
Now, we consider a variable v ∈ U \ U ′ , and prove that v ∈ L′ iff v ∈ L′′ . There
are several cases. If we assume that v ∈
/ L, by (8) we have v ∈
/ L′ . Moreover, if
′
Y ∈ max T and v ∈ TY U, by maximality of Y we have Y (v) = ∞. Hence, by
Theorem 5.12, we have v ∈
/ L′′ . If we assume that v ∈
/ X, by (8) we have v ∈ L′ iff
′′
v ∈ L. Since vars(X) = vars(T ), we also have v ∈ L iff v ∈ L and therefore v ∈ L′
iff v ∈ L′′ .
The only case it remains to prove is v ∈ vars(X) ∩ L which, combined with the
condition v ∈
/ U ′ , gives v ∈ vars(K) ∩ L. First of all, note that if v ∈ vars(Xxt )
′
then v ∈
/ L (by definition of L′ ) and v ∈
/ L′′ (since Xxt ) appears delinearized in
every 2-sharing group resulting from res or res ′ . If v ∈
/ vars(Xxt ), we distinguish
four subcases:
• x ∈ L and (S, L) linear for t. Given Y ⊆ max T ′ , checking the forth case
of Theorem 5.9 when χM (Yt , t) = 1, we have that res(Y, x, t) is not linear
for v iff v ∈ vars(Yxt ) or v ∈ vars(Yx ) ∩ vars(Yt ). Note that there exists
′
Y ⊆ max T ′ s.t. v ∈ vars(Yxt ) ∪ (vars(Yx ) ∩ vars(Yt )) iff v ∈ vars(Txt
)∪
′
′
′′
′
′
(vars(Tx ) ∩ vars (Tt )). Finally v ∈ L iff v ∈ vars(Txt ) ∪ (vars (Tx ) ∩ vars (Tt′ ))
iff v ∈ (Xxt ∪ (Xx ∩ Xt )) iff v ∈ L′ .
• x ∈ L and (S, L) not linear for t. Given Y ⊆ max T ′ , checking the third and
forth cases (when χM (Y, t) > 1) of Theorem 5.9, we have that res(Y, x, t)
non-linear for v implies v ∈ vars(Yxt ) or v ∈ vars(Yx ), which is equivalent to
v ∈ Xxt ∪ Xx , i.e. v ∈
/ L′ . On the other hand, if v ∈ Xx , we distinguish the
cases:
— (S, L) strongly non-linear for t. There exists o ∈ T ′ such that χM (o, t) =
′
∞ or o ∈ Txt
such that χM (o, t) > 1. Moreover, there exists o′ ∈ Tx′
such that v ∈ To′ U. If we take Y = {o, o′ }, we have that res(Y, x, t) is
not linear for v, hence v ∈
/ L′′ .
— (S, L) is not strongly non-linear for t. There exists o ∈ Tt′ such that
1 < χM (o, t) < ∞. Moreover, there exists o′ ∈ Tx′ such that v ∈ To′ U. If
we take Y ′ = {o, o′ }, by the fourth case in the definition of res, we have
res(Y, x, t) is not linear for v, i.e. v ∈
/ L′′ .
• x∈
/ L and (S, L) linear for t. If v ∈
/ L′′ then v ∈ vars(Yxt ) or v ∈ vars(Yt ).
This implies v ∈ Xxt ∪Xt , i.e. v ∈
/ L′ . On the other hand, if v ∈ Xt , there exist
′
o ∈ Tx such that χM (o, x) = ∞ and o′ ∈ Tt′ such that v ∈ To′ U. By definition
of res, we have that res({o, o′ }, x, y) is not linear for v, hence v ∈
/ L′′ .
′
• x∈
/ L and (S, L) non-linear for t. Since L = L \ X, it is obvious that v ∈
/ L′ .

On the interaction between sharing and linearity

63

Moreover, there exist o ∈ T ′ such that χM (o, x) = ∞, o′ ∈ T ′ such that
χM (o, t) > 1 and o′′ ∈ T ′ such that v ∈ To′′ U. Note that it is possible that
o = o′ = o′′ . By definition, we have res({o, o′ , o′′ }, x, t) is not linear for v,
hence v ∈
/ L′′ .
Theorem 5.19
The operator mgusl in Definition 5.18 is the optimal abstraction of mgu.
Proof
First of all, given a finite set of variables V , let us define the extension operator
extV : ShLin2 → ShLin2 such that extV ([S]U ) = [S ∪ {v | v ∈ V \ U }]U∪V . Given
V = vars(x/t) \ U , we have that
αsl (mgu2 (γsl ([S, L, U ], x/t)) = αsl (extV (mgu2 (γsl ([S, L, U ])), x/t)) .
By Theorem 5.16 we have that
mgusl ([S, L, U ], x/t) = mgusl ([S ∪ V, L ∪ V, U ∪ V ], x/t) =
αsl (mgu2 (γsl ([S ∪ V, L ∪ V, U ∪ V ], x/t))) .
Hence, it is enough to prove that
extV (γsl ([S, L, U ]) = γ2 ([S ∪ V, L ∪ V, U ∪ V ]) .
By definition of γ2 , we have that
γsl ([S ∪ V, L ∪ V, U ∪ V ]) =
= [{BL∪V | B ∈ S} ∪ {BL∪V | B ∈ V }]U∪V
= [{BL | B ∈ S} ∪ V ]U∪V

[since vL∪V = v]

= extV (γsl ([S, L, U ]) ,
which completes the proof.

References
Amato, G. and Scozzari, F. 2002. Optimality in goal-dependent analysis of sharing. In Proceedings of the Joint Conference on Declarative Programming (AGP’02),
J. J. Moreno-Navarro and J. Mariño-Carballo, Eds. Universidad Politécnica de Madrid,
Madrid, 189–205.
Amato, G. and Scozzari, F. 2003. A general framework for variable aliasing: Towards optimal operators for sharing properties. In Logic Based Program Synthesis and
Transformation 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17–20, 2002. Revised Selected Papers, M. Leuschel, Ed. Lecture Notes in Computer
Science, vol. 2664. Springer, Berlin Heidelberg, 52–70.
Amato, G. and Scozzari, F. 2005. On abstract unification for variable aliasing. Tech.
Rep. TR-05-08, Dipartimento di Informatica, Università di Pisa.
Amato, G. and Scozzari, F. 2009. Optimality in goal-dependent analysis of sharing.
To appear in Theory and Practice of Logic Programming (TPLP).

64

G. Amato and F. Scozzari

Armstrong, T., Marriott, K., Schachte, P., and Søndergaard, H. 1994. Boolean
functions for dependency analysis: Algebraic properties and efficient representation. In
Static Analysis, First International Static Analysis Symposium, SAS’94 Namur, Belgium, September 28–30, 1994, Proceedings, B. Le Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer, Berlin Heidelberg, 266–280.
Bagnara, R., Hill, P. M., and Zaffanella, E. 2002. Set-sharing is redundant for
pair-sharing. Theoretical Computer Science 277, 1–2 (Apr.), 3–46.
Bagnara, R., Zaffanella, E., and Hill, P. M. 2005. Enhanced sharing analysis techniques: A comprehensive evaluation. Theory and Practice of Logic Programming 5, 1–2
(Jan.), 1–43.
Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M. V., López-Garcı́a, P., and
Puebla, G. 1997. The Ciao Prolog system. reference manual. Tech. Rep. CLIP3/97,
School of Computer Science, Technical University of Madrid (UPM). Available from
http://www.ciaohome.org/. Last accessed July 14, 2009.
Bueno, F. and Garcı́a de la Banda, M. J. 2004. Set-sharing is not always redundant for pair-sharing. In Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7–9, 2004, Proceedings, Y. Kameyama and
P. J. Stuckey, Eds. Lecture Notes in Computer Science, vol. 2998. Springer, Berlin
Heidelberg, 117–131.
Codish, M., Dams, D., and Yardeni, E. 1991. Derivation and safety of an abstract
unification algorithm for groundness and aliasing analysis. In Logic Programming, Proceedings of the Eighth International Conference, K. Furukawa, Ed. Logic Programming.
The MIT Press, Cambridge, MA, USA, 79–93.
Codish, M., Lagoon, V., and Bueno, F. 2000. An algebraic approach to sharing analysis
of logic programs. The Journal of Logic Programming 42, 2 (Feb.), 110–149.
Codish, M., Marriott, K., and Taboch, C. 2000. Improving program analyses by
structure untupling. The Journal of Logic Programming 43, 3 (June), 251–263.
Codish, M., Søndergaard, H., and Stuckey, P. J. 1999. Sharing and groundness
dependencies in logic programs. ACM Transactions on Programming Languages and
Systems 21, 5 (Sept.), 948–976.
Cortesi, A. and Filé, G. 1999. Sharing is optimal. The Journal of Logic Programming 38, 3 (Mar.), 371–386.
Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C., and Ranzato, F. 1997. Complementation in abstract interpretation. ACM Transactions on Programming Languages
and Systems 19, 1 (Jan.), 7–47.
Cortesi, A., Filé, G., and Winsborough, W. W. 1998. The quotient of an abstract
interpretation. Theoretical Computer Science 202, 1–2 (July), 163–192.
Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In
POPL ’79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles
of programming languages. ACM Press, New York, NY, USA, 269–282.
Cousot, P. and Cousot, R. 1992a. Abstract interpretation and applications to logic
programs. The Journal of Logic Programming 13, 2–3 (July), 103–179.
Cousot, P. and Cousot, R. 1992b. Abstract interpretation frameworks. Journal of
Logic and Computation 2, 4 (Aug.), 511–549.
Cousot, P. and Cousot, R. 1992c. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In Programming Language Implementation and Logic Programming, 4th International Symposium, PLILP ’92 Leuven,
Belgium, August 26–28, 1992, Proceedings, M. Bruynooghe and M. Wirsing, Eds. Lecture Notes in Computer Science, vol. 631. Springer, Berlin Heidelberg, 269–295. Invited
paper.

On the interaction between sharing and linearity

65

Hans, W. and Winkler, S. 1992.
Aliasing and groundness analysis of
logic programs through abstract interpretation and its safety.
Tech. Rep.
92–27, Technical University of Aachen (RWTH Aachen).
Available from
http://sunsite.informatik.rwth-aachen.de/Publications/AIB. Last accessed July
10, 2009.
Hermenegildo, M. V. and Rossi, F. 1995. Strict and nonstrict independent andparallelism in logic programs: Correctness, efficiency, and compile-time conditions. The
Journal of Logic Programming 22, 1 (Jan.), 1–45.
Hill, P. M., Zaffanella, E., and Bagnara, R. 2004. A correct, precise and efficient
integration of set-sharing, freeness and linearity for the analysis of finite and rational
tree languages. Theory and Practice of Logic Programming 4, 3 (May), 289–323.
Howe, J. M. and King, A. 2003. Three optimisations for sharing. Theory and Practice
of Logic Programming 3, 2 (Jan.), 243–257.
Jacobs, D. and Langen, A. 1992. Static analysis of logic programs for independent
AND parallelism. The Journal of Logic Programming 13, 2–3 (July), 291–314.
Jones, N. D. and Søndergaard, H. 1987. A semantics-based framework for the abstract interpretation of Prolog. In Abstract Interpretation of Declarative Languages,
S. Abramsky and C. Hankin, Eds. Ellis Horwood, Chichester, UK, 123–142.
King, A. 1994. A synergistic analysis for sharing and groundness which traces linearity.
In Programming Languages and Systems — ESOP ’94, 5th European Symposium on
Programming Edinburg, U.K., April 11–13, 1994, Proceedings, D. Sannella, Ed. Lecture
Notes in Computer Science, vol. 788. Springer, Berlin Heidelberg, 363–378.
King, A. 2000. Pair-sharing over rational trees. The Journal of Logic Programming 46, 1–
2 (Nov.–Dec.), 139–155.
Lagoon, V. and Stuckey, P. J. 2002. Precise pair-sharing analysis of logic programs. In
PPDP ’02: Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming. ACM Press, New York, NY, USA, 99–108.
Langen, A. 1990. Static analysis for independent And-parallelism in logic programs.
Ph.D. thesis, University of Southern California, Los Angeles, California.
Levi, G. and Spoto, F. 2003. Pair-independence and freeness analysis through linear
refinement. Information and Computation 182, 1 (Apr.), 14–52.
Mac Lane, S. 1988. Categories for the Working Mathematician, Second ed. Graduate
Texts in Mathematics, vol. 5. Springer, Berlin Heidelberg.
Marriott, K., Søndergaard, H., and Jones, N. D. 1994. Denotational abstract interpretation of logic programs. ACM Transactions on Programming Languages and
Systems 16, 3 (May), 607–648.
Muthukumar, K. and Hermenegildo, M. V. 1992. Compile-time derivation of variable
dependency using abstract interpretation. The Journal of Logic Programming 13, 2–3
(July), 315–347.
Søndergaard, H. 1986. An application of abstract interpretation of logic programs: Occur check reduction. In ESOP 86, European Symposium on Programming Saarbrcken,
Federal Republic of Germany March 17–19, 1986, Proceedings, B. Robinet and R. Wilhelm, Eds. Lecture Notes in Computer Science, vol. 213. Springer, Berlin Heidelberg,
327–338.
Sterling, L. and Shapiro, E. Y. 1994. The Art of Prolog: Advanced Programming
Techniques, Second ed. Logic Programming. The MIT Press, Cambridge, MA, USA.

