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

Analysis of Finite and Rational Tree Languages^{∗}

Patricia M. Hill^{†}Enea Zaffanella^{‡}Roberto Bagnara^{§}

December 21, 2001

Abstract

It is well-known that freeness and linearity information positively interact with aliasing information, therefore 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 [3] 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 [34], the mutual interaction between linearity and aliasing information can improve the accuracy of a sharing analysis. This observation has been formally applied in [11] to the specification of the abstract mgu operator for the domain ASub. In his PhD thesis [30], Langen proposed a similar integration with linearity, 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 [27] also shown how a more refined tracking of linearity allows for further precision improvements.

∗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.

†School of Computing, University of Leeds, UK, hill@comp.leeds.ac.uk.

‡Department of Mathematics, University of Parma,, Italy, zaffanella@cs.unipr.it.

§Department of Mathematics, University of Parma, Italy, bagnara@cs.unipr.it.

The synergy attainable from a bi-directional interaction between aliasing and freeness information was initially pointed out by Muthukumar and Hermenegildo [32, 33]. Since then, several authors considered the integration of set-sharing with freeness, sometimes also including additional explicit structural information [9, 10, 29, 18].

Building on the results obtained in [34], [11] and [32], but independently from [30], Hans and Winkler [20] proposed a combined integration of freeness and linearity information with set-sharing. Similar combinations have been proposed in [5, 6, 7]. From a more pragmatic point of view, Codish et al. [12, 13] integrate the information captured by the domains of [34] and [32] 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 [4]. 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.

Given this state of affairs, we will now consider a domain combination whose carrier is essentially the same as specified by Langen [30] and Hans and Winkler [20] (the same domain combination was also considered by Bruynooghe et al. [6, 7], 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 [11, 28, 34].

By extending the results of [22] 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 [2, 3, 37] 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, which are groundness, independence, freeness and linearity.

2 Preliminaries

For a set S, ℘(S) is the powerset of S. The cardinality of S is denoted by #S and the emptyset 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).

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. To prove a few of the results of this thesis, it is useful to assume a total ordering, denoted with ‘≤’, on Vars.

Suppose s, t ∈ Terms: s and t are independent if vars(s) ∩ vars(t) = ∅; if y ∈ vars(t) and ¬(y mvars(t)) we say that variable y occurs linearly in t, more briefly written using the predication occ lin(y, 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.

The function size: HTerms → ℕ, for each t ∈ 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}

A path p ∈ (ℕ \ {0})^{⋆} 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.

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, it holds size(t) ≤ size(tσ).

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 the sets param(σ) and range(σ) (the parameter variables and the range variables of σ, respectively) as

param(σ) =^{def} vars(σ) \ dom(σ),
range(σ) =^{def} { y ∈ vars(t) | (x ↦ t) ∈ σ }.

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.

Example 1 The following hold:

{x ↦ y, y ↦ a} ∈ RSubst \ ISubst,
{x ↦ a, y ↦ a} ∈ ISubst,
{x ↦ y, y ↦ g(y)} ∈ RSubst \ ISubst,
{x ↦ y, y ↦ g(x)} ∈ RSubst \ ISubst,
{x ↦ y, y ↦ x} ∉ RSubst,
{x ↦ y, y ↦ x, z ↦ a} ∉ RSubst.

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

We will sometimes write t[x/s] to denote t{x ↦ s}.

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(σ), x ≠ xστ }

∪ { x ↦ xτ | x ∈ dom(τ) \ dom(σ) }. (1)

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

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

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

converges to a (possibly infinite) term, denoted σ^{∞}(s) [23, 28]. 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. Rational terms, even though infinite in the sense that they admit paths of infinite length, can be finitely represented.

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

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

rt(y, σ) ∈ Vars ⟺ rt(y, τ) ∈ Vars,  (2)
rt(y, σ) ∈ GTerms ⟺ rt(y, τ) ∈ GTerms,  (3)
rt(y, σ) ∈ LTerms ⟺ rt(y, τ) ∈ LTerms.  (4)

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,  (5)
s = t ↔ t = s,  (6)
r = s ∧ s = t → r = t,  (7)

s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n} → f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}).  (8)

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},  (9)
¬(f(s_{1}, …, s_{n}) = g(t_{1}, …, t_{m})).  (10)

The axioms characterized by schemata (9) and (10) 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 [8], 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).  (11)

Axioms characterized by the schema (11) 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 [14, 15], 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 parameter variable, the substitution uniquely defines a ground rational tree for each of its domain variables. Note that being in rational solved form is a very weak property. Indeed, unification algorithms returning a set of equations in rational solved form are allowed to be much more “lazy” than one would usually expect (e.g., see the first substitution in Example 1). We refer the interested reader to [25, 26, 31] for details on the subject.

In the sequel we will use the expression “equality theory” to denote any consistent, decidable theory T satisfying the congruence axioms. We will also use the expression “syntactic equality theory” to denote any equality theory T also satisfying the identity axioms. When the equality theory T is clear from the context, it is convenient to adopt the notations σ ⟹ τ and σ ⟺ τ, where σ, τ are sets of equations, to denote T ⊢ ∀(σ → τ) and T ⊢ ∀(σ ↔ τ), respectively.

Given an equality theory T, and a set of equations in rational solved form σ, we say that σ is satisfiable in T if T ⊢ ∀Vars \ dom(σ) : ∃ dom(σ) . σ. If T is a syntactic equality theory that also includes the occurs-check axioms, and σ is satisfiable in T, then we say that σ is Herbrand.

Given a satisfiable set of equations e ∈ ℘_{f}(Eqs) in an equality theory T, then a substitution σ ∈ RSubst is called a solution for e in T if σ is satisfiable in T and T ⊢ ∀(σ → e). If vars(σ) ⊆ vars(e), then σ is said to be a relevant solution for e. In addition, σ is a most general solution for e in T if T ⊢ ∀(σ ↔ e). In this thesis, 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).

Observe that, given an equality theory T, a set of equations in rational solved form may not be satisfiable in T. For example, ∃x . {x = f(x)} is false in the equality theory FT .

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.

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 [24], 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 3 (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 4 (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} };

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 ≠ ∅ };

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

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 [2, 3] it was shown that the domain SH contains many elements that are redundant for the computation of the actual observable properties of the analysis, that is groundness and pair-sharing. The following formalization of these observables is a rewording of the definitions provided in [36, 37].

Definition 5 (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) }.

Definition 6 (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 [24]; 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 7 (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}.

The domain SFL contains many redundancies: that is, different abstract elements represent the same set of concrete computation states. For instance, any element d = ⟨sh, f, l⟩ ∈ SFL where f ⊈ vars(sh), such as ⊥_{S}, represent the semantics of those program fragments that have no successful computations: this is because any free variable necessarily shares (at least, with itself). Similarly, the element d has the same meaning as the element ⟨sh, f, l′⟩, where l′ = (VI \ vars(sh)) ∪ f ∪ l: in this case, the reason is that any variable that is either ground or free is also necessarily linear.

All these redundancies can be removed by taking, as abstract domain, the image of the concrete domain under the abstraction function. Apart from the simple cases shown above, it is somehow difficult to explicitly characterize such a set. For instance, as observed in [18], the element

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

like ⊥_{S} does not correspond to the abstraction of any concrete computation state. 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 [4, 35].

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 we may end up with σ^{∞} ∉ RSubst, as σ^{∞} can map domain variables to infinite rational terms.

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 [22], the classical abstraction function for set-sharing analysis [16, 24], which was defined for idempotent substitutions only, does not enjoy this property when applied, as it is, to arbitrary substitutions in rational solved form. A possibility is to look for a more general abstraction function that allows to obtain the desired property. For example, in [21, 22] the sharing group operator ‘sg’ of [24] is replaced by an occurrence operator, ‘occ’, defined by means of a fixpoint computation. However, to simplify the presentation, here we define ‘occ’ directly by exploiting the fact that the number of iterations needed to reach the fixpoint is bounded by the number of bindings in the substitution.

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

Definition 8 (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, 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 9 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 in substitutions can be useful for proving properties concerning the linearity abstraction. Groundness is already encoded in the previously defined abstraction for set-sharing; 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 10 (Groundness operator.) For each σ ∈ RSubst, the groundness operator gvars: RSubst → ℘_{f}(Vars) is defined as

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

Example 11 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 12 (Freeness operator.) For each σ ∈ RSubst, the freeness operator fvars: RSubst → ℘(Vars) is defined as

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

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

Example 13 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 14 (Linearity operator.) For each σ ∈ RSubst, the linearity operator lvars: RSubst → ℘(Vars) is defined as

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 15 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 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, σ)),  (12)
y ∈ gvars(σ) ⟺ rt(y, σ) ∈ GTerms,  (13)
y ∈ fvars(σ) ⟺ rt(y, σ) ∈ Vars,  (14)
y ∈ lvars(σ) ⟺ rt(y, σ) ∈ LTerms.  (15)

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

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

ssets(σ) = ssets(τ),  (16)
gvars(σ) = gvars(τ),  (17)
fvars(σ) = fvars(τ),  (18)
lvars(σ) = lvars(τ).  (19)

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

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

With the definitions given in this section, one of our objectives is fulfilled: substitutions in RSubst that are equivalent have the same abstraction. The following is a simple consequence of Definition 18 and Proposition 17.

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

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));

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} ∃y ∈ VI . (y = t) ∧ (y ∈ 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_{−} =^{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′′ =^{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 [6, 20, 30]. Note that, when comparing our domain with the proposal in [6], 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 [6, 20, 30] 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 definitely cyclic bindings, i.e., when x ∈ vars(t). This is the rewording of a similar enhancement proposed in [1] 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 [6, 20], and is more precise than the one defined in [30].

• The computation of the linearity component l′ is the same as specified in [6], and is more precise than those defined in [20, 30].

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, 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_{−} = ∅,

sh_{t} = {yy_{1}, yy_{2}, xyz},  sh_{xt} = {xyz}.

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 [28]), 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 Defini-

tion 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, 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_{−} ∪ 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 problems.

4 SFL_{2}: Eliminating Redundancies

As done in [3] for the plain set-sharing domain, 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 of the analysis.

It is worth stressing that the results presented in [3] and [37] 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.

This stated, we will now show that the domain SFL can be simplified by applying the same notion of redundancy as identified in [3]. 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 leaves the freeness and linearity components untouched.

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

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

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

As proved in [37], we have that ρ_{PSD} ⊑ (ρ_{Con} ⊓ ρ_{PS}); by the above definitions, it is also straightforward to observe 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′, d_{1})) = ρ_{PSD}(alub_{S}(d′, d_{2})),
ρ_{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 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 ρ ∈ {ρ_{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 [3] 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 W = vars(t) \ \{x\} and sh_{−} =^{def} \overline{rel}(\{x\} ∪ vars(t), sh), sh_{x} =^{def} rel(\{x\}, sh),

sh_{t} =^{def} rel(vars(t), sh), sh_{W} =^{def} rel(W, sh), sh_{xt} =^{def} sh_{x} ∩ sh_{t} 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 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 setsharing 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

[1] R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, 1997. Printed as Report TD-1/97.

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

[3] R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. Theoretical Computer Science, 2002. To appear.

[4] R. Bagnara, E. Zaffanella, and P. M. Hill. Enhanced sharing analysis techniques: A comprehensive evaluation. In M. Gabbrielli and F. Pfenning, editors, Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 103–114, Montreal, Canada, 2000. Association for Computing Machinery.

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

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

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

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

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

[10] M. Codish, D. Dams, G. Filé, and M. Bruynooghe. On the design of a correct freeness analysis for logic programs. Journal of Logic Programming, 28(3):181–206, 1996.

[11] M. Codish, D. Dams, and E. Yardeni. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis. In Furukawa [19], pages 79–93.

[12] M. Codish, A. Mulkers, M. Bruynooghe, M. Garcìa de la Banda, and M. Hermenegildo. Improving abstract interpretations by combining domains. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 194–205, Copenhagen, Denmark, 1993. ACM Press. Also available as Technical Report CW 162, Department of Computer Science, K.U. Leuven, December 1992.

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

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

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

[16] A. Cortesi and G. Filé. Sharing is optimal. Journal of Logic Programming, 38(3):371–386, 1999.

[17] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.

[18] G. Filé. Share × Free: Simple and correct. Technical Report 15, Dipartimento di Matematica, Università di Padova, December 1994.

[19] K. Furukawa, editor. Logic Programming: Proceedings of the Eighth International Conference on Logic Programming, MIT Press Series in Logic Programming, Paris, France, 1991. The MIT Press.

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

[21] P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. In G. Levi, editor, Static Analysis: Proceedings of the 5th International Symposium, volume 1503 of Lecture Notes in Computer Science, pages 99– 114, Pisa, Italy, 1998. Springer-Verlag, Berlin.

[22] P. M. Hill, R. Bagnara, and E. Zaffanella. Soundness, idempotence and commutativity of set-sharing. Theory and Practice of Logic Programming, 2(2):155–201, 2002. To appear. Available at http://arXiv.org/abs/cs.

PL/0102030.

[23] B. Intrigila and M. Venturini Zilli. A remark on infinite matching vs infinite unification. Journal of Symbolic Computation, 21(3):2289–2292, 1996.

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

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

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

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

[28] A. King. Pair-sharing over rational trees. Journal of Logic Programming, 46(1–2):139–155, 2000.

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

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

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

[32] K. Muthukumar and M. Hermenegildo. Combined determination of sharing and freeness of program variables through abstract interpretation. In Furukawa [19], pages 49–63. An extended version appeared in [33].

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

[34] H. Søndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In B. Robinet and R. Wilhelm, editors, Proceedings of the 1986 European Symposium on Programming, volume 213 of Lecture Notes in Computer Science, pages 327–338. Springer-Verlag, Berlin, 1986.

[35] E. Zaffanella. Correctness, Precision and Efficiency in the Sharing Analysis of Real Logic Languages. PhD thesis, School of Computing, University of Leeds, Leeds, U.K., 2001. Available at http://www.cs.unipr.it/

    ~zaffanella/.

[36] E. Zaffanella, P. M. Hill, and R. Bagnara. Decomposing non-redundant sharing by complementation. In A. Cortesi and G. Filé, editors, Static Analysis: Proceedings of the 6th International Symposium, volume 1694 of Lecture Notes in Computer Science, pages 69–84, Venice, Italy, 1999. Springer-Verlag, Berlin.

[37] E. Zaffanella, P. M. Hill, and R. Bagnara. Decomposing non-redundant sharing by complementation. Theory and Practice of Logic Programming, 2(2):233–261, 2002. To appear. Available at http://arXiv.org/abs/cs.

    PL/0101025.

A Proofs of the Results of Section 2

The next three lemmas are needed for the proof of Proposition 2. The first two are proven in [22].

Lemma 33 Let T be an equality theory, σ ∈ RSubst and t ∈ HTerms. Then

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

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

Lemma 35 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 holds:

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 func-

tors.

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

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

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 (25), 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 (25), T ⊢ ∀(σ → (x = r)).

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

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

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

Consider (3). 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 33, we have T ⊢ ∀(σ → (yσ^{i} = yτ^{i})); from this, by the identity axioms, we obtain that

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

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 (26), T ⊢ ∀(τ → (x = r)).

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

Consider (4). 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 (2), 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 33 we have T ⊢ ∀(σ → (y = yτ^{i}σ^{j})). By Lemma 35, 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 36 (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. The above definition of variable-idempotence, which is the same originally provided in [21], is a bit stronger than the one adopted in [22] (weak variable-idempotence), where we were disregarding those variables that are in the domain of the substitution. Since any variable-idempo-tent substitution is also weak variable-idempotent, almost all the results proven in [22] still apply.

The next result provides an alternative characterization of variable-idempo-tence.

Lemma 37 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 36, 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 38 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 37.

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 37 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.

Lemma 39 Let σ, τ ∈ VSubst, where dom(σ) ∩ vars(τ) = ∅. Then τ ∘ σ has the following properties.

1. T ⊢ ∀((τ ∘ σ) ↔ (τ ∪ σ)), for any equality theory T;

2. dom(τ ∘ σ) = dom(σ) ∪ dom(τ);

3. τ ∘ σ ∈ VSubst.

Proof. We have that (τ ∪ σ) ∈ RSubst because, by hypothesis, σ, τ ∈ RSubst and dom(σ) ∩ vars(τ) = ∅. It follows from (1) that τ ∘ σ can be obtained from (τ ∪ σ) by a sequence of S-steps so that, by Theorem 47, we have properties 1 and 2.

To prove property 3, we will show that, for all terms t ∈ HTerms,

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

• We start by proving the inclusion vars(tστ) ⊆ vars(tστστ). Thus, 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 proof of the following result is the same as the proof of [22, Theorem 2] (where weaker properties were stated).

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

The following result is proven in [22, Lemma 6].

Lemma 41 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τ).

When σ ∈ VSubst, the following simplified characterizations for the operators occ, fvars, gvars and lvars can be used.

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

occ(σ, v) = { y ∈ Vars | v ∈ vars(yσ) \ dom(σ) },  (27)
gvars(σ) = { y ∈ Vars | vars(yσ) ⊆ dom(σ) },  (28)
fvars(σ) = { y ∈ Vars | yσ ∈ Vars \ dom(σ) },  (29)
lvars(σ) = \{ y ∈ Vars | \begin{matrix}∀z ∈ vars(yσ) \ dom(σ) : occ lin(z, yσ), \\ ∀z ∈ vars(yσ) ∩ dom(σ) : z ∈ gvars(σ) \end{matrix} \}. (30)

Proof. Let #σ = n. If n = 0, then, by Definitions 10, 12 and 14, gvars(σ) = ∅ and fvars(σ) = lvars(σ) = Vars. Thus equations (28), (29) and (30) hold. We assume now that n > 0 and prove each equation separately.

Consider equation (28). By Definition 10, y ∈ gvars(σ) if and only if, for all v ∈ Vars, we have y ∉ occ(σ, v). By Proposition 42, 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(σ).

Consider equation (29). By Definition 12, y ∈ fvars(σ) if and only if yσ^{n} ∈ Vars. First note that, if yσ^{n} ∉ Vars, then yσ ∉ Vars \ dom(σ). Conversely, if yσ^{n} ∈ Vars, then yσ ∈ Vars and, as σ ∈ VSubst, yσ = yσ^{n}. Thus, if n = 1, yσ ∉ dom(σ) and, if n > 1, then yσ = yσ^{2} and, again yσ ∉ dom(σ).

Consider equation (30). First, suppose that, for some z ∈ vars(yσ), either z ∉ dom(σ) and occ lin(z, yσ) does not hold or z ∉ gvars(σ). We show that, in both cases, 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 (28), there exists w ∈ vars(zσ) \ dom(σ). As σ ∈ VSubst, w ∈ vars(yσ). As n ≥ 1, w ≠ z and z ∈ vars(yσ), so that occ lin(w, yσ^{2}) does not hold. Thus, as w ∉ dom(σ) and n ≥ 1, occ lin(w, yσ^{2n}) does not hold. Therefore, by Definition 14, y ∉ lvars(σ).

Secondly, suppose that y ∉ lvars(σ). Then, by Definition 14, there exists z ∈ vars(yσ^{n})\dom(σ) and 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 (28), z ∉ gvars(σ).

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

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

y ∈ occ(σ, v) ⟺ v ∈ vars(rt(y, σ)),  (31)
y ∈ gvars(σ) ⟺ rt(y, σ) ∈ GTerms,  (32)
y ∈ fvars(σ) ⟺ rt(y, σ) ∈ Vars,  (33)
y ∈ lvars(σ) ⟺ rt(y, σ) ∈ LTerms.  (34)

Proof. We first prove item (31). By Proposition 42, 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, σ)). We prove by contradiction that v ∈ vars(yσ) \ dom(σ). In fact, assume that v ∉ vars(yσ) \ dom(σ). Then, since σ ∈ VSubst, by Definition 36 we obtain v ∉ vars(yσσ) \ dom(σ) so that, for all i > 0, v ∉ vars(yσ^{i}) \ dom(σ). Thus, by definition of ‘rt’, v ∉ vars(rt(y, σ)).

We now prove item (32). By Definition 10, we have y ∈ gvars(σ) if and only if y ∉ occ(σ, v), for all v ∈ Vars. By Proposition 16, this is equivalent to v ∉ vars(rt(y, σ)), for all v ∈ Vars. Thus, vars(rt(y, σ)) = ∅ and rt(y, σ) ∈ GTerms.

We now prove item (33). By Proposition 42, 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, so that there exists an n > 0 such that yσσ = f(t_{1}, …, t_{n}), and size(yσσ) > 1. Since rt(y, σ) ∈ Vars, this is a contradiction because we also have size(yσ^{2}) ≤ size(rt(y, σ)) = 1.

Finally, we prove item (34). In order to prove the first implication (⇒), assume y ∈ lvars(σ) so that, by Proposition 42, we have

∀z ∈ vars(yσ) \ dom(σ) : occ lin(z, yσ),  (35)
∀z ∈ vars(yσ) ∩ dom(σ) : vars(zσ) ⊆ dom(σ).  (36)

We need to show that rt(y, σ) ∈ LTerms and we proceed by contradiction, negating the conclusion. Thus assume 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 equation (35), 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(σ). Hence we have contradicted equation (36).

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 equations (35) and (36) hold. We proceed by contradiction, negating the conclusion. There are two cases.

1. Assume that equation (35) does not hold, i.e., there exists a variable 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, therefore obtaining the contradiction.

2. Assume now equation (36) does not hold. Namely, there exists a variable 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.

Proof of Proposition 16 on page 11. By Proposition 40, there exists τ ∈ VSubst such that σ ⟺ τ, dom(σ) = dom(τ) and T ⊢ ∀(σ ↔ τ). By Proposition 17, we have gvars(σ) = gvars(τ), fvars(σ) = fvars(τ) and lvars(σ) = lvars(τ). From all of the above, by Proposition 43, we obtain

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

Thus, the equivalences (13), (14) and (15) follow from Proposition 2.

In order to prove one of the statements of Proposition 17, in particular, to show that the linearity operators precisely capture the intended properties even for arbitrary substitutions in RSubst, we prove two preliminary results.

Lemma 44 Let T be a syntactic equality theory, σ, τ ∈ RSubst and s, t ∈ Terms where T ⊢ ∀(σ ↔ τ), T ⊢ ∀(σ → s = t), dom(σ) = dom(τ) and #τ = n. Then, if z ∈ vars(s) \ dom(σ), z ∈ vars(tτ^{n}).

Proof. Suppose that z ∈ vars(s) \ dom(σ), then we show that, by induction on the depth of s, that z ∈ vars(tτ^{n}).

Suppose first that s = z. Then rt(s, σ) = z. By Lemma 35, rt(s, σ) = rt(t, σ) and hence rt(t, σ) = z. Thus, for all i ∈ ℕ, tσ^{i} ∈ Vars and for some j ∈ ℕ, tσ^{j} = z. Since τ ∈ RSubst, σ has no circular subsets, tσ^{n} = z.

Secondly, suppose that s = f(s_{1}, …, s_{m}) and z ∈ vars(s_{j}), for some j ∈ {1, …, m}. We first show that tτ^{n} ∉ Vars. Suppose, by contraposition that tτ^{n} ∈ Vars, then as τ contains no circular subsets, tτ^{n} ∈ Vars \ dom(τ). Then, as dom(σ) = dom(τ), rt(tτ^{n}, σ) ∈ Vars. By Lemma 33, we have T ⊢ ∀(σ → (s = tτ^{n})). Thus, by Lemma 35, rt(s, σ) = rt(tτ^{n}, σ) so that rt(s, σ) ∈ Vars contradicting the assumption that s ∉ Vars. Thus we must have tτ^{n} = f(t_{1}, …, t_{m}), for some t_{1}, …, t_{m} ∈ Terms where, for each i = 1, …, n, T ⊢ ∀(σ → (s_{i} = t_{i})). Hence, by the inductive hypothesis, z ∈ vars(t_{j}τ^{n}). It follows that z ∈ vars(tτ^{2n}). This means that occ(z, τ) ∩ vars(t) ≠ ∅ and, therefore occ_{n}(z, τ) ∩ vars(t) ≠ ∅. Thus z ∈ vars(tτ^{2n}).

Lemma 45 Let T be a syntactic equality theory, σ, τ ∈ RSubst, s, t ∈ Terms and z ∈ Vars \ dom(σ) where T ⊢ ∀(σ ↔ τ), T ⊢ ∀(σ → s = t), dom(σ) = dom(τ) and #τ = n. Then, if z ∈ vars(s) ∩ vars(t) and occ lin(z, sσ^{n}) does not hold, then occ lin(z, tτ^{n}) does not hold

Proof. Suppose that z ∈ vars(s) ∩ vars(t) and occ lin(s, σ^{n}) does not hold. We show that, by induction on the depth of s, that occ lin(t, τ^{n}) does not hold.

Suppose first that s = z. Then occ lin(z, sσ^{n}) does not hold and the result follows.

Secondly, suppose that s = f(s_{1}, …, s_{m}) and z ∈ vars(s_{j}), for some j ∈ {1, …, m}. We first show that t ∉ Vars. Suppose, by contraposition that t ∈ Vars, then as z ∈ vars(t), t = z. Then, as dom(σ) = dom(τ), rt(t, σ) = z. Thus, by Lemma 35, rt(s, σ) = rt(t, σ) = z so that rt(s, σ) ∈ Vars contradicting the assumption that s ∉ Vars. Thus we must have t = f(t_{1}, …, t_{m}), for some t_{1}, …, t_{m} ∈ Terms where, for each i = 1, …, n, T ⊢ ∀(σ → (s_{i} = t_{i})). By Lemma 44, z ∈ vars(t_{j}) If occ lin(z, s_{j}σ^{n} does not hold, then, by the inductive hypothesis, occ lin(z, t_{j}τ^{n} does not hold and hence, occ lin(z, tτ^{n} does not hold.

Otherwise, there must exist k ∈ {1, …, m} where k ≠ j such that z ∈ vars(s_{k}). By Lemma 44, z ∈ vars(t_{k}) As k ≠ j, occ lin(tτ^{n}).

The next three results are needed in the proof of Proposition 17 below. The first Lemma is a consequence of the proof of [22, Lemma 15]. The other two results correspond to [22, Theorems 1 and 2].

Lemma 46 Let σ, σ′ ∈ RSubst be such that σ ⟼^{∗}^{S} σ′. Then, for all v ∈ Vars, we have occ(σ, v) = occ(σ′, v).

Theorem 47 Let T be an equality theory, σ ∈ RSubst and σ ⟼^{∗}^{S} σ′. Then σ′ ∈ RSubst, vars(σ) = vars(σ′), dom(σ) = dom(σ′) and T ⊢ ∀(σ ↔ σ′).

Theorem 48 Let σ ∈ RSubst. Then there exists σ′ ∈ VSubst such that σ ⟼^{∗}^{S} σ′ and y ∈ dom(σ′) ∩ range(σ′) implies y ∈ vars(yσ′).

Proof of Proposition 17 on page 12. Let n = #σ. Then, as dom(σ) = dom(τ), n = #τ.

Consider first (16). By Theorem 48, there exists τ ∈ VSubst such that σ ⟼^{∗}^{S} τ. By Theorem 47, dom(σ) = dom(τ) and T ⊢ ∀(σ ↔ τ). By Lemma 46, occ(σ, v) = occ(τ, v). Moreover, by Proposition 43, we have y ∈ occ(τ, v) if and only if v ∈ vars(rt(y, τ)). Thus, we have y ∈ occ(σ, v) if and only if v ∈ vars(rt(y, τ)) and, to complete the proof, it is sufficient to show that

v ∈ vars(rt(y, σ)) ⟺ v ∈ vars(rt(y, τ)).

We only prove the first implication, since the other one follows by symmetry.

Suppose v ∈ vars(rt(y, σ)). Then there exists an index i ≥ 0 such that v ∈ vars(yσ^{i}). Note that v ∉ dom(σ) = dom(τ), so that v ∈ vars(rt(yσ^{i}, τ)). Since T ⊢ ∀(τ → σ), by Lemma 33 we have T ⊢ ∀(τ → (y = yσ^{i})). By Lemma 35, rt(y, τ) = rt(yσ^{i}, τ). Thus, v ∈ vars(rt(y, τ)).

Consider (17). By Definition 10, this is a simple consequence of (16) proved above.

Consider (18). Suppose that y ∈ fvars(σ). Then, by Definition 12, yσ^{n} ∈ Vars \ dom(σ) and hence, yσ^{n} ∈ Vars \ dom(τ). By Lemma 33, we have T ⊢ ∀(τ → (y = yσ^{n})). Thus, by Lemma 35, rt(y, τ) = rt(yσ^{n}, τ) = yσ^{n}. Thus rt(y, τ) ∈ Vars \ dom(τ). Thus yτ^{i} ∈ Vars for all i ∈ ℕ. As τ ∈ RSubst, there are no circular subsets of τ so that yτ^{n} ∉ dom(τ) so that, by Definition 12, y ∈ fvars(τ).

Consider (18). Suppose y ∉ lvars(σ), Then there exists z ∈ vars(yσ^{n}) such that occ lin(z, yσ^{2n}) does not hold. By Lemma 44, z ∈ vars(yτ^{n}). As T ⊢ ∀(τ → (yσ^{n} = yτ^{n})), by Lemma 45, occ lin(z, yτ^{2n}) does not hold.

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. As already discussed, this result applies to any syntactic equality theory, including both the finite-tree theory FT and the rational-tree theory RT . In contrast, all the published proofs of correctness for a combination of set-sharing with freeness and linearity information assume the occurs-check is performed. As a consequence, they do not apply to the vast majority of implemented logic languages.

First we recall the definition of the abstract mgu operator on SH and the corresponding correctness result, as provided in [22].

Definition 49 (amgu.) The function amgu: SH × Bind → SH captures the effects of a binding on an SH element. Suppose x ∈ Vars, r ∈ HTerms, and sh ∈ SH . Let v_{x} =^{def} {x}, v_{r} =^{def} vars(r) and v_{xr} =^{def} v_{x} ∪ v_{r}. Then

amgu(sh, x ↦ r) =^{def} \overline{rel}(v_{xr}, sh) ∪ bin(rel(v_{x}, sh)^{⋆}, rel(v_{r}, sh)^{⋆}).

Theorem 50 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).

We now prove Theorem 21, stating that the auxiliary operators introduced in Definition 20 correctly approximate the intended properties.

Proof of Theorem 21 on page 13. 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.

The following simple lemma will be systematically used in the following correctness proofs.

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 (6) and (7), that, for any terms p, q, r ∈ HTerms,

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

Secondly note that, using Lemma 33, 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 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 52 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 40, we can assume there exist σ′, τ′ ∈ VSubst such that T ⊢ ∀(σ ↔ σ′) and T ⊢ ∀(τ ↔ τ′), so that T ⊢ ∀(τ′ → σ′). Also, by Proposition 17, we have gvars(σ) = gvars(σ′) and gvars(τ) = gvars(τ′). Therefore, it is sufficient to prove that x ∉ gvars(τ′) implies x ∉ gvars(σ′).

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

Another useful result is the following.

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

Proof. By definition of mgs, we have σ, τ ∈ RSubst and σ ⟺ e ⟺ τ. Thus, all the above equivalences follow from Proposition 17.

We now introduce a bit of terminology that will be helpful in order to simplify the notation in the following 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 53, this notation is not ambiguous.

Lemma 54 Let s̄, t̄ ∈ HTerms^{n} be such that mgs(s̄ = t̄) ≠ ∅. Let also G =^{def} gvars(s̄ = t̄). If s̄ is (Vars \ G)-linear, then there exists μ ∈ mgs(s̄ = t̄) such that, for each z ∈ Vars \ vars(s̄),

1. zμ is (Vars \ G)-linear;

2. vars(zμ) ∩ dom(μ) ⊆ G;

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

Proof. We assume that the congruence and identity axioms hold.

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 prove that the result holds by induction on the number of variables in W.

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 (8), 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 (5), 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̄)) ≠ ∅.  (37)

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 μ ⟹ {s_{1} = t_{1}}, by Lemma 35, 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 ≠ ∅.  (38)

By exploiting (37) and (38), 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 (6), μ ∈ mgs(s̄ = t̄).

As {t_{k+1}, …, t_{n}} ⊆ vars((s_{k+1}, …, s_{n})), we have dom(μ) \ vars(s̄) = ∅ so that the required result 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}),  (39)

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}) 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 μ ∈ mgs(s̄ = t̄). By (39), we have s_{1} ∉ vars(μ_{1}) so that s_{1} ∉ dom(μ_{1}). Also, since μ_{1} ∈ RSubst, μ has no identities or circular subsets. Thus we have μ ∈ RSubst. 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 1, 2 and 3 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 1, we have zμ_{1} is V_{1}-linear. As zμ = zμ_{1} and V = V_{1}, zμ is V -linear.

2. By inductive property 2, 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 3, 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}),  (40)

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}) 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}.  (41)

Note that, by (40), t_{1} ∉ vars(μ_{1}) and, in particular, t_{1} ∉ dom(μ_{1}). Thus, since μ_{1} ∈ RSubst, μ has no identities or circular subsets so that μ ∈ RSubst. 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 1, 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 1, uμ_{1} is V_{1}-linear. Moreover, by property 3, 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 2, 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 2, 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 3, 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}.  (42)

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 3 (taking z′ = u). As (42) 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}.  (43)

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 3 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 (43). 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.

Corollary 55 There exists μ′ ∈ VSubst that (under the same hypotheses) satisfies all the properties stated for μ ∈ RSubst in Lemma 54.

Proof. We start by proving that the properties stated for μ ∈ RSubst in Lemma 54 are invariant under the application of an S-step.

Suppose that μ ∈ RSubst satisfies the properties stated in Lemma 54 and μ ⟼^{S} μ′. First note that, by Theorem 47, we have μ′ ∈ mgs(s̄ = t̄) and dom(μ′) = dom(μ). Also, by Lemma 53, gvars(μ′) = gvars(μ) = G. By definition of S-step, there exist {x ↦ t, y ↦ s} ⊆ μ such that x ≠ y and

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

Let z ∈ Vars \ vars(s̄) and consider the term zμ′. If z ≠ y or x ∉ vars(s) then we have zμ′ = zμ and there is nothing to prove. Therefore, assume z = y, so that zμ = s, and x ∈ vars(zμ), so that zμ′ = zμ[x/t]. Note that x ∈ vars(zμ) ∩ dom(μ) so that, by property 2, we have x ∈ G. As a consequence, vars(t) ⊆ G and we obtain

vars(zμ) \ G = vars(zμ′) \ G.

From this, it is easy to conclude that properties 1, 2 and 3 hold for μ′.

By a simple induction, the above result generalizes to any finite sequence of S-steps. Then, by Theorem 48 it follows than we can construct such a μ′ ∈ VSubst.

In the following three sections, we prove the correctness of the abstract unification operator on each component of the SFL domain. A further section will join all of these results to establish the whole correctness of amgu_{S}.

C.1 The Correctness for Set-Sharing

Proposition 56 Let d = ⟨sh, f, l⟩ ∈ SFL, σ ∈ γ_{S}(d) ∩ VSubst and (x ↦ t) ∈ Bind, where {x}∪vars(t) ⊆ VI and y ∈ dom(σ)∩range(σ) implies y ∈ vars(yσ). Suppose that {r, r′} = {x, t} and free_{d}(r) holds. For all τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, letting

sh_{−} = \overline{rel}(\{x\} ∪ vars(t), sh),
sh_{r} = rel(vars(r), sh),
sh_{r′} = rel(vars(r′), sh),

we have

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

Proof. We assume that the congruence and identity axioms hold. Note that if σ ∪ {x = t} is not satisfiable, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (44) holds.

Since free_{d}(r) holds, by Theorem 21, rt(r, σ) ∈ Vars and hence, by Proposition 42,

rσ ∈ Vars \ dom(σ).  (45)

Let

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

Since σ ∈ γ_{S}(d), we have sh ⊇ ssets(σ) so that, using the monotonicity of \overline{rel}, rel and bin, we obtain

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

Thus, in order to prove (44) it is sufficient to show that

R_{−} ∪ bin(R_{r}, R_{r′}) ⊇ ssets(τ).  (46)

Note that, by Definition 8 and (45), we obtain

R_{r} = {occ(σ, rσ)}.  (47)

Suppose first xσ = tσ. Then we have σ ∈ mgs(σ ∪ {xσ = tσ}), so that by

Lemma 51, σ ∈ mgs(σ∪{x = t}). Thus, take τ =^{def} σ. Moreover, by (47), we also have R_{r′} = {occ(σ, rσ)} = R_{r}, so that R_{r} = bin(R_{r}, R_{r′}). As a consequence,

R_{−} ∪ bin(R_{r}, R_{r′}) = (ssets(σ) \ R_{r}) ∪ R_{r}
= ssets(σ)
= ssets(τ).

Otherwise, let xσ ≠ tσ and let ν, μ, τ ∈ RSubst be defined as

ν =^{def} { (y ↦ s) ∈ σ | y ∉ vars(xσ) ∪ vars(tσ) },
μ =^{def} {rσ ↦ r′σ},
τ =^{def} ν ∘ μ.

As ν ⊆ σ ∈ VSubst, by Lemma 38 we have ν ∈ VSubst; also, μ ∈ VSubst because it has a single binding; moreover, by construction, dom(ν) ∩ vars(μ) = ∅; thus we can apply Lemma 39 to obtain τ ∈ VSubst. By applying Lemma 51, we also have τ ∈ mgs(σ ∪ {x = t}).

Suppose S ∈ ssets(τ). By Definition 49 and Theorem 50, we have

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

If S ∈ R_{−}, then (46) holds trivially. Therefore suppose S ∈ bin(R_{r}^{⋆}, R_{r′}^{⋆}), so that there exist S_{r} ∈ R_{r}^{⋆} and S_{r′} ∈ R_{r′}^{⋆} such that S = S_{r} ∪ S_{r′}. Note that, by (47), R_{r}^{⋆} = R_{r}. Thus, to prove (46) holds, it is sufficient to show that S_{r′} ∈ R_{r′}.

As S ∈ ssets(τ), by Proposition 42, there exists v ∈ Vars \ dom(τ) such that S = { y ∈ VI | v ∈ vars(yτ) }. As v ∉ dom(τ), v ≠ rσ.

Let y ∈ S. We show that y ∈ occ(σ, rσ) ∪ occ(σ, v). Using Lemma 33, we have T ⊢ ∀(τ → yτ = y). Therefore, since T ⊢ ∀(τ → σ), by Lemma 41 (replacing s = t by yτ = y), there exists z ∈ vars(yσ) \ dom(σ) such that v ∈ vars(zτ). If z = rσ, then y ∈ S_{r}. If z ≠ rσ, then z ∉ dom(τ) and zτ = z. Therefore v = z and y ∈ occ(σ, v).

Proposition 57 Let d = ⟨sh, f, l⟩ ∈ SFL, σ ∈ γ_{S}(d) ∩ VSubst and (x ↦ t) ∈ Bind, where {x}∪vars(t) ⊆ VI and y ∈ dom(σ)∩range(σ) implies y ∈ vars(yσ). Suppose that lin_{d}(x) and lin_{d}(t) hold. For all τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, letting

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

we have

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

Proof. We assume that the congruence and identity axioms hold. Note that if σ ∪ {x = t} is not satisfiable, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (48) holds.

For every r ∈ {x, t}, by hypothesis, lin_{d}(r) holds. Then, by Theorem 21, rt(r, σ) ∈ LTerms and hence, by Proposition 16, vars(r) ⊆ lvars(σ). Thus, by Proposition 42,

∀v ∈ vars(rσ) \ dom(σ) : occ lin(v, rσ),
vars(rσ) ∩ dom(σ) ⊆ gvars(σ).  (49)

Therefore, by defining V_{σ} =^{def} Vars \ gvars(σ), we obtain that both terms xσ and tσ are V_{σ}-linear. Let

{u_{1}, …, u_{k}} =^{def} dom(σ) ∩ (vars(xσ) ∪ vars(tσ)),
s̄ =^{def} (u_{1}, …, u_{k}, xσ),
t̄ =^{def} (u_{1}σ, …, u_{k}σ, tσ).

Since xσ is V_{σ}-linear, it follows from (49) (letting r = x) that s̄ is V_{σ}-linear. It also follows from (49) (applied twice, once with r = x and once with r = t) that, for each i = 1, …, k we have u_{i} ∈ gvars(σ), so that vars(u_{i}σ) ⊆ gvars(σ). Therefore, since tσ is V_{σ}-linear, t̄ is also V_{σ}-linear. By Lemma 51 and the congruence axioms, σ ∪ {x = t} ⟹ s̄ = t̄. Thus, as σ ∪ {x = t} is satisfiable, there exists μ ∈ mgs(s̄ = t̄). Let V_{μ} = Vars\gvars(μ); since gvars(σ) ⊆ gvars(μ), then V_{μ} ⊆ V_{σ} and s̄, t̄ are also V_{μ}-linear. Therefore, we can apply Lemma 54 and Corollary 55 so that, by case (3), there exists μ ∈ mgs(s̄ = t̄) ∩ VSubst such that, for all w, w′ ∈ Vars where w ≠ w′ and either {w, w′} ∩ vars(s̄) = ∅ or {w, w′} ∩ vars(t̄) = ∅,

vars(wμ) ∩ vars(w′μ) ⊆ gvars(μ).  (50)

Note that, since σ ∈ VSubst, we have vars(u_{i}σ) ⊆ vars(xσ) ∪ vars(tσ) for each i = 1, …, k. Therefore

vars(μ) ⊆ vars(xσ) ∪ vars(tσ).  (51)

Let ν, τ ∈ RSubst be defined as

ν =^{def} { (y ↦ s) ∈ σ | y ∉ vars(xσ) ∪ vars(tσ) },
τ =^{def} ν ∘ μ.

As ν ⊆ σ ∈ VSubst, by Lemma 38 we have ν ∈ VSubst; moreover, by (51), dom(ν) ∩ vars(μ) = ∅; thus we can apply Lemma 39 to obtain τ ∈ VSubst. By applying Lemma 51, we also have τ ∈ mgs(σ ∪ {x = t}).

Let

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

Since σ ∈ γ_{S}(d), we have sh ⊇ ssets(σ) so that, using the monotonicity of \overline{rel}, rel, (·)^{⋆} and bin, 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}^{⋆})).

It follows that, in order to prove (48), it is sufficient to show

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

Let S be an arbitrary sharing set in ssets(τ). By Definition 49 and Theorem 50, we have

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

If S ∈ R_{−}, then (52) holds trivially. Therefore suppose S ∈ bin(R_{x}^{⋆}, R_{t}^{⋆}), so that there exist S_{x} ∈ R_{x}^{⋆} and S_{t} ∈ R_{t}^{⋆} such that S = S_{x} ∪ S_{t}. We prove that (52) holds by showing that S_{x} ∈ R_{x} ∪ bin(R_{x}, R_{xt}^{⋆}) and S_{t} ∈ R_{t} ∪ bin(R_{t}, R_{xt}^{⋆}).

We first show that S_{t} ∈ R_{t} ∪ bin(R_{t}, R_{xt}^{⋆}). As S_{t} ∈ R_{t}^{⋆}, S_{t} = S_{1} ∪ S_{2} where S_{1} ∈ (R_{t} \ R_{xt})^{⋆} ∪ {∅} and S_{2} ∈ R_{xt}^{⋆} ∪ {∅}. Note that as S_{t} ≠ ∅, we cannot have S_{1} = S_{2} = ∅. Suppose first that S_{1} = ∅ so that S_{t} = S_{2} ≠ ∅. Then S_{t} ∈ R_{xt}^{⋆}. However, since R_{xt} ⊆ R_{t}, R_{xt}^{⋆} ⊆ bin(R_{t}, R_{xt}^{⋆}). Thus S_{t} ∈ bin(R_{t}, R_{xt}^{⋆}). Suppose next that S_{1} ≠ ∅. As R_{t} \ R_{xt} = R_{t} \ R_{x}, we have S_{1} = ⋃{ occ(σ, w) | w ∈ S_{1} \ vars(xσ) }. However, as occ(σ, w) = ∅ for all w ∈ dom(σ) and vars(s̄) \ vars(xσ) ⊆ dom(σ),

S_{1} = ⋃{ occ(σ, w) | w ∈ S_{1} \ (dom(σ) ∪ vars(s̄)) }

Let w_{1}, w_{2} ∈ S_{1} \ (dom(σ) ∪ vars(s̄)). Then, as S_{1} ⊆ S, S ∈ ssets(τ) and τ ∈ VSubst, by Proposition 42, there exists v ∈ Vars \ dom(τ) such that v ∈ vars(w_{1}τ) ∩ vars(w_{2}τ). However, since w_{i} ∉ dom(σ), we have w_{i}τ = w_{i}μ, for i ∈ {1, 2}. Thus, noting that v ∉ dom(τ) implies v ∉ gvars(τ), we can apply (50) to conclude that w_{1} = w_{2}. As the choice of w_{1} and w_{2} was arbitrary, there exists a unique variable w ∈ S_{1} \ (dom(σ) ∪ vars(s̄)) such that S_{1} = occ(σ, w). Thus S_{1} ∈ R_{t}. If S_{2} = ∅ then S_{t} = S_{1} ∈ R_{t}. If S_{2} ≠ ∅, then S_{t} = S_{1} ∪ S_{2} ∈ bin(R_{t}, R_{xt}^{⋆}). Hence, in both cases, S_{t} ∈ R_{t} ∪ bin(R_{t}, R_{xt}^{⋆}).

By the same reasoning, (replacing x by t, t by x and s̄ by t̄ in the previous paragraph) we obtain S_{x} ∈ R_{x} ∪ bin(R_{x}, R_{xt}^{⋆}), thus completing the proof.

Corollary 58 Let d = ⟨sh, f, l⟩ ∈ SFL, σ ∈ γ_{S}(d) ∩ VSubst and (x ↦ t) ∈ Bind, where {x}∪vars(t) ⊆ VI and y ∈ dom(σ)∩range(σ) implies y ∈ vars(yσ). Suppose that lin_{d}(x), lin_{d}(t) and ind_{d}(x, t) hold. For all τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, letting

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

we have

sh_{−} ∪ bin(sh_{x}, sh_{t}) ⊇ ssets(τ).

Proof. Since ind_{d}(x, t) holds, by Definition 20 we have sh_{x} ∩ sh_{t} = ∅. The result then follows from Proposition 57.

Proposition 59 Let d = ⟨sh, f, l⟩ ∈ SFL, σ ∈ γ_{S}(d) ∩ VSubst and (x ↦ t) ∈ Bind, where {x}∪vars(t) ⊆ VI and y ∈ dom(σ)∩range(σ) implies y ∈ vars(yσ). Suppose that {r, r′} = {x, t} and lin_{d}(r) holds. For all τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, letting

sh_{−} = \overline{rel}(\{x\} ∪ vars(t), sh),
sh_{r} = rel(vars(r), sh),
sh_{r′} = rel(vars(r′), sh),

we have

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

Proof. We assume that the congruence and identity axioms hold. Note that if σ ∪ {x = t} is not satisfiable, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (53) holds.

Since lin_{d}(r) holds, by Theorem 21, rt(r, σ) ∈ LTerms and hence, by Proposition 16, vars(r) ⊆ lvars(σ). Thus, by Proposition 42,

∀v ∈ vars(rσ) \ dom(σ) : occ lin(v, rσ),
vars(rσ) ∩ dom(σ) ⊆ gvars(σ).  (54)

Therefore, by defining V_{σ} =^{def} Vars \ gvars(σ), we obtain that the term rσ is V_{σ}-linear. Let

{u_{1}, …, u_{k}} =^{def} dom(σ) ∩ (vars(xσ) ∪ vars(tσ)),
s̄ =^{def} (u_{1}, …, u_{k}, rσ),
t̄ =^{def} (u_{1}σ, …, u_{k}σ, r′σ).

Since rσ is V_{σ}-linear it follows from (54) that s̄ is V_{σ}-linear. By Lemma 51 and the congruence axioms, σ∪{x = t} ⟹ s̄ = t̄. Thus, as σ∪{x = t} is satisfiable, there exists μ ∈ mgs(s̄ = t̄). Let V_{μ} = Vars\gvars(μ); since gvars(σ) ⊆ gvars(μ), then V_{μ} ⊆ V_{σ} and s̄ is also V_{μ}-linear. Therefore, we can apply Lemma 54 and Corollary 55 so that, by case (3), there exists μ ∈ mgs(s̄ = t̄) ∩ VSubst such that, for all w, w′ ∈ Vars \ vars(s̄) where w ≠ w′,

vars(wμ) ∩ vars(w′μ) ⊆ gvars(μ).  (55)

Note that, since σ ∈ VSubst, we have vars(u_{i}σ) ⊆ vars(xσ) ∪ vars(tσ) for each i = 1, …, k. Therefore

vars(μ) ⊆ vars(xσ) ∪ vars(tσ).  (56)

Let ν, τ ∈ RSubst be defined as

ν =^{def} { (y ↦ s) ∈ σ | y ∉ vars(xσ) ∪ vars(tσ) },

τ =^{def} ν ∘ μ.

As ν ⊆ σ ∈ VSubst, by Lemma 38 we have ν ∈ VSubst; moreover, by (56), dom(ν) ∩ vars(μ) = ∅; thus we can apply Lemma 39 to obtain τ ∈ VSubst. By applying Lemma 51, we also have τ ∈ mgs(σ ∪ {x = t}).

Let

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

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

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

Thus, in order to prove (53) it is sufficient to show that

R_{−} ∪ bin(R_{r}^{⋆}, R_{r′}) ⊇ ssets(τ).  (57)

Suppose S ∈ ssets(τ). By Definition 49 and Theorem 50, we have

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

If S ∈ R_{−}, then (57) holds trivially. Therefore suppose S ∈ bin(R_{r}^{⋆}, R_{r′}^{⋆}), so that there exist S_{r} ∈ R_{r}^{⋆} and S_{r′} ∈ R_{r′}^{⋆} such that S = S_{r} ∪ S_{r′}. First note that, since S_{r′} ∈ R_{r′}^{⋆}, there exists S′ ⊆ S_{r′} such that S′ ∈ R_{r′}. Moreover, if S_{r′} ∈ R_{r}^{⋆}, then we have S ∈ R_{r}^{⋆}, so that S = S ∪ S′ ∈ bin(R_{r}^{⋆}, R_{r′}), proving (57). Thus, we now assume that S_{r′} ∉ R_{r}^{⋆}.

As S_{r′} ∈ R_{r′}^{⋆}, we have S_{r′} = ⋃{ occ(σ, w) | w ∈ S_{r′} \ dom(σ) }. From this, as S_{r′} ∉ R_{r}^{⋆}, vars(s̄) ⊆ dom(σ) ∪ vars(rσ) and vars(rσ) ⊆ vars(s̄), we obtain

S_{r′} = ⋃{ occ(σ, w) | w ∈ S_{r′} \ (dom(σ) ∪ vars(s̄)) }.

Let w_{1}, w_{2} ∈ S_{r′} \ (dom(σ) ∪ vars(s̄)). Note that, as S_{r′} ⊆ S, S ∈ ssets(τ) and τ ∈ VSubst, by Proposition 42 there exists v ∈ Vars \ dom(τ) such that v ∈ vars(w_{1}τ)∩vars(w_{2}τ). However, since w_{i} ∉ dom(σ), we have w_{i}τ = w_{i}μ, for i ∈ {1, 2}. Thus, noting that v ∉ dom(τ) implies v ∉ gvars(τ), we can apply (55) to conclude that w_{1} = w_{2}. As the choice of w_{1} and w_{2} was arbitrary, there exists a unique variable w ∈ S_{r′} \ (dom(σ) ∪ vars(s̄)) such that S_{r′} = occ(σ, w). Thus S_{r′} ∈ R_{r′} and (57) holds.

Lemma 60 Let sh ∈ SH and V, W ⊆ VI , where rel(V, sh) ⊆ rel(W, sh). Let (x ↦ t) ∈ Bind and sh′ =^{def} amgu(sh, x ↦ t), where {x} ∪ vars(t) ⊆ VI . 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 61 Let sh ∈ SH , (x ↦ t) ∈ Bind, where x ∈ vars(t) ⊆ VI . Let τ ∈ RSubst be satisfiable in the syntactic equality theory 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}).  (58)

The base case, when i = 0, follows directly from Definition 8; note that (58) 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, (58) holds for sh_{i−1}. Thus, by Lemma 60 (taking V = V_{x} and W = W_{t}), we obtain that (58) 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 53, 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.2 The Correctness for Freeness

Proposition 62 Let σ ∈ VSubst and (x ↦ y) ∈ Bind, where {x, y} ⊆ VI . Suppose also that {x, y} ⊆ fvars(σ). Then, for all τ ∈ mgs(σ ∪ {x = y}) in the syntactic equality theory T, we have

fvars(σ) ⊆ fvars(τ).  (59)

Proof. We assume that the congruence and identity axioms hold. Note that if σ∪{x = y} is not satisfiable in T, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = y} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = y}) such that (59) holds.

As {x, y} ⊆ fvars(σ) we have, using Proposition 42,

{xσ, yσ} ⊆ Vars \ dom(σ).  (60)

Suppose first xσ = yσ. Then we have σ ∈ mgs(σ ∪ {xσ = yσ}), so that by

Lemma 51, σ ∈ mgs(σ ∪ {x = y}). Thus, by taking τ =^{def} σ, we trivially obtain fvars(σ) = fvars(τ).

Otherwise, let xσ ≠ yσ and take τ =^{def} σ ∪ {xσ = yσ}. Then, since σ ∈ RSubst, it follows from (60) that τ ∈ Eqs has no identities or circular subsets so that τ ∈ RSubst. Note that dom(τ) = dom(σ) ∪ {xσ}. By Lemma 51, τ ∈ mgs(σ ∪ {x = t}). Suppose z ∈ fvars(σ), so that by Proposition 42, zσ ∈ Vars \ dom(σ). Then we show that z ∈ fvars(τ). If zσ = xσ then zτ = yσ. On the other hand, if zσ ≠ xσ, we have zτ = zσ. In both cases, zτ ∈ Vars \ dom(τ), which implies z ∈ fvars(τ).

Lemma 63 Let d ∈ SFL and σ ∈ γ_{S}(d) ∩ VSubst. Let also y ∈ VI and t ∈ HTerms be such that vars(t) ⊆ VI and y ∉ share with_{d}(t). Then vars(yσ) ∩ vars(tσ) ⊆ dom(σ).

Proof. Let d = ⟨sh, f, l⟩ and V_{t} = vars(t) so that, by Definition 20, y ∉ vars(rel(V_{t}, sh)). Thus

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

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

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

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

∀w ∈ V_{t} : vars(yσ) ∩ vars(wσ) ⊆ dom(σ),

which is equivalent to the thesis.

Proposition 64 Let d ∈ SFL, σ ∈ γ_{S}(d) ∩ VSubst and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Suppose also that x ∈ fvars(σ). Then, for all τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, we have

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

Proof. We assume that the congruence and identity axioms hold. Note that if σ ∪ {x = t} is not satisfiable, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (61) holds.

As x ∈ fvars(σ) we have, using Proposition 42,

xσ ∈ Vars \ dom(σ).  (62)

Suppose first xσ = tσ. Then we have σ ∈ mgs(σ ∪ {xσ = tσ}), so that by

Lemma 51, σ ∈ mgs(σ ∪ {x = t}). Thus, by taking τ =^{def} σ, we trivially obtain fvars(σ) = fvars(τ), which implies the thesis.

Otherwise, let xσ ≠ tσ and take τ =^{def} σ∪{xσ = tσ}. Then, since σ ∈ RSubst, it follows from (62) that τ ∈ Eqs has no identities or circular subsets so that τ ∈ RSubst. By Lemma 51, τ ∈ mgs(σ ∪ {x = t}).

Suppose y ∈ fvars(σ) \ share with_{d}(x). Then we show that y ∈ fvars(τ). Since y ∈ fvars(σ), it follows by Proposition 42 that

yσ ∈ Vars \ dom(σ).  (63)

Since y ∉ share with_{d}(x) and σ ∈ VSubst, it follows by Lemma 63 that we have vars(yσ) ∩ vars(xσ) ⊆ dom(σ). From this, by using (62) and (63), we obtain yσ ≠ xσ; from this, again by (62), we derive y ≠ xσ. Thus yτ = yσ, so that y ∈ fvars(τ).

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

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

Proof. We assume that the congruence and identity axioms hold. Note that if σ ∪ {x = t} is not satisfiable, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (64) holds.

Let

{u_{1}, …, u_{k}} =^{def} dom(σ) ∩ (vars(xσ) ∪ vars(tσ)),
s̄ =^{def} (u_{1}, …, u_{k}, xσ),
t̄ =^{def} (u_{1}σ, …, u_{k}σ, tσ).

Note that, since σ ∈ VSubst, for each i = 1, …, k, we have

vars(u_{i}σ) ⊆ vars(xσ) ∪ vars(tσ).

Thus, for any μ ∈ mgs(s̄ = t̄), we have

vars(μ) ⊆ vars(xσ) ∪ vars(tσ).  (65)

Let

ν =^{def} { z = zσμ | z ∈ dom(σ) \ (vars(xσ) ∪ vars(tσ)) },
τ =^{def} ν ∪ μ.

Then, as σ, μ ∈ RSubst, it follows from (65) that ν, τ ∈ Eqs have no identities or circular subsets so that ν, τ ∈ RSubst. Thus, using Lemma 51 and the assumption that σ ∪ {x = t} is satisfiable, τ ∈ mgs(σ ∪ {x = t}).

Suppose y ∈ fvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t)). We show that y ∈ fvars(τ). As y ∈ fvars(σ), by Proposition 42,

yσ ∈ Vars \ dom(σ).  (66)

As y ∉ share with_{d}(x) ∪ share with_{d}(t), it follows from Lemma 63 that

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

From this, by using (66), we obtain

yσ ∉ vars(xσ) ∪ vars(tσ).  (67)

By using either (67), if y ∉ dom(σ), or the fact that σ ∈ VSubst, if y ∈ dom(σ), it follows that

y ∉ vars(xσ) ∪ vars(tσ).  (68)

Thus, by (68), yτ = yν and, by (67), yν = yσ, so that yτ = yσ and y ∈ fvars(τ).

C.3 The Correctness for Linearity

Lemma 66 Let σ ∈ VSubst and y ∈ dom(σ). If y ∈ lvars(σ) \ gvars(σ) then y ∉ vars(yσ).

Proof. Suppose, by contraposition, that y ∈ vars(yσ). Since σ ∈ VSubst and y ∈ lvars(σ), by Proposition 42 we have

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

Therefore y ∈ gvars(σ), contradicting the assumption.

The following simple consequence of Proposition 16 will be used in the sequel.

Lemma 67 If σ ∈ RSubst then fvars(σ) ∪ gvars(σ) ⊆ lvars(σ).

Proof. Let y ∈ fvars(σ)∪gvars(σ). It follows from Proposition 16 that we have rt(y, σ) ∈ Vars ∪ GTerms. However, Vars ∪ GTerms ⊂ LTerms so that, again by Proposition 16, y ∈ lvars(σ).

Proposition 68 Let d ∈ SFL, σ ∈ γ_{S}(d) ∩ VSubst and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI and y ∈ dom(σ) ∩ range(σ) implies y ∈ vars(yσ). Suppose that {r, r′} = {x, t} and lin_{d}(r) holds. For all τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, we have

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

Proof. We assume that the congruence and identity axioms hold. Note that if σ ∪ {x = t} is not satisfiable, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (69) holds.

Since lin_{d}(r) holds, then vars(r) ⊆ lvars(σ). Thus, by Proposition 42,

∀v ∈ vars(rσ) \ dom(σ) : occ lin(v, rσ),  (70)
vars(rσ) ∩ dom(σ) ⊆ gvars(σ).  (71)

Therefore, by defining V_{σ} =^{def} Vars \ gvars(σ), we obtain that the term rσ is V_{σ}-linear. Let

{u_{1}, …, u_{k}} =^{def} dom(σ) ∩ (vars(xσ) ∪ vars(tσ)),
s̄ =^{def} (u_{1}, …, u_{k}, rσ),

t̄ =^{def} (u_{1}σ, …, u_{k}σ, r′σ).

Since rσ is V_{σ}-linear it follows from (71) that s̄ is V_{σ}-linear. By Lemma 51 and the congruence axioms, σ ∪ {x = t} ⟹ s̄ = t̄. Thus, as σ ∪ {x = t} is satisfiable, there exists μ ∈ mgs(s̄ = t̄). Let V_{μ} = Vars \ gvars(μ); since gvars(σ) ⊆ gvars(μ), then V_{μ} ⊆ V_{σ} and s̄ is also V_{μ}-linear. Therefore, we can apply Lemma 54 so that there exists μ ∈ mgs(s̄ = t̄) such that, for all w ∈ W =^{def} Vars \ vars(s̄),

wμ is V_{μ}-linear;  (72)
vars(wμ) ∩ dom(μ) ⊆ gvars(μ);  (73)
∀w′ ∈ W : w ≠ w′ ⟹ vars(wμ) ∩ vars(w′μ) ⊆ gvars(μ).  (74)

Note that, since σ ∈ VSubst, we have vars(u_{i}σ) ⊆ vars(xσ) ∪ vars(tσ) for each i = 1, …, k. Therefore

vars(μ) ⊆ vars(xσ) ∪ vars(tσ).  (75)

Let ν, τ ⊆ Eqs be defined as

ν =^{def} { z = zσμ | z ∈ dom(σ) \ (vars(xσ) ∪ vars(tσ)) },
τ =^{def} ν ∪ μ.

Then, as σ, μ ∈ RSubst, it follows from (75) that ν and τ have no identities or circular subsets so that ν, τ ∈ RSubst. By applying Lemma 51, we obtain τ ∈ mgs(σ ∪ {x = t}).

Suppose y ∈ lvars(σ) \ share with_{d}(r). Then we show that y ∈ lvars(τ). If y ∈ gvars(σ) then y ∈ gvars(τ). Thus, by Lemma 67, y ∈ lvars(τ).

Therefore, for the rest of the proof, we assume y ∈ lvars(σ) \ gvars(σ). Thus, by Lemma 66, we have y ∈ dom(σ) implies y ∉ vars(yσ) so that, by the hypothesis,

y ∉ dom(σ) ∩ range(σ).  (76)

As y ∈ lvars(σ), by Proposition 42,

∀v ∈ vars(yσ) \ dom(σ) : occ lin(v, yσ),  (77)
vars(yσ) ∩ dom(σ) ⊆ gvars(σ).  (78)

As y ∉ share with_{d}(r), by Definition 20 and Theorem 21, we have vars(yσ)∩ vars(rσ) ⊆ gvars(σ), so that, by (78), we obtain

vars(yσ) ∩ vars(s̄) ⊆ gvars(σ).  (79)

We now prove that y ∈ lvars(τ), by showing that

∀v ∈ vars(yτ) \ dom(τ) : occ lin(v, yτ),  (80)
vars(yτ) ∩ dom(τ) ⊆ gvars(τ).  (81)

Since dom(τ) = dom(ν) ∪ dom(μ), we have three cases.

1. Suppose first that y ∉ dom(τ). Then (80) holds because occ lin(y, y) is always true; similarly, (81) is true, because vars(yτ) = {y}.

2. Next, suppose that y ∈ dom(ν), so that yτ = yν = yσμ.

To prove (80) we have to prove, for all w ∈ vars(yσ),

∀v ∈ vars(wμ) \ gvars(τ) : occ lin(v, wμ),  (82)
∀w′ ∈ vars(yσ) \ {w} : vars(wμ) ∩ vars(w′μ) ⊆ gvars(τ).  (83)

We consider two subcases. If w ∈ vars(s̄) then, by (79), w ∈ gvars(σ). This implies w ∈ gvars(τ) and, as a consequence, vars(wμ) ⊆ gvars(τ). Thus, both (82) and (83) hold. Otherwise, if w ∉ vars(s̄), then we have w ∈ W and both (72) and (74) hold. Therefore, since gvars(μ) ⊆ gvars(τ),

(82) follows from (72). As for (83), this follows either from (74), when w′ ∉ vars(s̄), or from (79), when w′ ∈ vars(s̄). In order to prove (73), note that

vars(yσμ) ∩ dom(τ) = ⋃{ vars(wμ) ∩ dom(τ) | w ∈ vars(yσ) }.

We will prove that, for all w ∈ vars(yσ), vars(wμ) ∩ dom(τ) ⊆ gvars(τ). Let w ∈ vars(yσ). Suppose first that w ∈ gvars(σ). As a consequence, w ∈ gvars(τ), which implies vars(wτ) ⊆ gvars(τ). In particular, vars(wτ)∩ dom(τ) ⊆ gvars(τ). Otherwise, let w ∉ gvars(σ) so that, by (78), w ∉ dom(σ). If also w ∉ dom(μ), then w = wμ ∉ dom(τ) and there is nothing to prove. If w ∈ dom(μ), then vars(wμ) ⊆ vars(μ) so that, by (75) and the definition of ν, vars(wμ) ∩ dom(ν) = ∅. Moreover, by (79), we have w ∉ vars(s̄). Thus (73) applies so that, as gvars(μ) ⊆ gvars(τ), vars(wμ)∩ dom(τ) ⊆ gvars(τ).

3. Finally, suppose y ∈ dom(μ), so that yτ = yμ. First, we prove that y ∉ vars(s̄). In fact, by definition of s̄, if y ∈ vars(s̄) then y ∈ vars(rσ) ∪ vars(r′σ). Now, if y ∈ dom(σ), then y ∈ range(σ), therefore contradicting (76). Otherwise, if y ∉ dom(σ), then y ∈ vars(yσ) and, by (79), y ∈ gvars(σ), contradicting our previous assumption. Thus, we have y ∉ vars(s̄), so that y ∈ W and (72) holds. Note that (80) follows because gvars(μ) ⊆ gvars(τ) ⊆ dom(τ), so that vars(yτ)\dom(τ) ⊆ V_{μ}. Similarly, (73) holds and we can obtain (81) by observing that gvars(μ) ⊆ gvars(τ).

Proposition 69 Let d ∈ SFL, σ ∈ γ_{S}(d) ∩ VSubst and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI and y ∈ dom(σ) ∩ range(σ) implies y ∈ vars(yσ). For all τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T, we have

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

Proof. We assume that the congruence and identity axioms hold. Note that if σ ∪ {x = t} is not satisfiable, then the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Lemma 53 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (84) holds.

Let

{u_{1}, …, u_{k}} =^{def} dom(σ) ∩ (vars(xσ) ∪ vars(tσ)),

s̄ =^{def} (u_{1}, …, u_{k}, xσ),
t̄ =^{def} (u_{1}σ, …, u_{k}σ, tσ).

By Lemma 51 and the congruence axioms, σ ∪ {x = t} ⟹ s̄ = t̄. Thus, as σ ∪ {x = t} is satisfiable, there exists μ ∈ mgs(s̄ = t̄). Note that, since σ ∈ VSubst, we have vars(u_{i}σ) ⊆ vars(xσ) ∪ vars(tσ) for each i = 1, …, k. Therefore

vars(μ) ⊆ vars(xσ) ∪ vars(tσ).  (85)

Let ν, τ ⊆ Eqs be defined as

ν =^{def} { z = zσμ | z ∈ dom(σ) \ (vars(xσ) ∪ vars(tσ)) },
τ =^{def} ν ∪ μ.

Then, as σ, μ ∈ RSubst, it follows from (85) that ν and τ have no identities or circular subsets so that ν, τ ∈ RSubst. By applying Lemma 51, we obtain τ ∈ mgs(σ ∪ {x = t}).

Suppose y ∈ lvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t)). Then we show that y ∈ lvars(τ).

If y ∈ gvars(σ) then y ∈ gvars(τ). Thus, by Lemma 67, y ∈ lvars(τ). Therefore, for the rest of the proof, we assume y ∈ lvars(σ) \ gvars(σ). Thus, by Lemma 66, we have y ∈ dom(σ) implies y ∉ vars(yσ) so that, by the hypothesis,

y ∉ dom(σ) ∩ range(σ).  (86)

As y ∈ lvars(σ), by Proposition 42,

∀v ∈ vars(yσ) \ dom(σ) : occ lin(v, yσ),  (87)
vars(yσ) ∩ dom(σ) ⊆ gvars(σ).  (88)

As y ∉ share with_{d}(x) ∪ share with_{d}(t), by Definition 20 and Theorem 21, we have

vars(yσ) ∩ (vars(xσ) ∪ vars(tσ)) ⊆ gvars(σ).  (89)

Moreover, by (85), this implies

vars(yσ) ∩ vars(μ) ⊆ gvars(σ).  (90)

We now prove that y ∈ lvars(τ), by showing that

∀v ∈ vars(yτ) \ dom(τ) : occ lin(v, yτ),  (91)
vars(yτ) ∩ dom(τ) ⊆ gvars(τ).  (92)

Since dom(τ) = dom(ν) ∪ dom(μ), we have three cases.

1. Suppose first that y ∉ dom(τ). Then (91) holds because occ lin(y, y) is always true; similarly, (92) is true, because vars(yτ) = {y}.

2. Next, suppose that y ∈ dom(ν), so that yτ = yν = yσμ.

To prove (91), consider v ∈ vars(yσμ) \ dom(τ). If v ∈ vars(μ) then there exists a variable w ∈ vars(yσ) ∩ vars(μ) such that v ∈ vars(wμ).

By (90), we have w ∈ gvars(σ), which implies w ∈ gvars(τ). Thus, vars(wμ) ⊆ gvars(τ) ⊆ dom(τ), therefore contradicting our assumption that v ∉ dom(τ). Therefore, v ∉ vars(μ), so that v ∈ vars(yσ). Since dom(σ) ⊆ dom(τ), by (87), we have occ lin(v, yσ). Moreover, for all w ∈ vars(yσ)∩dom(μ), we have v ∉ vars(wμ), because v ∉ vars(μ). Thus, we obtain occ lin(v, yσμ).

In order to prove (92), note that

vars(yσμ) ∩ dom(τ) = ⋃{ vars(wμ) ∩ dom(τ) | w ∈ vars(yσ) }.

We will prove that, for all w ∈ vars(yσ), vars(wμ) ∩ dom(τ) ⊆ gvars(τ). Let w ∈ vars(yσ). If w ∈ vars(μ) then, by (90), w ∈ gvars(σ), which implies w ∈ gvars(τ). Thus, we obtain vars(wμ) ⊆ gvars(τ). Otherwise, let w ∉ vars(μ), so that w = wμ. Thus, w ∉ dom(μ). If also w ∉ dom(σ), then w ∉ dom(τ) and there is nothing to prove. If w ∈ dom(σ), by (88), w ∈ gvars(σ), which implies w ∈ gvars(τ). Thus, vars(wμ) ⊆ gvars(τ).

3. Finally, suppose y ∈ dom(μ), so that yτ = yμ. Suppose also that y ∈ vars(xσ) ∪ vars(tσ). Now, if y ∈ dom(σ), then y ∈ range(σ), thus contradicting (86). Otherwise, if y ∉ dom(σ), then y ∈ vars(yσ) and, by (89), y ∈ gvars(σ), contradicting our previous assumption.

Thus, we have y ∉ vars(xσ) ∪ vars(tσ), so that, by (85), we obtain yμ = y. As a consequence, (91) holds trivially. As for (92), this follows from (88) if y ∈ dom(σ), while being trivial if y ∉ dom(σ).

C.4 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 70 Let d = ⟨sh, f, l⟩ ∈ SFL and σ ∈ γ_{S}(d) ∩ VSubst be such that y ∈ dom(σ) ∩ range(σ) implies y ∈ vars(yσ). Let also (x ↦ t) ∈ Bind, where vars(σ) ∪ vars(x ↦ t) ⊆ VI , and suppose there exists τ ∈ mgs(σ ∪ {x = t}) in the syntactic equality theory T. Then τ ∈ γ_{S}(amgu_{S}(d, x ↦ t)).

Proof. Let d′ = ⟨sh′, f′, l′⟩ =^{def} amgu_{S}(d, x ↦ t). Note that, by the existence of σ, τ as specified in the hypotheses, we have both d ≠ ⊥_{S} and d′ ≠ ⊥_{S}. Since σ ∈ γ_{S}(d), it follows from Definition 18 that ssets(σ) ⊆ sh, fvars(σ) ⊇ f and lvars(σ) ⊇ l. Therefore, to prove τ ∈ γ_{S}(d′), we have to show that

ssets(τ) ⊆ sh′,  (93)
fvars(τ) ⊇ f′,  (94)
lvars(τ) ⊇ l′.  (95)

We prove each inclusion separately.

(93). By Definition 22, we have sh′ = cyclic_{x}^{t}(sh_{−} ∪ sh′′). We will show that

ssets(τ) ⊆ sh_{−} ∪ sh′′.  (96)

From this, the thesis will follow by Proposition 61. To prove (96) we need to consider five cases.

1. free_{d}(x) ∨ free_{d}(t) holds.

We can apply Proposition 56, taking r = x when free_{d}(x) holds and r = t when free_{d}(x) does not hold, to conclude that ssets(τ) ⊆ sh′.

2. lin_{d}(x) ∧ lin_{d}(t) holds.

We can apply Proposition 57, obtaining

ssets(τ) ⊆ sh_{−} ∪ bin(sh_{x} ∪ bin(sh_{x}, sh_{xt}^{⋆}), sh_{t} ∪ bin(sh_{t}, sh_{xt}^{⋆})) =^{def} sh′.

3. lin_{d}(x) holds.

We can apply Proposition 59, taking r = x to conclude that

ssets(τ) ⊆ sh_{−} ∪ bin(sh_{x}^{⋆}, sh_{t}) =^{def} sh′.

4. lin_{d}(t) holds. This case is symmetric to the previous one.

5. When nothing is known about x and t, we can apply Theorem 50 to conclude that

ssets(τ) ⊆ sh_{−} ∪ bin(sh_{x}^{⋆}, sh_{t}^{⋆}) =^{def} sh′.

(94). In order to show that fvars(τ) ⊇ f′, according to Definition 22, we consider four cases.

1. free_{d}(x) ∧ free_{d}(t) holds.

By Definition 20, {x, t} ⊆ f ⊆ fvars(σ). Therefore we can apply Proposition 62 (where y is replaced by t ∈ VI ) to conclude that

f′ =^{def} f ⊆ fvars(σ) ⊆ fvars(τ).

2. free_{d}(x) holds.

By Definition 20, x ∈ f ⊆ fvars(σ). Therefore we can apply Proposition 64 to conclude that

f′ =^{def} f \ share with_{d}(x)
⊆ fvars(σ) \ share with_{d}(x)
⊆ fvars(τ).

3. free_{d}(t) holds.

This case is symmetric to the previous one.

4. When nothing is known about x and t, we can apply Proposition 65 to conclude that

f′ =^{def} f \ (share with_{d}(x) ∪ share with_{d}(t))
⊆ fvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t))
⊆ fvars(τ).

(95). In order to show that lvars(τ) ⊇ l′, according to Definition 22, we start by proving lvars(τ) ⊇ l′′. There are four cases that have to be considered.

1. lin_{d}(x) ∧ lin_{d}(t) holds.

We can apply Proposition 68 twice, the first time taking r = x and the second time taking r = t, to conclude that

l′′ =^{def} l \ (share with_{d}(x) ∩ share with_{d}(t))
= (l \ share with_{d}(x)) ∪ (l \ share with_{d}(t))
⊆ (lvars(σ) \ share with_{d}(x)) ∪ (lvars(σ) \ share with_{d}(t))
⊆ lvars(τ).

2. lin_{d}(x) holds.

We can apply Proposition 68 (where we take r = x) to conclude that

l′′ =^{def} l \ share with_{d}(x)
⊆ lvars(σ) \ share with_{d}(x)
⊆ lvars(τ).

3. lin_{d}(t) holds.

This case is symmetric to the previous one.

4. When nothing is known about x and t, we can apply Proposition 69 to conclude that

l′′ =^{def} l \ (share with_{d}(x) ∪ share with_{d}(t))
⊆ lvars(σ) \ (share with_{d}(x) ∪ share with_{d}(t))
⊆ lvars(τ).

Therefore, we have lvars(τ) ⊇ l′′. By (93) proved above, ssets(τ) ⊆ sh′. By Definition 10, VI \ vars(sh′) ⊆ gvars(τ). Moreover, by (94) proved above, we have fvars(τ) ⊇ f′. Thus, by applying Lemma 67 we obtain the thesis:

lvars(τ) ⊇ gvars(τ) ∪ fvars(τ) ∪ lvars(τ)

⊇ (VI \ vars(sh′)) ∪ f′ ∪ l′′

=^{def} l′.

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

Proof of Theorem 23 on page 14. 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 40, 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 70.

D Proofs of the Results of Section 4

We will use results from [3], 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 71 Suppose sh_{1}, sh_{2} ∈ SH . Then, for each (x ↦ t) ∈ Bind,

ρ(sh_{1}) = ρ(sh_{2}) ⟹ ρ(amgu(sh_{1}, x ↦ t)) = ρ(amgu(sh_{2}, x ↦ t)).

Theorem 72 Let sh_{1}, sh_{2} ∈ SH be such that ρ_{PSD}(sh_{1}) ≠ ρ_{PSD}(sh_{2}). Then there exist σ ∈ RSubst such that

ρ_{PSD}(aunify(sh_{1}, σ)) ≠ ρ_{PSD}(aunify(sh_{2}, σ)).

The following result in [3] 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 73 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

ρ(amgu(sh, x ↦ t)) = ρ(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 74 For each V ⊆ VI and sh ∈ SH it holds

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 6, 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 75 For each V, W ⊆ VI and sh ∈ SH it holds

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

Proof. To prove the first 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 6, 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 76 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);  (97)
free_{d_{1}}(t) ⟺ free_{d_{2}}(t);  (98)
ground_{d_{1}}(t) ⟺ ground_{d_{2}}(t);  (99)
occ lin_{d_{1}}(y, t) ⟺ occ lin_{d_{2}}(y, t);  (100)
lin_{d_{1}}(t) ⟺ lin_{d_{2}}(t);  (101)
share with_{d_{1}}(t) = share with_{d_{2}}(t).  (102)

Proof. Consider equivalence (97) and let V = vars(s), W = vars(t). By Definition 20, Lemma 75 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).

The proof of (98) follows easily from Definition 20, since the predicate free_{d_{i}}(t) does not depend on the sharing component sh_{i} of d_{i}.

Consider now (99). By Definition 20, Lemma 74 and the hypothesis, we obtain

ground_{d_{1}}(t) ⟺ vars(t) ⊆ VI \ vars(sh_{1})
⟺ vars(t) ⊆ VI \ vars(rel(VI , sh_{1}))
⟺ vars(t) ⊆ VI \ vars(rel(VI , ρ_{PSD}(sh_{1})))

⟺ vars(t) ⊆ VI \ vars(rel(VI , ρ_{PSD}(sh_{2})))
⟺ vars(t) ⊆ VI \ vars(rel(VI , sh_{2}))
⟺ vars(t) ⊆ VI \ vars(sh_{2})
⟺ ground_{d_{2}}(t).

The proof of (100) follows easily from Definition 20, by applying the equivalences (97) and (99). Similarly, the proof of (101) follows from Definition 20 and (100). Finally, equation (102) follows from Definition 20 and Lemma 74.

Since both ρ (by [22, Theorem 7]) and (·)^{⋆} are upper closure operators it follows that

sh_{1} ⊆ ρ(sh_{2}) ⟺ ρ(sh_{1}) ⊆ ρ(sh_{2}),  (103)
sh_{1} ⊆ sh_{2}^{⋆} ⟺ sh_{1}^{⋆} ⊆ sh_{2}^{⋆}.  (104)

The following lemma needed below is stated and proved as Lemma 19 in [22].

Lemma 77 For each sh_{1}, sh_{2} ∈ SH and each V ∈ ℘_{f}(Vars),

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

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

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}));  (105)
bin(sh_{x,1}, sh_{t,1}^{⋆}) ⊆ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}^{⋆})).  (106)

Proof. Let S =^{def} S_{x} ∪ S_{t} ∈ bin(sh_{x,1}, sh_{t,1}) where S_{x} ∈ sh_{x,1} and S_{t} ∈ sh_{t,1}. Consider an arbitrary variable y ∈ S.

Suppose first that y ∈ S_{x} and let w ∈ W ∩ S_{t}. Since S_{x}, S_{t} ∈ sh_{1}, by hypothesis S_{x}, S_{t} ∈ ρ_{PSD}(sh_{2}). By Definition 6, S = ⋃(A ∪ B), where

A =^{def} { S′ ∈ sh_{2} | {y} ⊆ S′ ⊆ S_{x} },
B =^{def} { S′ ∈ sh_{2} | {w} ⊆ S′ ⊆ S_{t} }.

In particular, we can write A ∪ B = sh′_{−} ∪ sh′_{x} ∪ sh′_{t}, where

sh′_{−} =^{def} \overline{rel}(V ∪ W, A),
sh′_{x} =^{def} rel(V, A),
sh′_{t} =^{def} rel(W, A ∪ B).

Since V ∩ S_{x} ≠ ∅ and v ∈ W ∩ S_{t}, we have sh′_{x} ≠ ∅ and sh′_{t} ≠ ∅. Therefore ⋃(sh′_{x} ∪ sh′_{t}) = ⋃ bin(sh′_{x}, sh′_{t}), so that

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

By construction, we have {y} ⊆ S′ ⊆ S for all S′ ∈ A. Thus, it also holds {y} ⊆ S′ ⊆ S for all S′ ∈ sh′_{−} ∪ bin(sh′_{x}, sh′_{t}), so that

S = ⋃{ S′ ∈ sh′_{−} ∪ bin(sh′_{x}, sh′_{t}) | {y} ⊆ S′ ⊆ S }.

By a symmetric argument, the same conclusion can be obtained when y ∈ S_{t}. As the choice of y was arbitrary, by Definition 6,

S ∈ ρ_{PSD}(sh′_{−} ∪ bin(sh′_{x}, sh′_{t})).  (107)

Note that sh′_{−} ⊆ sh_{−,2}, sh′_{x} ⊆ sh_{x,2} and sh′_{t} ⊆ sh_{t,2}, so that it holds

sh′_{−} ∪ bin(sh′_{x}, sh′_{t}) ⊆ sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}).

Then, (105) follows from (107) by the monotonicity of ρ_{PSD}.

To prove (106), let S =^{def} S_{x} ∪ T_{t} ∈ bin(sh_{x,1}, sh_{t,1}^{⋆}), where S_{x} ∈ sh_{x,1} and T_{t} ∈ sh_{t,1}^{⋆}. Consider an arbitrary variable y ∈ S.

Suppose that y ∈ S_{x}. Since S_{x} ∈ sh_{1}, by hypothesis S_{x} ∈ ρ_{PSD}(sh_{2}), so that by Definition 6 we have S = ⋃(A ∪ {T_{t}}), where

A =^{def} { S′ ∈ sh_{2} | {y} ⊆ S′ ⊆ S_{x} }.

In particular, we can write S = ⋃(sh′_{−} ∪ sh′_{x} ∪ sh′_{t}), where

sh′_{−} =^{def} \overline{rel}(V ∪ W, A),
sh′_{x} =^{def} rel(V, A),
sh′_{t} =^{def} rel(W, A) ∪ {T_{t}}.

Since V ∩ S_{x} ≠ ∅, we have sh′_{x} ≠ ∅. Since it also holds sh′_{t} ≠ ∅, we have ⋃(sh′_{x} ∪ sh′_{t}) = ⋃ bin(sh′_{x}, sh′_{t}), so that

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

By construction, we have {y} ⊆ S′ ⊆ S for all S′ ∈ A. Thus, it also holds {y} ⊆ S′ ⊆ S for all S′ ∈ sh′_{−} ∪ bin(sh′_{x}, sh′_{t}), so that

S = ⋃{ S′ ∈ sh′_{−} ∪ bin(sh′_{x}, sh′_{t}) | {y} ⊆ S′ ⊆ S }.  (108)

Suppose now that y ∈ T_{t} and let v ∈ V ∩ S_{x}. Since S_{x} ∈ sh_{1} ⊆ ρ_{PSD}(sh_{2}), by Definition 6 we have S = ⋃(B ∪ {T_{t}}), where

B =^{def} { S′ ∈ sh_{2} | {v} ⊆ S′ ⊆ S_{x} }.

In particular, we can write S = ⋃(sh′_{−} ∪ sh′_{x} ∪ sh′_{t}), where

sh′_{−} =^{def} ∅,

sh′_{x} =^{def} rel(V, B) = B,
sh′_{t} =^{def} {T_{t}}.

Since v ∈ V ∩ S_{x}, we have sh′_{x} ≠ ∅; since it also holds sh′_{t} ≠ ∅, we obtain ⋃(sh′_{x} ∪ sh′_{t}) = ⋃(bin(sh′_{x}, sh′_{t})). Since y ∈ T_{t} and sh′_{−} = ∅, we have {y} ⊆ S′ ⊆ S for all S′ ∈ sh′_{−} ∪ bin(sh′_{x}, sh′_{t}), so that (108) holds even in this case.

As the choice of y was arbitrary, by (108) and Definition 6,

S ∈ ρ_{PSD}(sh′_{−} ∪ bin(sh′_{x}, sh′_{t})).  (109)

Clearly, sh′_{−} ⊆ sh_{−,2} and sh′_{x} ⊆ sh_{x,2}; also, by Lemma 77, T_{t} ∈ sh_{t,2}^{⋆}, so that sh′_{t} ⊆ sh_{t,2}^{⋆}. Thus, sh′_{−} ∪ bin(sh′_{x}, sh′_{t}) ⊆ sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}^{⋆}). The thesis (106) follows from (109) by the monotonicity of ρ_{PSD}.

Lemma 79 Let sh ∈ SH and V, W ⊆ VI . Let also sh_{x} =^{def} rel(V, sh), sh_{t} =^{def} rel(W, sh), sh_{xt} =^{def} sh_{x} ∩ sh_{t} and

sh^{⋄} =^{def} 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, since sh_{xt} ⊆ sh_{x} and sh_{xt} ⊆ sh_{t},

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}^{⋆}).  (110)

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})).  (111)

Let S ∈ sh^{⋄}. Then, by (110), S = S_{x} ∪ S_{t} ∪ T_{xt}, where S_{x} ∈ sh_{x}, S_{t} ∈ sh_{t}, 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.

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

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

Suppose first that y ∈ S_{x}. Then, since

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

it follows that (112) holds. By a similar argument, (112) holds also when y ∈ S_{t}, by taking

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

On the other hand, suppose now y ∉ S_{x} ∪ S_{t}, so that k > 0 and there exists j ∈ {1, …, k} such that y ∈ T_{j}. In this case we have

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

so that, since T_{j} ∈ sh_{xt}, (112) still holds.

As the choice of y ∈ S was arbitrary, by (112) and Definition 6 it follows S ∈ ρ_{PSD}(bin(sh_{x}, sh_{t})). Thus, by monotonicity and idempotence of ρ_{PSD}, (111) holds.

Lemma 80 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}));  (113)
bin(sh_{x}^{⋆}, sh_{W}) = cyclic_{x}^{t}(bin(sh_{x}^{⋆}, sh_{t}));  (114)
bin(sh_{x}^{⋆}, sh_{W}^{⋆}) = cyclic_{x}^{t}(bin(sh_{x}^{⋆}, sh_{t}^{⋆})).  (115)

Proof. We start by proving equations (113) and (114) at the same time. Therefore, let sh′_{x} ∈ {sh_{x}, sh_{x}^{⋆}}.

To prove the first inclusions (⊆), we assume S ∈ bin(sh′_{x}, sh_{W}) and show that S ∈ cyclic_{x}^{t}(bin(sh′_{x}, sh_{t})). Since sh_{W} ⊆ sh_{t}, we have S ∈ bin(sh′_{x}, sh_{t}). Moreover, S = S_{x} ∪ S_{W}, where x ∈ S_{x} and W ∩ S_{W} ≠ ∅. Thus W ∩ S ≠ ∅ and 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 and, by Definition 20, S ∈ rel(W, sh). If vars(t) ∩ S_{t} ≠ {x}, then S_{t} ∈ sh_{W} and S ∈ bin(sh′_{x}, sh_{W}), so that the two inclusions hold. Otherwise, let vars(t)∩S_{t} = {x}, so that S_{t} ∈ sh′_{x} and S_{t} ∉ sh_{W}. Since we know S ∈ rel(W, sh), there exists w ∈ W ∩ S_{x}, so that S_{x} ∈ sh_{W}. First, consider the case when sh′_{x} = sh_{x}. Then S_{t} ∈ sh_{x} and we have S ∈ bin(sh_{x}, sh_{W}), proving the second inclusion for (113). Secondly, consider the case when sh′_{x} = sh_{x}^{⋆}. Then we can write S_{x} = S_{W} ∪ S_{x}, where S_{W} ∈ sh_{W}. Thus S = (S_{x}∪S_{t})∪S_{W} ∈ bin(sh_{x}^{⋆}, sh_{W}), proving the second inclusion for (114).

Finally, we prove equation (115).

To prove the first inclusion (⊆), we assume S ∈ bin(sh_{x}^{⋆}, sh_{W}^{⋆}) and show that S ∈ cyclic_{x}^{t}(bin(sh_{x}^{⋆}, sh_{t}^{⋆})). As sh_{W} ⊆ sh_{t}, we have S ∈ bin(sh_{x}^{⋆}, sh_{t}^{⋆}). Moreover, S = S_{x} ∪ S_{W}, where x ∈ S_{x} and W ∩ S_{W} ≠ ∅. Thus W ∩ S ≠ ∅ and hence, 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, we have 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, S ∈ rel(W, sh). Suppose first that vars(t) ∩ S_{t} ≠ {x}. 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}^{⋆}). Suppose next that vars(t) ∩ S_{t} = {x}, so that S_{t} ∈ sh_{x}^{⋆} W ∩ S_{x} ≠ ∅. Then S_{x} = S_{W} ∪ S_{x}, where S_{W} ∈ sh_{W}^{⋆}. Thus S = (S_{x} ∪ S_{t}) ∪ S_{W} ∈ bin(sh_{x}^{⋆}, sh_{W}^{⋆}), completing the proof.

For the next theorem, we will use the following lemma corresponding to Lemmas 18 in [3].

Lemma 81 For each sh ∈ SH and V ∈ ℘_{f}(Vars), \overline{rel}(V, ρ(sh)) = ρ(\overline{rel}(V, sh)).

Theorem 82 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 of ρ_{PSD} on SFL, it holds d_{2} = ⟨sh_{2}, f, l⟩, where ρ_{PSD}(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:

ρ_{PSD}(sh′_{1}) = ρ_{PSD}(sh′_{2}),  (116)
f′_{1} = f′_{2},  (117)
l′_{1} = l′_{2}.  (118)

Equation (116). We will prove the result

sh_{1} ⊆ ρ_{PSD}(sh_{2}) ⟹ sh′_{1} ⊆ ρ_{PSD}(sh′_{2}).  (119)

Then, by using (104), we obtain

ρ_{PSD}(sh_{1}) ⊆ ρ_{PSD}(sh_{2}) ⟹ ρ_{PSD}(sh′_{1}) ⊆ ρ_{PSD}(sh′_{2}),

from which the thesis follows by symmetry.

Let W = vars(t) \ {x}. For each i ∈ {1, 2}, let

sh_{−,i} = \overline{rel}(\{x\} ∪ vars(t), sh_{i}),
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_{W,i} = rel(W, sh_{i}).

To prove (119), assume that sh_{1} ⊆ ρ_{PSD}(sh_{2}). By Definitions 22 and 20, for each i = 1, 2 we have

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

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

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

Thus, by Lemma 81, 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})). By applying cases (98) and (101) of Lemma 76, it can be seen that sh′′_{1} and sh′′_{2} are each computed by selecting the same alternative branch of Definition 22. 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 (113) of Lemma 80, cyclic_{x}^{t}(sh′′_{i}) = bin(sh_{x,i}, sh_{W,i}), for each i = 1, 2. Thus, by case (105) of Lemma 78, where we take V = {x},

bin(sh_{x,1}, sh_{W,1}) ⊆ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{W,2})),

from which the thesis follows.

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 suppose that x ∉ vars(t), so that cyclic_{x}^{t}(sh′′_{i}) = sh′′_{i}. Then, by Lemma 79, for each i = 1, 2, we have sh′′_{i} ⊆ ρ_{PSD}(bin(sh_{x,i}, sh_{t,i})). Therefore, by case (105) of Lemma 78 and the monotonicity of ρ_{PSD}, we obtain

sh′′_{1} ⊆ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2})),

so that the thesis holds. 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 (114) of Lemma 80, cyclic_{x}^{t}(sh′′_{i}) = bin(sh_{x,i}^{⋆}, sh_{W,i}). Thus, by case (106) of Lemma 78, where we take V = {x}, we obtain

sh′′_{1} ⊆ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}^{⋆}, sh_{W,2})),

so that the thesis holds.

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, by case (106) of Lemma 78, where we exchange the usual roles of V and W, we obtain

sh′′_{1} ⊆ ρ_{PSD}(sh_{−,2} ∪ bin(sh_{x,2}, sh_{t,2}^{⋆})),

so that the thesis holds.

5. In the fifth case we have, for i = 1, 2, sh′′_{i} = bin(sh_{x,i}^{⋆}, sh_{t,i}^{⋆}). By case (115) of Lemma 80, cyclic_{x}^{t}(sh′′_{i}) = bin(sh_{x,i}^{⋆}, sh_{W,i}^{⋆}). The thesis follows from Theorem 71, by replacing the term t by an arbitrary term t′ ∈ HTerms such that vars(t′) = W.

Equation (117). Consider the computation of f′_{i} as specified in Definition 22. By applying case (98) of Lemma 76, 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 (102) of Lemma 76.

Equation (118). Consider the computation of l′_{i} as specified in Definition 22: for each i ∈ {1, 2} we have

l′_{i} = (VI \ vars(sh′_{i})) ∪ f′_{i} ∪ l′′_{i}.

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 (116), we know that ρ_{PSD}(sh′_{1}) = ρ_{PSD}(sh′_{2}); thus, by case (102) of Lemma 76, we obtain vars(sh′_{1}) = vars(sh′_{2}). By equation (117), we also know that f′_{1} = f′_{2}. Therefore, to complete the proof, we only need to prove that l′′_{1} = l′′_{2}. Consider the computation of l′′_{i} as specified in Definition 22. By case (101) of Lemma 76, it can be seen that, in the computations of l′′_{1} and l′′_{2}, the same alternative branch is selected. Hence, the thesis is obtained by applying case (102) of Lemma 76.

Theorem 83 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 82, we have

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

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 (120), we can apply the inductive hypothesis and conclude the proof, since |bs′| = m − 1 < m.

For the next theorem, we will use the following lemma, corresponding to Lemma 24 in [3].

Lemma 84 Let sh_{1}, sh_{2} ∈ SH be such that ρ_{PSD}(sh_{1}) = ρ_{PSD}(sh_{2}). Then, for each V ⊆ VI ,

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

Theorem 85 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 also have ρ_{PSD}(sh_{1}) = ρ_{PSD}(sh_{2}), f_{1} = f_{2} and l_{1} = l_{2}. Thus, to complete the proof, we only need to show that

ρ_{PSD}(aexists(sh_{1})) = ρ_{PSD}(aexists(sh_{2})).

This follows from Lemma 84.

Proof of Theorem 30 on page 18. The congruence properties for aunify_{S} and aexists_{S} follow from Theorems 83 and 85, respectively. The congruence property for alub_{S} holds, as usual, because ρ_{PSD} is an upper closure operator.

Proof of Theorem 31 on page 19. Suppose ρ_{PSD}(d_{1}) ≠ ρ_{PSD}(d_{2}). By Definition 29, we have three cases:

1. Suppose ρ_{PSD}(sh_{1}) ≠ ρ_{PSD}(sh_{2}). Let t be a ground and finite term and let

σ =^{def} { x ↦ t | x ∈ VI \ S }.

Since σ binds all of its domain variables to terms that are ground and finite, then no binary union and/or star-union needs to be computed. As a consequence, the behavior of amgu_{S} on the sharing component is the same as the behavior of ‘amgu’. The proof therefore follows from Theorem 72.

2. Suppose now f_{1} ≠ f_{2}. In this case, by taking ρ = ρ_{F} and bs = ϵ, we obtain

ρ_{F} (aunify_{S}(d_{1}, ϵ)) = ρ_{F} (d_{1})

= ⟨SG, f_{1}, ∅⟩ ≠ ⟨SG, f_{2}, ∅⟩ = ρ_{F} (d_{2})

= ρ_{F} (aunify_{S}(d_{2}, ϵ)).

3. Finally, suppose l_{1} ≠ l_{2}. Similarly to the previous case, by taking ρ = ρ_{L} and bs = ϵ, we obtain

ρ_{L}(aunify_{S}(d_{1}, ϵ)) = ρ_{L}(d_{1})

= ⟨SG, ∅, l_{1}⟩ ≠ ⟨SG, ∅, l_{2}⟩ = ρ_{L}(d_{2})

= ρ_{L}(aunify_{S}(d_{2}, ϵ)).

Proof of Theorem 32 on page 19. Suppose first that x ∉ vars(t). Then it holds

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

so that the thesis is a simple corollary of Lemma 79, where V = {x} and W = vars(t).

Suppose now x ∈ vars(t). Then we have sh_{x} = sh_{xt}, so that sh^{⋄} = bin(sh_{x}^{⋆}, sh_{t}). In this case the thesis is a corollary of Theorem 73.