A Correct, Precise and Efficient Integration of Set-Sharing, Freeness and Linearity for the

Analysis of Finite and Rational Tree Languages∗

PATRICIA M. HILL

School of Computing, University of Leeds, Leeds, U.K.

                            (e-mail: hill@comp.leeds.ac.uk)

ENEA ZAFFANELLA, ROBERTO BAGNARA

Department of Mathematics, University of Parma, Italy

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

Abstract

It is well-known that freeness and linearity information positively interact with aliasing information, allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper we present a novel combination of set-sharing with freeness and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in (Bagnara, Hill and Zaffanella 2002, Zaffanella, Hill and Bagnara 2002) also applies to this abstract domain combination: this allows for the implementation of an abstract unification operator running in polynomial time and achieving the same precision on all the considered observable properties.

1 Introduction

Even though the set-sharing domain is, in a sense, remarkably precise, more precision is attainable by combining it with other domains. In particular, freeness and linearity information have received much attention by the literature on sharing analysis (recall that a variable is said to be free if it is not bound to a non-variable term; it is linear if it is not bound to a term containing multiple occurrences of another variable).

As argued informally by Søndergaard (Søndergaard 1986), the mutual interaction between linearity and aliasing information can improve the accuracy of a sharing analysis. This observation has been formally applied in (Codish, Dams and Yardeni 1991) to the specification of the abstract mgu operator for the domain ASub. In his PhD thesis (Langen 1990), Langen proposed a similar integration with linearity,

∗ The present work has been partly funded by MURST project “Certificazione automatica di programmi mediante interpretazione astratta” and by the University of Parma’s FIL scientific research project (ex 60%) “Matematica pura e matematica applicata”. The work of P. M. Hill and E. Zaffanella has been partly funded by EPSRC under grant M05645.

but for the set-sharing domain. He also shown how the aliasing information allows to compute freeness with a good degree of accuracy (however, freeness information was not exploited to improve aliasing). King (King 1994) also shown how a more refined tracking of linearity allows for further precision improvements.

The synergy attainable from a bi-directional interaction between aliasing and freeness information was initially pointed out by Muthukumar and Hermenegildo (Muthukumar and Hermenegildo 1991, Muthukumar and Hermenegildo 1992). Since then, several authors considered the integration of set-sharing with freeness, sometimes also including additional explicit structural information (Codish, Dams, Filé and Bruynooghe 1993a, Codish, Dams, Filé and Bruynooghe 1996, Filé 1994, King and Soper 1994).

Building on the results obtained in (Søndergaard 1986), (Codish et al. 1991) and (Muthukumar and Hermenegildo 1991), but independently from (Langen 1990), Hans and Winkler (Hans and Winkler 1992) proposed a combined integration of freeness and linearity information with set-sharing. Similar combinations have been proposed in (Bruynooghe and Codish 1993, Bruynooghe, Codish and Mulkers 1994a, Bruynooghe, Codish and Mulkers 1994b). From a more pragmatic point of view, Codish et al. (Codish, Mulkers, Bruynooghe, Garcìa de la Banda and Hermenegildo 1993b, Codish, Mulkers, Bruynooghe, Garcìa de la Banda and Hermenegildo 1995) integrate the information captured by the domains of (Søndergaard 1986) and (Muthukumar and Hermenegildo 1991) by performing the analysis with both the domains at the same time, exchanging information between the two components at each step.

Most of the above proposals differ in the carrier of the underlying abstract domain. Even when considering the simplest domain combinations, where no explicit structural information is considered, there is no general consensus on the specification of the abstract unification procedure. From a theoretical point of view, once the abstract domain has been related to the concrete one by means of a Galois connection, it is always possible to specify the best correct approximation of each operator of the concrete semantics. However, empirical observations suggest that sub-optimal operators are likely to result in better complexity/precision trade-offs (Bagnara, Zaffanella and Hill 2000b). As a consequence, it is almost impossible to identify “the right combination” of variable aliasing with freeness and linearity information, at least when practical issues, such as the complexity of the abstract unification procedure, are taken into account.

Precise and Efficient Integration of Set-Sharing, Freeness and Linearity 3

Given this state of affairs, we will now consider a domain combination whose carrier is essentially the same as specified by Langen (Langen 1990) and Hans and Winkler (Hans and Winkler 1992). (The same domain combination was also considered by Bruynooghe et al. (Bruynooghe et al. 1994a, Bruynooghe et al. 1994b), but with the addition of compoundness and explicit structural information.) The novelty of our proposal lies in the specification of an improved abstract unification procedure, better exploiting the interaction between sharing and linearity. As a matter of fact, we provide an example showing that all previous approaches to the combination of set-sharing with freeness and linearity are not uniformly more precise than the analysis based on the ASub domain (Codish et al. 1991, King 2000, Søndergaard 1986).

By extending the results of (Hill, Bagnara and Zaffanella 2002) to this combination, we provide a new abstraction function that can be applied to any logic language computing on domains of syntactic structures, with or without the occurs-check; by using this abstraction function, we also prove the correctness of the new abstract unification procedure. Moreover, we show that the same notion of redundant information as identified in (Bagnara et al. 2002, Zaffanella et al. 2002) also applies to this abstract domain combination. As a consequence, it is possible to implement an algorithm for abstract unification running in polynomial time and still obtain the same precision on all the considered observables: groundness, independence, freeness and linearity.

This paper is based on (Zaffanella 2001, Chapter 6), the PhD thesis of the second author. In Section 2, we define some notation and recall the basic concepts used later in the paper. In Section 3, we present the domain SFL that integrates setsharing, freeness and linearity. In Section 4, we show that the domain SFL can be simplified by removing some redundant information. In Section 5, we provide an experimental evaluation using the China analyzer (Bagnara 1997). In Section 6 we discuss some related work. Section 7 concludes with some final remarks. The proofs of the results stated in Sections 2, 3.1, 3.2 and 4 are given in Appendices A, B, C and D, respectively.

2 Preliminaries

For a set S, ℘(S) is the powerset of S. The cardinality of S is denoted by #S and the empty set is denoted by ∅. The notation ℘_{f}(S) stands for the set of all the finite subsets of S, while the notation S ⊆_{f} T stands for S ∈ ℘_{f}(T). The set of all finite sequences of elements of S is denoted by S^{∗}, the empty sequence by ϵ, and the concatenation of s_{1}, s_{2} ∈ S^{∗} is denoted by s_{1} . s_{2}.

2.1 Terms and Trees

Let Sig denote a possibly infinite set of function symbols, ranked over the set of natural numbers. Let Vars denote a denumerable set of variables, disjoint from Sig. Then Terms denotes the free algebra of all (possibly infinite) terms in the signature Sig having variables in Vars. Thus a term can be seen as an ordered labeled tree, possibly having some infinite paths and possibly containing variables: every inner node is labeled with a function symbol in Sig with a rank matching the number of the node’s immediate descendants, whereas every leaf is labeled by either a variable in Vars or a function symbol in Sig having rank 0 (a constant). It is assumed that Sig contains at least two distinct function symbols, one having rank 0 (so that there exist finite terms having no variables) and one having rank greater than 0 (so that there exist infinite terms).

If t ∈ Terms then vars(t) and mvars(t) denote the set and the multiset of variables occurring in t, respectively. We will also write vars(o) to denote the set of variables occurring in an arbitrary syntactic object o.

Suppose s, t ∈ Terms: s and t are independent if vars(s) ∩ vars(t) = ∅; we say that variable y occurs linearly in t, more briefly written using the predication occ lin(y, t), if y occurs exactly once in mvars(t); t is said to be ground if vars(t) = ∅; t is free if t ∈ Vars; t is linear if, for all y ∈ vars(t), we have occ lin(y, t); finally, t is a finite term (or Herbrand term) if it contains a finite number of occurrences of function symbols. The sets of all ground, linear and finite terms are denoted by GTerms, LTerms and HTerms, respectively.

2.2 Substitutions

A substitution is a total function σ: Vars → HTerms that is the identity almost everywhere; in other words, the domain of σ,

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

is finite. Given a substitution σ: Vars → HTerms, we overload the symbol ‘σ’ so as to denote also the function σ: HTerms → HTerms defined as follows, for each term t ∈ HTerms:

σ(t) =^{def} \begin{cases}t, & if t is a constant symbol; \\ σ(t), & if t ∈ Vars; \\ f(σ(t_{1}), …, σ(t_{n})), & if t = f(t_{1}, …, t_{n}). \end{cases}

If t ∈ HTerms, we write tσ to denote σ(t). Note that, for each substitution σ and each finite term t ∈ HTerms, if tσ ∈ Vars, then t ∈ Vars.

If x ∈ Vars and t ∈ HTerms \ {x}, then x ↦ t is called a binding. The set of all bindings is denoted by Bind. Substitutions are denoted by the set of their bindings, thus a substitution σ is identified with the (finite) set

{ x ↦ xσ | x ∈ dom(σ) }.

We denote by vars(σ) the set of variables occurring in the bindings of σ. We also define range(σ) =^{def} ⋃{ vars(xσ) | x ∈ dom(σ) }.

A substitution is said to be circular if, for n > 1, it has the form

{x_{1} ↦ x_{2}, …, x_{n−1} ↦ x_{n}, x_{n} ↦ x_{1}},

where x_{1}, …, x_{n} are distinct variables. A substitution is in rational solved form if it has no circular subset. The set of all substitutions in rational solved form is denoted by RSubst. A substitution σ is idempotent if, for all t ∈ Terms, we have tσσ = tσ. Equivalently, σ is idempotent if and only if dom(σ) ∩ range(σ) = ∅. The set of all idempotent substitutions is denoted by ISubst and ISubst ⊂ RSubst.

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

t(τ ∘ σ) = tστ

and has the formulation

τ ∘ σ = { x ↦ xστ | x ∈ dom(σ) ∪ dom(τ), x ≠ xστ }.  (1)

As usual, σ^{0} denotes the identity function (i.e., the empty substitution) and, when i > 0, σ^{i} denotes the substitution (σ ∘ σ^{i−1}).

For each σ ∈ RSubst and s ∈ HTerms, the sequence of finite terms

σ^{0}(s), σ^{1}(s), σ^{2}(s), …

converges to a (possibly infinite) term, denoted σ^{∞}(s) (Intrigila and Zilli 1996, King 2000). Therefore, the function rt: HTerms × RSubst → Terms such that

rt(s, σ) =^{def} σ^{∞}(s)

is well defined. Note that, in general, this function is not a substitution: while having a finite domain, its “bindings” x ↦ rt(x, σ) can map a domain variable x into a term rt(x, σ) ∈ Terms \ HTerms. However, as the name of the function suggests, the term rt(x, σ) is granted to be rational, meaning that it can only have a finite number of distinct subterms and hence, be finitely represented.

2.3 Equality Theories

An equation is of the form s = t where s, t ∈ HTerms. Eqs denotes the set of all equations. A substitution σ may be regarded as a finite set of equations, that is, as the set { x = t | (x ↦ t) ∈ σ }. We say that a set of equations e is in rational solved form if { s ↦ t | (s = t) ∈ e } ∈ RSubst. In the rest of the paper, we will often write a substitution σ ∈ RSubst to denote a set of equations in rational solved form (and vice versa). As is common in research work involving equality, we overload the symbol ‘=’ and use it to denote both equality and to represent syntactic identity. The context makes it clear what is intended.

Let {r, s, t, s_{1}, …, s_{n}, t_{1}, …, t_{n}} ⊆ HTerms. We assume that any equality theory T over Terms includes the congruence axioms denoted by the following schemata:

s = s,  (2)
s = t ↔ t = s,  (3)
r = s ∧ s = t → r = t,  (4)
s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n} → f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}).  (5)

In logic programming and most implementations of Prolog it is usual to assume an equality theory based on syntactic identity. This consists of the congruence axioms together with the identity axioms denoted by the following schemata, where f and g are distinct function symbols or n ≠ m:

f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}) → s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n},  (6)
¬(f(s_{1}, …, s_{n}) = g(t_{1}, …, t_{m})).  (7)

The axioms characterized by schemata (6) and (7) ensure the equality theory depends only on the syntax. The equality theory for a non-syntactic domain replaces these axioms by ones that depend instead on the semantics of the domain and, in particular, on the interpretation given to functor symbols.

The equality theory of Clark (Clark 1978), denoted FT , on which pure logic programming is based, usually called the Herbrand equality theory, is given by the congruence axioms, the identity axioms, and the axiom schema

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

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

An alternative approach used in some implementations of logic programming systems, such as Prolog II, SICStus and Oz, does not require the occurs-check axioms. This approach is based on the theory of rational trees (Colmerauer 1982, Colmerauer 1984), denoted RT . It assumes the congruence axioms and the identity axioms together with a uniqueness axiom for each substitution in rational solved form. Informally speaking these state that, after assigning a ground rational tree to each variable which is not in the domain, the substitution uniquely defines a ground rational tree for each of its domain variables. Note that being in rational solved form is a very weak property. Indeed, unification algorithms returning a set of equations in rational solved form are allowed to be much more “lazy” than one would expect. We refer the interested reader to (Jaffar, Lassez and Maher 1987, Keisu 1994, Maher 1988) for details on the subject.

In the sequel we use the expression “equality theory” to denote any consistent, decidable theory T satisfying the congruence axioms. We also use the expression “syntactic equality theory” to denote any equality theory T also satisfying the identity axioms.

We say that a set of equations in rational solved form σ is satisfiable in an equality theory T if

T ⊢ ∀Vars \ dom(σ) : ∃ dom(σ) . σ.

Observe that, when the occurs-check axioms do not hold for σ (for instance, when σ = {x = f(x)}), then σ is not satisfiable in the equality theory FT .

Given a satisfiable set of equations e ∈ ℘_{f}(Eqs) in an equality theory T, then a substitution σ ∈ RSubst is called a solution for e in T if σ is satisfiable in T and T ⊢ ∀(σ → e). If vars(σ) ⊆ vars(e), then σ is said to be a relevant solution for e. In addition, σ is a most general solution for e in T if T ⊢ ∀(σ ↔ e). In this paper, a most general solution is always a relevant solution of e. When the theory T is clear from the context, the set of all the relevant most general solutions for e in T is denoted by mgs(e).

We have the following useful result regarding ‘rt’ and satisfiable substitutions that are equivalent with respect to any given syntactic equality theory.

Proposition 1 Let σ, τ ∈ RSubst be satisfiable in the syntactic equality theory T and suppose that T ⊢ ∀(σ ↔ τ). Then

rt(y, σ) ∈ Vars ⟺ rt(y, τ) ∈ Vars,  (9)

rt(y, σ) ∈ GTerms ⟺ rt(y, τ) ∈ GTerms,  (10)
rt(y, σ) ∈ LTerms ⟺ rt(y, τ) ∈ LTerms.  (11)

2.4 Galois Connections and uco’s

Given two complete lattices (C, ≤_{C}) and (A, ≤_{A}), a Galois connection is a pair of monotonic functions α: C → A and γ: A → C such that

∀c ∈ C : c ≤_{C} γ(α(c)),  ∀a ∈ A : α(γ(a)) ≤_{A} a.

The functions α and γ are said to be the abstraction and concretization functions, respectively. A Galois insertion is a Galois connection where the concretization function γ is injective.

An upper closure operator (uco) ρ: C → C on the complete lattice (C, ≤_{C}) is a monotonic, idempotent and extensive^{1} self-map. The set of all uco’s on C, denoted by uco(C), is itself a complete lattice. Given a Galois connection, the function ρ =^{def} γ ∘ α is an element of uco(C). The presentation of abstract interpretation in terms of Galois connections can be rephrased by using uco’s. In particular, the partial order ⊑ defined on uco(C) formalizes the intuition of an abstract domain being more precise than another one; moreover, given two elements ρ_{1}, ρ_{2} ∈ uco(C), their reduced product, denoted ρ_{1} ⊓ ρ_{2}, is their glb on uco(C).

2.5 The Set-Sharing Domain

The set-sharing domain of Jacobs and Langen (Jacobs and Langen 1989), encodes both aliasing and groundness information. Let VI ⊆_{f} Vars be a fixed and finite set of variables of interest. An element of the set-sharing domain (a sharing set) is a set of subsets of VI (the sharing groups). Note that the empty set is not a sharing group.

Definition 2 (The set-sharing lattice.) Let SG =^{def} ℘(VI ) \ {∅} be the set of sharing groups. The set-sharing lattice is defined as SH =^{def} ℘(SG), ordered by subset inclusion.

The following operators on SH are needed for the specification of the abstract semantics.

Definition 3 (Auxiliary operators on SH .) For each sh, sh_{1}, sh_{2} ∈ SH and each V ⊆ VI , we define the following functions: the star-union function (·)^{⋆}: SH → SH , is defined as

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

1 Namely, c ≤_{C} ρ(c) for each c ∈ C.

the extraction of the relevant component of sh with respect to V is encoded by rel: ℘(VI ) × SH → SH defined as

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

the irrelevant component of sh with respect to V is thus defined as

\overline{rel}(V, sh) =^{def} sh \ rel(V, sh);

the binary union function bin: SH × SH → SH is defined as

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

the self-bin-union operation on SH is defined as

sh^{2} =^{def} bin(sh, sh);

the abstract existential quantification function aexists: SH ×℘(VI ) → SH is defined as

aexists(sh, V) =^{def} { S \ V | S ∈ sh, S \ V ≠ ∅ } ∪ { {x} | x ∈ V }.

In (Bagnara, Hill and Zaffanella 1997, Bagnara et al. 2002) it was shown that the domain SH contains many elements that are redundant for the computation of the actual observable properties of the analysis, definite groundness and definite independence. The following formalization of these observables is a rewording of the definitions provided in (Zaffanella, Hill and Bagnara 1999b, Zaffanella et al. 2002).

Definition 4 (The observables of SH .) The groundness and pair-sharing observables (on SH ) ρ_{Con}, ρ_{PS} ∈ uco(SH ) are defined, for each sh ∈ SH , by

ρ_{Con}(sh) =^{def} { S ∈ SG | S ⊆ vars(sh) },
ρ_{PS}(sh) =^{def} { S ∈ SG | (P ⊆ S ∧ #P = 2) ⟹ (∃T ∈ sh . P ⊆ T) }.

Note that, as usual in sharing analysis domains, definite groundness and independence are both represented by encoding possible non-groundness and possible pair-sharing information.

Definition 5 (The pair-sharing dependency lattice PSD.) The operator ρ_{PSD} ∈ uco(SH ) is defined, for each sh ∈ SH , by

ρ_{PSD}(sh) =^{def} { S ∈ SG | ∀y ∈ S : S = ⋃{ U ∈ sh | y ∈ U ⊆ S } }.

The pair-sharing dependency lattice is PSD =^{def} ρ_{PSD}(SH ).

3 The Domain SFL

The abstract domain SFL is made up of three components, providing different kinds of sharing information regarding the set of variables of interest VI : the first component is the set-sharing domain SH of Jacobs and Langen (Jacobs and Langen 1989); the other two components provide freeness and linearity information, each represented by simply recording those variables of interest that are known to enjoy the corresponding property.

Definition 6 (The domain SFL.) Let F =^{def} ℘(VI ) and L =^{def} ℘(VI ) be partially ordered by reverse subset inclusion. The abstract domain SFL is defined as

SFL =^{def} { ⟨sh, f, l⟩ | sh ∈ SH , f ∈ F, l ∈ L }

and is ordered by ≤_{S}, the component-wise extension of the orderings defined on the sub-domains. With this ordering, SFL is a complete lattice whose least upper bound operation is denoted by alub_{S}. The bottom element (∅, VI , VI ) will be denoted by ⊥_{S}.

3.1 The Abstraction Function

When the concrete domain is based on the theory of finite trees, idempotent substitutions provide a finitely computable strong normal form for domain elements, meaning that different substitutions describe different sets of finite trees.^{2} In contrast, when working on a concrete domain based on the theory of rational trees, substitutions in rational solved form, while being finitely computable, no longer satisfy this property: there can be an infinite set of substitutions in rational solved form all describing the same set of rational trees (i.e., the same element in the “intended” semantics). For instance, the substitutions

σ_{n} = \{x ↦ \overbrace{f(⋯ f(}^{n} x) ⋯)\},

for n = 1, 2, …, all map the variable x into the same rational tree (which is usually denoted by f^{ω}).

Ideally, a strong normal form for the set of rational trees described by a substitution σ ∈ RSubst can be obtained by computing the limit σ^{∞}. The problem is that σ^{∞} can map domain variables to infinite rational terms and may not be in RSubst.

This poses a non-trivial problem when trying to define “good” abstraction functions, since it would be really desirable for this function to map any two equivalent concrete elements to the same abstract element. As shown in (Hill et al. 2002), the classical abstraction function for set-sharing analysis (Cortesi and Filé 1999, Jacobs and Langen 1989), which was defined only for substitutions that are idempotent, does not enjoy this property when applied, as it is, to arbitrary substitutions in rational solved form. In (Hill, Bagnara and Zaffanella 1998, Hill et al. 2002), this problem is solved by replacing the sharing group operator ‘sg’ of (Jacobs and Langen 1989) by an occurrence operator, ‘occ’, defined by means of a fixpoint computation. However, to simplify the presentation, here we define ‘occ’ directly by exploiting

2 As usual, this is modulo the possible renaming of variables.

the fact that the number of iterations needed to reach the fixpoint is bounded by the number of bindings in the substitution.

Definition 7 (Occurrence operator.) For each σ ∈ RSubst and v ∈ Vars, the occurrence operator occ: RSubst × Vars → ℘_{f}(Vars) is defined as

occ(σ, v) =^{def} { y ∈ Vars | n = #σ, v ∈ vars(yσ^{n}) \ dom(σ) }.

For each σ ∈ RSubst, the operator ssets: RSubst → SH is defined as

ssets(σ) =^{def} { occ(σ, v) ∩ VI | v ∈ Vars } \ {∅}.

The operator ‘ssets’ is introduced for notational convenience only; its additive extension corresponds to the abstraction function mapping concrete elements into elements of the set-sharing domain SH .

Example 8 Let

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

Then dom(σ) = dom(τ) = {x_{1}, x_{2}, x_{3}} so that occ(σ, x_{i}) = occ(τ, x_{i}) = ∅, for i = 1, 2, 3 and occ(σ, x_{4}) = occ(τ, x_{4}) = {x_{1}, x_{2}, x_{3}, x_{4}}.

In a similar way, it is possible to define suitable operators for freeness, groundness and linearity. As all ground trees are linear, a knowledge of the definite groundness information can be useful for proving properties concerning the linearity abstraction. Groundness is already encoded in the previously defined abstraction for setsharing; nonetheless, for both a simplified notation and a clearer intuitive reading, we now explicitly define the set of variables that are associated to ground trees by a substitution in RSubst.

Definition 9 (Groundness operator.) The groundness operator gvars: RSubst → ℘_{f}(Vars) is defined, for each σ ∈ RSubst, by

gvars(σ) =^{def} { y ∈ dom(σ) | ∀v ∈ Vars : y ∉ occ(σ, v) }.

Example 10 Consider σ ∈ RSubst, where

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

Then gvars(σ) = {x_{1}, x_{2}, x_{3}, x_{4}}. Observe that x_{1} ∈ gvars(σ) although x_{1}σ ∈ Vars. Also, x_{3} ∈ gvars(σ) although vars(x_{3}σ^{i}) = {x_{2}, x_{4}} ≠ ∅ for all i ≥ 2.

As for possible sharing, the definite freeness information can be extracted from a substitution in rational solved form by observing the result of a bounded number of applications of the substitution.

Definition 11 (Freeness operator.) The freeness operator fvars: RSubst → ℘(Vars) is defined, for each σ ∈ RSubst, by

fvars(σ) =^{def} { y ∈ Vars | n = #σ, yσ^{n} ∈ Vars }.

As σ ∈ RSubst has no circular subset, y ∈ fvars(σ) implies yσ^{n} ∈ Vars \ dom(σ).

Example 12 Consider σ ∈ RSubst, where

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

Then, fvars(σ) = {x_{3}, x_{4}, x_{5}}. Thus, x_{1} ∉ fvars(σ) although x_{1}σ ∈ Vars. Also, x_{3} ∈ fvars(σ) although x_{3}σ ∈ dom(σ).

As in previous cases, the definite linearity information can be extracted by observing the result of a bounded number of applications of the considered substitution.

Definition 13 (Linearity operator.) The linearity operator lvars: RSubst → ℘(Vars) is defined, for each σ ∈ RSubst, by

lvars(σ) =^{def} { y ∈ Vars | n = #σ, ∀z ∈ vars(yσ^{n}) \ dom(σ) : occ lin(z, yσ^{2n}) }.

In the next example we consider the extraction of linearity from two substitutions. The substitution σ shows that, in contrast with respect to set-sharing and freeness, for linearity we may need to compute up to 2n applications, where n = #σ; the substitution τ shows that, when observing the term yτ^{2n}, multiple occurrences of domain variables have to be disregarded.

Example 14 Let VI = {x_{1}, x_{2}, x_{3}, x_{4}} and consider σ ∈ RSubst, where

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

Then, lvars(σ) = {x_{4}}. Observe that x_{1} ∉ lvars(σ) since x_{4} ∉ dom(σ), x_{4} ∈ x_{1}σ^{3} = f(x_{1}, x_{4}) and x_{1}σ^{6} = f(f(x_{1}, x_{4}), x_{4}), so that occ lin(x_{4}, x_{1}σ^{6}) does not hold. Note also that occ lin(x_{4}, x_{1}σ^{i}) holds for i = 3, 4, 5.

Let now τ ∈ RSubst, where

τ = {x_{1} ↦ f(x_{2}, x_{2}), x_{2} ↦ f(x_{2})}.

Then lvars(τ) = VI . Note that we have x_{1} ∈ lvars(τ), although, for all i > 0, x_{2} ∈ dom(τ) occurs more than once in the term x_{1}τ^{i}.

The properties of sharing, groundness, freeness and linearity are invariant with respect to substitutions that are equivalent in the given syntactic equality theory.

Proposition 15 Let σ, τ ∈ RSubst be satisfiable in the syntactic equality theory T and suppose that T ⊢ ∀(σ ↔ τ). Then

ssets(σ) = ssets(τ),  (12)

gvars(σ) = gvars(τ),  (13)
fvars(σ) = fvars(τ),  (14)
lvars(σ) = lvars(τ).  (15)

Moreover, the occurrence, groundness, freeness and linearity operators precisely capture the intended properties over the domain of rational trees.

Proposition 16 If σ ∈ RSubst and y, v ∈ Vars then

y ∈ occ(σ, v) ⟺ v ∈ vars(rt(y, σ)),  (16)
y ∈ gvars(σ) ⟺ rt(y, σ) ∈ GTerms,  (17)
y ∈ fvars(σ) ⟺ rt(y, σ) ∈ Vars,  (18)
y ∈ lvars(σ) ⟺ rt(y, σ) ∈ LTerms.  (19)

It follows from (16) and (18) that any free variable necessarily shares (at least, with itself). Also, as Vars ∪ GTerms ⊂ LTerms, it follows from (17), (18) and (19) that any variable that is either ground or free is also necessarily linear. Thus we have the following corollary.

Corollary 17 If σ ∈ RSubst, then

fvars(σ) ⊆ vars(ssets(σ)),
fvars(σ) ∪ gvars(σ) ⊆ lvars(σ).

We are now in position to define the abstraction function mapping rational trees to elements of the domain SFL.

Definition 18 (The abstraction function for SFL.) For each substitution σ ∈ RSubst, the function α_{S}: RSubst → SFL is defined by

α_{S}(σ) =^{def} ⟨ssets(σ), fvars(σ) ∩ VI , lvars(σ) ∩ VI ⟩,

The concrete domain ℘(RSubst) is related to SFL by means of the abstraction function α_{S}: ℘(RSubst) → SFL such that, for each Σ ∈ ℘(RSubst),

α_{S}(Σ) =^{def} alub_{S}{ α_{S}(σ) | σ ∈ Σ }.

Since the abstraction function α_{S} is additive, the concretization function is given by the adjoint (Cousot and Cousot 1977)

γ_{S}(⟨sh, f, l⟩) =^{def} { σ ∈ RSubst | ssets(σ) ⊆ sh, fvars(σ) ⊇ f, lvars(σ) ⊇ l }.

With Definition 18 and Proposition 15, one of our objectives is fulfilled: substitutions in RSubst that are equivalent have the same abstraction.

Corollary 19 Let σ, τ ∈ RSubst be satisfiable in the syntactic equality theory T and suppose T ⊢ ∀(σ ↔ τ). Then α_{S}(σ) = α_{S}(τ).

Observe that the Galois connection defined by the functions α_{S} and γ_{S} is not a Galois insertion since different abstract elements are mapped by γ_{S} to the same set of concrete computation states. To see this, suppose that ⟨sh, f, l⟩ ∈ SFL. If (as is the case for ⊥_{S}) f ⊈ vars(sh), then it follows from Corollary 17 that γ_{S}(⟨sh, f, l⟩) = γ_{S}(⊥_{S}) = ∅. Thus all such elements represent the semantics of those program fragments that have no successful computations. Also, if V = (VI \ vars(sh)) ∪ f, then, for any l′, such that V ∪ l = V ∪ l′, we have, by Corollary 17, γ_{S}(⟨sh, f, l′⟩) = γ_{S}(⟨sh, f, l⟩).

Of course, by taking the abstract domain as the subset of SFL that is the codomain of α_{S}, we would have a Galois insertion. However, apart from the simple cases shown above, it is somehow difficult to explicitly characterize such a set. For instance, as observed in (Filé 1994), if^{3}

d = ⟨{xy, xz, yz}, {x, y, z}, {x, y, z}⟩ ∈ SFL

we have γ_{S}(d) = γ_{S}(⊥_{S}) = ∅. It is worth stressing that these “spurious” elements do not compromise the correctness of the analysis and, although they can affect the precision of the analysis, they rarely occur in practice (Bagnara et al. 2000b, Zaffanella 2001).

3.2 The Abstract Operators

The specification of the abstract unification operator on the domain SFL is rather complex, since it is based on a very detailed case analysis. To achieve some modularity, that will be also useful when proving its correctness, in the next definition we introduce several auxiliary abstract operators.

Definition 20 (Auxiliary operators.) Let s, t ∈ HTerms be finite terms such that vars(s) ∪ vars(t) ⊆ VI . For each d = ⟨sh, f, l⟩ ∈ SFL we define the following predicates: s and t are independent in d if and only if ind_{d} : HTerms^{2} → Bool holds for (s, t), where

ind_{d}(s, t) =^{def} (rel(vars(s), sh) ∩ rel(vars(t), sh) = ∅);

t is ground in d if and only if ground_{d} : HTerms → Bool holds for t, where

ground_{d}(t) =^{def} (vars(t) ⊆ VI \ vars(sh));

3 In this and all the following examples, we will adopt a simplified notation for the setsharing component sh, omitting inner braces. For instance, we will write {xy, xz, yz} to denote {{x, y}, {x, z}, {y, z}}.

y ∈ vars(t) occurs linearly (in t) in d if and only if occ lin_{d} : VI × HTerms → Bool holds for (y, t), where

occ lin_{d}(y, t) =^{def} ground_{d}(y) ∨ (occ lin(y, t) ∧ (y ∈ l)
∧ ∀z ∈ vars(t) : (y ≠ z ⟹ ind_{d}(y, z)));

t is free in d if and only if free_{d} : HTerms → Bool holds for t, where

free_{d}(t) =^{def} (t ∈ f);

t is linear in d if and only if lin_{d} : HTerms → Bool holds for t, where

lin_{d}(t) =^{def} ∀y ∈ vars(t) : occ lin_{d}(y, t).

The function share with_{d} : HTerms → ℘(VI ) yields the set of variables of interest that may share with the given term. For each t ∈ HTerms,

share with_{d}(t) =^{def} vars(rel(vars(t), sh)).

The function cyclic_{x}^{t}: SH → SH strengthens the sharing set sh by forcing the coupling of x with t. For each sh ∈ SH and each (x ↦ t) ∈ Bind,

cyclic_{x}^{t}(sh) =^{def} \overline{rel}(\{x\} ∪ vars(t), sh) ∪ rel(vars(t) \ \{x\}, sh).

As a first correctness result, we have that the auxiliary operators correctly approximate the corresponding concrete properties.

Theorem 21 Let d ∈ SFL, σ ∈ γ_{S}(d), y ∈ VI and s, t ∈ HTerms be such that vars(s) ∪ vars(t) ⊆ VI . Then

ind_{d}(s, t) ⟹ vars(rt(s, σ)) ∩ vars(rt(t, σ)) = ∅;  (20)
ind_{d}(y, t) ⟺ y ∉ share with_{d}(t);  (21)
free_{d}(t) ⟹ rt(t, σ) ∈ Vars;  (22)
ground_{d}(t) ⟹ rt(t, σ) ∈ GTerms;  (23)
lin_{d}(t) ⟹ rt(t, σ) ∈ LTerms.  (24)

We now introduce the abstract mgu operator, specifying how a single binding affects each component of the domain SFL in the context of a syntactic equality theory T.

Definition 22 (amgu_{S}.) The function amgu_{S}: SFL×Bind → SFL captures the effects of a binding on an element of SFL. Let d = ⟨sh, f, l⟩ ∈ SFL and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also

sh′ =^{def} cyclic_{x}^{t}(sh_{−} ∪ sh′′),

where

sh_{x} =^{def} rel({x}, sh),  sh_{t} =^{def} rel(vars(t), sh),

sh_{xt} =^{def} sh_{x} ∩ sh_{t},  sh_{−} =^{def} \overline{rel}(\{x\} ∪ vars(t), sh),

sh′′ =^{def} \begin{cases}bin(sh_{x}, sh_{t}), & if free_{d}(x) ∨ free_{d}(t); \\ bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), \\ sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})), & if lin_{d}(x) ∧ lin_{d}(t); \\ bin(sh_{x}^{⋆}, sh_{t}), & if lin_{d}(x); \\ bin(sh_{x}, sh_{t}^{⋆}), & if lin_{d}(t); \\ bin(sh_{x}^{⋆}, sh_{t}^{⋆}), & otherwise. \end{cases}

Letting S_{x} =^{def} share with_{d}(x) and S_{t} =^{def} share with_{d}(t), we also define

f′ =^{def} \begin{cases}f, & if free_{d}(x) ∧ free_{d}(t); \\ f \ S_{x}, & if free_{d}(x); \\ f \ S_{t}, & if free_{d}(t); \\ f \ (S_{x} ∪ S_{t}), & otherwise; \end{cases}

l′ =^{def} (VI \ vars(sh′)) ∪ f′ ∪ l′′,

where

l′′ =^{def} \begin{cases}l \ (S_{x} ∩ S_{t}), & if lin_{d}(x) ∧ lin_{d}(t); \\ l \ S_{x}, & if lin_{d}(x); \\ l \ S_{t}, & if lin_{d}(t); \\ l \ (S_{x} ∪ S_{t}), & otherwise. \end{cases}

Then

amgu_{S}(d, x ↦ t) =^{def} \begin{cases}⊥_{S}, & if d = ⊥_{S} ∨ (T = FT ∧ x ∈ vars(t)); \\ ⟨sh′, f′, l′⟩ & otherwise. \end{cases}

The next result states that the abstract mgu operator is a correct approximation of the concrete one.

Theorem 23 Let d ∈ SFL and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Then, for all σ ∈ γ_{S}(d) and τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, we have τ ∈ γ_{S}(amgu_{S}(d, x ↦ t)).

We now highlight the similarities and differences of the operator amgu_{S} with respect to the corresponding ones defined in the “classical” proposals for an integration of set-sharing with freeness and linearity, such as (Bruynooghe et al. 1994a, Hans and Winkler 1992, Langen 1990). Note that, when comparing our domain with the proposal in (Bruynooghe et al. 1994a), we deliberately ignore all those enhancements that depend on properties that cannot be represented in SFL (i.e., compoundness and explicit structural information).

• In the computation of the set-sharing component, the main difference can be observed in the second, third and fourth cases of the definition of sh′′: here we omit one of the star-unions even when the terms x and t possibly share. In contrast, in (Bruynooghe et al. 1994a, Hans and Winkler 1992, Langen 1990) the corresponding star-union is avoided only when ind_{d}(x, t) holds. Note that when ind_{d}(x, t) holds in the second case of sh′′, then we have sh_{xt} = ∅; thus, the whole computation for this case reduces to sh′′ = bin(sh_{x}, sh_{t}), as was the case in the previous proposals.

• Another improvement on the set-sharing component can be observed in the definition of sh′: the cyclic_{x}^{t} operator allows the set-sharing description to be further enhanced when dealing with explicitly cyclic bindings, i.e., when x ∈ vars(t). This is the rewording of a similar enhancement proposed in (Bagnara 1997) for the domain Pos in the context of groundness analysis. Its net effect is to recover some groundness and sharing dependencies that would have been unnecessarily lost when using the standard operators. When x ∉ vars(t), we have cyclic_{x}^{t}(sh_{−} ∪ sh′′) = sh_{−} ∪ sh′′.

• The computation of the freeness component f′ is the same as specified in (Bruynooghe et al. 1994a, Hans and Winkler 1992), and is more precise than the one defined in (Langen 1990).

• The computation of the linearity component l′ is the same as specified in (Bruynooghe et al. 1994a), and is more precise than those defined in (Hans and Winkler 1992, Langen 1990).

In the following examples we show that the improvements in the abstract computation of the sharing component allow, in particular cases, to derive better information than that obtainable by using the classical abstract unification operators.

Example 24 Let VI = {x, x_{1}, x_{2}, y, y_{1}, y_{2}, z} and σ ∈ RSubst such that

σ =^{def} {x ↦ f(x_{1}, x_{2}, z), y ↦ f(y_{1}, z, y_{2})}.

By Definition 18, we have d =^{def} α_{S}({σ}) = ⟨sh, f, l⟩, where

sh = {xx_{1}, xx_{2}, xyz, yy_{1}, yy_{2}},  f = VI \ {x, y},  l = VI .

Consider the binding (x ↦ y) ∈ Bind. In the concrete domain, we compute (a substitution equivalent to) τ ∈ mgs(σ ∪ {x = y}), where

τ = {x ↦ f(y_{1}, y_{2}, y_{2}), y ↦ f(y_{1}, y_{2}, y_{2}), x_{1} ↦ y_{1}, x_{2} ↦ y_{2}, z ↦ y_{2}}.

Note that α_{S}({τ}) = ⟨sh_{τ} , f_{τ} , l_{τ} ⟩, where sh_{τ} = {xx_{1}yy_{1}, xx_{2}yy_{2}z}, so that the pairs of variables P_{x} = {x_{1}, x_{2}} and P_{y} = {y_{1}, y_{2}} keep their independence.

When abstractly evaluating the binding, both lin_{d}(x) and lin_{d}(y) hold so that we apply the second case of the definition of sh′′. By using the notation of Definition 22, we have

sh_{x} = {xx_{1}, xx_{2}, xyz},  sh_{t} = {yy_{1}, yy_{2}, xyz},
sh_{xt} = {xyz},  sh_{−} = ∅.

Since we compute the star-closure of sh_{xt} only, we obtain the set-sharing component

sh′ = {xx_{1}yy_{1}, xx_{1}yy_{2}, xx_{1}yz, xx_{2}yy_{1}, xx_{2}yy_{2}, xx_{2}yz, xyy_{1}z, xyy_{2}z, xyz}.

Thus, we precisely capture the fact that pairs P_{x} and P_{y} keep their independence.

In contrast, since ind_{d}(x, y) does not hold, all of the classical definitions of abstract unification would have required the star-closure of both sh_{x} and sh_{t}, resulting in an abstract element including, among others, the sharing group S = {x, x_{1}, x_{2}, y, y_{1}, y_{2}}. Since P_{x} ∪ P_{y} ⊂ S, this independence information would have been unnecessarily lost.

Similar examples can be devised for the third and fourth cases of the definition of sh′′, where only one side of the binding is known to be linear. Example 24 has another interesting, unexpected consequence. By repeating the above abstract computation on the domain ASub (e.g., using the abstract semantics operators specified in (King 2000)), we discover that even this simpler domain precisely captures the independence of pairs P_{x} and P_{y}. Therefore, the example provides a formal proof that all the classical approaches based on set-sharing are not uniformly more precise than the pair-sharing domain ASub. Such a property is enjoyed by our combination SFL with the improved abstract unification operator. The next example shows the precision improvements arising from the use of the ‘cyclic_{x}^{t}’ operator.

Example 25 Let VI = {x, x_{1}, x_{2}, y} and σ =^{def} {x ↦ f(x_{1}, x_{2})}. By Definition 18, we have

d =^{def} α_{S}({σ}) = ⟨sh, f, l⟩, where

sh = {xx_{1}, xx_{2}, y},  f = VI \ {x},  l = VI .

Let t = f(x, y) and consider the cyclic binding (x ↦ t) ∈ Bind. In the concrete domain, we compute (a substitution equivalent to) τ ∈ mgs(σ ∪ {x = t}), where

τ = {x ↦ f(x_{1}, x_{2}), x_{1} ↦ f(x_{1}, x_{2}), y ↦ x_{2}, }.

Note that if we further instantiate τ by grounding y, then variables x, x_{1} and x_{2} would become ground too. Formally, α_{S}({τ}) = ⟨sh_{τ} , f_{τ} , l_{τ} ⟩, where sh_{τ} = {xyx_{1}x_{2}}. Thus, as observed above, y covers x, x_{1} and x_{2}.

When abstractly evaluating the binding, we compute

sh_{x} = {xx_{1}, xx_{2}},  sh_{t} = {xx_{1}, xx_{2}, y},
sh_{xt} = sh_{x},  sh_{−} = ∅,

so that

sh_{−} ∪ sh′′ = {xx_{1}, xx_{1}x_{2}, xx_{1}x_{2}y, xx_{1}y, xx_{2}, xx_{2}y},
sh′ = cyclic_{x}^{t}(sh_{−} ∪ sh′′)
= {xx_{1}x_{2}y, xx_{1}y, xx_{2}y}.

Note that, in the element sh_{−} ∪ sh′′ (which is the abstract element that would have been computed when not exploiting the cyclic_{x}^{t} operator) variable y covers none of variables x, x_{1} and x_{2}. Thus, by applying the cyclic_{x}^{t} operator, this covering information is restored.

The full abstract unification operator aunify_{S}, capturing the effect of a sequence of bindings on an abstract element, can now be specified by a straightforward inductive definition using the operator amgu_{S}.

Definition 26 (aunify_{S}.) The operator aunify_{S}: SFL × Bind^{∗} → SFL is defined, for each d ∈ SFL and each sequence of bindings bs ∈ Bind^{∗}, by

aunify_{S}(d, bs) =^{def} \begin{cases}d, & if bs = ϵ; \\ aunify_{S}(amgu_{S}(d, x ↦ t), bs′), & if bs = (x ↦ t) . bs′. \end{cases}

Note that the second argument of aunify_{S} is a sequence of bindings (i.e., it is not a substitution, which is a set of bindings), because amgu_{S} is neither commutative nor idempotent, so that the multiplicity and the actual order of application of the bindings can influence the overall result of the abstract computation. The correctness of the aunify_{S} operator is simply inherited from the correctness of the underlying amgu_{S} operator. In particular, any reordering of the bindings in the sequence bs still results in a correct implementation of aunify_{S}.

The ‘merge-over-all-path’ operator on the domain SFL is provided by alub_{S} and is correct by definition. Finally, we define the abstract existential quantification operator for the domain SFL.

Definition 27 (aexists_{S}.) The function aexists_{S}: SFL × ℘_{f}(VI ) → SFL provides the abstract existential quantification of an element with respect to a subset of the variables of interest. For each d =^{def} ⟨sh, f, l⟩ ∈ SFL and V ⊆ VI ,

aexists_{S}(⟨sh, f, l⟩, V ) =^{def} ⟨aexists(sh, V), f ∪ V, l ∪ V ⟩.

Note that the correctness of the aexists_{S} operator does not pose any problem.

4 SFL_{2}: Eliminating Redundancies

As done in (Bagnara et al. 2002, Zaffanella et al. 2002) for the plain set-sharing domain SH , even when considering the richer domain SFL it is natural to question whether it contains redundancies with respect to the computation of the observable properties.

It is worth stressing that the results presented in (Bagnara et al. 2002) and (Zaffanella et al. 2002) cannot be simply inherited by the new domain. The concept of “redundancy” depends on both the starting domain and the given observables: in the SFL domain both of these have changed. First of all, as can be seen by looking at the definition of amgu_{S}, freeness and linearity positively interact in the computation of sharing information: a priori it is an open issue whether or not the “redundant” sharing groups can play a role in such an interaction. Secondly, since freeness and linearity information can be themselves usefully exploited in a number of applications of static analysis (e.g., in the optimized implementation of concrete unification or in occurs-check reduction), these properties have to be included in the observables.

We will now show that the domain SFL can be simplified by applying the same notion of redundancy as identified in (Bagnara et al. 2002). Namely, in the definition of SFL it is possible to replace the set-sharing component SH by PSD without affecting the precision on groundness, pair-sharing, freeness and linearity. In order to prove such a claim, we now formalize the new observable properties.

Definition 28 (The observables of SFL.) The (overloaded) groundness and pair-sharing observables ρ_{Con}, ρ_{PS} ∈ uco(SFL) are defined, for each ⟨sh, f, l⟩ ∈ SFL, by

ρ_{Con}(⟨sh, f, l⟩) =^{def} ⟨ρ_{Con}(sh), ∅, ∅⟩,
ρ_{PS}(⟨sh, f, l⟩) =^{def} ⟨ρ_{PS}(sh), ∅, ∅⟩;

the freeness and linearity observables ρ_{F} , ρ_{L} ∈ uco(SFL) are defined, for each ⟨sh, f, l⟩ ∈ SFL, by

ρ_{F} (⟨sh, f, l⟩) =^{def} ⟨SG, f, ∅⟩,
ρ_{L}(⟨sh, f, l⟩) =^{def} ⟨SG, ∅, l⟩.

The overloading of ρ_{PSD} working on the domain SFL is the straightforward extension of the corresponding operator on SH : in particular, the freeness and linearity components are left untouched.

Definition 29 (Non-redundant SFL.) For each ⟨sh, f, l⟩ ∈ SFL, the operator ρ_{PSD} ∈ uco(SFL) is defined by

ρ_{PSD}(⟨sh, f, l⟩) =^{def} ⟨ρ_{PSD}(sh), f, l⟩.

This operator induces the lattice SFL_{2} =^{def} ρ_{PSD}(SFL).

As proved in (Zaffanella et al. 2002), we have that ρ_{PSD} ⊑ (ρ_{Con} ⊓ ρ_{PS}); by the above definitions, it is also clear that ρ_{PSD} ⊑ (ρ_{F} ⊓ ρ_{L}); thus, ρ_{PSD} is more precise than the reduced product (ρ_{Con} ⊓ ρ_{PS} ⊓ ρ_{F} ⊓ ρ_{L}). Informally, this means that the domain SFL_{2} is able to represent all of our observable properties without precision losses.

The next theorem shows that ρ_{PSD} is a congruence with respect to the aunify_{S}, alub_{S} and aexists_{S} operators. This means that the domain SFL_{2} is able to propagate the information on the observables as precisely as SFL, therefore providing a completeness result.

Theorem 30 Let d_{1}, d_{2} ∈ SFL be such that ρ_{PSD}(d_{1}) = ρ_{PSD}(d_{2}). Then, for each sequence of bindings bs ∈ Bind^{∗}, for each d′ ∈ SFL and V ∈ ℘(VI ),

ρ_{PSD}(aunify_{S}(d_{1}, bs)) = ρ_{PSD}(aunify_{S}(d_{2}, bs)),
ρ_{PSD}(alub_{S}(d_{1}, d′)) = ρ_{PSD}(alub_{S}(d_{2}, d′)),
ρ_{PSD}(aexists_{S}(d_{1}, V)) = ρ_{PSD}(aexists_{S}(d_{2}, V)).

Finally, by providing the minimality result, we show that the domain SFL_{2} is indeed the generalized quotient (Cortesi, Filé and Winsborough 1998, Giacobazzi, Ranzato and Scozzari 1998) of SFL with respect to the reduced product

(ρ_{Con} ⊓ ρ_{PS} ⊓ ρ_{F} ⊓ ρ_{L}).

Theorem 31 For each i ∈ {1, 2}, let d_{i} = ⟨sh_{i}, f_{i}, l_{i}⟩ ∈ SFL be such that ρ_{PSD}(d_{1}) ≠ ρ_{PSD}(d_{2}). Then there exist a sequence of bindings bs ∈ Bind^{∗} and an observable property ρ ∈ {ρ_{Con}, ρ_{PS}, ρ_{F} , ρ_{L}} such that

ρ(aunify_{S}(d_{1}, bs)) ≠ ρ(aunify_{S}(d_{2}, bs)).

As far as the implementation is concerned, the results proved in (Bagnara et al. 2002) for the domain PSD can also be applied to SFL_{2}. In particular, in the definition of amgu_{S} every occurrence of the star-union operator can be safely replaced by the self-bin-union operator. As a consequence, it is possible to provide an implementation where the time complexity of the amgu_{S} operator is bounded by a polynomial in the number of sharing groups of the set-sharing component.

The following result provides another optimization that can be applied when both terms x and t are definitely linear, but none of them is definitely free (i.e., when we compute sh′′ by the second case stated in Definition 22).

Theorem 32 Let sh ∈ SH and (x ↦ t) ∈ Bind, where \{x\} ∪ vars(t) ⊆ VI . Let sh_{−} =^{def} \overline{rel}(\{x\} ∪ vars(t), sh), sh_{x} =^{def} rel({x}, sh), sh_{t} =^{def} rel(vars(t), sh), sh_{xt} =^{def} sh_{x} ∩ sh_{t}, sh_{W} =^{def} rel(W, sh), where W = vars(t) \ {x}, and

sh^{⋄} =^{def} sh_{−} ∪ bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})).

Then it holds

ρ_{PSD}(cyclic_{x}^{t}(sh^{⋄})) = \begin{cases}ρ_{PSD}(sh_{−} ∪ bin(sh_{x}, sh_{t})), & if x ∉ vars(t); \\ ρ_{PSD}(sh_{−} ∪ bin(sh_{x}^{2}, sh_{W})), & otherwise. \end{cases}

Therefore, even when terms x and t possibly share (i.e., when sh_{xt} ≠ ∅), by using SFL_{2} we can avoid the expensive computation of at least one of the two inner binary unions in the expression for sh^{⋄}.

5 Experimental Evaluation

Example 24 shows that an analysis based on the new abstract unification operator can be strictly more precise than one based on the classical proposal. However, that example is artificial and leaves open the question as to whether or not such a phenomenon actually happens during the analysis of real programs and, if so, how often. This was the motivation for the experimental evaluation we describe in this section. We consider the abstract domain Pos ×SFL_{2} (Bagnara, Zaffanella and Hill n.d.), where the non-redundant version SFL_{2} of the domain SFL is further combined, as described in (Bagnara et al. n.d., Section 4), with the definite groundness information computed by Pos and compare the results using the (classical) abstract unification operator of (Bagnara et al. n.d., Definition 4) with the (new) operator amgu_{S} given in Definition 22. Taking this as a starting point, we experimentally evaluate eight variants of the analysis arising from all possible combinations of the following options:

1. the analysis can be goal independent or goal dependent;

2. the set-sharing component may or may not have widening enabled (Zaffanella, Bagnara and Hill 1999a);

3. the abstract domain may or may not be upgraded with structural information using the Pattern(·) operator (see (Bagnara, Hill and Zaffanella 2000a) and (Bagnara et al. n.d., Section 5)).

The experiments have been conducted using the China analyzer (Bagnara 1997) on a GNU/Linux PC system. China is a data-flow analyzer for (constraint) logic programs performing bottom-up analysis and deriving information on both callpatterns and success-patterns by means of program transformations and optimized fixpoint computation techniques. An abstract description is computed for the calland success-patterns for each predicate defined in the program. The benchmark suite, which is composed of 372 logic programs of various sizes and complexity, can be considered representative.

The precision results for the goal independent comparisons are summarized in Table 1. For each benchmark, precision is measured by counting the number of independent pairs as well as the numbers of definitely ground, free and linear variables detected. For each variant of the analysis, these numbers are then compared by computing the relative precision improvements and expressing them using percentages. The benchmark suite is then partitioned into several precision equivalence classes and the cardinalities of these classes are shown in Table 1. For example, when considering a goal independent analysis without structural information and without widenings, the value 5 found at the intersection of the row labeled ‘0 < p ≤ 2’ with the column labeled ‘I’ should be read: “for five benchmarks there has been a (positive) increase in the number of independent pairs of variables which is less than or equal to two percent.” Note that we only report on independence and linearity (in the columns labelled ‘I’ and ‘L’, respectively), because no differences have been observed for groundness and freeness. The precision class labeled ‘unknown’ identifies those benchmarks for which the analyses timed-out (the time-out threshold was fixed at 600 seconds). Hence, for goal independent analyses, a precision improvement affects from 1.6% to 3% of the benchmarks, depending on the considered variant.

When considering the goal dependent analyses, we obtain a single, small improvement, so that no comparison tables are included here: the improvement, affecting linearity information, can be observed when the abstract domain includes structural information.

With respect to differences in the efficiency, the introduction of the new abstract unification operator has no significant effect on the computation time: small differences (usually improvements) are observed on as many as 6% of the benchmarks for

Goal  Without Widening With Widening
Independent  w/o SI with SI w/o SI with SI
Prec. class  I L I L I L I L
5 < p ≤ 10  — 2 — 2 — 2 — 2
2 < p ≤ 5  — — — — — — — 1
0 < p ≤ 2  5 5 9 6 6 6 12 8
same precision 357 355 337 338 366 364 360 361
unknown  10 10 26 26 — — — —

Table 1. Classical Pos × SFL_{2} versus enhanced one: precision.

the goal independent analysis without structural information and without widenings; other combinations register even less differences.

We note that it is not surprising that the precision and efficiency improvements occur very rarely since the abstract unification operators behave the same except under very specific conditions: the two terms being unified must not only be definitely linear, but also possibly non-free and share a variable.

6 Related work

Sharing information has been shown to be important for finite-tree analysis (Bagnara, Gori, Hill and Zaffanella 2001a, Bagnara, Zaffanella, Gori and Hill 2001b). This aims at identifying those program variables that, at a particular program point, cannot be bound to an infinite rational tree (in other words, they are necessarily bound to acyclic terms). This novel analysis is irrelevant for those logic languages computing over a domain of finite trees, while having several applications for those (constraint) logic languages that are explicitly designed to compute over a domain including rational trees, such as Prolog II and its successors (Colmerauer 1982, Colmerauer 1990), SICStus Prolog (SIC 1995), and Oz (Smolka and Treinen 1994). The analysis specified in (Bagnara et al. 2001a) is based on a parametric abstract domain H × P, where the H component (the Herbrand component) is a set of variables that are known to be bound to finite terms, while the parametric component P can be any domain capturing aliasing, groundness, freeness and linearity information that is useful to compute finite-tree information. An obvious choice for such a parameter is the domain combination SFL. It is worth noting that, in (Bagnara et al. 2001a), the correctness of the finite-tree analysis is proved by assuming the correctness of the underlying analysis on the parameter P. Thus, thanks to the results shown in this paper, the proof for the domain H × SFL can now be considered complete.

Codish et al. (Codish, Lagoon and Bueno 2000) describe an algebraic approach to the sharing analysis of logic programs that is based on set logic programs. A set logic program is a logic program in which the terms are sets of variables and standard unification is replaced by a suitable unification for sets, called ACI1-unification (unification in the presence of an associative, commutative, and idempotent equality theory with a unit element). The authors show that the domain of set-substitutions, with a few modifications, can be used as an abstract domain for sharing analysis.

They also provide an isomorphism between this domain and the set-sharing domain SH of Jacobs and Langen. The approach using set logic programs is also generalized to include linearity information, by suitably annotating the set-substitutions, and the authors formally state the optimality of the corresponding abstract unification operator lin-mgu_{ACI1} (Lemma A.10 in the Appendix of (Codish et al. 2000)). However, this operator is very similar to the classical combinations of set-sharing with linearity (Bruynooghe et al. 1994a, Hans and Winkler 1992, Langen 1990): in particular, the precision improvements arising from this enhancement are only exploited when the two terms being unified are definitely independent. As we have seen in this paper, such a choice results in a sub-optimal abstract unification operator, so that the optimality result cannot hold. By looking at the proof of Lemma A.10 in (Codish et al. 2000), it can be seen that the case when the two terms possibly share a variable is dealt with by referring to an example:^{4} this one is supposed to show that all the possible sharing groups can be generated. However, even our improved operator correctly characterizes the given example, so that the proof is wrong. It should be stressed that the amgu_{S} operator presented in this paper, though remarkably precise, is not meant to subsume all of the proposals for an improved sharing analysis that appeared in the recent literature (for a thorough experimental evaluation of many of these proposals, the reader is referred to (Bagnara et al. 2000b, Zaffanella 2001)). In particular, it is not difficult to show that our operator is not the optimal approximation of concrete unification.

In a very recent technical report (Howe and King 2001), J. Howe and A. King consider the domain SFL and propose three optimizations to improve both the precision and the efficiency of the (classical) abstract unification operator. The first optimization is based on the same observation we have made in this paper, namely that the independence check between the two terms being unified is not necessary for ensuring the correctness of the analysis. However, the proposed enhancement does not fully exploit this observation, so that the resulting operator is strictly less precise than our amgu_{S} operator (even when the operator cyclic_{x}^{t} does not come into play). In fact, the first optimization of (Howe and King 2001) is not uniformly more precise than the classical proposals. The following example illustrates this point.

Example 33 Let VI = {x, y, z_{1}, z_{2}, z_{3}}, (x ↦ y) ∈ Bind and d =^{def} ⟨sh, ∅, VI ⟩, where sh = {xz_{1}, xz_{2}, xz_{3}, yz_{1}, yz_{2}, yz_{3}}.

Since x and y are linear and independent, amgu_{S} as well as all the classical abstract unification operators will compute d_{1} = ⟨sh_{1}, ∅, {x, y}⟩, where

sh_{1} =^{def} bin(sh_{x}, sh_{y}) = {xyz_{1}, xyz_{1}z_{2}, xyz_{1}z_{3}, xyz_{2}, xyz_{2}z_{3}, xyz_{3}}.

In contrast, a computation based on (Howe and King 2001, Definition 3.2), results

4 The proof refers to Example 8, which however has nothing to do with the possibility that the two terms share; we believe that Example 2 was intended.

in the less precise abstract element d_{2} = ⟨sh_{2}, ∅, {x, y}⟩, where

sh_{2} =^{def} bin(sh_{x}^{⋆}, sh_{y}) ∩ bin(sh_{x}, sh_{y}^{⋆}) = sh_{1} ∪ {xyz_{1}z_{2}z_{3}}.

The second optimization shown in (Howe and King 2001) is based on the enhanced combination of set-sharing and freeness information, which was originally proposed in (Filé 1994). In particular, the authors propose a slightly different precision enhancement, less powerful as far as precision is concerned, which however seems to be amenable for an efficient implementation. The third optimization in (Howe and King 2001) exploits the combination of the domain SFL with the groundness domain Pos.

7 Conclusion

In this paper we have introduced the abstract domain SFL, combining the setsharing domain SH with freeness and linearity information. While the carrier of SFL can be considered standard, we have provided the specification of a new abstract unification operator, showing examples where this operator achieves more precision than the classical proposals. The main contributions of this paper are the following:

• we have defined a precise abstraction function, mapping arbitrary substitutions in rational solved form into their most precise approximation on SFL;

• using this abstraction function, we have provided the mandatory proof of correctness for the new abstract unification operator, for both finite-tree and rational-tree languages;

• we have shown that, in the definition of SFL, we can replace the set-sharing domain SH by its non-redundant version PSD. As a consequence, it is possible to implement an algorithm for abstract unification running in polynomial time and still obtain the same precision on all the considered observables, that is groundness, independence, freeness and linearity.

References

Bagnara, R. (1997). Data-Flow Analysis for Constraint Logic-Based Languages, PhD thesis,

Dipartimento di Informatica, Università di Pisa, Pisa, Italy. Printed as Report TD-1/97. Bagnara, R., Gori, R., Hill, P. M. and Zaffanella, E. (2001a). Finite-tree analysis for

constraint logic-based languages, in P. Cousot (ed.), Static Analysis: 8th International Symposium, SAS 2001, Vol. 2126 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Paris, France, pp. 165–184.

Bagnara, R., Hill, P. M. and Zaffanella, E. (1997). Set-sharing is redundant for pairsharing, in P. Van Hentenryck (ed.), Static Analysis: Proceedings of the 4th International Symposium, Vol. 1302 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Paris, France, pp. 53–67.

Bagnara, R., Hill, P. M. and Zaffanella, E. (2000a). Efficient structural information analysis for real CLP languages, in M. Parigot and A. Voronkov (eds), Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR 2000), Vol. 1955 of Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, Réunion Island, France, pp. 189–206.

Bagnara, R., Hill, P. M. and Zaffanella, E. (2002). Set-sharing is redundant for pair-sharing,

Theoretical Computer Science. To appear. Bagnara, R., Zaffanella, E. and Hill, P. M. (2000b). Enhanced sharing analysis techniques:

A comprehensive evaluation, in M. Gabbrielli and F. Pfenning (eds), Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Association for Computing Machinery, Montreal, Canada, pp. 103–114.

Bagnara, R., Zaffanella, E. and Hill, P. M. (n.d.). Enhanced sharing analysis techniques: A comprehensive evaluation, Submitted for publication. Available at http://www.cs.

unipr.it/~bagnara/.

Bagnara, R., Zaffanella, E., Gori, R. and Hill, P. M. (2001b). Boolean functions for finitetree dependencies, in R. Nieuwenhuis and A. Voronkov (eds), Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2001), Vol. 2250 of Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, Havana, Cuba, pp. 575–589.

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

Bruynooghe, M., Codish, M. and Mulkers, A. (1994a). Abstract unification for a composite domain deriving sharing and freeness properties of program variables, in F. S. de Boer and M. Gabbrielli (eds), Verification and Analysis of Logic Languages, Proceedings of the W2 Post-Conference Workshop, International Conference on Logic Programming, Santa Margherita Ligure, Italy, pp. 213–230.

Bruynooghe, M., Codish, M. and Mulkers, A. (1994b). A composite domain for freeness, sharing, and compoundness analysis of logic programs, Technical Report CW 196, Department of Computer Science, K.U. Leuven, Belgium.

Clark, K. L. (1978). Negation as failure, in H. Gallaire and J. Minker (eds), Logic and

Databases, Plenum Press, Toulouse, France, pp. 293–322. Codish, M., Dams, D. and Yardeni, E. (1991). Derivation and safety of an abstract unifi-

cation algorithm for groundness and aliasing analysis, in Furukawa (1991), pp. 79–93. Codish, M., Dams, D., Filé, G. and Bruynooghe, M. (1993a). Freeness analysis for logic

programs — and correctness?, in D. S. Warren (ed.), Logic Programming: Proceedings of the Tenth International Conference on Logic Programming, MIT Press Series in Logic Programming, The MIT Press, Budapest, Hungary, pp. 116–131. An extended version is available as Technical Report CW 161, Department of Computer Science, K.U. Leuven, December 1992.

Codish, M., Dams, D., Filé, G. and Bruynooghe, M. (1996). On the design of a correct

freeness analysis for logic programs, Journal of Logic Programming 28(3): 181–206. Codish, M., Lagoon, V. and Bueno, F. (2000). An algebraic approach to sharing analysis

of logic programs, Journal of Logic Programming 42(2): 111–149. Codish, M., Mulkers, A., Bruynooghe, M., Garcìa de la Banda, M. and Hermenegildo, M.

(1993b). Improving abstract interpretations by combining domains, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ACM Press, Copenhagen, Denmark, pp. 194–205. Also available as Technical Report CW 162, Department of Computer Science, K.U. Leuven, December 1992.

Codish, M., Mulkers, A., Bruynooghe, M., Garcìa de la Banda, M. and Hermenegildo, M. (1995). Improving abstract interpretations by combining domains, ACM Transactions on Programming Languages and Systems 17(1): 28–44.

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

Colmerauer, A. (1982). Prolog and infinite trees, in K. L. Clark and S. Å. Tärnlund (eds), Logic Programming, APIC Studies in Data Processing, Vol. 16, Academic Press, New York, pp. 231–251.

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

Colmerauer, A. (1990). An introduction to Prolog-III, Communications of the ACM

33(7): 69–90. Cortesi, A. and Filé, G. (1999). Sharing is optimal, Journal of Logic Programming

38(3): 371–386. Cortesi, A., Filé, G. and Winsborough, W. (1998). The quotient of an abstract interpreta-

tion for comparing static analyses, Theoretical Computer Science 202(1&2): 163–192. Cousot, P. and Cousot, R. (1977). Abstract interpretation: A unified lattice model for static

analysis of programs by construction or approximation of fixpoints, Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238–252.

Filé, G. (1994). Share × Free: Simple and correct, Technical Report 15, Dipartimento di

Matematica, Università di Padova. Furukawa, K. (ed.) (1991). Logic Programming: Proceedings of the Eighth International

Conference on Logic Programming, MIT Press Series in Logic Programming, The MIT Press, Paris, France.

Giacobazzi, R., Ranzato, F. and Scozzari, F. (1998). Complete abstract interpretations made constructive, in J. Gruska and J. Zlatuska (eds), Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS’98), Vol. 1450 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 366–377.

Hans, W. and Winkler, S. (1992). Aliasing and groundness analysis of logic programs through abstract interpretation and its safety, Technical Report 92–27, Technical University of Aachen (RWTH Aachen).

Hill, P. M., Bagnara, R. and Zaffanella, E. (1998). The correctness of set-sharing, in G. Levi (ed.), Static Analysis: Proceedings of the 5th International Symposium, Vol. 1503 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Pisa, Italy, pp. 99–114.

Hill, P. M., Bagnara, R. and Zaffanella, E. (2002). Soundness, idempotence and commutativity of set-sharing, Theory and Practice of Logic Programming 2(2): 155–201. To

appear. Available at http://arXiv.org/abs/cs.PL/0102030.

Howe, J. and King, A. (2001). Three optimisations for sharing, Technical Report 11-01,

Computing Laboratory, University of Kent at Canterbury. Intrigila, B. and Zilli, M. V. (1996). A remark on infinite matching vs infinite unification,

Journal of Symbolic Computation 21(3): 2289–2292. Jacobs, D. and Langen, A. (1989). Accurate and efficient approximation of variable aliasing

in logic programs, in E. L. Lusk and R. A. Overbeek (eds), Logic Programming: Proceedings of the North American Conference, MIT Press Series in Logic Programming, The MIT Press, Cleveland, Ohio, USA, pp. 154–165.

Jaffar, J., Lassez, J.-L. and Maher, M. J. (1987). Prolog-II as an instance of the logic programming scheme, in M. Wirsing (ed.), Formal Descriptions of Programming Concepts III, North-Holland, pp. 275–299.

Keisu, T. (1994). Tree Constraints, PhD thesis, The Royal Institute of Technology, Stock-

holm, Sweden. Also available in the SICS Dissertation Series: SICS/D–16–SE. King, A. (1994). A synergistic analysis for sharing and groundness which traces linearity, in

D. Sannella (ed.), Proceedings of the Fifth European Symposium on Programming, Vol.

788 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Edinburgh, UK, pp. 363–378.

King, A. (2000). Pair-sharing over rational trees, Journal of Logic Programming 46(1–

2): 139–155. King, A. and Soper, P. (1994). Depth-k sharing and freeness, in P. Van Hentenryck (ed.),

Logic Programming: Proceedings of the Eleventh International Conference on Logic Programming, MIT Press Series in Logic Programming, The MIT Press, Santa Margherita Ligure, Italy, pp. 553–568.

Langen, A. (1990). Advanced Techniques for Approximating Variable Aliasing in Logic Programs, PhD thesis, Computer Science Department, University of Southern California. Printed as Report TR 91-05.

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

Muthukumar, K. and Hermenegildo, M. (1991). Combined determination of sharing and freeness of program variables through abstract interpretation, in Furukawa (1991), pp. 49–63. An extended version appeared in (Muthukumar and Hermenegildo 1992).

Muthukumar, K. and Hermenegildo, M. (1992). Compile-time derivation of variable depen-

dency using abstract interpretation, Journal of Logic Programming 13(2&3): 315–347. SIC (1995). SICStus Prolog User’s Manual, release 3 #0 edn. Smolka, G. and Treinen, R. (1994). Records for logic programming, Journal of Logic Pro-

gramming 18(3): 229–258. Søndergaard, H. (1986). An application of abstract interpretation of logic programs: Occur

check reduction, in B. Robinet and R. Wilhelm (eds), Proceedings of the 1986 European Symposium on Programming, Vol. 213 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 327–338.

Zaffanella, E. (2001). Correctness, Precision and Efficiency in the Sharing Analysis of Real Logic Languages, PhD thesis, School of Computing, University of Leeds, Leeds, U.K.

Available at http://www.cs.unipr.it/~zaffanella/.

Zaffanella, E., Bagnara, R. and Hill, P. M. (1999a). Widening Sharing, in G. Nadathur (ed.), Principles and Practice of Declarative Programming, Vol. 1702 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Paris, France, pp. 414–431.

Zaffanella, E., Hill, P. M. and Bagnara, R. (1999b). Decomposing non-redundant sharing by complementation, in A. Cortesi and G. Filé (eds), Static Analysis: Proceedings of the 6th International Symposium, Vol. 1694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Venice, Italy, pp. 69–84.

Zaffanella, E., Hill, P. M. and Bagnara, R. (2002). Decomposing non-redundant sharing by complementation, Theory and Practice of Logic Programming 2(2): 233–261. To appear.

Available at http://arXiv.org/abs/cs.PL/0101025.

A Proofs of the Results of Section 2

The proof of Proposition 1 requires the concept of a path p ∈ (ℕ \ {0})^{∗} which is any finite sequence of (non-zero) natural numbers. Given a path p and a (possibly infinite) term t ∈ Terms, we denote by t[p] the subterm of t found by following path p. Formally,

t[p] = \begin{cases}t & if p = ϵ; \\ t_{i}[q] & if p = i . q ∧ (1 ≤ i ≤ n) ∧ t = f(t_{1}, …, t_{n}). \end{cases}

Note that t[p] is only defined for those paths p actually corresponding to subterms of t.

The following two lemmas, proven in (Hill et al. 2002), state some basic properties of equality theories.

Lemma 34 ((Hill et al. 2002, Lemma 1).) Let σ ∈ RSubst be satisfiable in the equality theory T and consider (x ↦ t) ∈ Bind such that x ∉ dom(σ) and t ∈ GTerms ∩ HTerms. Then, σ′ =^{def} σ ∪ {x ↦ t} ∈ RSubst and σ′ is satisfiable in T.

Lemma 35 ((Hill et al. 2002, Lemma 2).) Let T be an equality theory, σ ∈ RSubst and t ∈ HTerms. Then

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

The next lemma provides a link between syntactic equality theories and the function ‘rt’.

Lemma 36 Let σ ∈ RSubst be satisfiable in the syntactic equality theory T. Suppose s, t ∈ HTerms are such that T ⊢ ∀(σ → (s = t)). Then rt(s, σ) = rt(t, σ).

Proof We suppose, toward a contradiction, that rt(s, σ) ≠ rt(t, σ). Then, there must exist a finite path p such that:

a. x = rt(s, σ)[p] ∈ Vars \ dom(σ), y = rt(t, σ)[p] ∈ Vars \ dom(σ) and x ≠ y; or b. x = rt(s, σ)[p] ∈ Vars \ dom(σ) and r = rt(t, σ)[p] ∉ Vars or, symmetrically,

we have r = rt(s, σ)[p] ∉ Vars and x = rt(t, σ)[p] ∈ Vars \ dom(σ); or c. r_{1} = rt(s, σ)[p] ∉ Vars, r_{2} = rt(t, σ)[p] ∉ Vars and r_{1} and r_{2} have different

principal functors.

Then, by definition of ‘rt’, there must exists an index i ∈ ℕ such that one of these hold:

1. x = sσ^{i}[p] ∈ Vars \ dom(σ), y = tσ^{i}[p] ∈ Vars \ dom(σ) and x ≠ y; or

2. x = sσ^{i}[p] ∈ Vars \ dom(σ) and r = tσ^{i}[p] ∉ Vars or, symmetrically, we have r = sσ^{i}[p] ∉ Vars and x = tσ^{i}[p] ∈ Vars \ dom(σ); or

3. r_{1} = sσ^{i}[p] ∉ Vars and r_{2} = tσ^{i}[p] ∉ Vars have different principal functors.

By Lemma 35, we have T ⊢ ∀(σ → (sσ^{i} = tσ^{i})); from this, by the identity axioms, we obtain that

T ⊢ ∀(σ → (sσ^{i}[p] = tσ^{i}[p])).  (A 1)

We now prove that each case leads to a contradiction.

Consider case 1. Let r_{1}, r_{2} ∈ GTerms ∩ HTerms be two ground and finite terms having different principal functors, so that T ⊢ ∀(r_{1} ≠ r_{2}). By Lemma 34, we have that σ′ = σ ∪ {x ↦ r_{1}, y ↦ r_{2}} ∈ RSubst is satisfiable; moreover, T ⊢ ∀(σ′ → σ), T ⊢ ∀(σ′ → (x = r_{1})) and T ⊢ ∀(σ′ → (y = r_{2})). This is a contradiction, since, by (A 1), we have T ⊢ ∀(σ → (x = y)).

Consider case 2. Without loss of generality, consider the first subcase, where x = sσ^{i} and r = tσ^{i}[p] ∉ Vars. Let r′ ∈ GTerms ∩ HTerms be such that r and r′ have different principal functors, so that T ⊢ ∀(r ≠ r′). By Lemma 34, σ′ = σ ∪ {x ↦ r′} ∈ RSubst is satisfiable; we also have T ⊢ ∀(σ′ → σ) and T ⊢ ∀(σ′ → (x = r′)). This is a contradiction, since, by (A 1), T ⊢ ∀(σ → (x = r)).

Finally, consider case 3. In this case T ⊢ ∀(r_{1} ≠ r_{2}). This immediately leads to a contradiction, since, by (A 1), T ⊢ ∀(σ → (r_{1} = r_{2})).

Proof of Proposition 1 on page 6 For each stated equivalence, we will prove only one implication since the other one will follow by symmetry.

Consider (9). Reasoning by contraposition, suppose rt(y, σ) ∉ Vars. Then there exists an index i ≥ 0 such that yσ^{i} ∉ Vars. Since T ⊢ ∀(τ → σ), by Lemma 35 we have T ⊢ ∀(τ → (y = yσ^{i})). By Lemma 36, we obtain rt(y, τ) = rt(yσ^{i}, τ), so that rt(y, τ) ∉ Vars.

Consider (10). We suppose, toward a contradiction, that rt(y, σ) ∈ GTerms but rt(y, τ) ∉ GTerms. Then, there must exist a finite path p such that:

a. r = rt(y, σ)[p] ∈ GTerms and x = rt(y, τ)[p] ∈ Vars \ dom(τ); or b. r_{1} = rt(y, σ)[p] ∉ Vars, r_{2} = rt(y, τ)[p] ∉ Vars and r_{1} and r_{2} have different

principal functors.

Then, by definition of ‘rt’, there must exists an index i ∈ ℕ such that one of these holds:

1. r = yσ^{i}[p] ∉ Vars and x = yτ^{i}[p] ∈ Vars \ dom(τ); or

2. r_{1} = yσ^{i}[p] ∉ Vars and r_{2} = yτ^{i}[p] ∉ Vars have different principal functors.

By Lemma 35, we have T ⊢ ∀(σ → (yσ^{i} = yτ^{i})); from this, by the identity axioms, we obtain that

T ⊢ ∀(σ → (yσ^{i}[p] = yτ^{i}[p])).  (A 2)

We now prove that both cases lead to a contradiction.

Consider case 1. Let r′ ∈ GTerms ∩ HTerms be such that r and r′ have different principal functors, so that T ⊢ ∀(r ≠ r′). By Lemma 34, τ′ = τ ∪{x ↦ r′} ∈ RSubst is satisfiable; we also have T ⊢ ∀(τ′ → τ) and T ⊢ ∀(τ′ → (x = r′)). This is a contradiction, since, by (A 2), T ⊢ ∀(τ → (x = r)).

Finally, consider case 2. In this case T ⊢ ∀(r_{1} ≠ r_{2}). This immediately leads to a contradiction, since, by (A 2), T ⊢ ∀(σ → (r_{1} = r_{2})).

Consider (11). Reasoning by contraposition, suppose that rt(y, τ) ∉ LTerms, so that there exists v ∈ vars(rt(y, τ)) such that occ lin(v, rt(y, τ)) does not hold. By definition of ‘rt’, there exists an index i ≥ 0 such that v ∈ vars(yτ^{i}) and occ lin(v, yτ^{i}) does not hold. Thus, as v ∉ dom(τ), so that rt(v, τ) = v ∈ Vars. By (9), rt(v, σ) = w ∈ Vars \ dom(σ). Therefore there exists j ≥ 0 such that w = vσ^{j}. Hence, we obtain that w ∈ vars(rt(yτ^{i}σ^{j}, σ)) and occ lin(w, rt(yτ^{i}σ^{j}, σ)) does not hold, so that rt(yτ^{i}σ^{j}, σ) ∉ LTerms. Since T ⊢ ∀(σ → τ), by Lemma 35 we have T ⊢ ∀(σ → (y = yτ^{i}σ^{j})). By Lemma 36, we obtain rt(y, σ) = rt(yτ^{i}σ^{j}, σ), so that rt(y, σ) ∉ LTerms.

B Proofs of the Results of Subsection 3.1.

The definition of idempotence requires that repeated applications of a substitution do not change the syntactic structure of a term. However, several abstractions of terms, such as the ones commonly used for sharing analysis, are only interested in the variables and not in the structure that contains them. Thus, an obvious way to relax the definition of idempotence to allow for a non-Herbrand substitution is to ignore the structure and just require that its repeated application leaves the set of variables in a term invariant.

Definition 37 (Variable-idempotence.) A substitution σ ∈ RSubst is variable-idempotent if and only if for all t ∈ HTerms we have

vars(tσσ) = vars(tσ).

The set of variable-idempotent substitutions is denoted VSubst.

Note that any idempotent substitution is also variable-idempotent, so that ISubst ⊂ VSubst ⊂ RSubst. This definition of variable-idempotence, which is the same as that originally provided in (Hill et al. 1998), is slightly stronger than the one adopted in (Hill et al. 2002) (weak variable-idempotence), where we disregard the domain variables of the substitution. Since variable-idempotent substitutions are weak variable-idempotent, many results in (Hill et al. 2002) also hold when weak variable-idempotence is replaced by variable-idempotence as given in Definition 37.

The following result provides an alternative characterization of variable-idempo-tence. The proof is by induction on the size of a term where, for each t ∈ HTerms, the function size: HTerms → ℕ is defined by

size(t) =^{def} \begin{cases}1, & if t ∈ Vars; \\ 1 + ∑_{i=1}^{n} size(t_{i}), & if t = f(t_{1}, …, t_{n}). \end{cases}

Lemma 38 Let σ ∈ RSubst. Then

σ ∈ VSubst ⟺ ∀(x ↦ r) ∈ σ : vars(rσ) = vars(r).

Proof Suppose first that σ ∈ VSubst and let (x ↦ r) ∈ σ. Then

vars(xσσ) = vars(xσ)

and hence, vars(rσ) = vars(r).

Next, suppose that for all (x ↦ r) ∈ σ, vars(rσ) = vars(r) and consider t ∈ HTerms. We will show that vars(tσσ) = vars(tσ) by induction on the size of t. If t is a constant or t ∈ Vars \dom(σ), then the result follows from the fact that tσ = t.

If t ∈ dom(σ), then there exists (y ↦ s) ∈ σ such that t = y, so that tσ = s. Thus, we have

vars(tσσ) = vars(sσ) = vars(s) = vars(tσ).

Finally, if t = f(t_{1}, …, t_{n}), then by the inductive hypothesis vars(t_{i}σσ) = vars(t_{i}σ) for i = 1, …, n. Therefore we have

vars(tσσ) = ⋃_{i=1}^{n} vars(t_{i}σσ) = ⋃_{i=1}^{n} vars(t_{i}σ) = vars(tσ).

Thus, by Definition 37, as σ ∈ RSubst, σ ∈ VSubst.

The next result provides a sufficient condition for a variable-idempotent substitution so that all of its subsets are variable-idempotent too.

Lemma 39 Let σ ∈ VSubst be such that for all y ∈ range(σ), y ∈ vars(yσ). Then, for all σ′ ⊆ σ, σ′ ∈ VSubst.

Proof Let (x ↦ t) ∈ σ′ ⊆ σ. We will prove that vars(tσ′) = vars(t), so that the thesis will follow from Lemma 38.

To prove the first implication, let y ∈ vars(tσ′), so that y ∈ range(σ). If it also holds y ∈ dom(σ), then by the hypothesis y ∈ vars(yσ), so that y ∈ vars(tσ). Otherwise, if y ∉ dom(σ), then again y ∈ vars(tσ). Thus, in both cases, since σ ∈ VSubst, by Lemma 38 we obtain y ∈ vars(t).

To prove the other implication, let y ∈ vars(t), so that y ∈ range(σ). If y ∉ dom(σ′) then y ∈ vars(tσ′). Otherwise, if y ∈ dom(σ′), then we have y ∈ dom(σ) ∩ range(σ). Thus, by hypothesis, y ∈ vars(yσ). Since yσ = yσ′, we have y ∈ vars(yσ′), so that y ∈ vars(tσ′).

The following result concerns the composition of variable idempotent substitutions and shows that, under the right conditions, the composition of variable idempotent substitutions is also variable idempotent.

Lemma 40 If σ, τ ∈ VSubst and dom(σ) ∩ vars(τ) = ∅, then τ ∘ σ ∈ VSubst.

Proof We will show that, for all terms t ∈ HTerms,

vars(tστ) = vars(tστστ).

To prove the inclusion vars(tστ) ⊆ vars(tστστ), let z ∈ vars(tστ). First note that, if z ∉ dom(σ) ∪ dom(τ), then the result is trivial.

Suppose z ∈ dom(σ). By hypothesis, z ∉ vars(τ) so that z ∈ vars(tσ). Since σ is variable-idempotent, z ∈ vars(tσσ), so that there exists v ∈ vars(tσ) ∩ dom(σ) such that z ∈ vars(vσ). Thus v ∉ vars(τ), so that v ∈ vars(tστ). Therefore z ∈ vars(tστσ) and, since z ∉ vars(τ), we can conclude z ∈ vars(tστστ).

Otherwise, let z ∈ dom(τ), so that z ∉ dom(σ). There exists v ∈ vars(tσ)∩dom(τ) such that z ∈ vars(vτ). Since τ is variable-idempotent, z ∈ vars(vττ) so that there exists w ∈ vars(vτ) ∩ dom(τ) such that z ∈ vars(wτ). Since w ∉ dom(σ) then w ∈ vars(tστσ). Therefore we can conclude z ∈ vars(tστστ).

To prove the other inclusion, let z ∈ vars(tστστ), so that there exists v ∈ vars(tστσ) such that z ∈ vars(vτ). Similarly, there exists w ∈ vars(tστ) such that v ∈ vars(wσ).

Suppose v ≠ w. Then w ∈ dom(σ), so that by hypothesis w ∉ vars(τ). As a consequence, w ∈ vars(tσ), v ∈ vars(tσσ) and z ∈ vars(tσστ). Thus, as σ ∈ VSubst, we obtain z ∈ vars(tστ).

Otherwise, if v = w, there exists x ∈ vars(tσ) such that z ∈ vars(xττ). Thus, z ∈ vars(tσττ) and, since τ ∈ VSubst, z ∈ vars(tστ).

The following result shows that there is no loss in generality in considering variable-idempotent substitutions only.

Proposition 41 Suppose T is an equality theory and σ ∈ RSubst. Then there exists σ′ ∈ VSubst such that dom(σ) = dom(σ′), vars(σ) = vars(σ′) and T ⊢ ∀(σ ↔ σ′); also, for all y ∈ range(σ′), y ∈ vars(yσ′).

Proof The proof is the same as the proofs of (Hill et al. 2002, Theorems 1 and 2) where weaker properties were stated.

The next useful result applies to any substitution in rational solved form.

Lemma 42 If σ ∈ RSubst, n = #σ and t ∈ HTerms, then tσ^{n} ∉ dom(σ).

Proof Suppose tσ^{n} ∈ Vars. Then, tσ^{i} ∈ Vars for all i = 1, …, n, so that, as σ ∈ RSubst has no circular subsets, we have tσ^{n} ∉ dom(σ).

For variable-idempotent substitutions, the following simplified characterizations for the operators occ, fvars, gvars and lvars can be used.

Proposition 43 For each σ ∈ VSubst and v ∈ Vars, we have

occ(σ, v) = { y ∈ Vars | v ∈ vars(yσ) \ dom(σ) },  (B 1)
gvars(σ) = { y ∈ Vars | vars(yσ) ⊆ dom(σ) },  (B 2)
fvars(σ) = { y ∈ Vars | yσ ∈ Vars \ dom(σ) },  (B 3)
lvars(σ) = \{ y ∈ Vars | \begin{matrix}∀z ∈ vars(yσ) \ dom(σ) : occ lin(z, yσ), \\ ∀z ∈ vars(yσ) ∩ dom(σ) : z ∈ gvars(σ) \end{matrix} \}.  (B 4)

Proof We prove each equation separately.

(B 1). This has been proved in (Hill et al. 2002, Lemma 13).

(B 2). By Definition 9, y ∈ gvars(σ) if and only if, for all v ∈ Vars, we have y ∉ occ(σ, v). By equation (B 1) proven above, this holds if and only if there does not exist v ∈ Vars such that v ∈ vars(yσ) \ dom(σ), i.e., if and only if vars(yσ) ⊆ dom(σ).

In order to prove the remaining equations, let n = #σ.

(B 3). By Definition 11, y ∈ fvars(σ) if and only if yσ^{n} ∈ Vars. First note that, if yσ^{n} ∉ Vars, then n ≥ 1 and yσ ∉ Vars \ dom(σ). Conversely, if yσ^{n} ∈ Vars, then yσ ∈ Vars. As σ ∈ VSubst, {yσ} = {yσ^{n}}, so that, by Lemma 42, yσ = yσ^{n} ∈ Vars \ dom(σ).

(B 4). First, suppose that, for some z ∈ vars(yσ), we have either z ∉ dom(σ) and occ lin(z, yσ) does not hold or z ∈ dom(σ) and z ∉ gvars(σ). In both cases, we have n ≥ 1 and we show that y ∉ lvars(σ). In the first case it follows that z ∈ vars(yσ^{n}) and occ lin(z, yσ^{2n}) does not hold. For the second case, by equation (B 2) proved above, there exists w ∈ vars(zσ) \ dom(σ). As σ ∈ VSubst, we have w ∈ vars(yσ) \ dom(σ). Since z ∈ vars(yσ), we obtain that occ lin(w, yσ^{2}) does not hold and, as n ≥ 1, occ lin(w, yσ^{2n}) does not hold. Therefore, by Definition 13, y ∉ lvars(σ).

Secondly, suppose that y ∉ lvars(σ) so that n ≥ 1. Then, by Definition 13, there exists z ∈ vars(yσ^{n}) \ dom(σ) such that occ lin(z, yσ^{2n}) does not hold. Thus, as σ ∈ VSubst, z ∈ vars(yσ). Also, if occ lin(z, yσ) holds, there must exist v ∈ vars(yσ) ∩ dom(σ) and z ∈ vars(vσ^{2n−1}). Thus, as σ ∈ VSubst, z ∈ vars(vσ) and vars(vσ) \ dom(σ) ≠ ∅ and hence, by equation (B 2), z ∉ gvars(σ).

The following proposition shows that, for a substitution σ ∈ VSubst, the occurrence, groundness, freeness and linearity operators precisely capture the intended properties.

Proposition 44 Let σ ∈ VSubst, y ∈ VI and v ∈ Vars. Then:

y ∈ occ(σ, v) ⟺ v ∈ vars(rt(y, σ)),  (B 5)
y ∈ gvars(σ) ⟺ rt(y, σ) ∈ GTerms,  (B 6)
y ∈ fvars(σ) ⟺ rt(y, σ) ∈ Vars,  (B 7)
y ∈ lvars(σ) ⟺ rt(y, σ) ∈ LTerms.  (B 8)

Proof We prove each item separately.

(B 5). By Proposition 43, y ∈ occ(σ, v) if and only if v ∈ vars(yσ) \ dom(σ). To prove the first implication (⇒), let v ∈ vars(yσ) \ dom(σ). Then, for all i > 0, we have v ∈ vars(yσ^{i}) \ dom(σ), so that v ∈ vars(rt(y, σ)). To prove the other implication (⇐), assume that v ∈ vars(rt(y, σ)). Then, by definition of rt, v ∉ dom(σ) and v ∈ vars(yσ^{i}) for some i ≥ 1. Assume that i ≥ 1 is minimal such that v ∈ vars(yσ^{i}). If i > 1, then we have v ∉ vars(yσ^{i−1}) which contradicts the assumption that σ ∈ VSubst. Thus i = 1 and v ∈ vars(yσ).

(B 6). By Definition 9, we have y ∈ gvars(σ) if and only if y ∉ occ(σ, v), for all v ∈ Vars. By item (B 5) proved above, this is equivalent to v ∉ vars(rt(y, σ)), for all v ∈ Vars. Thus, vars(rt(y, σ)) = ∅ and rt(y, σ) ∈ GTerms.

(B 7). By Proposition 43, y ∈ fvars(σ) if and only if yσ ∈ Vars \dom(σ). To prove the first implication (⇒), let yσ ∈ Vars \ dom(σ). Then, rt(y, σ) ∈ Vars \ dom(σ) and, more generally, rt(y, σ) ∈ Vars. To prove the other implication (⇐), assume that rt(y, σ) ∈ Vars. We prove by contradiction that yσ ∈ Vars \ dom(σ). In fact, assume that yσ ∉ Vars \ dom(σ). We have two cases:

1. if yσ ∉ Vars then, by definition, rt(y, σ) ∉ Vars.

2. otherwise, let yσ ∈ dom(σ). Thus, we have y ≠ yσ ≠ yσσ, so that (y ↦ yσ) ∈ σ and (yσ ↦ yσσ) ∈ σ. Since σ ∈ VSubst, we also have {yσ} = vars(yσ) = vars(yσσ). Therefore, yσσ ∉ Vars. Hence, by definition, rt(y, σ) ∉ Vars.

(B 8). In order to prove the first implication (⇒), assume y ∈ lvars(σ) so that, by Proposition 43, we have

∀z ∈ vars(yσ) \ dom(σ) : occ lin(z, yσ),  (B 9)
∀z ∈ vars(yσ) ∩ dom(σ) : vars(zσ) ⊆ dom(σ).  (B 10)

We need to show that rt(y, σ) ∈ LTerms and we proceed by contradiction, negating the conclusion. Thus assume that there exists v ∈ vars(rt(y, σ)) such that occ lin(v, rt(y, σ)) does not hold. Note that v ∉ dom(σ); also, since σ ∈ VSubst, vars(yσ) = vars(yσ^{i}), for all i > 0, so that v ∈ vars(yσ). If occ lin(v, yσ) does not hold, then we obtain the negation of (B 9), hence a contradiction. So, assume that occ lin(v, yσ) hold. As a consequence, there exists an index j > 1 such that occ lin(v, yσ^{j−1}) holds and occ lin(v, yσ^{j}) does not hold. Thus, there exists w ∈ vars(yσ^{j−1}) ∩ dom(σ) such that v ∈ vars(wσ) \ dom(σ). Since σ ∈ VSubst, w ∈ vars(yσ^{j−1}) if and only if w ∈ vars(yσ). Hence j = 2, w ∈ vars(yσ) ∩ dom(σ) and vars(wσ) ⊈ dom(σ), therefore contradicting (B 10).

To prove the other implication (⇐), assume rt(y, σ) ∈ LTerms, so that, by definition, we have occ lin(z, rt(y, σ)), for all z ∈ vars(rt(y, σ)). We need to show that both (B 9) and (B 10) hold. We proceed by contradiction, negating the conclusion. There are two cases.

1. Assume that (B 9) does not hold, i.e., there exists z ∈ vars(yσ) \ dom(σ) such that occ lin(z, yσ) does not hold. Then, for all i > 0, we have that z ∈ vars(yσ^{i}), but occ lin(z, yσ^{i}) does not hold. Hence, occ lin(z, rt(y, σ)) does not hold and rt(y, σ) ∉ LTerms, obtaining the contradiction.

2. Assume now (B 10) does not hold, i.e., there exists z ∈ vars(yσ) ∩ dom(σ) such that vars(zσ) ⊈ dom(σ). Thus, let v ∈ vars(zσ) \ dom(σ). Since σ ∈ VSubst and v ∈ vars(yσσ), then v ∈ vars(yσ). Then, since z ∈ vars(yσ) ∩ dom(σ), occ lin(v, yσσ) does not hold. Also, since v ∉ dom(σ), for all i ≥ 2, occ lin(v, yσ^{i}) does not hold. By definition, occ lin(v, rt(y, σ)) does not hold and rt(y, σ) ∉ LTerms, obtaining the contradiction.

In order to simplify the proof of Proposition 15, we first prove some preliminary results.

Let T be a syntactic equality theory and σ, τ ∈ RSubst be satisfiable substitutions such that T ⊢ ∀(σ ↔ τ). Let m = #σ, n = #τ and s, t ∈ HTerms, where T ⊢ ∀(σ → (s = t)). Then sσ^{m} ∈ Vars if and only if tτ^{n} ∈ Vars.

Proof We prove only one implication since the other follows by symmetry. Suppose sσ^{m} ∈ Vars. Then, by Lemma 42, sσ^{m} ∈ Vars \ dom(σ) so that rt(sσ^{m}, σ) = sσ^{m}. Moreover, by Lemma 35, T ⊢ ∀(σ → (sσ^{m} = tτ^{n})) so that, by Lemma 36, rt(tτ^{n}, σ) = sσ^{m} ∈ Vars. Therefore tτ^{n} ∈ Vars.

Lemma 46 Let T be a syntactic equality theory and σ, τ ∈ RSubst be satisfiable substitutions such that T ⊢ ∀(σ ↔ τ). Let also n = #τ and s, t ∈ HTerms be such that T ⊢ ∀(σ → (s = t)). If z ∈ vars(s)\dom(σ), then there exists z′ ∈ vars(tτ^{n})\dom(τ) and T ⊢ ∀(τ → (z = z′)).

Proof The proof is by induction on the size of term s.

If size(s) = 1 and z ∈ vars(s), then we have s = z. Then, for all i ≥ 1, sσ^{i} ∈ Vars. Thus, by Lemma 45, tτ^{n} ∈ Vars and hence, by Lemma 42, tτ^{n} ∈ Vars \ dom(τ). By Lemma 35, T ⊢ ∀(τ → (z = tτ^{n})). Thus, in this case let z′ = tτ^{n}.

For the inductive step, suppose that s = f(s_{1}, …, s_{m}) and z ∈ vars(s_{j}), for some j ∈ {1, …, m}. Then, by Lemma 45, we obtain tτ^{n} ∉ Vars. By the satisfiability hypothesis and the identity axioms, there exist t_{1}, …, t_{m} ∈ HTerms such that tτ^{n} = f(t_{1}, …, t_{m}) and, in particular, T ⊢ ∀(σ → (s_{j} = t_{j})). By the inductive hypothesis, there exists z′ ∈ vars(t_{j}τ^{n}) \ dom(τ) such that T ⊢ ∀(τ → (z = z′)). It follows that z′ ∈ vars(tτ^{2n}) and, since n = #τ, z′ ∈ vars(tτ^{n}).

Lemma 47 Let T be a syntactic equality theory and σ, τ ∈ RSubst be satisfiable substitutions such that T ⊢ ∀(σ ↔ τ). Let also n = #τ and s, t ∈ HTerms be such that T ⊢ ∀(σ → (s = t)). If there exists z ∈ vars(s) \ dom(σ) such that occ lin(z, s) does not hold, then there exists z′ ∈ vars(tτ^{n}) \ dom(τ) such that occ lin(z′, tτ^{2n}) does not hold and T ⊢ ∀(τ → (z = z′)).

Proof The proof is by induction on the size of term s.

If size(s) = 1 and z ∈ vars(s), then we have s = z. In this case there is nothing to prove, since occ lin(z, s) necessarily holds.

For the inductive step, suppose that s = f(s_{1}, …, s_{m}) and there exists z ∈ vars(s) \ dom(σ) such that occ lin(z, s) does not hold. For all i ≥ 0, we have sσ^{i} ∉ Vars so that, by Lemma 45, tτ^{n} ∉ Vars. By the satisfiability hypothesis and the identity axioms, there exist t_{1}, …, t_{m} ∈ HTerms such that tτ^{n} = f(t_{1}, …, t_{m}) and T ⊢ ∀(σ → (s_{i} = t_{i})), for all i ∈ {1, …, m}. Since occ lin(z, s) does not hold, there are two cases.

1. There exist j, k ∈ {1, …, m} such that j ≠ k and z ∈ vars(s_{j}) ∩ vars(s_{k}). By applying Lemma 46 twice, there exist z′ ∈ vars(t_{j}τ^{n}) \ dom(τ) and z′′ ∈ vars(t_{k}τ^{n})\dom(τ) such that T ⊢ ∀(τ → (z = z′)) and T ⊢ ∀(τ → (z = z′′)). Thus T ⊢ ∀(τ → (z′ = z′′)) and, since z′, z′′ ∉ dom(τ), by Lemma 36, we have that z′ = z′′. Hence, occ lin(z′, tτ^{2n}) does not hold.

2. There exists j ∈ {1, …, m} such that occ lin(z, s_{j}) does not hold. Then, by the inductive hypothesis, there exists z′ ∈ vars(t_{j}τ^{n}) \ dom(τ) such that occ lin(z′, t_{j}τ^{2n}) does not hold and T ⊢ ∀(τ → (z = z′)). Thus occ lin(z′, tτ^{3n}) does not hold. We now show that occ lin(z′, tτ^{2n}) does not hold. As n = #τ, z′ ∈ vars(tτ^{n}). Clearly, if occ lin(z′, tτ^{n}) does not hold, then occ lin(z′, tτ^{2n}) does not hold. On the other hand, if occ lin(z′, tτ^{n}) holds, then there exists y ∈ vars(tτ^{n}) such that y ≠ z′ and z′ ∈ vars(yτ^{2n}). Again, as n = #τ, z′ ∈ vars(yτ^{n}), so that occ lin(z′, tτ^{2n}) does not hold.

Proof of Proposition 15 on page 11. As the operator ‘ssets’ basically corresponds to the abstraction function defined in (Hill et al. 2002), equation (12) follows from (Hill et al. 2002, Theorem 4). Also, by Definition 9, equation (13) is a simple consequence of equation (12).

To prove (14) and (15), let m = #σ and n = #τ. We will prove one inclusion only, as the other one follows by a symmetric reasoning.

Consider (14) and let y ∈ fvars(σ). Then, by Definition 11, yσ^{m} ∈ Vars. so that, by Lemma 45, yτ^{n} ∈ Vars. Hence, by Definition 11, y ∈ fvars(τ).

Consider (15) and let y ∉ lvars(σ). Then, by Definition 13, there exists z ∈ vars(yσ^{m}) \ dom(σ) such that occ lin(z, yσ^{2m}) does not hold. By Lemma 35, T ⊢ ∀(σ → (yσ^{2m} = y)) so that, by Lemma 47, there exists z′ ∈ vars(yτ^{n}) \ dom(τ) such that occ lin(z′, yτ^{2n}) does not hold. Therefore, by Definition 13, y ∉ lvars(τ).

Lemma 48 Let T be a syntactic equality theory and σ, τ ∈ RSubst be satisfiable substitutions such that dom(σ) = dom(τ) and T ⊢ ∀(σ ↔ τ). Then vars(rt(y, σ)) = vars(rt(y, τ)).

Proof We only prove vars(rt(y, σ)) ⊆ vars(rt(y, τ)), since the other direction follows by symmetry. Suppose v ∈ vars(rt(y, σ)). Then v ∉ dom(σ) and hence v ∉ dom(τ). Moreover, there exists an index i ≥ 0 such that v ∈ vars(yσ^{i}). Hence we have v ∈ vars(rt(yσ^{i}, τ)). Since, by Lemma 36, rt(y, τ) = rt(yσ^{i}, τ), it follows that v ∈ vars(rt(y, τ)).

Proof of Proposition 16 on page 12. By Proposition 41, there exists τ ∈ VSubst such that dom(σ) = dom(τ) and T ⊢ ∀(σ ↔ τ). By Proposition 15, we have ssets(σ) = ssets(τ), gvars(σ) = gvars(τ), fvars(σ) = fvars(τ) and lvars(σ) = lvars(τ). From all of the above, by Proposition 44, we obtain

y ∈ occ(σ, v) ⟺ v ∈ vars(rt(y, τ)),
y ∈ gvars(σ) ⟺ rt(y, τ) ∈ GTerms,

y ∈ fvars(σ) ⟺ rt(y, τ) ∈ Vars,
y ∈ lvars(σ) ⟺ rt(y, τ) ∈ LTerms.

Thus (16) follows from Lemma 48 while (17), (18) and (19) follow from Proposition 1.

C Proofs of the Results of Subsection 3.2

In this section we prove that the abstract unification operator defined on the domain SFL is a correct approximation of the concrete unification procedure.

The section is composed of several subsections. In Subsection C.1, we recall the definition of the abstract mgu operator on SH and the corresponding correctness result, as provided in (Hill et al. 2002). Then, in Subsection C.2, we prove the correctness of the auxiliary operations given in Definition 20. Subsection C.3, proves some general results and introduces some notation that helps to simplify the main correctness results. In the next three Subsections C.4, C.5 and C.6, we prove the correctness of the abstract unification operator on set-sharing, freeness and linearity, respectively. Then, finally, in Subsection C.7, we combine these results to establish the correctness of amgu_{S} in the proof of Theorem 23.

C.1 Abstract unification for SH

Definition 49 (amgu and aunify.) The function amgu: SH × Bind → SH captures the effects of a binding on an SH element. For each sh ∈ SH and (x ↦ t) ∈ Bind such that {x} ∪ vars(t) ⊆ VI , let sh_{x} =^{def} rel({x}, sh), sh_{t} =^{def} rel(vars(t), sh) and sh_{−} =^{def} \overline{rel}(\{x\} ∪ vars(t), sh). Then

amgu(sh, x ↦ t) =^{def} sh_{−} ∪ bin(sh_{x}^{⋆}, sh_{t}^{⋆}).

The operator aunify: SH × RSubst → SH is defined, for each sh ∈ SH and each substitution σ ∈ RSubst such that vars(σ) ⊆ VI , by

aunify(sh, σ) =^{def} \begin{cases}sh, & if σ = ∅; \\ aunify(amgu(sh, x ↦ t), σ \ \{x ↦ t\}), & if (x ↦ t) ∈ σ. \end{cases}

Theorem 50 ((Hill et al. 2002, Theorem 5).) Let sh ∈ SH and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let σ ∈ RSubst be such that ssets(σ) ⊆ sh and suppose that τ ∈ mgs({x = t} ∪ σ) in the syntactic equality theory T. Then

ssets(τ) ⊆ amgu(sh, x ↦ t).

C.2 The Correctness of the auxiliary operations

Proof of Theorem 21 on page 14. Let d = ⟨sh, f, l⟩, V_{s} = vars(s) and V_{t} = vars(t). By Definition 18, we have ∀v ∈ Vars : occ(σ, v) ∩ VI ∈ sh ∪ {∅}, f ⊆ fvars(σ), and l ⊆ lvars(σ).

Consider the implication (20). By Definition 20, the hypothesis and Proposition 16, we have

ind_{d}(s, t) ⟺ rel(V_{s}, sh) ∩ rel(V_{t}, sh) = ∅
⟺ ∀S ∈ sh, w_{1} ∈ V_{s}, w_{2} ∈ V_{t} : {w_{1}, w_{2}} ⊈ S
⟹ ∀v ∈ Vars, w_{1} ∈ V_{s}, w_{2} ∈ V_{t} : {w_{1}, w_{2}} ⊈ occ(σ, v)
⟺ ∀w_{1} ∈ V_{s}, w_{2} ∈ V_{t} : vars(rt(w_{1}, σ)) ∩ vars(rt(w_{1}, σ)) = ∅
⟺ vars(rt(s, σ)) ∩ vars(rt(t, σ)) = ∅.

Consider the equivalence (21). By Definition 20, we have

ind_{d}(y, t) ⟺ rel({y}, sh) ∩ rel(V_{t}, sh) = ∅
⟺ ∀S ∈ rel(V_{t}, sh) : y ∉ S
⟺ y ∉ share with_{d}(t).

Consider now the implication (22). By Definition 20, the hypothesis and Proposition 16, we have

free_{d}(t) ⟺ t ∈ f
⟹ t ∈ fvars(σ)
⟺ rt(t, σ) ∈ Vars.

Consider now the implication (23). By Definition 20, the hypothesis and Proposition 16, we have

ground_{d}(t) ⟺ vars(t) ⊆ VI \ vars(sh)
⟹ ∀w ∈ V_{t} : w ∈ gvars(σ)
⟺ ∀w ∈ V_{t} : vars(rt(w, σ)) = ∅
⟺ rt(t, σ) ∈ GTerms.

Finally consider the implication (24). By Definition 20, the hypothesis, the above results and Proposition 16, we have

lin_{d}(t) ⟺ ∀y, z ∈ vars(t) : ground_{d}(y)
∨ ((y ∈ l) ∧ occ lin(y, t) ∧ (y ≠ z ⟹ ind_{d}(y, z)))
⟹ ∀y, z ∈ vars(t) : ground_{d}(y)
∨ ((y ∈ lvars(σ)) ∧ occ lin(y, t) ∧ (y ≠ z ⟹ ind_{d}(y, z)))
⟹ ∀y, z ∈ vars(t) : rt(y, σ) ∈ GTerms
∨ ((rt(y, σ) ∈ LTerms) ∧ occ lin(y, t)
∧ (y ≠ z ⟹ vars(rt(y, σ)) ∩ vars(rt(z, σ)) = ∅))
⟺ rt(t, σ) ∈ LTerms.

C.3 Additional results and notation used for the correctness results

Lemma 51 Assume T is an equality theory and σ ∈ RSubst. Then, for each s, t ∈ HTerms,

mgs(σ ∪ {s = t}) = mgs(σ ∪ {s = tσ}).

Proof First, note, using the congruence axioms (3) and (4), that, for any terms p, q, r ∈ HTerms,

T ⊢ ∀(p = q ∧ q = r) ↔ ∀(p = r ∧ q = r).

Secondly note that, using Lemma 35, for any substitution τ ∈ RSubst and term r ∈ HTerms, T ⊢ ∀(τ → (r = rτ)), so that

T ⊢ ∀(τ ↔ τ ∪ {r = rτ}).

Using these results,

T ⊢ ∀(σ ∪ {s = t} ↔ σ ∪ {s = t, t = tσ}),
T ⊢ ∀(σ ∪ {s = t} ↔ σ ∪ {s = tσ, t = tσ}),
T ⊢ ∀(σ ∪ {s = t} ↔ σ ∪ {s = tσ}).

The thesis follows by the definition of mgs.

The following rather technical result is required more than once in the proofs in this section.

Lemma 52 ((Hill et al. 2002, Lemma 6).) Let τ, σ ∈ VSubst be satisfiable in the syntactic equality theory T and suppose T ⊢ ∀(τ → σ). In addition, let s, t ∈ HTerms be such that T ⊢ ∀(τ → (s = t)) and v ∈ vars(s)\dom(τ). Then there exists a variable z ∈ vars(tσ) \ dom(σ) such that v ∈ vars(zτ).

The following lemma, which will be used several times in the following proofs without an explicit reference to it, states the well-known result that groundness is closed by entailment.

Lemma 53 Let σ, τ ∈ RSubst be satisfiable in the syntactic equality theory T and such that T ⊢ ∀(τ → σ). Then gvars(σ) ⊆ gvars(τ).

Proof We prove the result by showing that x ∉ gvars(τ) implies x ∉ gvars(σ).

By Proposition 41, we can assume there exist σ′, τ′ ∈ VSubst such that T ⊢ ∀(σ ↔ σ′) and T ⊢ ∀(τ ↔ τ′), so that T ⊢ ∀(τ′ → σ′). Also, by Proposition 15, we have gvars(σ) = gvars(σ′) and gvars(τ) = gvars(τ′). Therefore, it is sufficient to prove that x ∉ gvars(τ′) implies x ∉ gvars(σ′).

Assume x ∉ gvars(τ′). By Definition 9, there exists v ∈ Vars such that x ∈ occ(τ′, v). By Proposition 43, v ∈ vars(xτ′) \ dom(τ′). Also, by Lemma 35, T ⊢ ∀(τ′ → xτ′ = x). Therefore, by Lemma 52 (taking s = xτ′ and t = x) there exists z ∈ vars(xσ′) \ dom(σ′) such that v ∈ vars(zτ′). By Definition 7, we have x ∈ occ(σ′, z) so that, by Definition 9, x ∉ gvars(σ′).

Since all substitutions in mgs(e) are equivalent, they also have the same sharing groups, ground the same variables and have the same sets of free and linear variables.

Lemma 54 Let e ⊆ Eqs be satisfiable in the syntactic equality theory T. If σ, τ ∈ mgs(e), then ssets(σ) = ssets(τ), gvars(σ) = gvars(τ), fvars(σ) = fvars(τ) and lvars(σ) = lvars(τ).

Proof By definition of mgs, we have σ, τ ∈ RSubst and T ⊢ ∀(σ ↔ e ↔ τ). Thus, all the stated equivalences follow from Proposition 15.

We now introduce a bit of terminology that helps simplify the notation used in the next and later proofs. Given V ⊆ Vars, we say that t ∈ HTerms is V -linear if occ lin(v, t) holds for all variables v ∈ vars(t) ∩ V. Note that if a term is V - linear, then it is also W -linear, for all W ⊆ V. This terminology also applies to n-tuples of terms, by simply regarding the n-tuple construction as a term functor of arity n. Moreover, if s̄, t̄ ∈ HTerms^{n} are such that mgs(s̄ = t̄) ≠ ∅, then we write gvars(s̄ = t̄) to denote the set gvars(μ), where μ ∈ mgs(s̄ = t̄). Note that, by Lemma 54, this notation is not ambiguous.

The next proposition shows under what conditions the properties of linearity and independence are preserved.

Proposition 55 Suppose s̄, t̄ ∈ HTerms^{n} and mgs(s̄ = t̄) ≠ ∅. Let G =^{def} gvars(s̄ = t̄) and suppose also that s̄ is (Vars \ G)-linear. Then there exists μ ∈ mgs(s̄ = t̄) ∩ VSubst such that

Vars \ vars(s̄) ⊆ lvars(μ),  (C 1)
∀z, z′ ∈ Vars \ vars(s̄) :
z ≠ z′ ⟹ rel({z}, ssets(μ)) ∩ rel({z′}, ssets(μ)) = ∅.

(C 2)

Proof By Proposition 15 and 41, we just have to show that there exists μ ∈ VSubst such that (C 1) and (C 2) hold.

By Proposition 43, if z ∈ Vars, then z ∈ lvars(μ) if and only if

∀y ∈ vars(zμ) \ dom(μ) : occ lin(y, zμ),
vars(zμ) ∩ dom(μ) ⊆ G.

As G ⊆ dom(μ), it follows from Proposition 43, that (C 1) and (C 2) will hold if and only if, for each z ∈ Vars \ vars(s̄):

zμ is (Vars \ G)-linear;  (C 3)
vars(zμ) ∩ dom(μ) ⊆ G;  (C 4)

∀z′ ∈ Vars \ vars(s̄) : z ≠ z′ ⟹ vars(zμ) ∩ vars(z′μ) ⊆ G.  (C 5)

Let s̄ = (s_{1}, …, s_{n}), and t̄= (t_{1}, …, t_{n}), W = vars(s̄)∪vars(t̄) and V = Vars \G. We assume that s̄ is V -linear and show, by induction on the number of variables in W, that there exists μ ∈ mgs(s̄ = t̄)∩VSubst such that, for each z ∈ Vars \vars(s̄), Properties (C 3), (C 4) and (C 5) hold.

Suppose first that, for some i = 1, …, n, we have s_{i} = f(r_{1}, …, r_{m}) and t_{i} = f(u_{1}, …, u_{m}), where m ≥ 0. Let

s̄_{i} =^{def} (s_{1}, …, s_{i−1}, r_{1}, …, r_{m}, s_{i+1}, …, s_{n}),
t̄_{i} =^{def} (t_{1}, …, t_{i−1}, u_{1}, …, u_{m}, t_{i+1}, …, t_{n}).

Then mvars(s̄_{i}) = mvars(s̄) and mvars(t̄_{i}) = mvars(t̄) so that, since s̄ is V -linear, s̄_{i} is V -linear. Moreover, by the congruence axiom (5), we have mgs(s̄_{i} = t̄_{i}) = mgs(s̄ = t̄). (Note that in the case that s_{i} and t_{i} are identical constants, the equation s_{i} = t_{i} is just removed.) Thus, as s̄ and t̄ are finite sequences of finite terms, we can assume that s_{i} ∈ Vars or t_{i} ∈ Vars, for all i = 1, …, n.

Secondly, suppose that for some i = 1, …, n, s_{i} = t_{i}. By the previous paragraph, we can assume that s_{i} ∈ Vars. Let

s̄_{i} =^{def} (s_{1}, …, s_{i−1}, s_{i+1}, …, s_{n}),
t̄_{i} =^{def} (t_{1}, …, t_{i−1}, t_{i+1}, …, t_{n}).

Then mvars(s̄_{i}) ∪ {s_{i}} = mvars(s̄) and mvars(t̄_{i}) ∪ {s_{i}} = mvars(t̄) so that, as s̄ is V -linear, s̄_{i} is V -linear. Furthermore, by the congruence axiom (2), mgs(s̄_{i} = t̄_{i}) = mgs(s̄ = t̄). Thus, as s̄ and t̄ are sequences of finite length n, we can assume that s_{i} ≠ t_{i}, for all i = 1, …, n.

Therefore, for the rest of the proof, we will assume that s_{i} ≠ t_{i} and s_{i} ∈ Vars or t_{i} ∈ Vars, for all i = 1, …, n.

The base case is when W = ∅, so that we have vars(μ) = ∅ for all μ ∈ mgs(s̄ = t̄). Thus all three properties hold trivially.

To prove the inductive step, we assume that W ≠ ∅, so that n > 0. Note that, in the case that vars(t̄) ⊆ vars(s̄), then all three properties hold trivially. This is because for all μ ∈ mgs(s̄ = t̄) and for all z ∈ Vars \ vars(s̄), we have z ∉ vars(μ). Similarly, the three properties hold trivially whenever vars(t̄) ⊆ G. This is because, if z ∈ dom(μ), then vars(zμ) ⊆ G. We therefore assume for the rest of the proof that for some i = 1, …, n, vars(t_{i}) \ (vars(s̄) ∪ G) ≠ ∅. As the order of equations is irrelevant, without loss of generality we assume that this property holds when i = 1, so that vars(t_{1}) \ (vars(s̄) ∪ G) ≠ ∅. This can be re-written as

vars(t_{1}) ∩ (V \ vars(s̄)) ≠ ∅.  (C 6)

Note that this implies that t_{1} ≠ s_{1}. By Proposition 16, another consequence of the above assumption is that, for all μ ∈ mgs(s̄ = t̄), we have rt(t_{1}, μ) ∉ GTerms. Since T ⊢ ∀(μ → (s_{1} = t_{1})), by Lemma 36, we obtain rt(s_{1}, μ) ∉ GTerms, so that again by Proposition 16, vars(s_{1}) \ G ≠ ∅. This in turn can be re-written as

vars(s_{1}) ∩ V ≠ ∅.  (C 7)

By exploiting (C 6) and (C 7), we can identify three different cases:

a. for all i = 1, …, n, V ∩ vars(s_{i}) ∩ vars(t_{i}) ≠ ∅; b. s_{1} ∈ V \ vars(t_{1}); c. t_{1} ∈ V \ vars(s̄) and s_{1} ∉ Vars;

Case a. For all i = 1, …, n, V ∩ vars(s_{i}) ∩ vars(t_{i}) ≠ ∅.

For each i = 1, …, n, we are assuming that s_{i} ∈ V or t_{i} ∈ V. Therefore, for each i = 1, …, n, s_{i} ∈ vars(t_{i}) or t_{i} ∈ vars(s_{i}) so that, without loss of generality, we can assume, for some k where 0 ≤ k ≤ n, s_{i} ∈ V if 1 ≤ i ≤ k and t_{i} ∈ V if k + 1 ≤ i ≤ n.

Let μ′ ⊆ Eqs be defined as

μ′ =^{def} {s_{1} = t_{1}, …, s_{k} = t_{k}} ∪ {t_{k+1} = s_{k+1}, …, t_{n} = s_{n}}.

We show that μ′ ∈ mgs(s̄ = t̄). First we must show that μ′ ∈ RSubst. As s̄ is V - linear, (s_{1}, …, s_{k}) is linear; (t_{k+1}, …, t_{n}) is also linear, because s̄ is V -linear and t_{i} ∈ V ∩ vars(s_{i}) if k + 1 ≤ i ≤ n; moreover, for the same reasons, {s_{1}, …, s_{k}} ∩ {t_{k+1}, …, t_{n}} = ∅. As we are assuming that, for all i = 1, …, n, s_{i} ≠ t_{i} and V ∩ vars(s_{i}) ∩ vars(t_{i}) ≠ ∅, it follows that t_{i} ∉ Vars when 1 ≤ i ≤ k and s_{i} ∉ Vars when k + 1 ≤ i ≤ n, so that each equation in μ′ is a binding and μ′ has no circular subsets. Thus μ′ ∈ RSubst and hence, by the congruence axiom (3), μ′ ∈ mgs(s̄ = t̄).

By Proposition 41, there exists μ ∈ VSubst such that dom(μ) = dom(μ′) and μ ∈ mgs(s̄ = t̄). As {t_{k+1}, …, t_{n}} ⊆ vars((s_{k+1}, …, s_{n})), we have dom(μ) = dom(μ′) ⊆ vars(s̄) so that the required result for μ holds trivially.

Case b. Suppose s_{1} ∈ V \ vars(t_{1}) Let

s̄_{1} =^{def} (s_{2}, …, s_{n}),
t̄_{1} =^{def} (t_{2}{s_{1} ↦ t_{1}}, …, t_{n}{s_{1} ↦ t_{1}}).

As s̄ is V -linear, s̄_{1} is V -linear and s_{1} ∉ vars(s̄_{1}). Also, all occurrences of s_{1} in t̄ are replaced in t̄_{1} by t_{1} so that, as s_{1} ∉ vars(t_{1}) (by the assumption for this case), s_{1} ∉ vars(t̄_{1}). Thus,

s_{1} ∉ W_{1} =^{def} vars(s̄_{1}) ∪ vars(t̄_{1}),  (C 8)

so that W_{1} ⊂ W. Let G_{1} =^{def} gvars(s̄_{1} = t̄_{1}) and V_{1} =^{def} Vars \ G_{1}. Note that G_{1} ⊆ G and, by the assumption for this case, s_{1} ∈ V, so that s_{1} ∉ G. As a consequence, G_{1} = G, V_{1} = V and s̄_{1} is V_{1}-linear, so that the inductive hypothesis applies to s̄_{1} and t̄_{1}. Thus, there exists μ_{1} ∈ mgs(s̄_{1} = t̄_{1}) ∩ VSubst such that, for each z ∈ Vars \ vars(s̄_{1}), the three inductive properties hold.

Let μ ⊆ Eqs be defined as

μ =^{def} {s_{1} = t_{1}μ_{1}} ∪ μ_{1}.

We show that μ ∈ VSubst. Note that ν =^{def} {s_{1} ↦ t_{1}} ∈ VSubst and, by (C 8), we have dom(ν) ∩ vars(μ_{1}) = {s_{1}} ∩ vars(μ_{1}) = ∅. Hence, since μ_{1} ∈ VSubst, by Lemma 40 we obtain μ = μ_{1} ∘ ν ∈ VSubst. Also note that, by Lemma 51, μ ∈ mgs(s̄ = t̄).

Suppose that z ∈ Vars \ vars(s̄). Then, as vars(s̄) = vars(s̄_{1}) ∪ {s_{1}}, z ∈ Vars \ vars(s̄_{1}). Thus, the inductive properties C 3, C 4 and C 5 using μ_{1} and s̄_{1} can be applied to zμ_{1}. Knowing this, we now show that the same properties using μ and s̄ can be applied to zμ. Since dom(μ) = dom(μ_{1})∪{s_{1}} and z ≠ s_{1}, we have zμ_{1} = zμ and s_{1} ∉ vars(zμ). Each property is proved separately.

1. By the inductive property C 3, we have zμ_{1} is V_{1}-linear. As zμ = zμ_{1} and V = V_{1}, zμ is V -linear.

2. By inductive property C 4, we have vars(zμ_{1})∩dom(μ_{1}) ⊆ G_{1}. Since zμ = zμ_{1}, G = G_{1}, dom(μ) = dom(μ_{1}) ∪ {s_{1}} and s_{1} ∉ vars(zμ), we obtain vars(zμ) ∩ dom(μ) ⊆ G.

3. Let z′ ∈ Vars \ vars(s̄) be such that z ≠ z′. Since z′ ∉ vars(s̄), we have z′ ∉ vars(s̄_{1}) and z′μ = z′μ_{1}. By applying inductive property C 5, vars(zμ_{1})∩ vars(z′μ_{1}) ⊆ G_{1}. As zμ = zμ_{1}, z′μ = z′μ_{1} and G = G_{1}, we obtain vars(zμ) ∩ vars(z′μ) ⊆ G.

Case c. Assume that t_{1} ∈ V \ vars(s̄) and s_{1} ∉ Vars. Let

s̄_{1} =^{def} (s_{2}, …, s_{n}),
t̄_{1} =^{def} (t_{2}{t_{1} ↦ s_{1}}, …, t_{n}{t_{1} ↦ s_{1}}).

As s̄ is V -linear, s̄_{1} is V -linear. Also, since by the assumption for this case t_{1} ∉ vars(s̄), we have t_{1} ∉ vars(s̄_{1}). Moreover, all occurrences of t_{1} in t̄ are replaced in t̄_{1} by s_{1} so that t_{1} ∉ vars(t̄_{1}). Thus

t_{1} ∉ W_{1} =^{def} vars(s̄_{1}) ∪ vars(t̄_{1}),  (C 9)

so that W_{1} ⊂ W. Let G_{1} =^{def} gvars(s̄_{1} = t̄_{1}) and V_{1} =^{def} Vars \ G_{1}. Note that G_{1} ⊆ G and, by the assumption for this case, t_{1} ∈ V, so that t_{1} ∉ G. As a consequence, G_{1} = G, V_{1} = V and s̄_{1} is V_{1}-linear, so that the inductive hypothesis applies to s̄_{1} and t̄_{1}. Thus, there exists μ_{1} ∈ mgs(s̄_{1} = t̄_{1}) ∈ VSubst such that, for each z ∈ Vars \ vars(s̄_{1}), the three inductive properties hold.

Let μ ⊆ Eqs be defined as

μ =^{def} {t_{1} = s_{1}μ_{1}} ∪ μ_{1}.  (C 10)

We show that μ ∈ VSubst. Note that ν =^{def} {t_{1} ↦ s_{1}} ∈ VSubst and, by (C 9), dom(ν) ∩ vars(μ_{1}) = {t_{1}} ∩ vars(μ_{1}) = ∅. Thus, since μ_{1} ∈ RSubst, by Lemma 40 we obtain μ = μ_{1} ∘ ν ∈ VSubst. Also note that, by Lemma 51, μ ∈ mgs(s̄ = t̄).

Suppose that z ∈ Vars \ vars(s̄). Then either z ≠ t_{1}, so that zμ = zμ_{1}, or z = t_{1}, so that zμ = s_{1}μ_{1}. We show in each case that zμ satisfies the three required properties.

1. Suppose z ≠ t_{1}. By inductive property C 3, zμ_{1} is V_{1}-linear. As zμ = zμ_{1} and V = V_{1}, zμ is V -linear. Otherwise, let z = t_{1}, so that zμ = s_{1}μ_{1}. Consider an arbitrary variable u ∈ vars(s_{1}). Then u ∈ Vars \ vars(s̄_{1}) and the inductive properties using μ_{1} and s̄_{1} can be applied to uμ_{1}. Therefore, by property C 3, uμ_{1} is V_{1}-linear.

Moreover, by property C 5, we have

∀u′ ∈ Vars \ vars(s̄_{1}) : u ≠ u′ ⟹ vars(uμ_{1}) ∩ vars(u′μ_{1}) ⊆ G_{1}.

In particular, this holds for all u′ ∈ vars(s_{1}) such that u ≠ u′. As a consequence, zμ = s_{1}μ_{1} is V_{1}-linear. As V = V_{1}, zμ is V -linear.

2. Suppose z ≠ t_{1}. By property C 4, we have vars(zμ_{1}) ∩ dom(μ_{1}) ⊆ G_{1}. Since zμ = zμ_{1}, G = G_{1}, dom(μ) = dom(μ_{1}) ∪ {t_{1}} and t_{1} ∉ vars(zμ), we obtain vars(zμ) ∩ dom(μ) ⊆ G. Otherwise, let z = t_{1} so that zμ = s_{1}μ_{1}. Consider u ∈ vars(s_{1}). Then u ∈ Vars \vars(s̄_{1}), so that the inductive properties using μ_{1} and s̄_{1} can be applied to uμ_{1}. By property C 4, vars(uμ_{1}) ∩ dom(μ_{1}) ⊆ G_{1}. As this holds for all u ∈ vars(s_{1}), we have vars(s_{1}μ_{1}) ∩ dom(μ_{1}) ⊆ G_{1}. As zμ = s_{1}μ_{1}, G = G_{1}, dom(μ) = dom(μ_{1})∪{t_{1}} and t_{1} ∉ vars(zμ), we obtain vars(zμ)∩dom(μ) ⊆ G.

3. Suppose z ≠ t_{1} and let z′ ∈ Vars \ vars(s̄) be such that z ≠ z′. Then, by inductive property C 5, we have vars(zμ_{1}) ∩ vars(z′μ_{1}) ⊆ G_{1}. Since zμ = zμ_{1} and G = G_{1}, if also z′ ≠ t_{1} (so that z′μ = z′μ_{1}) we obtain vars(zμ) ∩ vars(z′μ) ⊆ G. Otherwise, let z′ = t_{1} (so that z′μ = s_{1}μ_{1}). We will show that

∀u ∈ vars(s_{1}) : vars(zμ_{1}) ∩ vars(uμ_{1}) ⊆ G_{1}.  (C 11)

In fact, in the case that u ∈ G_{1} then vars(uμ_{1}) ⊆ G_{1}. On the other hand, if u ∈ vars(s_{1}) \ G_{1}, then we have u ≠ z. As s̄ is V -linear, u ∈ Vars \ vars(s̄_{1}) so that the property holds by inductive property C 5 (taking z′ = u). As (C 11) holds, we have vars(zμ_{1})∩vars(s_{1}μ_{1}) ⊆ G_{1}. Thus, by observing that zμ = zμ_{1}, z′μ = s_{1}μ_{1} and G = G_{1}, we can conclude vars(zμ) ∩ vars(z′μ) ⊆ G. Otherwise, let z = t_{1} so that zμ = s_{1}μ_{1}. Let z′ ∈ Vars \ vars(s̄) be such that z ≠ z′ (note that this implies z′ ≠ t_{1}, so that z′μ = z′μ_{1}). We will prove that, for all u ∈ vars(s_{1}),

vars(uμ_{1}) ∩ vars(z′μ_{1}) ⊆ G_{1}.  (C 12)

In fact, if u ∈ G_{1} then vars(uμ_{1}) ⊆ G_{1}. Suppose now u ∈ vars(s_{1}) \ G_{1}. As s̄ is V -linear, u ∈ Vars \ vars(s̄_{1}) so that the inductive property C 5 can be applied to uμ_{1}. Thus, for all u′ ∈ Vars \ vars(s̄_{1}), if u ≠ u′ we have vars(uμ_{1})∩vars(u′μ_{1}) ⊆ G_{1}. In particular, since u ∈ vars(s_{1}) and z′ ∉ vars(s̄), we have u ≠ z′ so that, by taking u′ = z′, we obtain (C 12). As the choice of u ∈ vars(s_{1}) is arbitrary, we have vars(s_{1}μ_{1}) ∩ vars(z′μ_{1}) ⊆ G_{1}. By observing that zμ = s_{1}μ_{1}, z′μ = z′μ_{1} and G = G_{1} we obtain vars(zμ) ∩ vars(z′μ) ⊆ G.

For all the proofs of correctness in the next four subsections, as far as possible, we will use the same notation and assume a common set of initial hypotheses. Namely, we will assume that:

d = ⟨sh, f, l⟩ ∈ SFL and σ ∈ γ_{S}(d) ∩ VSubst; y ∈ dom(σ) ∩ range(σ) ⟹ y ∈ vars(yσ); (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI ; r, r′ ∈ HTerms are such that {r, r′} = {x, t}; σ ∪ {x = t} is satisfiable in the syntactic equality theory T .

(C 13)

Let

{u_{1}, …, u_{k}} =^{def} dom(σ) ∩ (vars(xσ) ∪ vars(tσ)),
σ′ =^{def} {u_{i} = u_{i}σ | 1 ≤ i ≤ k},
μ ∈ mgs(σ′ ∪ {rσ = r′σ}) ∩ VSubst,
ν =^{def} σ \ σ′.

(C 14)

As σ ∪ {x = t} is satisfiable, by Lemma 35, mgs(σ′ ∪ {xσ = tσ}) ≠ ∅. Therefore, by Proposition 41, μ is well defined and, by Lemma 39, ν ∈ VSubst. Note also that, since σ ∈ VSubst, we have vars(u_{i}σ) ⊆ vars(xσ) ∪ vars(tσ) for each i = 1, …, k. Therefore, we have

vars(μ) ⊆ vars(xσ) ∪ vars(tσ)  (C 15)

and hence, as dom(ν) = dom(σ) \ (vars(xσ) ∪ vars(tσ)), we have

dom(ν) ∩ vars(μ) = ∅.  (C 16)

Thus we can apply Lemma 40 to obtain ν ∘ μ ∈ VSubst. By applying Lemma 51, we have

ν ∘ μ ∈ mgs(σ ∪ {x = t}) ∩ VSubst.  (C 17)

The following result is used in Subsections C.4 and C.6.

Lemma 56 Let rt(r, σ) ∈ LTerms. Then (u_{1}, …, u_{k}, rσ) is (Vars \ gvars(μ))-linear.

Proof Let s̄ = (u_{1}, …, u_{k}, rσ). Then, for each y ∈ vars(r), rt(y, σ) ∈ LTerms so that, by Proposition 16, y ∈ lvars(σ). It follows that vars(r) ⊆ lvars(σ) and hence, by Proposition 43,

∀v ∈ vars(rσ) \ dom(σ) : occ lin(v, rσ),

vars(rσ) ∩ dom(σ) = gvars(σ).

Therefore s̄ is (Vars \gvars(σ))-linear. Since gvars(σ)∩vars(s̄) ⊆ gvars(μ), we have s̄ is (Vars \ gvars(μ))-linear.

The following result is used in Subsections C.5 and C.6.

Lemma 57 Assume the notation and hypotheses given in (C 13) and (C 14) and let y ∈ lvars(σ)\ gvars(σ). Then y ∈ dom(μ) implies that y ∉ dom(σ).

Proof Suppose y ∈ dom(σ). Then we show that y ∉ dom(μ). Since σ ∈ VSubst and y ∈ lvars(σ), by Proposition 43 we have

vars(yσ) ∩ dom(σ) ⊆ gvars(σ).

Therefore, as y ∉ gvars(σ), y ∉ vars(yσ). and hence, by the definition of σ, y ∉ dom(σ) ∩ range(σ). Thus, by (C 15), y ∉ dom(μ).

In Subsections C.4 and C.7, we use the following subsets of sh.

sh_{x} = rel(vars(x), sh),  sh_{t} = rel(vars(t), sh),
sh_{r} = rel(vars(r), sh), sh_{r′} = rel(vars(r′), sh), (C 18)
sh_{−} = \overline{rel}(\{x\} ∪ vars(t), sh),  sh_{xt} = sh_{x} ∩ sh_{t}.

We also use the corresponding subsets of ssets(σ).

R_{x} = rel(vars(x), ssets(σ)),  R_{t} = rel(vars(t), ssets(σ)),
R_{r} = rel(vars(r), ssets(σ)), R_{r′} = rel(vars(r′), ssets(σ)), (C 19)
R_{−} = \overline{rel}(\{x\} ∪ vars(t), ssets(σ)),  R_{xt} = R_{x} ∩ R_{t}.

C.4 The Correctness for Set-Sharing

Lemma 58 Assume the notation and hypotheses in (C 13), (C 14) and (C 19). Suppose also rt(r, σ) ∈ LTerms, τ = ν ∘ μ, S ∈ ssets(τ), S_{r′} ⊆ S and S_{r′} ∈ R_{r′}^{⋆}. Then S_{r′} ∈ R_{r′} ∪ bin(R_{r′}, R_{xt}^{⋆}).

Proof As S_{r′} ∈ R_{r′}^{⋆}, S_{r′} = S_{1} ∪S_{2} where S_{1} ∈ (R_{r′} \R_{xt})^{⋆} ∪{∅} and S_{2} ∈ R_{xt}^{⋆} ∪{∅}. Note that as S_{r′} ≠ ∅, we cannot have S_{1} = S_{2} = ∅. Suppose first that S_{1} = ∅ so that S_{r′} = S_{2} ≠ ∅. Then S_{r′} ∈ R_{xt}^{⋆}. However, since R_{xt} ⊆ R_{r′}, R_{xt}^{⋆} ⊆ bin(R_{r′}, R_{xt}^{⋆}). Thus S_{r′} ∈ bin(R_{r′}, R_{xt}^{⋆}). Suppose next that S_{1} ≠ ∅. As R_{r′} \ R_{xt} = R_{r′} \ R_{r}, we have S_{1} = ⋃{ occ(σ, w) | w ∈ S_{1} \ (dom(σ) ∪ vars(r′σ)) }. Let w_{1}, w_{2} ∈ S_{r′} \ (dom(σ) ∪ vars(rσ)). Then, it remains to show that w_{1} = w_{2}.

As S_{r′} ⊆ S and S ∈ ssets(τ), by (C 17) and Proposition 43, (vars(w_{1}τ) ∩ vars(w_{2}τ)) \ dom(τ) ≠ ∅. Note that dom(μ) ⊆ dom(τ). and, as w_{i} ∉ dom(σ), we have w_{i}τ = w_{i}μ, for i ∈ {1, 2}. Thus, (vars(w_{1}μ) ∩ vars(w_{2}μ)) \ dom(μ) ≠ ∅. By definition, μ ∈ VSubst so that by Proposition 43,

rel({w_{1}}, ssets(μ)) ∩ rel({w_{2}}, ssets(μ)) ≠ ∅.

By definition, u_{1}, …, u_{k} ∈ dom(σ) so that w_{1}, w_{2} ∉ {u_{1}, …, u_{k}} ∪ vars(rσ). By hypothesis, rt(r, σ) ∈ LTerms. Therefore Lemma 56 can be applied to obtain (u_{1}, …, u_{k}, rσ) is (Vars \ gvars(μ))-linear. Thus, we can apply property (C 2) of Proposition 55. to conclude that w_{1} = w_{2}.

Proposition 59 Assume the notation and hypotheses given in (C 13) and (C 18) and suppose that free_{d}(r) holds. Then, for some τ ∈ mgs(σ ∪ {x = t}),

sh_{−} ∪ bin(sh_{r}, sh_{r′}) ⊇ ssets(τ).  (C 20)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘ μ satisfies (C 20).

Since σ ∈ γ_{S}(d), we have sh ⊇ ssets(σ) so that, using the monotonicity of \overline{rel}, rel, (·)^{⋆} and bin and assuming the notation given in (C 19),

sh_{−} ∪ bin(sh_{r}, sh_{r′}) ⊇ R_{−} ∪ bin(R_{r}, R_{r′}).

Let S be an arbitrary sharing set in ssets(τ). Then, in order to prove (C 20), it is sufficient to show that

S ∈ R_{−} ∪ bin(R_{r}, R_{r′}).  (C 21)

By hypothesis, free_{d}(r) holds so that, by Theorem 21, rt(r, σ) ∈ Vars.

By Definition 49 and Theorem 50, S ∈ R_{−} ∪ bin(R_{r}^{⋆}, R_{r′}^{⋆}). If S ∈ R_{−}, then (C 21) holds trivially. Therefore suppose, for some S_{r} ∈ R_{r}^{⋆} and S_{r′} ∈ R_{r′}^{⋆}, S = S_{r} ∪ S_{r′}. As rt(r, σ) ∈ LTerms, we can apply Lemma 58 to obtainS_{r′} ∈ R_{r′} ∪ bin(R_{r′}, R_{xt}^{⋆}). However, as R_{xt} ⊆ R_{r}, bin(R_{r}^{⋆}, R_{r′} ∪ bin(R_{r′}, R_{xt}^{⋆})) = bin(R_{r}^{⋆}, R_{r′}). Thus S ∈ bin(R_{r}^{⋆}, R_{r′}).

As rt(r, σ) ∈ Vars, by Propositions 16 and 43, rσ ∈ Vars \ dom(σ). Therefore, by Definition 7, R_{r} = {occ(σ, rσ)} so that R_{r}^{⋆} = R_{r}. Thus S ∈ bin(R_{r}, R_{r′}) and (C 21) holds.

Proposition 60 Assume the notation and hypotheses given in (C 13) and (C 18) and suppose that both lin_{d}(x) and lin_{d}(t) hold. Then, for some τ ∈ mgs(σ ∪ {x = t}),

sh_{−} ∪ bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})) ⊇ ssets(τ).  (C 22)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘ μ satisfies (C 22).

Since σ ∈ γ_{S}(d), we have sh ⊇ ssets(σ) so that, using the monotonicity of \overline{rel}, rel, (·)^{⋆} and bin and assuming the notation given in (C 19), we obtain

sh_{−} ∪ bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆}))

⊇ R_{−} ∪ bin(R_{x} ∪ bin(R_{x}, R_{xt}^{⋆}), R_{t} ∪ bin(R_{t}, R_{xt}^{⋆})).

Let S be an arbitrary sharing set in ssets(τ). Then, in order to prove (C 22), it is sufficient to show

S ∈ R_{−} ∪ bin(R_{x} ∪ bin(R_{x}, R_{xt}^{⋆}), R_{t} ∪ bin(R_{t}, R_{xt}^{⋆}))  (C 23)

By Definition 49 and Theorem 50, we have

S ∈ R_{−} ∪ bin(R_{x}^{⋆}, R_{t}^{⋆}).

If S ∈ R_{−}, then (C 23) holds trivially. Therefore suppose S ∈ bin(R_{x}^{⋆}, R_{t}^{⋆}). That is, there are S_{x} ∈ R_{x}^{⋆} and S_{t} ∈ R_{t}^{⋆} such that S = S_{x} ∪ S_{t}. By hypothesis, lin_{d}(x) and lin_{d}(t) hold. Hence, by Theorem 21, rt(x, σ) and rt(t, σ) ∈ LTerms so that we can apply Lemma 58 twice, once with r = x and r′ = t and once with r = t and r′ = x to obtain S_{x} ∈ R_{x} ∪ bin(R_{x}, R_{xt}^{⋆}) and S_{t} ∈ R_{t} ∪ bin(R_{t}, R_{xt}^{⋆}). Thus (C 23) holds.

Proposition 61 Assume the notation and hypotheses given in (C 13) and (C 18) and suppose lin_{d}(r) holds. Then, for some τ ∈ mgs(σ ∪ {x = t}),

sh_{−} ∪ bin(sh_{r}^{⋆}, sh_{r′}) ⊇ ssets(τ).  (C 24)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘ μ satisfies (C 24).

Since σ ∈ γ_{S}(d), we have sh ⊇ ssets(σ) so that, using the monotonicity of \overline{rel}, rel, (·)^{⋆} and bin and assuming the notation given in (C 19), we obtain

sh_{−} ∪ bin(sh_{r}^{⋆}, sh_{r′}) ⊇ R_{−} ∪ bin(R_{r}^{⋆}, R_{r′}).

Let S be an arbitrary sharing set in ssets(τ). Then, in order to prove (C 24) it is sufficient to show that

S ∈ R_{−} ∪ bin(R_{r}^{⋆}, R_{r′}).  (C 25)

By Definition 49 and Theorem 50, we have

S ∈ R_{−} ∪ bin(R_{r}^{⋆}, R_{r′}^{⋆}).

If S ∈ R_{−}, then (C 25) holds trivially. Therefore suppose S ∈ bin(R_{r}^{⋆}, R_{r′}^{⋆}). That is, there are S_{r} ∈ R_{r}^{⋆} and S_{r′} ∈ R_{r′}^{⋆} such that S = S_{r}∪S_{r′}. By hypothesis, lin_{d}(r) holds. Hence, by Theorem 21, rt(r, σ) ∈ LTerms so that we can apply Lemma 58, to obtain S_{r′} ∈ R_{r′} ∪ bin(R_{r′}, R_{xt}^{⋆}). However, as R_{xt} ⊆ R_{r}, bin(R_{r}^{⋆}, R_{r′} ∪ bin(R_{r′}, R_{xt}^{⋆})) = bin(R_{r}^{⋆}, R_{r′}). Thus S ∈ bin(R_{r}^{⋆}, R_{r′}) and (C 25) holds.

To prove the main correctness result for set-sharing in the case that the binding is cyclic, we need the following lemma.

Lemma 62 Let sh ∈ SH and V, W ⊆ VI where rel(V, sh) ⊆ rel(W, sh). Let x ↦ t ∈ Bind where {x} ∪ vars(t) ⊆ VI and sh′ =^{def} amgu(sh, x ↦ t). Then rel(V, sh′) ⊆ rel(W, sh′).

Proof Suppose that S ∈ rel(V, sh′). By Definition 49, we have two cases.

1. Suppose first that S ∈ \overline{rel}(\{x\} ∪ vars(t), sh). Then, S ∈ sh and, in particular, S ∈ rel(V, sh). Thus, by hypothesis, S ∈ rel(W, sh) and we can conclude S ∈ rel(W, sh′).

2. Otherwise, let S ∈ bin(rel({x}, sh)^{⋆}, rel(vars(t), sh)^{⋆}). Then, it holds S = S_{0} ∪ ⋯ ∪ S_{n} where n ∈ ℕ and S_{i} ∈ sh, for each 0 ≤ i ≤ n. Moreover, since S ∈ rel(V, sh′), there exists an index j ∈ {0, …, n} such that S_{j} ∈ rel(V, sh). Hence, by the hypothesis, S_{j} ∈ rel(W, sh) and, since S_{j} ⊆ S, we can conclude S ∈ rel(W, sh′).

Proposition 63 Let sh ∈ SH and τ ∈ RSubst be satisfiable in T and suppose that T ⊢ ∀(τ → x = t) and ssets(τ) ⊆ sh. Then ssets(τ) ⊆ cyclic_{x}^{t}(sh).

Proof Take V_{x} = {x} and W_{t} = vars(t) \ {x}. Let τ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}, where n = #τ. Define

τ_{0} =^{def} {x ↦ t},  sh_{0} =^{def} ssets({x ↦ t}),

and, for each i = 1, …, n,

τ_{i} ∈ mgs({x_{1} = t_{1}, …, x_{i} = t_{i}} ∪ {x = t}), sh_{i} =^{def} amgu(sh_{i−1}, x_{i} ↦ t_{i}).

We show by induction on i = 0, …, n that ssets(τ_{i}) ⊆ sh_{i} and

rel(V_{x}, sh_{i}) ⊆ rel(W_{t}, sh_{i}).  (C 26)

The base case, when i = 0, follows directly from Definition 7; note that (C 26) holds because x ∈ dom(τ_{0}), so that occ(τ_{0}, x) = ∅.

Consider the inductive case, when 0 < i ≤ n. By the inductive hypothesis, ssets(τ_{i−1}) ⊆ sh_{i−1} so that, by Theorem 50, ssets(τ_{i}) ⊆ sh_{i}. By the inductive hypothesis, (C 26) holds for sh_{i−1}. Thus, by Lemma 62 (taking V = V_{x} and W = W_{t}), we obtain that (C 26) also holds for sh_{i}.

By taking i = n, we obtain rel(V_{x}, sh_{n}) ⊆ rel(W_{t}, sh_{n}). Note that, by hypothesis, we have τ ∈ mgs(τ ∪ {x = t}) = mgs(τ_{n}), so that T ⊢ ∀(τ ↔ τ_{n}). By Lemma 54, we have ssets(τ) = ssets(τ_{n}), so that ssets(τ) ⊆ sh_{n}. As a consequence, ssets(τ) ⊆ sh ∩ sh_{n}. Thus, by Definition 20, we obtain ssets(τ) ⊆ cyclic_{x}^{t}(sh).

C.5 The Correctness for Freeness

Lemma 64 Assume the notation and definitions given in (C 13) and (C 14) and suppose τ = ν∘μ and y ∈ fvars(σ) be such that yσ ∈ fvars(μ). Then y ∈ fvars(τ).

Proof If y ∉ dom(τ), then y ∈ fvars(τ). Suppose now that y ∈ dom(τ). By hypothesis, y ∈ fvars(σ) so that y ∈ lvars(σ) \ gvars(σ) and Lemma 57 applies. Thus, if y ∈ dom(μ), y ∉ dom(σ) and hence yτ = yσμ. In addition, as ν ⊆ σ, if y ∈ dom(ν), then again yτ = yσμ.

As yσ ∈ fvars(μ) and μ ∈ VSubst, by Proposition 43, yσμ ∈ Vars \ dom(μ). If yσ ∈ dom(μ), then yσμ ∈ vars(μ), so that, by (C 16), yσμ ∉ dom(ν). On the other hand, if yσ ∉ dom(μ), then yσμ ∉ dom(μ). Thus, in both cases, yσμ ∈ Vars \ (dom(σ)∪dom(μ)) and hence, as dom(τ) ⊆ dom(σ)∪dom(μ), yσμ ∈ Vars \dom(τ). Since, by (C 17), τ ∈ VSubst, we can apply Proposition 43 to obtain y ∈ fvars(τ) as required.

Proposition 65 Assume the notation and hypotheses given in (C 13) and suppose {x, t} ⊆ fvars(σ). Then, for some τ ∈ mgs(σ ∪ {x = t}), we have

fvars(σ) ⊆ fvars(τ).  (C 27)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘μ satisfies (C 27). Suppose y ∈ fvars(σ). As {x, t} ⊆ fvars(σ) we have, using Proposition 43, {xσ, tσ} ⊆ Vars \ dom(σ). Thus μ ∈ mgs({xσ = tσ}) ∩ VSubst. As a single binding is in VSubst, we can assume that either xσ ≠ tσ and μ = {xσ ↦ tσ} or μ = ∅. In both cases, fvars(μ) = Vars so that yσ ∈ fvars(μ). Therefore Lemma 64 can be applied to give y ∈ fvars(τ).

The following simple consequence of Proposition 43 will be used to complete the proofs of correctness for the freeness component.

Lemma 66 Suppose y ∈ VI and s ∈ HTerms are such that vars(s) ⊆ VI . Suppose also that y ∉ share with_{d}(s). Then vars(yσ) ∩ vars(sσ) ⊆ dom(σ).

Proof Let V = vars(s) so that, by Definition 20, y ∉ vars(rel(V, sh)). Thus

∀w ∈ V, S ∈ sh : {y, w} ⊈ S.

By Definition 18, since σ ∈ γ_{S}(d), this implies

∀v ∈ Vars, w ∈ V : {y, w} ⊈ occ(σ, v).

Thus, since σ ∈ VSubst, by Proposition 43 we obtain

∀w ∈ V : vars(yσ) ∩ vars(wσ) ⊆ dom(σ),

which is equivalent to the thesis.

Proposition 67 Assume the notation and hypotheses given in (C 13) and suppose that x ∈ fvars(σ). Then, for some τ ∈ mgs(σ ∪ {x = t}), we have

fvars(σ) \ share with_{d}(x) ⊆ fvars(τ).  (C 28)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘ μ satisfies (C 28). If xσ = tσ, then t ∈ fvars(σ) and the result follows from Proposition 65. Suppose next that xσ ≠ tσ and that y ∈ fvars(σ) \ share with_{d}(x). We prove that y ∈ fvars(τ). First we show that yσ ∈ fvars(μ).

As x ∈ fvars(σ) and σ ∈ VSubst, by Proposition 43, xσ ∈ Vars \ dom(σ). Thus μ′ =^{def} σ′ ∪ {xσ = tσ} has no identities or circular subsets so that μ′ ∈ RSubst. We show that yσ ∈ fvars(μ′). Moreover, σ ∈ VSubst, so that, by Proposition 43, yσ ∉ dom(σ). However, since y ∉ share with_{d}(x) and σ ∈ VSubst, we can apply Lemma 66 to give vars(yσ) ∩ vars(xσ) ⊆ dom(σ). Therefore yσ ≠ xσ and hence yσ ∉ dom(σ)∪{xσ}. Thus yσ ∉ dom(μ′) so that yσ ∈ fvars(μ′). By Proposition 54, we have yσ ∈ fvars(μ).

Therefore Lemma 64 can be applied to give y ∈ fvars(τ).

Proposition 68 Assume the notation and hypotheses given in (C 13). Therefore we have, for some τ ∈ mgs(σ ∪ {x = t}),

fvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t)) ⊆ fvars(τ).  (C 29)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘μ satisfies (C 29). Suppose y ∈ fvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t)). Then we need to show that y ∈ fvars(τ).

As y ∈ fvars(σ), we have y ∈ Vars and yσ ∈ Vars. Moreover, as

y ∉ share with_{d}(x) ∪ share with_{d}(t),

we can apply Lemma 66 to obtain

vars(yσ) ∩ (vars(xσ) ∪ vars(tσ)) ⊆ dom(σ)

so that, by (C 15), yσ ∉ vars(μ). It follows that yσ ∈ fvars(μ). Therefore Lemma 64 can be applied to give y ∈ fvars(τ) as required.

C.6 The Correctness for Linearity

Lemma 69 Assume the notation and definitions given in (C 13) and (C 14). Suppose also that τ = ν ∘ μ, W ⊆ lvars(μ) and y ∈ lvars(σ) ∩ W where vars(yσ) \ W ⊆ gvars(σ) and, for all w, w′ ∈ W such that w ≠ w′, we have vars(wμ)∩vars(w′μ) ⊆ gvars(μ). Then y ∈ lvars(τ).

Proof By Lemma 53, we have gvars(σ) ⊆ gvars(τ) and gvars(μ) ⊆ gvars(τ).

If y ∉ dom(τ) then y ∈ fvars(τ). Also, if y ∈ gvars(σ) then y ∈ gvars(τ). Thus, in both cases, by Corollary 17, y ∈ lvars(τ). Therefore, for the rest of the proof, we assume y ∈ dom(τ) \ gvars(σ).

By Lemma 57, if y ∈ dom(μ) then y ∉ dom(σ). Thus, as ν ⊆ σ, we have

yτ = yσμ.  (C 30)

By definition μ ∈ VSubst. Thus, by Proposition 43, for all w ∈ lvars(μ) (and hence, for all w ∈ W),

∀v ∈ vars(wμ) \ dom(μ) : occ lin(v, wμ),  (C 31)
vars(wμ) ∩ dom(μ) ⊆ gvars(μ).  (C 32)

By definition, σ ∈ VSubst. Thus, as y ∈ lvars(σ), by Proposition 43,

∀v ∈ vars(yσ) \ dom(σ) : occ lin(v, yσ),  (C 33)

vars(yσ) ∩ dom(σ) ⊆ gvars(σ).  (C 34)

By (C 17), τ ∈ VSubst. Thus, by Proposition 43, to prove y ∈ lvars(τ), we just need to show that

∀v ∈ vars(yτ) \ dom(τ) : occ lin(v, yτ),  (C 35)
vars(yτ) ∩ dom(τ) ⊆ gvars(τ).  (C 36)

Let w ∈ vars(yσ). Then, it follows from (C 30) that to prove (C 35) and (C 36), we need to prove:

vars(wμ) ∩ dom(τ) ⊆ gvars(τ),  (C 37)
∀v ∈ vars(wμ) \ gvars(τ) : occ lin(v, wμ),  (C 38)
∀w′ ∈ vars(yσ) \ {w} : vars(wμ) ∩ vars(w′μ) ⊆ gvars(τ).  (C 39)

We first prove (C 37) and (C 38) hold. Suppose w ∈ vars(yσ) \ W. Then, by hypothesis, w ∈ gvars(σ) and hence, w ∈ gvars(τ). Thus, as T ⊢ ∀(τ → μ), by Lemma 35, Lemma 36 and Proposition 16, vars(wμ) ⊆ gvars(τ). Thus (C 37) and (C 38) hold. Suppose now that w ∈ vars(yσ) ∩ W so that (C 31) and (C 32) hold. Thus, as dom(μ) ⊆ dom(τ) and gvars(μ) ⊆ gvars(τ), both (C 37) and (C 38) hold.

We now prove (C 39) holds. Suppose w′ ∈ vars(yσ). If w, w′ ∉ dom(τ). Then w, w′ ∉ dom(μ) so that vars(wμ) ∩ vars(w′μ) = {w} ∩ {w′} = ∅. If w ∈ dom(τ), then, by (C 37), vars(wμ) ⊆ gvars(τ). Similarly, if w′ ∈ dom(τ), then, by (C 37) where w is replaced by w′, vars(w′μ) ⊆ gvars(τ). Thus, in all cases (C 39) holds.

Proposition 70 Assume the notation and hypotheses given in (C 13) and suppose lin_{d}(r) holds. Then, for some τ ∈ mgs(σ ∪ {x = t}),

lvars(σ) \ share with_{d}(r) ⊆ lvars(τ).  (C 40)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘μ satisfies (C 40). To prove this, we assume that y ∈ lvars(σ) \ share with_{d}(r) and show that y ∈ lvars(τ).

Let s̄ =^{def} (u_{1}, …, u_{k}, rσ). We will show that the hypothesis of Lemma 69 holds where W = Vars \ vars(s̄)

As y ∈ lvars(σ), by Proposition 43, vars(yσ) ∩ dom(σ) ⊆ gvars(σ). As y ∉ share with_{d}(r), by Definition 20 and Theorem 21, we have y ∉ vars(rσ) and vars(yσ) ∩ vars(rσ) ⊆ gvars(σ), so that, we obtain vars(yσ) \ W ⊆ gvars(σ). As y ∉ vars(rσ) and {u_{1}, …, u_{k}} ⊆ dom(σ), we also have y ∉ vars(s̄) and hence, y ∈ W.

Since lin_{d}(r) holds, by Theorem 21, rt(r, σ) ∈ LTerms so that, by Lemma 56, s̄ is (Vars \ gvars(μ))-linear. We can thus apply Proposition 55 to obtain W ⊆ lvars(μ) and for all w, w′ ∈ W where w ≠ w′, rel({w}, ssets(μ)) ∩ rel({w′}, ssets(μ)) = ∅. By Proposition 43, as μ ∈ VSubst, we have, for all w, w′ ∈ W where w ≠ w′, vars(wμ) ∩ vars(w′μ) ⊆ gvars(μ). Thus we can apply Lemma 69, and obtain y ∈ lvars(τ).

Proposition 71 Assume the notation and hypotheses given in (C 13) and suppose lin_{d}(x) and lin_{d}(t) hold. Then, for some τ ∈ mgs(σ ∪ {x = t}),

lvars(σ) \ (share with_{d}(x) ∩ share with_{d}(t)) ⊆ lvars(τ).

Proof By applying Proposition 70 twice, the first time taking r = x and the second time taking r = t, we can conclude that

lvars(σ) \ (share with_{d}(x) ∩ share with_{d}(t)) ⊆ (lvars(σ) \ share with_{d}(x)) ∪ (lvars(σ) \ share with_{d}(t)) ⊆ lvars(τ).

Proposition 72 Assume the notation and hypotheses given in (C 13). Then, for some τ ∈ mgs(σ ∪ {x = t}), we have

lvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t)) ⊆ lvars(τ).  (C 41)

Proof Assuming the definitions in (C 14), we show that τ =^{def} ν ∘ μ satisfies (C 41). To prove this, we assume that y ∈ lvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t)) and show that y ∈ lvars(τ).

We will show that the hypothesis of Lemma 69 holds where

W = Vars \ (vars(xσ) ∪ vars(tσ)).

As y ∉ share with_{d}(x) ∪ share with_{d}(t), by Definition 20 and Theorem 21, y ∉ vars(xσ) ∪ vars(tσ) and also vars(yσ) ∩ (vars(xσ) ∪ vars(tσ)) ⊆ gvars(σ). Thus we can apply Lemma 69, to obtain y ∈ lvars(τ).

C.7 Putting Results Together

By exploiting the correctness results regarding each of the three components of the domain SFL, we now prove the correctness of the amgu_{S} operator. We start by proving a restricted result that only applies to variable-idempotent substitutions.

Lemma 73 Assume the notation and hypotheses given in (C 13). Suppose τ ∈ mgs(σ∪{x = t}). Then τ ∈ γ_{S}(amgu_{S}(d, x ↦ t)).

Proof Let d′ = ⟨sh′, f′, l′⟩ =^{def} amgu_{S}(d, x ↦ t). It follows from Definition 18 that to prove τ ∈ γ_{S}(d′), we have to show that

ssets(τ) ⊆ sh′,  (C 42)

fvars(τ) ⊇ f′,  (C 43)
lvars(τ) ⊇ l′.  (C 44)

We prove, for each component of d′ separately, that there exists τ ∈ mgs(σ ∪ {x = t}) such that (C 42), (C 43) and (C 44) hold. By Lemma 54 the same inclusions hold for any τ ∈ mgs(σ ∪ {x = t}) so that we have the thesis.

(C 42). By Definition 22, we have sh′ = cyclic_{x}^{t}(sh_{−} ∪ sh′′) where

sh′′ =^{def} \begin{cases}bin(sh_{x}, sh_{t}), & if free_{d}(x) ∨ free_{d}(t); \\ bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), \\ sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})), & if lin_{d}(x) ∧ lin_{d}(t); \\ bin(sh_{x}^{⋆}, sh_{t}), & if lin_{d}(x); \\ bin(sh_{x}, sh_{t}^{⋆}), & if lin_{d}(t); \\ bin(sh_{x}^{⋆}, sh_{t}^{⋆}), & otherwise. \end{cases}

It follows from Definition 18 and the hypothesis σ ∈ γ_{S}(d) that ssets(σ) ⊆ sh. Therefore we apply Proposition 59 (when free_{d}(x) ∨ free_{d}(t) holds), Proposition 60 (when lin_{d}(x) ∧ lin_{d}(t) holds), Proposition 61 (when lin_{d}(x) or lin_{d}(t) holds) or Theorem 50 (when nothing is known about x or t) to conclude that ssets(τ) ⊆ sh_{−} ∪ sh′′. The thesis now follows from Proposition 63.

(C 43). It follows from Definition 18 and the hypothesis σ ∈ γ_{S}(d) that f ⊆ fvars(σ). Therefore we can apply Proposition 65 (when free_{d}(x) ∧ free_{d}(t) holds), Proposition 67 (when free_{d}(x) or free_{d}(t) holds) or Proposition 68 (when nothing is known about x or t) to conclude that fvars(τ) ⊇ f′.

(C 44). It follows from Definition 18 and the hypothesis σ ∈ γ_{S}(d) that l ⊆ fvars(σ). Therefore we can apply Proposition 71 (when lin_{d}(x) ∧ lin_{d}(t) holds), Proposition 70 (when lin_{d}(x) or lin_{d}(t) holds) or Proposition 72 (when nothing is known about x or t) to conclude that

lvars(τ) ⊇ l′′.

By (C 42) proved above, ssets(τ) ⊆ sh′. By Definition 9, VI \ vars(sh′) ⊆ gvars(τ). Moreover, by (C 43) proved above, we have fvars(τ) ⊇ f′. Thus, by applying Corollary 17 we obtain the thesis:

lvars(τ) ⊇ gvars(τ) ∪ fvars(τ) ∪ lvars(τ)
⊇ (VI \ vars(sh′)) ∪ f′ ∪ l′′
= l′.

Finally, by exploiting the results of Subsection 3.1, we drop the assumption about variable-idempotent substitutions.

Proof of Theorem 23 on page 15. Let d′ = amgu_{S}(d, x ↦ t).

If d = ⊥_{S} then we have d′ = ⊥_{S} and the result holds trivially, since γ_{S}(d) = ∅. Similarly, if T = FT is the theory of finite trees and x ∈ vars(t), then d′ = ⊥_{S}.

Again, the result holds trivially, since the equation {x = t} is not satisfiable in FT , so that mgs(σ ∪ {x = t}) = ∅.

Therefore suppose there exists σ ∈ γ_{S}(d) and τ ∈ mgs(σ ∪ {x = t}). By Proposition 41, there exists σ′ ∈ VSubst such that T ⊢ ∀(σ ↔ σ′) and y ∈ dom(σ′) ∩ range(σ′) implies y ∈ vars(yσ′). By Corollary 19 and Definition 18, we have σ ∈ γ_{S}(d) if and only if σ′ ∈ γ_{S}(d). Therefore, the result follows by application of Lemma 73.

D Proofs of the Results of Section 4

We will use results from (Bagnara et al. 2002, Zaffanella et al. 2002), that show that the domain PSD is the weakest abstraction of SH achieving the same precision for the computation of groundness and pair-sharing.

Theorem 74 (Zaffanella et al. 2002, Theorem 3). Let sh_{1}, sh_{2} ∈ SH be such that ρ_{PSD}(sh_{1}) = ρ_{PSD}(sh_{2}). Then, for each σ ∈ RSubst and V ⊆ VI ,

ρ_{PSD}(aunify(sh_{1}, σ)) = ρ_{PSD}(aunify(sh_{2}, σ)),  (D 1)
ρ_{PSD}(aexists(sh_{1}, V)) = ρ_{PSD}(aexists(sh_{2}, V)).  (D 2)

Theorem 75 (Zaffanella et al. 2002, Theorem 4). Let sh_{1}, sh_{2} ∈ SH be such that ρ_{PSD}(sh_{1}) ≠ ρ_{PSD}(sh_{2}). Then there exist σ ∈ RSubst and ρ ∈ {ρ_{Con}, ρ_{PS}} such that

ρ(aunify(sh_{1}, σ)) ≠ ρ(aunify(sh_{2}, σ)).  (D 3)

The following result in (Bagnara et al. 2002) shows that, for groundness and pair-sharing information, the exponential star-union operator can be replaced by a quadratic operation without loss of precision.

Theorem 76 (Bagnara et al. 2002, Theorem 15). Let sh ∈ SH and (x ↦ t) ∈ Bind. Let also

sh_{−} =^{def} \overline{rel}(\{x\} ∪ vars(t), sh), sh_{x} =^{def} rel(\{x\}, sh), sh_{t} =^{def} rel(vars(t), sh).

Then

ρ_{PSD}(amgu(sh, x ↦ t)) = ρ_{PSD}(sh_{−} ∪ bin(sh_{x}^{2}, sh_{t}^{2})).

The next three lemmas show that the precision of the abstract evaluation of the operators specified in Definition 20 is not affected by ρ_{PSD}.

Lemma 77 Let V ⊆ VI and sh ∈ SH . Then

vars(rel(V, sh)) = vars(rel(V, ρ_{PSD}(sh))).

Proof If V = ∅, the result is trivial. Thus, assume V ≠ ∅.

The first inclusion (⊆) follows from the extensivity of ρ_{PSD} and the monotonicity of the operators rel and vars. To prove the other inclusion, let S ∈ rel(V, ρ_{PSD}(sh)). By Definition 5, we have

∀x ∈ S : S = ⋃{ T ∈ sh | {x} ⊆ T ⊆ S }.

In particular, for all x ∈ S ∩ V, it holds

S = ⋃{ T ∈ sh | {x} ⊆ T ⊆ S }
= ⋃{ T ∈ rel(V, sh) | {x} ⊆ T ⊆ S }
⊆ ⋃ rel(V, sh)
= vars(rel(V, sh)).

Since the choice of S was arbitrary, we obtain the desired inclusion

vars(rel(V, sh)) ⊇ vars(rel(V, ρ_{PSD}(sh))).

Lemma 78 Let V, W ⊆ VI and sh ∈ SH . Then

(rel(V, sh) ∩ rel(W, sh) = ∅) ⟺ (rel(V, ρ_{PSD}(sh)) ∩ rel(W, ρ_{PSD}(sh)) = ∅).

Proof To prove the implication (⇒), we reason by contraposition and suppose

rel(V, ρ_{PSD}(sh)) ∩ rel(W, ρ_{PSD}(sh)) ≠ ∅.

Thus, there exists S ∈ ρ_{PSD}(sh) such that S ∩ V ≠ ∅ and S ∩ W ≠ ∅. Consider x ∈ S ∩ V and y ∈ S ∩ W, so that we have {x, y} ⊆ S.

By Definition 5, we have

∀v ∈ S : S = ⋃{ T ∈ sh | {v} ⊆ T ⊆ S }.

In particular, by taking v = x, there must exist a sharing group T ∈ sh such that {x, y} ⊆ T, so that

T ∈ rel(V, sh) ∩ rel(W, sh) ≠ ∅.

The other implication (⇐) follows by the extensivity of ρ_{PSD} and the monotonicity of rel.

Lemma 79 For each i ∈ {1, 2}, let d_{i} = ⟨sh_{i}, f, l⟩ ∈ SFL and suppose that ρ_{PSD}(sh_{1}) = ρ_{PSD}(sh_{2}). Then, for all s, t ∈ HTerms and y ∈ VI ,

ind_{d_{1}}(s, t) ⟺ ind_{d_{2}}(s, t);  (D 4)
free_{d_{1}}(t) ⟺ free_{d_{2}}(t);  (D 5)
ground_{d_{1}}(t) ⟺ ground_{d_{2}}(t);  (D 6)

occ lin_{d_{1}}(y, t) ⟺ occ lin_{d_{2}}(y, t);  (D 7)
lin_{d_{1}}(t) ⟺ lin_{d_{2}}(t);  (D 8)
share with_{d_{1}}(t) = share with_{d_{2}}(t).  (D 9)

Proof (D 4). Let V = vars(s), W = vars(t). By Definition 20, Lemma 78 and the hypothesis, we obtain

ind_{d_{1}}(s, t) ⟺ rel(V, sh_{1}) ∩ rel(W, sh_{1}) ≠ ∅
⟺ rel(V, ρ_{PSD}(sh_{1})) ∩ rel(W, ρ_{PSD}(sh_{1})) ≠ ∅
⟺ rel(V, ρ_{PSD}(sh_{2})) ∩ rel(W, ρ_{PSD}(sh_{2})) ≠ ∅
⟺ rel(V, sh_{2}) ∩ rel(W, sh_{2}) ≠ ∅
⟺ ind_{d_{2}}(s, t).

(D 5). This follows from Definition 20, since the predicate free_{d_{i}}(t) does not depend on the sharing component sh_{i} of d_{i}.

(D 6). By applying Lemma 77 with V = VI , we have that, for i ∈ {1, 2}, vars(sh_{i}) = vars(ρ_{PSD}(sh_{i})). Thus, by the hypothesis, vars(sh_{1}) = vars(sh_{2}). Therefore, by Definition 20, equivalence (D 6) holds.

(D 7). This follows from Definition 20 and equivalences (D 4) and (D 6).

(D 8). This follows from Definition 20 and equivalence (D 7).

(D 9). By applying Lemma 77 with V = vars(t), we have that, for i ∈ {1, 2},

vars(rel(V, sh_{i})) = vars(rel(V, ρ_{PSD}(sh_{i}))).

Thus, by the hypothesis, vars(rel(V, sh_{1})) = vars(rel(V, sh_{2})). Therefore, by Definition 20, equation (D 9) holds.

Since both ρ_{PSD} (by (Hill et al. 2002, Theorem 7)) and (·)^{⋆} are upper closure operators it follows that

sh_{1} ⊆ ρ_{PSD}(sh_{2}) ⟺ ρ_{PSD}(sh_{1}) ⊆ ρ_{PSD}(sh_{2}),  (D 10)
sh_{1} ⊆ sh_{2}^{⋆} ⟺ sh_{1}^{⋆} ⊆ sh_{2}^{⋆}.  (D 11)

We next establish a number of results needed to show that the precision of the abstract operator amgu_{S} specified in Definition 22 is not affected by ρ_{PSD} (see Theorem 85).

Lemma 80 (Bagnara et al. 2002, Lemma 18). For each sh ∈ SH and V ⊆ VI ,

\overline{rel}(V, ρ_{PSD}(sh)) = ρ_{PSD}(\overline{rel}(V, sh)).

Lemma 81 (Bagnara et al. 2002, Lemma 19). For each sh_{1}, sh_{2} ∈ SH and V ⊆ VI ,

sh_{1} ⊆ ρ_{PSD}(sh_{2}) ⟹ rel(V, sh_{1})^{⋆} ⊆ rel(V, sh_{2})^{⋆}.

Let sh_{1}, sh_{2} ∈ SH be such that sh_{1} ⊆ ρ_{PSD}(sh_{2}). Let also V, W ⊆ VI and, for each i ∈ {1, 2},

sh_{−,i} = \overline{rel}(V ∪ W, sh_{i}),  sh_{x,i} = rel(V, sh_{i}),  sh_{t,i} = rel(W, sh_{i}).

Then, we have

bin(sh_{x,1}, sh_{t,1}) ⊆ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}));  (D 12)
bin(sh_{x,1}, sh_{t,1}^{⋆}) ⊆ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}^{⋆})).  (D 13)

Proof (D 12). Let S = S_{x} ∪ S_{t} ∈ bin(sh_{x,1}, sh_{t,1}) where S_{x} ∈ sh_{x,1} and S_{t} ∈ sh_{t,1}. We show that, for any y ∈ S,

S = ⋃{ S′ ∈ sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}) | {y} ⊆ S′ ⊆ S }.  (D 14)

Suppose first that y ∈ S_{x}. Let

sh_{y} =^{def} {S′ ∈ sh_{2} | {y} ⊆ S′ ⊆ S},
sh′_{t} =^{def} { S′ ∈ sh_{2} | ∃w ∈ W . {w} ⊆ S′ ⊆ S }.

Since S_{x} ∈ sh_{x,1} and S_{t} ∈ sh_{t,1}, by hypothesis, S_{x}, S_{t} ∈ ρ_{PSD}(sh_{2}). Thus, by Definition 5, S_{x} ⊆ ⋃ sh_{y} ⊆ S and S_{t} ⊆ ⋃ sh′_{t} ⊆ S. As a consequence, S = ⋃(sh_{y}∪sh′_{t}). By the definition of sh′_{t}, we have sh′_{t} = {S′ ∈ sh_{t,2} | S′ ⊆ S}, so that (sh_{y} ∩sh_{t,2}) ⊆ sh′_{t} and hence,

S = ⋃((sh_{y} ∩ sh_{−,2}) ∪ (sh_{y} ∩ sh_{x,2}) ∪ sh′_{t}).

Since S_{x}, S_{t} ≠ ∅, it follows that sh′_{t} ≠ ∅ and sh_{y} ∩ sh_{x,2} ≠ ∅. As a consequence, ⋃((sh_{y} ∩ sh_{x,2}) ∪ sh′_{t}) = ⋃(bin(sh_{y} ∩ sh_{x,2}, sh′_{t})) so that we have

S = ⋃((sh_{y} ∩ sh_{−,2}) ∪ bin(sh_{y} ∩ sh_{x,2}, sh′_{t})).

Moreover, by definition of sh_{y}, for all S′ ∈ (sh_{y} ∩ sh_{−,2}) ∪ bin(sh_{y} ∩ sh_{x,2}, sh′_{t}), we have y ∈ S′. Hence (D 14) holds for all y ∈ S_{x}.

By a symmetric argument, (D 14) holds for all y ∈ S_{t}. Thus (D 14) holds for all y ∈ S. Therefore, by Definition 5,

S ∈ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2})).

(D 13). Let S = S_{x} ∪ T_{t} ∈ bin(sh_{x,1}, sh_{t,1}^{⋆}) where S_{x} ∈ sh_{x,1} and T_{t} ∈ sh_{t,1}^{⋆}. Thus, by hypothesis, S_{x} ∈ ρ_{PSD}(sh_{2}) and, by Lemma 81, T_{t} ∈ sh_{t,2}^{⋆}. We show that, for any y ∈ S,

S = ⋃{ S′ ∈ sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}^{⋆}) | {y} ⊆ S′ ⊆ S }.  (D 15)

We first consider the case that y ∈ S_{x}. Let

sh_{y} =^{def} {S′ ∈ sh_{2} | {y} ⊆ S′ ⊆ S},
sh′_{t} =^{def} {S′ ∈ sh_{t,2}^{⋆} | S′ ⊆ S}.

By Definition 5, as S_{x} ∈ ρ_{PSD}(sh_{2}), S_{x} ⊆ ⋃ sh_{y} ⊆ S. Also, as T_{t} ∈ sh_{t,2}^{⋆}, T_{t} ⊆ ⋃ sh′_{t} ⊆ S. As a consequence, S = ⋃(sh_{y}∪sh′_{t}). However, we also have (sh_{y}∩sh_{t,2}) ⊆ sh′_{t} so that

S = ⋃((sh_{y} ∩ sh_{−,2}) ∪ (sh_{y} ∩ sh_{x,2}) ∪ sh′_{t}).

Since S_{x}, T_{t} ≠ ∅, it follows that sh′_{t} ≠ ∅ and sh_{y} ∩ sh_{x,2} ≠ ∅. As a consequence, ⋃((sh_{y} ∩ sh_{x,2}) ∪ sh′_{t}) = ⋃(bin(sh_{y} ∩ sh_{x,2}, sh′_{t})). Therefore

S = ⋃((sh_{y} ∩ sh_{−,2}) ∪ bin(sh_{y} ∩ sh_{x,2}, sh′_{t})).

Moreover, by definition of sh_{y}, for all S′ ∈ (sh_{y} ∩ sh_{−,2}) ∪ bin(sh_{y} ∩ sh_{x,2}, sh′_{t}), we have y ∈ S′. Hence (D 15) holds for all y ∈ S_{x}.

Secondly, consider the case y ∈ T_{t}. As T_{t} ∈ sh_{t,2}^{⋆}, there exists R ⊆ T_{t} such that y ∈ R and R ∈ sh_{t,2}. Let

sh_{y} =^{def} {S′ ∈ sh_{t,2}^{⋆} | R ⊆ S′ ⊆ S},
sh′_{x} =^{def} { S′ ∈ sh_{2} | ∃v ∈ V . {v} ⊆ S′ ⊆ S }.

Then T_{t} ⊆ ⋃ sh_{y} ⊆ S. By Definition 5, as S_{x} ∈ ρ_{PSD}(sh_{2}), S_{x} ⊆ ⋃ sh′_{x} ⊆ S and hence S = ⋃(sh′_{x} ∪ sh_{y}). Since S_{x}, T_{t} ≠ ∅, ⋃(sh′_{x} ∪ sh_{y}) = ⋃ bin(sh′_{x}, sh_{y}). Therefore S = ⋃ bin(sh′_{x}, sh_{y}). Moreover, for all S′ ∈ bin(sh′_{x}, sh_{y}), we have y ∈ S′. Hence, as sh′_{x} ⊆ sh_{x,2} and sh_{y} ⊆ sh_{t,2}^{⋆}, (D 15) holds for all y ∈ T_{t}.

Therefore, (D 15) holds for all y ∈ S. Thus, by Definition 5,

S ∈ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}^{⋆})).

Lemma 83 Let sh_{x}, sh_{t}, sh_{xt}, sh^{⋄} ∈ SH , where sh_{xt} = sh_{x} ∩ sh_{t} and

sh^{⋄} = bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})).

Then ρ_{PSD}(sh^{⋄}) = ρ_{PSD}(bin(sh_{x}, sh_{t})).

Proof Observe that

bin(bin(sh_{x}, sh_{xt}^{⋆}), bin(sh_{t}, sh_{xt}^{⋆})) = bin(bin(sh_{x}, sh_{t}), sh_{xt}^{⋆}).

Thus

sh^{⋄} = bin(sh_{x}, sh_{t}) ∪ bin(bin(sh_{x}, sh_{t}), sh_{xt}^{⋆}).  (D 16)

Thus, the inclusion ρ_{PSD}(sh^{⋄}) ⊇ ρ_{PSD}(bin(sh_{x}, sh_{t})) follows by the monotonicity of ρ_{PSD}. We now prove the other inclusion

ρ_{PSD}(sh^{⋄}) ⊆ ρ_{PSD}(bin(sh_{x}, sh_{t})).  (D 17)

Let S ∈ sh^{⋄}. Then, by (D 16), S = S_{x} ∪ S_{t} ∪ T_{xt}, where S_{x} ∈ sh_{x}, S_{t} ∈ sh_{t} and T_{xt} ∈ sh_{xt}^{⋆} ∪ ∅. Thus, for some k ≥ 0, T_{xt} = T_{1} ∪ ⋯ ∪ T_{k}, where T_{i} ∈ sh_{xt} for each i = 1, …, k. Thus we have

S = (S_{x} ∪ S_{t}) ∪ (T_{1} ∪ S_{x}) ∪ ⋯ ∪ (T_{k} ∪ S_{x}),  (D 18)

S = (S_{x} ∪ S_{t}) ∪ (T_{1} ∪ S_{t}) ∪ ⋯ ∪ (T_{k} ∪ S_{t}),  (D 19)

and, for all j ∈ {1, …, k},

S = (S_{x} ∪ T_{j}) ∪ (S_{t} ∪ T_{j}) ∪ (T_{1} ∪ T_{j}) ∪ ⋯ ∪ (T_{k} ∪ T_{j}).  (D 20)

Consider an arbitrary variable y ∈ S. We will show that

S = ⋃{ S′ ∈ bin(sh_{x}, sh_{t}) | {y} ⊆ S′ ⊆ S }.  (D 21)

If y ∈ S_{x}, then (D 21) follows from (D 18). Similarly, if y ∈ S_{t}, then (D 21) follows from (D 19). Finally, if y ∉ S_{x} ∪ S_{t}, then k > 0 and there exists j ∈ {1, …, k} such that y ∈ T_{j}. Thus, as T_{j} ∈ sh_{xt}, (D 21) follows from (D 20).

As (D 21) holds for any y ∈ S, by Definition 5, S ∈ ρ_{PSD}(bin(sh_{x}, sh_{t})). Thus, by monotonicity and idempotence of ρ_{PSD}, (D 17) holds.

Lemma 84 Let sh ∈ SH and (x ↦ t) ∈ Bind where {x} ∪ vars(t) ⊆ VI . Consider W = vars(t) \ {x} and let sh_{x}, sh_{t}, sh_{W} ∈ SH be defined as

sh_{x} = rel({x}, sh),  sh_{t} = rel(vars(t), sh),  sh_{W} = rel(W, sh).

Then

bin(sh_{x}, sh_{W}) = cyclic_{x}^{t}(bin(sh_{x}, sh_{t}));  (D 22)
bin(sh_{x}^{⋆}, sh_{W}) = cyclic_{x}^{t}(bin(sh_{x}^{⋆}, sh_{t}));  (D 23)
bin(sh_{x}^{⋆}, sh_{W}^{⋆}) = cyclic_{x}^{t}(bin(sh_{x}^{⋆}, sh_{t}^{⋆})).  (D 24)

Proof We prove equations (D 22) and (D 23) together, letting sh′_{x} ∈ {sh_{x}, sh_{x}^{⋆}}.

To prove the first inclusions (⊆), let S ∈ bin(sh′_{x}, sh_{W}). Since sh_{W} ⊆ sh_{t}, we have S ∈ bin(sh′_{x}, sh_{t}). Moreover, as S ∈ bin(sh′_{x}, sh_{W}), W ∩ S ≠ ∅. Hence, by Definition 20, S ∈ cyclic_{x}^{t}(bin(sh′_{x}, sh_{t})).

To prove the opposite inclusions (⊇), let S ∈ cyclic_{x}^{t}(bin(sh′_{x}, sh_{t})). Then, S ∈ bin(sh′_{x}, sh_{t}), so that S = S_{x}∪S_{t}, where S_{x} ∈ sh′_{x} and S_{t} ∈ sh_{t}. Thus x ∈ S so that, by Definition 20, W ∩S ≠ ∅. If W ∩S_{t} ≠ ∅ then S_{t} ∈ sh_{W} and S ∈ bin(sh′_{x}, sh_{W}), so that the two inclusions hold. If W ∩S_{t} = ∅, then W ∩S_{x} ≠ ∅ and x ∈ S_{t} and hence S_{t} ∈ sh′_{x}. Thus, in the case that sh′_{x} = sh_{x}, S_{t} ∈ sh_{x} so that S ∈ bin(sh_{x}, sh_{W}), proving the inclusion for (D 22). On the other hand, when sh′_{x} = sh_{x}^{⋆}, as S_{x} = S_{W} ∪S_{x} for some S_{W} ∈ sh_{W}, we have S = (S_{x} ∪S_{t})∪S_{W} ∈ bin(sh_{x}^{⋆}, sh_{W}), proving the inclusion for (D 23).

We now prove equation (D 24).

To prove the first inclusion (⊆), let S ∈ bin(sh_{x}^{⋆}, sh_{W}^{⋆}). As sh_{W} ⊆ sh_{t}, we have S ∈ bin(sh_{x}^{⋆}, sh_{t}^{⋆}). Moreover, as S ∈ bin(sh_{x}^{⋆}, sh_{W}^{⋆}), W ∩ S ≠ ∅. By Definition 20, S ∈ cyclic_{x}^{t}(bin(sh_{x}^{⋆}, sh_{t}^{⋆})).

To prove the opposite inclusion (⊇), let S ∈ cyclic_{x}^{t}(bin(sh_{x}^{⋆}, sh_{t}^{⋆})). Then S ∈ bin(sh_{x}^{⋆}, sh_{t}^{⋆}) so that S = S_{x} ∪S_{t} where S_{x} ∈ sh_{x}^{⋆} and S_{t} ∈ sh_{t}^{⋆}. Thus x ∈ S and, by Definition 20, W ∩S ≠ ∅. If W ∩S_{t} ≠ ∅, then S_{t} = S_{W} ∪S_{xt}, where S_{W} ∈ sh_{W}^{⋆} and S_{xt} ∈ sh_{x}^{⋆} ∪ {∅}. Thus S = (S_{x} ∪ S_{xt}) ∪ S_{W} ∈ bin(sh_{x}^{⋆}, sh_{W}^{⋆}). If W ∩ S_{t} = ∅, then S_{t} ∈ sh_{x}^{⋆} and W ∩ S_{x} ≠ ∅. In this case, since S_{x} = S_{W} ∪ S_{x} for some S_{W} ∈ sh_{W}, S = (S_{x} ∪ S_{t}) ∪ S_{W} ∈ bin(sh_{x}^{⋆}, sh_{W}^{⋆}). Thus, in both cases, we have the inclusion.

Theorem 85 Let d_{1}, d_{2} ∈ SFL be such that ρ_{PSD}(d_{1}) = ρ_{PSD}(d_{2}). Then, for all (x ↦ t) ∈ Bind,

ρ_{PSD}(amgu_{S}(d_{1}, x ↦ t)) = ρ_{PSD}(amgu_{S}(d_{2}, x ↦ t)).

Proof Let d_{1} = ⟨sh_{1}, f, l⟩. Then, by Definition 29, d_{2} = ⟨sh_{2}, f, l⟩, where ρ_{PSD}(sh_{1}) = ρ_{PSD}(sh_{2}). By (D 10), it follows that sh_{1} ⊆ ρ_{PSD}(sh_{2}).

For each i ∈ {1, 2}, let ⟨sh′_{i}, f′_{i}, l′_{i}⟩ = amgu_{S}(d_{i}, x ↦ t). We will prove the following results:

sh′_{1} ⊆ ρ_{PSD}(sh′_{2}),  (D 25)
f′_{1} = f′_{2},  (D 26)
l′_{1} = l′_{2}.  (D 27)

From (D 25) using (D 10), we obtain ρ_{PSD}(sh′_{1}) ⊆ ρ_{PSD}(sh′_{2}) and hence, by symmetry, we have ρ_{PSD}(sh′_{1}) = ρ_{PSD}(sh′_{2}) The thesis then follows from Definition 29.

(D 25). For each i ∈ {1, 2}, let

sh_{x,i} = rel({x}, sh_{i}),  sh_{t,i} = rel(vars(t), sh_{i}),
sh_{xt,i} = sh_{x,i} ∩ sh_{t,i},  sh_{−,i} = \overline{rel}(\{x\} ∪ vars(t), sh_{i}).

Let also sh_{W,i} = rel(W, sh_{i}), where W = vars(t) \ {x} and i ∈ {1, 2}.

By Definitions 20 and 22, for each i ∈ {1, 2} we have

sh′_{i} = cyclic_{x}^{t}(sh_{−,i} ∪ sh′′_{i}) = sh_{−,i} ∪ cyclic_{x}^{t}(sh′′_{i})

where

sh′′_{i} =^{def} \begin{cases}bin(sh_{x,i}, sh_{t,i}), & if free_{d_{i}}(x) ∨ free_{d_{i}}(t); \\ bin(sh_{x,i} ∪ bin(sh_{x,i}, sh_{xt}^{⋆}), \\ sh_{t,i} ∪ bin(sh_{t,i}, sh_{xt}^{⋆})), & if lin_{d_{i}}(x) ∧ lin_{d_{i}}(t); \\ bin(sh_{x,i}^{⋆}, sh_{t,i}), & if lin_{d_{i}}(x); \\ bin(sh_{x,i}, sh_{t,i}^{⋆}), & if lin_{d_{i}}(t); \\ bin(sh_{x,i}^{⋆}, sh_{t,i}^{⋆}), & otherwise. \end{cases}

We first show that sh_{−,1} ⊆ ρ_{PSD}(sh_{−,2} ∪ cyclic_{x}^{t}(sh′′_{2})). By the definition of sh_{−,1} and the monotonicity of \overline{rel}, we have

sh_{−,1} ⊆ \overline{rel}(\{x\} ∪ vars(t), ρ_{PSD}(sh_{2})).

Thus, by Lemma 80, sh_{−,1} ⊆ ρ_{PSD}(sh_{−,2}), from which the required result follows by monotonicity of ρ_{PSD}.

We next show that

cyclic_{x}^{t}(sh′′_{1}) ⊆ ρ_{PSD}(sh_{−,2} ∪ cyclic_{x}^{t}(sh′′_{2})).  (D 28)

By applying cases (D 5) and (D 8) of Lemma 79 to the conditions in the definition of sh′′_{1} and sh′′_{2}, it can be seen that they are each computed using the same alternative branch. We have five cases.

1. In the first case, for each i = 1, 2, we have sh′′_{i} = bin(sh_{x,i}, sh_{t,i}). By case (D 22) of Lemma 84, cyclic_{x}^{t}(sh′′_{i}) = bin(sh_{x,i}, sh_{W,i}), for each i = 1, 2. Thus, using case (D 12) of Lemma 82, where we take V = {x}, we obtain (D 28).

2. In the second case we have, for each i = 1, 2,

sh′′_{i} = bin(sh_{x,i} ∪ bin(sh_{x,i}, sh_{xt,i}^{⋆}), sh_{t,i} ∪ bin(sh_{t,i}, sh_{xt,i}^{⋆})).

There are two cases. First assume x ∉ vars(t), so that cyclic_{x}^{t}(sh′′_{i}) = sh′′_{i}. Then, by Lemma 83, we have sh′′_{i} ⊆ ρ_{PSD}(bin(sh_{x,i}, sh_{t,i})) for each i = 1, 2. Therefore, using case (D 12) of Lemma 82 and the monotonicity of ρ_{PSD}, we obtain (D 28). Secondly, suppose that x ∈ vars(t). In this case, for each i = 1, 2, we have sh_{xt,i} = sh_{x,i}, so that sh′′_{i} = bin(sh_{x,i}^{⋆}, sh_{t,i}). This case is therefore equivalent to the third case, proven below.

3. In the third case, for each i = 1, 2, we have sh′′_{i} = bin(sh_{x,i}^{⋆}, sh_{t,i}). By case (D 23) of Lemma 84, cyclic_{x}^{t}(sh′′_{i}) = bin(sh_{x,i}^{⋆}, sh_{W,i}). Thus, by using case (D 13) of Lemma 82 (exchanging the roles of V = {x} and W), we obtain (D 28).

4. In the fourth case, for each i = 1, 2, we have sh′′_{i} = bin(sh_{x,i}, sh_{t,i}^{⋆}). Moreover, as lin_{d}(t) holds and lin_{d}(x) does not hold, we can assume that x ∉ vars(t), so that cyclic_{x}^{t}(sh′′_{i}) = sh′′_{i}. Thus, using case (D 13) of Lemma 82 where V = {x}, we obtain (D 28).

5. In the fifth case we have, for i = 1, 2, sh′′_{i} = bin(sh_{x,i}^{⋆}, sh_{t,i}^{⋆}). By case (D 24) of Lemma 84, cyclic_{x}^{t}(sh′′_{i}) = bin(sh_{x,i}^{⋆}, sh_{W,i}^{⋆}). The thesis follows from item (D 1) of Theorem 74, by considering σ = {x ↦ t′} such that t′ ∈ HTerms and vars(t′) = W.

(D 26). Consider f′_{i} as specified in Definition 22. By applying case (D 5) of Lemma 79, it can be seen that f′_{1} and f′_{2} are computed by selecting the same alternative branch. The thesis f′_{1} = f′_{2} thus follows from case (D 9) of Lemma 79.

(D 27). Consider l′_{i} as specified in Definition 22: for each i ∈ {1, 2} we have

l′_{i} = (VI \ vars(sh′_{i})) ∪ f′_{i} ∪ l′′_{i}

where

l′′_{i} =^{def} \begin{cases}l_{i} \ (share with_{d_{i}}(x) ∩ share with_{d_{i}}(t)), & if lin_{d_{i}}(x) ∧ lin_{d_{i}}(t); \\ l_{i} \ share with_{d_{i}}(x), & if lin_{d_{i}}(x); \\ l_{i} \ share with_{d_{i}}(t), & if lin_{d_{i}}(t); \\ l_{i} \ (share with_{d_{i}}(x) ∪ share with_{d_{i}}(t)) & otherwise. \end{cases}

Let r ∈ HTerms be such that vars(r) = VI . Then, for each i ∈ {1, 2}, we have vars(sh′_{i}) = share with_{d′_{i}}(r); also, by equation (D 25), we know that ρ_{PSD}(sh′_{1}) = ρ_{PSD}(sh′_{2}); thus, by case (D 9) of Lemma 79, we obtain vars(sh′_{1}) = vars(sh′_{2}). By equation (D 26), we also know that f′_{1} = f′_{2}. By case (D 8) of Lemma 79, it can be seen that the conditions determining which branch will be selected in the definitions of l′′_{1} and l′′_{2} are equivalent. Hence, by applying case (D 9) of Lemma 79, l′′_{1} = l′′_{2}. Therefore equation (D 27) holds.

Theorem 86 Let d_{1}, d_{2} ∈ SFL be such that ρ_{PSD}(d_{1}) = ρ_{PSD}(d_{2}). Then, for each sequence of bindings bs ∈ Bind^{∗},

ρ_{PSD}(aunify_{S}(d_{1}, bs)) = ρ_{PSD}(aunify_{S}(d_{2}, bs)).

Proof The proof is by induction on the length of bs. The base case, when |bs| = 0 and thus bs = ϵ, is obvious from the definition of aunify_{S}. For the inductive case, when |bs| = m > 0, let bs = (x ↦ t) . bs′. By the hypothesis and Theorem 85, we have

ρ_{PSD}(amgu_{S}(d_{1}, x ↦ t)) = ρ_{PSD}(amgu_{S}(d_{2}, x ↦ t)).  (D 29)

Moreover, for each i ∈ {1, 2}, by definition of aunify_{S} we have

aunify_{S}(d_{i}, bs) = aunify_{S}(amgu_{S}(d_{i}, x ↦ t), bs′).

Thus, by (D 29), we can apply the inductive hypothesis and conclude the proof, since |bs′| = m − 1 < m.

We now prove that the precision of the abstract existential operator aexists_{S} specified in Definition 27 is not affected by ρ_{PSD}.

Theorem 87 Let d_{1}, d_{2} ∈ SH be such that ρ_{PSD}(d_{1}) = ρ_{PSD}(d_{2}). Then, for each V ⊆ VI ,

ρ_{PSD}(aexists_{S}(d_{1}, V)) = ρ_{PSD}(aexists_{S}(d_{2}, V)).

Proof Let d_{i} = ⟨sh_{i}, f_{i}, l_{i}⟩, for each i = 1, 2. By applying Definitions 27 and 29, for each i = 1, 2, we have

ρ_{PSD}(aexists_{S}(d_{i}, V)) = ρ_{PSD}(⟨aexists(sh_{i}), f_{i} ∪ V, l_{i} ∪ V ⟩)
= ⟨ρ_{PSD}(aexists(sh_{i})), f_{i} ∪ V, l_{i} ∪ V ⟩.

By the hypothesis and Definition 29, we have ρ_{PSD}(sh_{1}) = ρ_{PSD}(sh_{2}), f_{1} = f_{2} and l_{1} = l_{2}. We can therefore apply item (D 2) of Theorem 74 to complete the proof.

Proof of Theorem 30 on page 19. The congruence properties for aunify_{S} and aexists_{S} follow from Theorems 86 and 87, respectively. The congruence property for alub_{S} holds, as usual, because ρ_{PSD} is an upper closure operator.

Proof of Theorem 31 on page 20. Suppose ρ_{PSD}(d_{1}) ≠ ρ_{PSD}(d_{2}). By Definition 29, we have three cases:

1. Suppose ρ_{PSD}(sh_{1}) ≠ ρ_{PSD}(sh_{2}). Let bs ∈ Bind^{∗} be any sequence of the bindings in the substitution σ constructed in the proof of Theorem 75 (i.e., the proof of Theorem 3 in (Zaffanella et al. 2002)). Then the behavior of aunify_{S} on the sharing component of SFL using bs is exactly the same as the behavior of the aunify operator on the plain set-sharing domain SH using σ. This is because, as σ binds all of its domain variables to terms that are ground and finite, the binary union and star-union operators are never used and the result of the abstract computation is independent of the order in which the bindings in σ are considered. Thus, letting ρ ∈ {ρ_{Con}, ρ_{PS}}, the result follows from (D 3) of Theorem 75.

2. Suppose f_{1} ≠ f_{2}. Then, by taking ρ = ρ_{F} and bs = ϵ, we have the result since, for i = 1, 2,

ρ_{F} (aunify_{S}(d_{i}, ϵ)) = ρ_{F} (d_{i}) = ⟨SG, f_{i}, ∅⟩.

3. Finally, suppose l_{1} ≠ l_{2}. Then, by taking ρ = ρ_{L} and bs = ϵ, we have the result since, for i = 1, 2,

ρ_{L}(aunify_{S}(d_{i}, ϵ)) = ρ_{F} (d_{i}) = ⟨SG, ∅, l_{i}⟩.

Proof of Theorem 32 on page 20. If x ∉ vars(t), then

cyclic_{x}^{t}(sh_{−} ∪ sh^{⋄}) = sh_{−} ∪ sh^{⋄}.

Thus, in this case, the thesis is a corollary of Lemma 83, where V = {x} and W = vars(t). If, on the other hand, x ∈ vars(t), then sh_{x} = sh_{xt}, so that sh^{⋄} = bin(sh_{x}^{⋆}, sh_{t}). In this case the thesis is a corollary of Theorem 76.