Finite-Tree Analysis

for Constraint Logic-Based Languages^{⋆}

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

1 Department of Mathematics, University of Parma, Italy.

               {bagnara,zaffanella}@cs.unipr.it

2 Department of Computer Science, University of Pisa, Italy.

                       gori@di.unipi.it

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

                    hill@comp.leeds.ac.uk

Abstract. Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the omission of the occurs-check) and increased expressivity. Note that cyclic terms can provide a very efficient representation of grammars and other useful objects. Unfortunately, the use of infinite rational trees has problems. For instance, many of the built-in and library predicates are ill-defined for such trees and need to be supplemented by run-time checks whose cost may be significant. Moreover, some widelyused program analysis and manipulation techniques are only correct for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of those program variables (the finite variables) that, at the program points of interest, will always be bound to finite terms. For these reasons, we propose here a new data-flow analysis that captures such information. We present a parametric domain where a simple component for recording finite variables is coupled with a generic domain (the parameter of the construction) providing sharing information. The sharing domain is abstractly specified so as to guarantee the correctness of the combined domain and the generality of the approach.

1 Introduction

The intended computation domain of most logic-based languages^{1} includes the algebra (or structure) of finite trees. Other (constraint) logic-based languages, such as Prolog II and its successors [9, 11], SICStus Prolog [34], and Oz [32], refer to a computation domain of rational trees. A rational tree is a possibly infinite tree with a finite number of distinct subtrees and, as is the case for finite trees,

⋆ This work has been partly supported by MURST project “Certificazione automatica di programmi mediante interpretazione astratta.” Some of this work was done during visits of the fourth author to Leeds, funded by EPSRC under grant M05645.

1 That is, ordinary logic languages, (concurrent) constraint logic languages, functional logic languages and variations of the above.

where each node has a finite number of immediate descendants. These properties will ensure that rational trees, even though infinite in the sense that they admit paths of infinite length, can be finitely represented. One possible representation makes use of connected, rooted, directed and possibly cyclic graphs where nodes are labeled with variable and function symbols as is the case of finite trees.

Applications of rational trees in logic programming include graphics [16], parser generation and grammar manipulation [9, 19], and computing with finitestate automata [9]. Other applications are described in [18] and [21]. Going from Prolog to CLP, [29] combines constraints on rational trees and record structures, while the logic-based language Oz allows constraints over rational and feature trees [32]. The expressive power of rational trees is put to use, for instance, in several areas of natural language processing. Rational trees are used in implementations of the HPSG formalism (Head-driven Phrase Structure Grammar) [30], in the ALE system (Attribute Logic Engine) [7], and in the ProFIT system (Prolog with Features, Inheritance and Templates) [17].

While rational trees allow for increased expressivity, they also come equipped with a surprising number of problems. As we will see, some of these problems are so serious that rational trees must be used in a very controlled way, disallowing them in any context where they are “dangerous”. This, in turn, causes a secondary problem: in order to disallow rational trees in selected contexts one must first detect them, an operation that may be expensive.

The first thing to be aware of is that almost any semantics-based program manipulation technique developed in the field of logic programming —whether it be an analysis, a transformation, or an optimization— assumes a computation domain of finite trees. Some of these techniques might work with the rational trees but their correctness has only been proved in the case of finite trees. Others are clearly inapplicable. Let us consider a very simple Prolog program:

                     list([]).
                     list([ |T]) :- list(T).

Most automatic and semi-automatic tools for proving program termination and for complexity analysis agree on the fact that list/1 will terminate when invoked with a ground argument. Consider now the query

                     ?- X = [a|X], list(X).

and note that, after the execution of the first rational unification, the variable X will be bound to a rational term containing no variables, i.e., the predicate list/1 will be invoked with X ground. However, if such a query is given to, say, SICStus Prolog, then the only way to get the prompt back is by pressing ^C. The problem stems from the fact that the analysis techniques employed by these tools are only sound for finite trees: as soon as they are applied to a system where the creation of cyclic terms is possible, their results are inapplicable. The situation can be improved by combining these termination and/or complexity analyses by a finiteness analysis providing the precondition for the applicability of the other techniques.

The implementation of built-in predicates is another problematic issue. Indeed, it is widely acknowledged that, for the implementation of a system that provides real support for the rational trees, the biggest effort concerns proper handling of built-ins. Of course, the meaning of ‘proper’ depends on the actual built-in. Built-ins such as copy_term/2 and ==/2 maintain a clear semantics when passing from finite to rational trees. For others, like sort/2, the extension can be questionable:^{2} both raising an exception and answering Y = [a] can be argued to be “the right reaction” to the query

                    ?- X = [a|X], sort(X, Y).

Other built-ins do not tolerate infinite trees in some argument positions. A good implementation should check for finiteness of the corresponding arguments and make sure “the right thing” —failing or raising an appropriate exception— always happens. However, such behavior appears to be uncommon. A small experiment we conducted on six Prolog implementations with queries like

                    ?- X = 1+X, Y is X.
                    ?- X = [97|X], name(Y, X).
                    ?- X = [X|X], Y =.. [f|X].

resulted in infinite loops, memory exhaustion and/or system thrashing, segmentation faults or other fatal errors. One of the implementations tested, SICStus Prolog, is a professional one and implements run-time checks to avoid most cases where built-ins can have catastrophic effects.^{3} The remaining systems are a bit more than research prototypes, but will clearly have to do the same if they evolve to the stage of production tools. Again, a data-flow analysis aimed at the detection of those variables that are definitely bound to finite terms would allow to avoid a (possibly significant) fraction of the useless run-time checks. Note that what has been said for built-in predicates applies to libraries as well. Even though it may be argued that it is enough for programmers to know that they should not use a particular library predicate with infinite terms, it is clear that the use of a “safe” library, including automatic checks which ensure that such predicates are never called with an illegal argument, will result in more robust systems. With the appropriate data-flow analyses, safe libraries do not have to be inefficient libraries.

Another serious problem is the following: the ISO Prolog standard term ordering cannot be extended to rational trees [M. Carlsson, Personal communication, October 2000]. Consider the rational trees defined by A = f(B, a) and B = f(A, b). Clearly, A == B does not hold. Since the standard term ordering is total, we must have either A @< B or B @< A. Assume A @< B. Then f(A, b) @< f(B, a), since the ordering of terms having the same principal functor is inherited by the ordering of subterms considered in a left-to-right fashion. Thus B @< A must hold, which is a contradiction. A dual contradiction

2 Even though sort/2 is not required to be a built-in by the standard, it is offered as

such by several implementations. 3 SICStus 3.8.5 still loops on ?- X = [97|X], name(Y, X).

is obtained by assuming B @< A. As a consequence, applying one of the Prolog term-ordering predicates to one or two infinite terms may cause inconsistent results, giving rise to bugs that are exceptionally difficult to diagnose. For this reason, any system that extends ISO Prolog with rational trees ought to detect such situations and make sure they are not ignored (e.g., by throwing an exception or aborting execution with a meaningful message). However, predicates such as the term-ordering ones are likely to be called a significant number of times, since they are often used to maintain structures implementing ordered collections of terms. This is another instance of the efficiency issue mentioned above.

In this paper, we present a parametric abstract domain for finite-tree analysis, denoted by H × P. This domain combines a simple component H (the finiteness component), recording the set of definitely finite variables, with a generic domain P (the parameter of the construction), providing sharing information. The term “sharing information” is to be understood in its broader meaning, which includes variable aliasing, groundness, linearity, freeness and any other kind of information that can improve the precision on these components, such as explicit structural information. Several domain combinations and abstract operators, characterized by different precision/complexity trade-offs, have been proposed to capture these properties (see [4] for an account of some of them). By giving a generic specification for this parameter component, it is possible to define and establish the correctness of the abstract operators on the finite-tree domain independently from any particular domain for sharing analysis.

The paper is structured as follows. The required notations and preliminary concepts are given in Section 2. The finite-tree domain is then introduced in Section 3: Section 3.1 provides the specification of the parameter domain P; Section 3.2 defines the abstraction function for the finiteness component H ; Section 3.3 defines the abstract unification operator for H ×P. A brief description of some ongoing work on the subject is given in Section 4. We conclude in Section 5.

2 Preliminaries

2.1 Infinite Terms and Substitutions

For a set S, ℘(S) is the powerset of S, whereas ℘_{f}(S) is the set of all the finite subsets of S. Let Sig denote a possibly infinite set of function symbols, ranked over the set of natural numbers. It is assumed that Sig contains at least two distinct function symbols, one having rank 0 (so that there exist finite ground terms) and one having rank greater than 0 (so that there exist infinite terms). 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).

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. If a occurs more than once in a multiset M we write a M.

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.

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

If t ∈ HTerms, we write tσ to denote σ(t) and 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(σ) }.

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, 27]. 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 ↦ t can map a domain variable x into a term t ∈ Terms \ HTerms.

2.2 Equations

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

Some logic-based languages, such as Prolog II, SICStus and Oz, are based on RT , the theory of rational trees [9, 10]. This is a syntactic equality theory (i.e., a theory where the function symbols are uninterpreted), augmented with a uniqueness axiom for each substitution in rational solved form. Informally speaking these axioms 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. Thus, any set of equations in rational solved form is, by definition, satisfiable in RT . 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. We refer the interested reader to [25, 26, 28] for details on the subject.

Given a set of equations e ∈ ℘_{f}(Eqs) that is satisfiable in RT , a substitution σ ∈ RSubst is called a solution for e in RT if RT ⊢ ∀(σ → e). If in addition vars(σ) ⊆ vars(e), then σ is said to be a relevant solution for e. Finally, σ is a most general solution for e in RT if RT ⊢ ∀(σ ↔ e). In this paper, the set of all the relevant most general solution for e in RT will be denoted by mgs(e).

2.3 The Concrete Domain

Throughout the paper, we assume a knowledge of the basic concepts of abstract interpretation theory [13, 14].

For the purpose of this paper, we assume a concrete domain constituted by pairs of the form (Σ, V), where V is a finite set of variables of interest and Σ is a (possibly infinite) set of substitutions in rational solved form.

Definition 1. (The concrete domain.) Let D^{♭} =^{def} ℘(RSubst) × ℘_{f}(Vars). If (Σ, V) ∈ D^{♭}, then (Σ, V) represents the (possibly infinite) set of first-order formulas { ∃Δ . σ | σ ∈ Σ, Δ = vars(σ)\V } where σ is interpreted as the logical conjunction of the equations corresponding to its bindings.

Concrete domains for constraint languages would be similar. If the analyzed language allows the use of constraints on various domains to restrict the values of the variable leaves of rational trees, the corresponding concrete domain would have one or more extra components to account for the constraints (see [2] for an example).

The concrete element ({{x ↦ f(y)}}, {x, y}) expresses a dependency between x and y. In contrast, ({{x ↦ f(y)}}, {x}) only constrains x. The same concept can be expressed by saying that in the first case the variable name ‘y’ matters, but it does not in the second case. Thus, the set of variables of interest is crucial for defining the meaning of the concrete and abstract descriptions. Despite this, always specifying the set of variables of interest would significantly clutter the presentation. Moreover, most of the needed functions on concrete and abstract descriptions, preserve the set of variables of interest. For these reasons, we assume the existence of a set VI ∈ ℘_{f}(Vars) that contains, at each stage of the analysis, the current variables of interest.^{4} As a consequence, when the context makes it clear that Σ ∈ ℘(RSubst), we will write Σ ∈ D^{♭} as a shorthand for (Σ, VI ) ∈ D^{♭}.

3 An Abstract Domain for Finiteness Analysis

Finite-tree analysis applies to logic-based languages computing over a domain of rational trees where cyclic structures are allowed. In contrast, analyses aimed at occurs-check reduction [15, 33] apply to programs that are meant to compute on a domain of finite trees only, but have to be executed over systems that are either designed for rational trees or intended just for the finite trees but omit the occurs-check for efficiency reasons. Despite their different objectives, finite-tree and occurs-check analyses have much in common: in both cases, it is important to detect all program points where cyclic structures can be generated.

Note however that, when performing occurs-check reduction, one can take advantage of the following invariant: all data structures generated so far are finite. This property is maintained by transforming the program so as to force finiteness whenever it is possible that a cyclic structure could have been built.^{5}

4 This parallels what happens in the efficient implementation of data-flow analyzers. In fact, almost all the abstract domains currently in use do not need to represent explicitly the set of variables of interest. In contrast, this set is maintained externally and in a unique copy, typically by the fixpoint computation engine.

5 Such a requirement is typically obtained by replacing the unification with a call to unify with occur check/2. As an alternative, in some systems based on rational trees it is possible to insert, after each problematic unification, a finiteness test for the generated term.

In contrast, a finite-tree analysis has to deal with the more general case when some of the data structures computed so far may be cyclic. It is therefore natural to consider an abstract domain made up of two components. The first one simply represents the set of variables that are guaranteed not to be bound to infinite terms. We will denote this finiteness component by H (from Herbrand).

Definition 2. (The finiteness component.) The finiteness component is the set H =^{def} ℘(VI ) partially ordered by reverse subset inclusion.

The second component of the finite-tree domain should maintain any kind of information that may be useful for computing and possibly propagating finiteness information.

It is well-known that sharing information as a whole, therefore including possible variable aliasing, definite linearity, and definite freeness, has a crucial role in occurs-check reduction so that, as observed before, it can be exploited for finite-tree analysis too. Thus, a first choice for the second component of the finite-tree domain would be to consider one of the standard combinations of sharing, freeness and linearity as defined, e.g., in [4, 5, 20]. However, this would tie our specification to a particular sharing analysis domain, whereas the overall approach seems to be inherently more general. For this reason, we will define a finite-term analysis based on the abstract domain schema H × P, where the generic sharing component P is a parameter of the abstract domain construction.

3.1 The parameter component P

Elements of P can encode any kind of information. We only require that substitutions that are equivalent in the theory RT are identified in P.

Definition 3. (The parameter component.) The parameter component P is an abstract domain related to the concrete domain D^{♭} by means of the concretization function γ_{P} : P → ℘(RSubst) such that, for all p ∈ P,

(σ ∈ γ_{P} (p) ∧ (RT ⊢ ∀(σ ↔ τ))) ⟹ τ ∈ γ_{P} (p).

The interface between H and P is provided by a set of predicates and functions that satisfy suitable correctness criteria. Note that, for space limitations, we will only specify those abstract operations that are useful to define abstract unification on the combined domain H × P. The other operations needed for a full description of the analysis, such as renamings, upper bound operators and projections, are very simple and, as usual, do not pose any problems.

Definition 4. (Abstract operators on P.) Let s, t ∈ HTerms be finite terms. For each p ∈ P, we define the following predicates: s and t are independent in p if and only if ind_{p} : HTerms^{2} → Bool holds for (s, t), where

ind_{p}(s, t) ⟹ ∀σ ∈ γ_{P} (p) : vars(rt(s, σ)) ∩ vars(rt(t, σ)) = ∅;

s and t share linearly in p if and only if share lin_{p} : HTerms^{2} → Bool holds for (s, t), where

share lin_{p}(s, t) ⟹ ∀σ ∈ γ_{P} (p) :
∀y ∈ vars(rt(s, σ)) ∩ vars(rt(t, σ)) :
occ lin(y, rt(s, σ)) ∧ occ lin(y, rt(t, σ));

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

ground_{p}(t) ⟹ ∀σ ∈ γ_{P} (p) : rt(t, σ) ∈ GTerms;

t is ground-or-free in p if and only if gfree_{p} : HTerms → Bool holds for t, where

gfree_{p}(t) ⟹ ∀σ ∈ γ_{P} (p) : rt(t, σ) ∈ GTerms ∨ rt(t, σ) ∈ Vars;

s and t are or-linear in p if and only if or lin_{p} : HTerms^{2} → Bool holds for (s, t), where

or lin_{p}(s, t) ⟹ ∀σ ∈ γ_{P} (p) : rt(s, σ) ∈ LTerms ∨ rt(t, σ) ∈ LTerms;

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

lin_{p}(s) ⟺^{def} or lin_{p}(s, s).

For each p ∈ P, the following functions compute subsets of the set of variables of interest: the function share same var_{p} : HTerms × HTerms → ℘(VI ) returns a set of variables that may share with the given terms via the same variable. For each s, t ∈ HTerms,

share same var_{p}(s, t) ⊇ \{ y ∈ VI | \begin{matrix}∃σ ∈ γ_{P} (p) . \\ ∃z ∈ vars(rt(y, σ)) . \\ z ∈ vars(rt(s, σ)) ∩ vars(rt(t, σ)) \end{matrix} \};

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

share with_{p}(t) =^{def} { y ∈ VI | y ∈ share same var_{p}(y, t) }.

The function amgu_{P} : P×Bind → P correctly captures the effects of a binding on an element of P. For each (x ↦ t) ∈ Bind and p ∈ P, let

p′ =^{def} amgu_{P} (p, x ↦ t).

For all σ ∈ γ_{P} (p), if τ ∈ mgs(σ ∪ {x = t}), then τ ∈ γ_{P} (p′).

Some of these generic operators can be directly mapped into the corresponding abstract operators defined for well-known sharing analysis domains (e.g., see those defined in [5]). However, the specification given in Definition 4, besides being more general than a particular implementation, also allows for a modular approach when proving correctness results.

3.2 The abstraction function for H

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.^{6} 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 a “good” abstraction function, 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 [12, 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 [22] the sharing-group operator sg of [24] is replaced by an occurrence operator, occ, defined by means of a fixpoint computation. We now provide a similar fixpoint construction defining the finiteness operator.

Definition 5. (Finiteness functions.) For each n ∈ ℕ, the finiteness function hvars_{n}: RSubst → ℘(Vars) is defined, for each σ ∈ RSubst, by

hvars_{0}(σ) =^{def} Vars \ dom(σ)

and, for n > 0, by

hvars_{n}(σ) =^{def} hvars_{n−1}(σ) ∪ { y ∈ dom(σ) | vars(yσ) ⊆ hvars_{n−1}(σ) }.

6 As usual, this is to be intended modulo the possible renaming of variables.

For each σ ∈ RSubst and each i > 0, we have hvars_{i}(σ) ⊆ hvars_{i+1}(σ). Note also that Vars \ hvars_{i}(σ) ⊆ dom(σ) is a finite set. By these two properties, the following fixpoint computation is well defined and finitely computable.

Definition 6. (Finiteness operator.) For each σ ∈ RSubst, the finiteness operator hvars: RSubst → ℘(Vars) is given by

hvars(σ) =^{def} hvars_{ℓ}(σ)

where ℓ =^{def} ℓ(σ) ∈ ℕ is such that hvars_{ℓ}(σ) = hvars_{n}(σ) for all n ≥ ℓ.

The following proposition shows that the hvars operator precisely captures the intended property.

Proposition 1. If σ ∈ RSubst and x ∈ Vars then

x ∈ hvars(σ) ⟺ rt(x, σ) ∈ HTerms.

Example 1. Consider σ ∈ RSubst, where

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

Then,

hvars_{0}(σ) = Vars \ {x_{1}, x_{2}, x_{3}, x_{4}},
hvars_{1}(σ) = Vars \ {x_{1}, x_{3}, x_{4}},
hvars_{2}(σ) = Vars \ {x_{3}, x_{4}}
= hvars(σ).

Thus, x_{1} ∈ hvars(σ), even if vars(x_{1}σ) ⊆ dom(σ).

The abstraction function for H can then be defined in the obvious way.

Definition 7. (The abstraction function for H .) The abstraction function α_{H}: RSubst → H is defined, for each σ ∈ RSubst, by

α_{H}(σ) =^{def} VI ∩ hvars(σ).

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

α_{H}(Σ) =^{def} ⋂{ α_{H}(σ) | σ ∈ Σ }.

Since the abstraction function α_{H} is additive, the concretization function is given by its adjoint [13]:

γ_{H}(h) =^{def} { σ ∈ RSubst | α_{H}(σ) ⊇ h }.

With these definitions, we have the desired result: equivalent substitutions in rational solved form have the same finiteness abstraction.

Theorem 1. If σ, σ′ ∈ RSubst and RT ⊢ ∀(σ ↔ σ′), then α_{H}(σ) = α_{H}(σ′).

3.3 Abstract unification on H × P

The abstract unification for the combined domain H × P is defined by using the abstract predicates and functions as specified for P as well as a new finiteness predicate for the domain H .

Definition 8. (Abstract unification on H × P.) A term t ∈ HTerms is a finite tree in h if and only if the predicate hterm_{h} : HTerms → Bool holds for t, where hterm_{h}(t) =^{def} vars(t) ⊆ h.

The function amgu_{H}: (H × P) × Bind → H captures the effects of a binding on an H element. Let ⟨h, p⟩ ∈ H × P and (x ↦ t) ∈ Bind. Then

amgu_{H}(⟨h, p⟩, x ↦ t) =^{def} h′,

where

h′ =^{def} \begin{cases}h ∪ vars(t), & if hterm_{h}(x) ∧ ground_{p}(x); \\ h ∪ \{x\}, & if hterm_{h}(t) ∧ ground_{p}(t); \\ h, & if hterm_{h}(x) ∧ hterm_{h}(t) \\ & ∧ ind_{p}(x, t) ∧ or lin_{p}(x, t); \\ h, & if hterm_{h}(x) ∧ hterm_{h}(t) \\ & ∧ gfree_{p}(x) ∧ gfree_{p}(t); \\ h \ share same var_{p}(x, t), & if hterm_{h}(x) ∧ hterm_{h}(t) \\ & ∧ share lin_{p}(x, t) \\ & ∧ or lin_{p}(x, t); \\ h \ share with_{p}(x), & if hterm_{h}(x) ∧ lin_{p}(x); \\ h \ share with_{p}(t), & if hterm_{h}(t) ∧ lin_{p}(t); \\ h \ (share with_{p}(x) ∪ share with_{p}(t)), & otherwise. \end{cases}

The abstract unification function amgu: (H × P) × Bind → H × P, for any ⟨h, p⟩ ∈ H × P and (x ↦ t) ∈ Bind, is given by

amgu(⟨h, p⟩, x ↦ t) =^{def} ⟨amgu_{H}(⟨h, p⟩, x ↦ t), amgu_{P} (p, x ↦ t)⟩.

In the computation of h′ (the new finiteness component resulting from the abstract evaluation of a binding) there are eight cases based on properties holding for the concrete terms described by x and t.

1. In the first case, the concrete term described by x is both finite and ground. Thus, after a successful execution of the binding, any concrete term described by t will be finite. Note that t could have contained possibly cyclic variables just before the execution of the binding.

2. The second case is symmetric to the first one. Note that these are the only cases when a “positive” propagation of finiteness information is correct. In contrast, in all the remaining cases, the goal is to limit as much as possible the propagation of “negative” information, i.e., the possible cyclicity of terms.

3. The third case exploits the classical results proved in research work on occurscheck reduction [15, 33]. Accordingly, it is required that both x and t describe finite terms. The use of the implicitly disjunctive predicate or lin_{p} allows for the application of this case even when neither x nor t are known to be definitely linear. For instance, as observed in [15], this may happen when the component P embeds the domain Pos for groundness analysis.^{7}

4. The fourth case exploits the observation that cyclic terms cannot be created when unifying two finite terms that are either ground or free. Ground-or-freeness has been identified in [4] as a safe and inexpensive replacement for the classical freeness property when combining sharing analysis domains.

5. The fifth case applies when unifying a linear and finite term with another finite term possibly sharing with it, provided they can only share linearly (namely, all the shared variables occur linearly in the considered terms). In such a context, cycles could have been introduced by means of the shared variables only. This case shows that, when observing the term finiteness property, set-sharing is strictly more precise than pair-sharing, since a setsharing domain can be strictly more precise when computing the functions share same var_{p} and share lin_{p}.^{8} This is true regardless of the pair-sharing variant considered, including ASub [33, 8], PSD [1, 3] and Sh^{PSh} [31].

6. In the sixth case, we drop the assumption about the finiteness of the term described by t. As a consequence, all variables sharing with x become possibly cyclic. However, provided x describes a finite and linear term, all finite variables independent from x preserve their finiteness.

7. The seventh case is symmetric to the sixth one.

8. The last case states that term finiteness is preserved for all variables that are independent from both x and t. Note that this case is only used when none of the other cases apply.

The following result, together with the assumption on amgu_{P} as specified in Definition 4, ensures that abstract unification on the combined domain H × P is correct.

Theorem 2. Let ⟨h, p⟩ ∈ H ×P and (x ↦ t) ∈ Bind, where {x}∪vars(t) ⊆ VI . Let also σ ∈ γ_{H}(h) ∩ γ_{P} (p) and h′ = amgu_{H}(⟨h, p⟩, x ↦ t). Then

τ ∈ mgs(σ ∪ {x = t}) ⟹ τ ∈ γ_{H}(h′).

7 Take t = y. From the Pos formula ϕ =^{def} (x ∨ y), both ind_{ϕ}(x, y) and or lin_{ϕ}(x, y) can be correctly inferred. Note that from ϕ we cannot infer that x is definitely linear and neither that y is definitely linear.

8 For the expert: on the classical set-sharing domain by Jacobs and Langen [24], we can define share same var_{sh}(x, t) =^{def} vars(rel({x}, sh) ∩ rel(vars(t), sh)). For instance, taking t = y and sh = {{x, y}, {x, z}, {y, z}}, we have z ∉ share same var_{sh}(x, y). In contrast, when using a pair-sharing domain such as PSD, the element sh is equivalent to sh′ = sh ∪ {{x, y, z}}, so that we have z ∈ share same var_{sh}′(x, y). The point is that, in sh, the information provided by the lack of the sharing group {x, y, z} is redundant when observing pair-sharing and groundness, but it is not redundant when observing term finiteness.

4 Ongoing and Further Work

The parametric domain H × P basically captures the negative aspect of termfiniteness, that is, the circumstances under which finiteness can be lost. When a binding has the potential for creating one or more rational terms, the operator amgu_{H} removes from h all the variables that may be bound to non-finite terms. However, term-finiteness has also a positive aspect: there are cases where a variable is guaranteed to be bound to a finite term and this knowledge can be propagated to other variables. Guarantees of finiteness are provided by several

built-ins like unify_with_occurs_check/2, var/1, name/2, all the arithmetic

predicates, and so forth. SICStus Prolog also provides an explicit acyclic/1 predicate.

The term-finiteness information provided by the h component of H × P does not capture the information concerning how finiteness of one variable affects the finiteness of other variables. This kind of information, usually termed relational information, is very important as it allows the propagation of positive finiteness information. An important source of relational information comes from dependencies. Consider the terms t_{1} =^{def} f(x), t_{2} =^{def} g(y), and t_{3} =^{def} h(x, y): it is clear that, for each assignment of rational terms to x and y, t_{3} is finite if and only if t_{1} and t_{2} are so. We can capture this by the Boolean formula t_{3} ↔ (t_{1} ∧ t_{2}). The reasoning is based on the following facts:

1. t_{1}, t_{2}, and t_{3} are finite terms, so that the finiteness of their instances depends only on the finiteness of the terms that take the place of x and y.

2. t_{3} covers both t_{1} and t_{2}, that is, vars(t_{3}) ⊇ vars(t_{1}) ∪ vars(t_{2}); this means that, if an assignment to the variables of t_{3} produces a finite instance of t_{3}, that very same assignment will necessarily result in finite instances of t_{1} and t_{2}. Conversely, an assignment producing non-finite instances of t_{1} or t_{2} will forcibly result in a non-finite instance of t_{3}.

3. Similarly, t_{1} and t_{2}, taken together, cover t_{3}.

The important point to notice is that the indicated dependency will continue to hold for any further simultaneous instantiation of t_{1}, t_{2}, and t_{3}. In other words, such dependencies are preserved by forward computations (since they proceed by consistently instantiating program variables).

Consider the abstract binding x ↦ t where t is a finite term such that vars(t) = {y_{1}, …, y_{n}}. After this binding has been successfully performed, the destinies of x and t concerning term-finiteness are tied together forever. This tie can be described by the dependency formula

x ↔ (y_{1} ∧ ⋯ ∧ y_{n}),  (1)

meaning that x will be bound to a finite term if and only if, for each i = 1, …, n, y_{i} is bound to a finite term. While the dependency expressed by (1) is a correct description of any computation state following the application of the binding x ↦ t, it is not as precise as it could be. Suppose that x and y_{k} are indeed the same variable. Then (1) is logically equivalent to

x → (y_{1} ∧ ⋯ ∧ y_{k−1} ∧ y_{k+1} ∧ ⋯ ∧ y_{n}).  (2)

Correct: whenever x is bound to a finite term, all the other variables will be bound to finite terms. The point is that x has just been bound to a non-finite term, irrevocably: no forward computation can change this. Thus, the implication (2) holds vacuously. The precise and correct description for the state of affairs caused by the cyclic binding is, instead, the negated atom ¬x, whose intuitive reading is “x is not (and never will be) finite.”

Following the intuition outlined above, we are studying a domain, whose carrier is the set of all Boolean functions, for representing and propagating finiteness dependencies. We believe that coupling this new domain with H ×P can greatly improve the precision of the analysis.

An implementation of the finite-tree domain, where the parametric component P will be instantiated to the sharing domain SFL as presented in [4], is currently under development. We also plan to work on the correctness, with respect to rational unification, of the abstract operators defined on the domain SFL, therefore generalizing and extending the results proved in [22] for the setsharing domain of Jacobs and Langen.

We believe that information about the actual structure of terms can have a key role in improving the precision of finite-tree analysis, since it allows to better identify where cyclic structures may appear. As soon as the implementation of H × SFL will be finished, it will be possible to experiment with the integration of the explicit structural information provided by the generic Pattern(·) construction [2].

5 Conclusion

Several modern logic-based languages offer a computation domain based on rational trees. On the one hand, the use of such trees is encouraged by the possibility of using efficient and correct unification algorithms and by an increase in expressivity. On the other hand, these gains are countered by the extra problems rational trees bring with themselves and that can be summarized as follows: several built-ins, library predicates, program analysis and manipulation techniques are only well-defined for program fragments working with finite trees.

In this paper we propose an abstract-interpretation based solution to the problem of detecting program variables that can only be bound to finite terms. The rationale behind this is that applications exploiting rational trees tend to do so in a very controlled way. If the analysis we propose proves to be precise enough, then we will have a practical way of taking advantage of rational trees while minimizing the impact of their disadvantages.

References

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

2. R. Bagnara, P. M. Hill, and E. Zaffanella. Efficient structural information analysis for real CLP languages. In M. Parigot and A. Voronkov, editors, Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR 2000), volume 1955 of Lecture Notes in Computer Science, pages 189–206, Reunion Island, France, 2000. Springer-Verlag, Berlin.

3. R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. Theoretical Computer Science, 2001. 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, 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.

6. J. A. Campbell, editor. Implementations of Prolog. Ellis Horwood/Halsted Press/Wiley, 1984.

7. B. Carpenter. The Logic of Typed Feature Structures with Applications to Unification-based Grammars, Logic Programming and Constraint Resolution, volume 32 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, New York, 1992.

8. M. Codish, D. Dams, and E. Yardeni. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis. In K. Furukawa, editor, Logic Programming: Proceedings of the Eighth International Conference on Logic Programming, MIT Press Series in Logic Programming, pages 79–93, Paris, France, 1991. The MIT Press.

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

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

11. A. Colmerauer. An introduction to Prolog-III. Communications of the ACM, 33(7):69–90, 1990.

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

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

14. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.

15. L. Crnogorac, A. D. Kelly, and H. Søndergaard. A comparison of three occur-check analysers. In R. Cousot and D. A. Schmidt, editors, Static Analysis: Proceedings of the 3rd International Symposium, volume 1145 of Lecture Notes in Computer Science, pages 159–173, Aachen, Germany, 1996. Springer-Verlag, Berlin.

16. P. R. Eggert and K. P. Chow. Logic programming, graphics and infinite terms. Technical Report UCSB DoCS TR 83-02, Department of Computer Science, University of California at Santa Barbara, 1983.

17. G. Erbach. ProFIT: Prolog with Features, Inheritance and Templates. In Proceedings of the 7th Conference of the European Chapter of the Association for Computational Linguistics, pages 180–187, Dublin, Ireland, 1995.

18. M. Filgueiras. A Prolog interpreter working with infinite terms. In Campbell [6], pages 250–258.

19. F. Giannesini and J. Cohen. Parser generation and grammar manipulation using Prolog’s infinite trees. Journal of Logic Programming, 3:253–265, 1984.

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. S. Haridi and D. Sahlin. Efficient implementation of unification of cyclic structures. In Campbell [6], pages 234–249.

22. P. M. Hill, R. Bagnara, and E. Zaffanella. Soundness, idempotence and commutativity of set-sharing. Theory and Practice of Logic Programming, 2001. To appear.

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. Pair-sharing over rational trees. Journal of Logic Programming, 46(1– 2):139–155, 2000.

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

29. K. Mukai. Constraint Logic Programming and the Unification of Information. PhD thesis, Department of Computer Science, Faculty of Engineering, Tokio Institute of Technology, 1991.

30. C. Pollard and I. A. Sag. Head-Driven Phrase Structure Grammar. University of Chicago Press, Chicago, 1994.

31. F. Scozzari. Abstract domains for sharing analysis by optimal semantics. In J. Palsberg, editor, Static Analysis: 7th International Symposium, SAS 2000, volume 1824 of Lecture Notes in Computer Science, pages 397–412, Santa Barbara, CA, USA, 2000. Springer-Verlag, Berlin.

32. Gert Smolka and Ralf Treinen. Records for logic programming. Journal of Logic Programming, 18(3):229–258, 1994.

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

34. Swedish Institute of Computer Science, Programming Systems Group. SICStus Prolog User’s Manual, release 3 #0 edition, 1995.

Appendices

Appendix A provides a candidate implementation of the domain parameter P, showing how the functions and predicates specified in Definition 4 can be actually mapped into finitely computable operations over a well-known abstract domain for sharing analysis.

Appendix B provides the proofs of the results stated in the paper. Section B.1 introduces the notations and preliminary concepts that are subsequently used in the proofs; Section B.2 recalls a few general results holding for (syntactic) equality theories; the definition of (strongly) variable idempotent substitutions is given in Section B.3, together with some properties holding for them; these are then used in Section B.4 to prove Proposition 1 and Theorem 1; finally, in Section B.5 we provide the proof of Theorem 2.

This appendix has a separate bibliography on page 48.

A An implementation for the parameter domain P

As discussed in Section 3, several abstract domains for sharing analysis can be used to implement the parameter component P. As a basic implementation, one could consider the well-known set-sharing domain of Jacobs and Langen [JL89]. In such a case, all the non-trivial correctness results have already been established in [HBZ01]: in particular, the abstraction function provided in [HBZ01] satisfies the requirement of Definition 3 and the abstract unification operator has been proven correct with respect to rational-tree unification. Note however that, since no freeness and linearity information is recorded in the plain set-sharing domain, some of the predicates of Definition 4 need to be grossly approximated. For instance, the predicate gfree_{p} will provide useful information only when applied to an argument that is known to be definitely ground.

Therefore, in order to better highlight the generality of our specification of the sharing component P, we now instantiate it to the abstract domain SFL [BZH00] (see also [BCM94]). The domain SFL represents sharing, freeness and linearity information. Possible sharing is encoded by the set-sharing domain of Jacobs and Langen. Definite freeness and linearity information are each encoded by the set of variables of interest that enjoy the corresponding property.

Definition 9. (The set-sharing domain SH .) The set SH is defined by SH =^{def} ℘(SG), where the set of sharing groups SG is defined as

SG =^{def} ℘(VI ) \ {∅}.

SH is ordered by subset inclusion.

Definition 10. (The domain SFL.) Let F =^{def} ℘(VI ) and L =^{def} ℘(VI ) be partially ordered by reverse subset inclusion. The domain SFL is defined by the Cartesian product

SFL =^{def} SH × F × L

ordered by ‘≤_{S}’, the component-wise extension of the orderings defined on the sub-domains.

A complete definition, besides explicitly dealing with the set of relevant variables VI , would require the addition of a bottom element ⊥ representing the semantics of those program fragments that have no successful computations. We could also define an equivalence relation identifying the bottom element with all the elements in SFL corresponding to an impossible concrete computation state: for example, elements ⟨sh, f, l⟩ ∈ SFL such that f ⊈ vars(sh) (because a free variable does share with itself) or VI \ vars(sh) ⊈ l (because variables that cannot share are also linear). Note however that these spurious elements are never generated during the analysis process.

In the next definition we introduce a few well-known operations on the setsharing domain SH . These will be used to define the operations on the domain SFL.

Definition 11. (Abstract operators on SH .) For each sh ∈ SH and each V ⊆ VI , the extraction of the relevant component of sh with respect to V is given by the function rel: ℘(VI ) × SH → SH defined as

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

For each sh ∈ SH and each V ⊆ VI , the function \overline{rel}: ℘(VI ) × SH → SH gives the irrelevant component of sh with respect to V. It is defined as

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

The function (·)^{⋆}: SH → SH , called star-union, is given, for each sh ∈ SH , by

sh^{⋆} =^{def} { S ∈ SG | ∃n ≥ 1 . ∃T_{1}, …, T_{n} ∈ sh . S = ⋃_{i=1}^{n} T_{i} }.

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

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

It is now possible to define the implementation, on the domain SFL, of all the predicates and functions specified in Definition 4.

Definition 12. (Abstract operators on SFL.) For each d = ⟨sh, f, l⟩ ∈ SFL, for each s, t ∈ HTerms, where vars(s) ∪ vars(t) ⊆ VI , let R_{s} = rel(vars(s), sh) and R_{t} = rel(vars(t), sh). Then

ind_{d}(s, t) =^{def} (R_{s} ∩ R_{t} = ∅);
share lin_{d}(s, t) =^{def} ∀y, z ∈ vars(R_{s} ∩ R_{t}) :
(y ∈ l) ∧ occ lin(y, s) ∧ occ lin(y, t)
∧ (y ≠ z ⟹ ind_{d}(y, z));
ground_{d}(t) =^{def} (vars(t) ⊆ VI \ vars(sh));
free_{d}(t) =^{def} ∃y ∈ VI . (y = t) ∧ (y ∈ f);
gfree_{d}(t) =^{def} ground_{d}(t) ∨ free_{d}(t);
lin_{d}(t) =^{def} ∀y, z ∈ vars(t) :
(y ∈ l) ∧ (y ≠ z ⟹ ind_{d}(y, z))
∧ (¬ground_{d}(y) ⟹ occ lin(y, t));
or lin_{d}(s, t) =^{def} lin_{d}(s) ∨ lin_{d}(t);
share same var_{d}(s, t) =^{def} vars(R_{s} ∩ R_{t});
share with_{d}(t) =^{def} vars(R_{t}).

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 V_{xt} = {x} ∪ vars(t) ⊆ VI . Let R_{x} = rel({x}, sh) and R_{t} = rel(vars(t), sh). Let also

sh′ =^{def} \overline{rel}(V_{xt}, sh) ∪ bin(S_{x}, S_{t}),
S_{x} =^{def} \begin{cases}R_{x}, & if free_{d}(x) ∨ free_{d}(t) ∨ (lin_{d}(t) ∧ ind_{d}(x, t)); \\ R_{x}^{⋆}, & otherwise; \end{cases}

S_{t} =^{def} \begin{cases}R_{t}, & if free_{d}(x) ∨ free_{d}(t) ∨ (lin_{d}(x) ∧ ind_{d}(x, t)); \\ R_{t}^{⋆}, & otherwise; \end{cases}

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

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

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

Then

amgu_{S}(d, x ↦ t) =^{def} ⟨sh′, f′, l′⟩.

As said in Section 4, further work includes proving that these definitions satisfy all the requirements of Definitions 3 and 4. Note however that the generic specification we have provided is not targeted at SFL. For instance, it can be seen that the above implementations of the predicates gfree_{d} and or lin_{d} cannot fully exploit the disjunctive nature of their specification as given in Definition 4. Thus, even more powerful sharing domains can fit in this schema, including all the enhanced combinations considered in [BZH00].

B Proofs

B.1 Notations and preliminaries for the proofs

To simplify the expressions in the paper, any variable in a formula that is not in the scope of a quantifier is assumed to be universally quantified.

The function size: HTerms → ℕ is defined, for each t ∈ HTerms, by

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

A substitution σ is idempotent if, for all t ∈ HTerms, we have tσσ = tσ. The set of all idempotent substitutions is denoted by ISubst and ISubst ⊂ RSubst.

If t ∈ HTerms, we denote the set of variables that occur more than once in t by: nlvars(t) =^{def} { y ∈ vars(t) | ¬occ lin(y, t) }.

If s̄ = (s_{1}, …, s_{n}) ∈ HTerms^{n} and t̄ = (t_{1}, …, t_{n}) ∈ HTerms^{n} are two tuples of finite terms, then we let s̄ = t̄ denote the set of equations between corresponding components of s̄ and t̄. Namely,

(s̄ = t̄) =^{def} {s_{i} = t_{i} | 1 ≤ i ≤ n}.

Moreover, we overload the functions mvars, occ lin and nlvars to work on tuples of terms; thus, we will say that s̄ is linear if and only if nlvars(s̄) = ∅.

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

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

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

The axioms characterized by schemata (7) and (8) 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 [Cla78] on which pure logic programming is based, usually called the Herbrand equality theory and denoted FT , is given by the congruence axioms, the identity axioms, and the axiom schema

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

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

An alternative approach used in some implementations of Prolog, does not require the occur-check axioms. This approach is based on the theory of rational trees RT [Col82, Col84]. 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.

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.^{9} Note that both FT and RT are syntactic equality theories. 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(σ) . σ.

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

9 Note that, as a consequence of axiom (8) and the assumption that there are at least two distinct function symbols in the language, one of which is a constant, there exist two terms a_{1}, a_{2} ∈ GTerms ∩ HTerms such that, for any syntactic equality theory T, we have T ⊢ a_{1} ≠ a_{2}.

Observe that, given an arbitrary equality theory T, a set of equations in rational solved form may not be satisfiable in T. For example, ∃x . {x = f(x)} is false in the Clark equality theory. However, by the uniqueness axioms, any set of equations in rational solved form is satisfiable in RT .

B.2 General properties of equality theories.

Lemma 1. Suppose T is an equality theory, σ ∈ RSubst is satisfiable in T, x ∈ Vars \dom(σ), and t ∈ HTerms ∩GTerms. Then, τ =^{def} σ∪{x ↦ t} ∈ RSubst and τ is satisfiable in T.

Proof. Proven in [HBZ01, Lemma 1]. ⊓ ⊔

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

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

Proof. Proven in [HBZ01, Lemma 2]. ⊓ ⊔

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

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

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

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

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

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

Using these results,

T ⊢∀(σ ∪ {s = t} ↔ σ ∪ {s = t, t = tσ}),  [by (11)]
∀(σ ∪ {s = t} ↔ σ ∪ {s = tσ, t = tσ}),  [by (10)]
∀(σ ∪ {s = t} ↔ σ ∪ {s = tσ}).  [by (11)]
⊓ ⊔

Lemma 4. Let T be a syntactic equality theory. Let s ∈ HTerms ∩ GTerms and t ∈ HTerms be such that size(t) > size(s). Then T ⊢ ∀(s ≠ t).

Proof. By induction on m = size(s). For the base case, when m = 1, we have that s is a term functor of arity 0. Since size(t) > 1, then t = f(t_{1}, …, t_{n}), where n > 0. Then, by the identity axioms, we have T ⊢ ∀(s ≠ t).

For the inductive case, when m > 1, assume that the result holds for all m′ < m and let s = f(s_{1}, …, s_{n}), where n > 0. Since size(t) > m, we have t = f′(t_{1}, …, t_{n′}), where n′ > 0. If f ≠ f′ or n ≠ n′ then, by the identity axioms, we have T ⊢ ∀(s ≠ t). Otherwise, let f = f′ and n = n′. Note that, for all i ∈ {1, …, n}, we have size(s_{i}) < m. Also, there exists an index j ∈ {1, …, n} such that size(t_{j}) > size(s_{j}). By the inductive hypothesis, T ⊢ ∀(s_{j} ≠ t_{j}) so that, by the identity axioms, T ⊢ ∀(s ≠ t). ⊓ ⊔

B.3 (Strong) variable idempotence.

In [HBZ01], (weak) variable-idempotent substitutions were introduced as a subclass of substitutions in rational solved form in order to allow a more convenient reasoning about the sharing of variables for possibly non-idempotent substitutions.

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

vars(tσσ) \ dom(σ) = vars(tσ) \ dom(σ).

The set of variable-idempotent substitutions is denoted VSubst.

In [HBZ98] a stronger definition was used, taking into consideration also the variables in the domain of the substitution. Strong variable-idempotence is a useful concept when dealing with the finiteness of a rational term and the multiplicity of variables occurring in it (i.e., its linearity).

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

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

The set of strongly variable-idempotent substitutions is denoted MSubst.

Note that we have ISubst ⊂ MSubst ⊂ VSubst ⊂ RSubst.

Definition 15. (S-transformation.) The relation ⟼^{S} ⊆ RSubst × RSubst, called S-step, is defined by

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

If we have a finite sequence of S-steps σ_{1} ⟼^{S} ⋯ ⟼^{S} σ_{n} mapping σ_{1} to σ_{n}, then we write σ_{1} ⟼^{∗}^{S} σ_{n} and say that σ_{1} can be rewritten, by S-transformation, to σ_{n}.

The following theorems show that considering substitutions in MSubst is not a restrictive hypothesis.

Theorem 3. Suppose σ ∈ RSubst and σ ⟼^{∗}^{S} σ′. Then we have σ′ ∈ RSubst, dom(σ) = dom(σ′), vars(σ) = vars(σ′) and, if T is any equality theory, then T ⊢ ∀(σ ↔ σ′).

Proof. Proven in [HBZ01, Theorem 1]. ⊓ ⊔

Theorem 4. Suppose σ ∈ RSubst. Then there exists σ′ ∈ MSubst such that σ ⟼^{∗}^{S} σ′ and, for all τ ⊆ σ′, τ ∈ MSubst.

Proof. The proof is the same given for [HBZ01, Theorem 2], where a weaker result, using VSubst, was stated. ⊓ ⊔

Theorem 5. Let T be an equality theory and σ ∈ RSubst. Then there exists σ′ ∈ MSubst such that dom(σ) = dom(σ′), vars(σ) = vars(σ′), T ⊢ ∀(σ ↔ σ′) and for all τ ⊆ σ′, τ ∈ MSubst.

Proof. The result easily follows from Theorems 3 and 4. ⊓ ⊔

B.4 Abstracting finiteness.

For a substitution σ ∈ MSubst, when computing the operator hvars the fixpoint is reached after a single iteration.

Lemma 5. For each σ ∈ MSubst we have hvars(σ) = hvars_{1}(σ).

Proof. We show that hvars_{2}(σ) ⊆ hvars_{1}(σ). Let y ∈ hvars_{2}(σ). By Definition 5, we have two cases:

1. if y ∈ hvars_{1}(σ) then there is nothing to prove;

2. assume now y ∈ dom(σ) and vars(yσ) ⊆ hvars_{1}(σ). By Definition 5, we have two subcases:

(a) vars(yσ) ⊆ Vars \ dom(σ). Then vars(yσ) ⊆ hvars_{0}(σ), so that y ∈ hvars_{1}(σ);

(b) V = vars(yσ) ∩ dom(σ) ≠ ∅ and, for all z ∈ V, vars(zσ) ∩ V = ∅. Let z ∈ V so that z ∈ vars(yσ). By hypothesis, we have σ ∈ MSubst so that z ∈ vars(yσσ). As z ∈ dom(σ) and vars(zσ) ∩ dom(σ) = ∅, z ∉ vars(zσ). This means that z ∉ vars(yσσ), which is a contradiction since σ ∈ MSubst. ⊓ ⊔

Proposition 2. For each σ ∈ MSubst, we have

hvars(σ) = {y ∈ Vars | vars(yσ) ∩ dom(σ) = ∅}.

Proof. The result is obtained by applying Lemma 5 and then unfolding Definition 5. ⊓ ⊔

The following proposition shows that, for a substitution σ ∈ MSubst, the finiteness operator precisely captures the intended property.

Proposition 3. Let σ ∈ MSubst and y ∈ Vars. Then

rt(y, σ) ∈ HTerms ⟺ y ∈ hvars(σ).

Proof. Since σ ∈ MSubst, by Proposition 2 we have y ∈ hvars(σ) if and only if vars(yσ) ∩ dom(σ) = ∅.

Let vars(yσ)∩dom(σ) = ∅. Then, for any i > 0, we have yσ^{i} = yσ ∈ HTerms. Hence rt(y, σ) = yσ ∈ HTerms.

In order to prove the other inclusion, let now rt(y, σ) ∈ HTerms so that, by definition, we have size(rt(y, σ)) = n < ω. We will prove by contradiction that vars(yσ) ∩ dom(σ) = ∅. In fact, assume that there exists a variable

z ∈ vars(yσ) ∩ dom(σ),

so that (z ↦ zσ) ∈ σ. Since σ ∈ MSubst, we also have that z ∈ vars(yσσ), hence z ∈ vars(zσ) and size(zσ) > 1. As a consequence, for all i > 0, we have size(yσ^{i+1}) > size(yσ^{i}). Therefore we obtain a contradiction, since there exists an index j < ω such that for all i ≥ j we have size(yσ^{i}) > n. ⊓ ⊔

Proposition 4. Let σ ∈ MSubst and r ∈ HTerms such that vars(r) ⊆ hvars(σ). Then

rt(r, σ) = rσ,
vars(rσ) ∩ dom(σ) = ∅.

Proof. Suppose y ∈ vars(r). Then, by Proposition 2, vars(yσ) ∩ dom(σ) = ∅. Thus, for any i > 0, we have yσ^{i} = yσ ∈ HTerms. Thus rt(y, σ) = yσ. As this holds for all y ∈ vars(r), it follows that rt(r, σ) = rσ and vars(rσ)∩dom(σ) = ∅.

⊓ ⊔

In order to prove Proposition 1, i.e., to show that the finiteness operator precisely captures the intended property even for arbitrary substitutions in RSubst, we now prove that this operator is invariant under the application of S-steps.

Lemma 6. For each m > 0, we have hvars_{m−1}(σ) ⊆ hvars_{m}(σ).

Proof. Straightforward by Definition 5. ⊓ ⊔

Lemma 7. Let σ, σ′ ∈ RSubst where σ ⟼^{S} σ′. Then hvars(σ) = hvars(σ′).

Proof. Let (x ↦ t), (y ↦ s) ∈ σ, where x ≠ y, such that

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

If x ∉ vars(s) then we have σ = σ′ and the result trivially holds. Thus, we assume x ∈ vars(s). We prove the two inclusions separately.

In order to prove hvars(σ) ⊆ hvars(σ′) we show, by induction on m ≥ 0, that we have

hvars_{m}(σ) ⊆ hvars_{m}(σ′).

For the base case, when m = 0, by Theorem 3 we have dom(σ) = dom(σ′) so that

hvars_{0}(σ) = Vars \ dom(σ)
= Vars \ dom(σ′)
= hvars_{0}(σ′).

For the inductive step, when m > 0, assume hvars_{m−1}(σ) ⊆ hvars_{m−1}(σ′) and let z ∈ hvars_{m}(σ). By Definition 5, we have two cases: if z ∈ hvars_{m−1}(σ) then the result follows by a straight application of the inductive hypothesis; otherwise, we have

z ∈ dom(σ) ∧ vars(zσ) ⊆ hvars_{m−1}(σ).

Now, if z ≠ y we have zσ = zσ′, so that, by Theorem 3 and the inductive hypothesis we have

z ∈ dom(σ′) ∧ vars(zσ′) ⊆ hvars_{m−1}(σ′),

so that, by Definition 5, z ∈ hvars_{m}(σ′). Otherwise, if z = y, then

vars(zσ) = vars(s)
⊆ hvars_{m−1}(σ).

Since x ∈ vars(s),

vars(zσ′) = vars(s[x/t])
= (vars(s) \ {x}) ∪ vars(t),

and we need to show vars(zσ′) ⊆ hvars_{m−1}(σ′). By the inductive hypothesis we have

vars(s) ⊆ hvars_{m−1}(σ′);

Note that, since x ∈ vars(s), it follows x ∈ hvars_{m−1}(σ′) so that, by Definition 5 and Lemma 6,

vars(t) ⊆ hvars_{m−2}(σ′)
⊆ hvars_{m−1}(σ′).

In order to prove hvars(σ) ⊇ hvars(σ′) we show, by induction on m ≥ 0, that we have

hvars_{m+1}(σ) ⊇ hvars_{m}(σ′).

For the base case, when m = 0, by Lemma 6 and Theorem 3 we have

hvars_{1}(σ) ⊇ hvars_{0}(σ)
= Vars \ dom(σ)
= Vars \ dom(σ′)
= hvars_{0}(σ′).

For the inductive step, when m > 0, assume hvars_{m}(σ) ⊇ hvars_{m−1}(σ′) and let z ∈ hvars_{m}(σ′). By Definition 5, we have two cases: if z ∈ hvars_{m−1}(σ′) then the result follows by the inductive hypothesis and Lemma 6; otherwise, we have

z ∈ dom(σ′) ∧ vars(zσ′) ⊆ hvars_{m−1}(σ′).

Now, if z ≠ y we have zσ = zσ′, so that, by Theorem 3 and the inductive hypothesis we have

z ∈ dom(σ) ∧ vars(zσ) ⊆ hvars_{m}(σ),

so that, by Definition 5, z ∈ hvars_{m+1}(σ). Otherwise, if z = y, by definition of σ′, the inductive hypothesis and Lemma 6, we have

vars(zσ′) = vars(s[x/t])
= (vars(s) \ {x}) ∪ vars(t)
⊆ hvars_{m−1}(σ′)
⊆ hvars_{m}(σ)
⊆ hvars_{m+1}(σ).

Also note that we have

vars(xσ) = vars(t)
⊆ hvars_{m}(σ)

so that, by Definition 5 we have

x ∈ hvars_{m+1}(σ).

The result follows by observing that

vars(zσ) = vars(s) = (vars(s) \ {x}) ∪ {x}.
⊓ ⊔

Lemma 8. Let σ, σ′ ∈ RSubst, where σ ⟼^{∗}^{S} σ′. Then hvars(σ) = hvars(σ′).

Proof. By induction on the length n ≥ 0 of the derivation. For the base case, when n = 0, there is nothing to prove. Suppose now that

σ = σ_{0} ⟼^{S} ⋯ ⟼^{S} σ_{n−1} ⟼^{S} σ_{n} = σ′,

where n > 1. By the inductive hypothesis, since the derivation σ ⟼^{∗}^{S} σ_{n−1} has length n − 1, we have hvars(σ) = hvars(σ_{n−1}). Then the thesis follows by Lemma 7. ⊓ ⊔

Proof (Proof of Proposition 1.). By Theorem 5, there exists σ′ ∈ MSubst such that σ ⟼^{∗}^{S} σ′ and, for all equality theories T, T ⊢ ∀(σ ↔ σ′). Thus, by Lemma 8, we have hvars(σ) = hvars(σ′). The thesis then follows by applying Proposition 3.

⊓ ⊔

Lemma 9. Let σ, τ ∈ MSubst be satisfiable in a syntactic equality theory T and suppose that T ⊢ ∀(σ ↔ τ). Then hvars(σ) = hvars(τ).

Proof. We assume that the congruence and identity axioms hold. We will prove the inclusion hvars(σ) ⊆ hvars(τ), while the other inclusion will follow by symmetry.

Let y ∈ hvars(σ). Then, by Proposition 2, vars(yσ) ∩ dom(σ) = ∅. We will show that vars(yτ) ∩ dom(τ) = ∅ so that, again by Proposition 2, y ∈ hvars(τ).

Take a_{1} ∈ HTerms ∩ GTerms and let

σ′ =^{def} σ ∪ {z ↦ a_{1} | z ∈ vars(yσ)}.

Then, by Lemma 1, we have σ′ ∈ RSubst is satisfiable in T. By Lemma 2, we have σ′ ⟹ {y = yσσ′} and, for all i ≥ 0,

σ′ ⟹ σ ⟹ τ ⟹ {y = yτ^{i}},

so that, by the congruence axioms, σ′ ⟹ {yσσ′ = yτ^{i}}.

Note that yσσ′ ∈ HTerms ∩ GTerms, so that size(yσσ′) = n < ω.

Suppose that there exists z ∈ vars(yτ) ∩ dom(τ). Then, since τ ∈ MSubst, we have z ∈ vars(yττ), so that z ∈ vars(zτ) and size(zτ) > 1. As a consequence, for all i > 0, we have size(yτ^{i+1}) > size(yτ^{i}) and therefore there exists an index j < ω such that size(yτ^{j}) > n. By Lemma 4, T ⊢ ∀(yσσ′ ≠ yτ^{j}), therefore obtaining a contradiction. Thus vars(yτ) ∩ dom(τ) = ∅. ⊓ ⊔

Lemma 10. Suppose σ, τ ∈ RSubst such that T ⊢ ∀(σ ↔ τ) for any syntactic equality theory T. Then hvars(σ) = hvars(τ).

Proof. We assume that the congruence and the identity axioms hold. By Theorem 4 and Lemma 8, there exists σ′, τ′ ∈ MSubst such that σ ⟺ σ′, hvars(σ) = hvars(σ′), τ ⟺ τ′ and hvars(τ) = hvars(τ′). By hypothesis, σ ⟺ τ so that σ′ ⟺ τ′. By Lemma 9, hvars(σ′) = hvars(τ′). Therefore hvars(σ) = hvars(τ). ⊓ ⊔ Corollary 1. Let e ⊆ Eqs be satisfiable in the syntactic equality theory T. If σ, τ ∈ mgs(e), then hvars(σ) = hvars(τ).

Proof. By definition of mgs, we have σ, τ ∈ RSubst and σ ⟺ e ⟺ τ. Thus, the result follows by Lemma 10. ⊓ ⊔

Proof (Proof of Theorem 1). By Definition 7, we have α_{H}(σ) = hvars(σ) ∩ VI and α_{H}(σ′) = hvars(σ′) ∩ VI . Since RT is a syntactic equality theory and RT ⊢ ∀(σ ↔ σ′), the result is a simple consequence of Lemma 10. ⊓ ⊔

B.5 Correctness of abstract unification on H × P

Lemma 11. Let σ ∈ MSubst be satisfiable in a syntactic equality theory T. Let s ∈ HTerms ∩ GTerms and t ∈ HTerms and suppose that T ⊢ ∀(σ → s = t). Then s = tσ.

Proof. Since s ∈ GTerms, we must have s = f(s_{1}, …, s_{m}) where m ≥ 0. Moreover, by the assumption of the existence of two different function symbols in the signature Sig, there exists a term r ∈ HTerms ∩GTerms whose top-level function symbol is distinct from that in s. Thus, by the identity axioms, T ⊢ ∀(r ≠ s). Note also that, by Lemma 2 and the congruence axioms, T ⊢ ∀(σ → s = tσ).

We show that s = tσ by induction on the size of s.

First we show that tσ is not a variable. To prove this, we suppose that tσ = y ∈ Vars and derive a contradiction. If y ∉ dom(σ) then, by Lemma 1, σ′ = σ ∪ {y ↦ r} ∈ RSubst and σ′ is satisfiable in T. Therefore, using the congruence axioms, T ⊢ ∀(σ′ → r = s), which is a contradiction. If otherwise y ∈ dom(σ) then, since σ ∈ MSubst, we have y ∈ vars(yσ) and size(yσ) > 1, so that, for all i ≥ 0, size(tσ^{i+1}) > size(tσ^{i}). Thus, by Lemma 4, there exists an index j > 0 such that T ⊢ ∀(s ≠ tσ^{j}). However, by the hypothesis and Lemma 2, we have T ⊢ ∀(σ → s = tσ^{i}) for all i ≥ 0, therefore obtaining a contradiction. Thus tσ ∉ Vars.

Therefore, by the identity axioms, we can assume that tσ = f(t_{1}, …, t_{m}). If size(s) = 1, then m = 0 so that, by the congruence axioms, s = tσ. If size(s) > 1, then m > 0 and, by the identity axioms, we have, for each i = 1, …, m, that T ⊢ ∀(σ → s_{i} = t_{i}). Note that, for each i = 1, …, m, we have s_{i} ∈ HTerms ∩GTerms, t_{i} ∈ HTerms and size(s_{i}) < size(s), so that we can apply the inductive hypothesis, obtaining s_{i} = t_{i}σ. Thus, by the congruence axioms, s = tσσ. Thus tσσ ∈ GTerms so that vars(tσσ) = ∅. As σ ∈ MSubst, we have vars(tσ) = ∅ so that tσσ = tσ. Hence s = tσ. ⊓ ⊔

Lemma 12. Let s̄ = (s_{1}, …, s_{n}) ∈ HTerms^{n} be linear, and suppose the tuple of terms t̄ = (t_{1}, …, t_{n}) ∈ HTerms^{n} is such that vars(s̄) ∩ nlvars(t̄) = ∅ and mgs(s̄ = t̄) ≠ ∅. Then there exists μ ∈ mgs(s̄ = t̄) such that, for each variable z ∈ dom(μ) \ (vars(s̄) ∩ vars(t̄)), we have vars(zμ) ∩ dom(μ) = ∅.

Proof. We assume that the congruence and identity axioms hold. The proof is by induction on the number of variables in vars(s̄) ∪ vars(t̄).

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}) (with m ≥ 0). Let

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

Then mvars(s̄′) = mvars(s̄) and mvars(t̄′) = mvars(t̄) so that, as s̄ is linear, s̄′ is linear, vars(s̄′) ∩ nlvars(t̄′) = ∅ and vars(s̄′) ∩ vars(t̄′) = vars(s̄) ∩ vars(t̄). Moreover, by the congruence axiom (6), mgs(s̄′ = t̄′) = 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, for all i = 1, …, n, either s_{i} ∈ Vars or t_{i} ∈ Vars.

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 linear, s̄_{i} is linear, vars(s̄_{i}) ∩ nlvars(t̄_{i}) = ∅ and

(vars(s̄_{i}) ∩ vars(t̄_{i})) ∪ {s_{i}} = vars(s̄) ∩ vars(t̄).

As s̄ is linear and vars(s̄) ∩ nlvars(t̄) = ∅, s_{i} ∉ vars(s̄_{i}) ∪ vars(t̄_{i}) and hence s_{i} ∉ dom(μ) for all μ ∈ mgs(s̄ = t̄). Therefore

dom(μ) \ (vars(s̄) ∩ vars(t̄)) = dom(μ) \ (vars(s̄_{i}) ∩ vars(t̄_{i})).

Furthermore, by the congruence axiom (3), 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 for each i = 1, …, n, s_{i} ≠ t_{i} and either s_{i} ∈ Vars or t_{i} ∈ Vars.

For the base case, we have vars(s̄) ∪ vars(t̄) = ∅ and the result holds.

For the inductive step, vars(s̄) ∪ vars(t̄) ≠ ∅ so that n > 0. As the order of the equations in s̄ = t̄ is not relevant to the hypothesis, we assume, without loss of generality that if, for some i = 1, …, n, vars(s_{i}) ∩ vars(t_{i}) = ∅, then vars(s_{1}) ∩ vars(t_{1}) = ∅. There are three cases we consider separately:

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

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

For each i = 1, …, n, we are assuming that either s_{i} ∈ Vars or t_{i} ∈ Vars, 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} ∈ Vars if 1 ≤ i ≤ k and t_{i} ∈ Vars if k + 1 ≤ i ≤ n.

Let

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

We now show that μ ⊆ Eqs is in rational solved form. As s̄ is linear, (s_{1}, …, s_{k}) is linear. As s̄ is linear and t_{i} ∈ vars(s_{i}) if k + 1 ≤ i ≤ n, then (t_{k+1}, …, t_{n}) is linear and {s_{1}, …, s_{k}} ∩ {t_{k+1}, …, t_{n}} = ∅. As we are assuming that, for all i = 1, …, n, s_{i} ≠ t_{i} and 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 (4), μ ∈ mgs(s̄ = t̄).

As s_{i} ∈ vars(t_{i}) when 1 ≤ i ≤ k and t_{i} ∈ vars(s_{i}) when k + 1 ≤ i ≤ n, dom(μ) \ (vars(s̄) ∩ vars(t̄)) = ∅. Therefore the required result holds.

Case b. s_{1} ∈ Vars \ vars(t_{1}).

Let

\begin{matrix}s̄_{1} & =^{def} (s_{2}, …, s_{n}), \\ t̄_{1} & =^{def} (t_{2}[s_{1}/t_{1}], …, t_{n}[s_{1}/t_{1}]). \end{matrix}  (12)

As s̄ is linear, 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}), s_{1} ∉ vars(t̄_{1}). Thus

s_{1} ∉ vars(s̄_{1}) ∪ vars(t̄_{1}).  (13)

Therefore vars(s̄_{1})∪vars(t̄_{1}) ⊂ vars(s̄)∪vars(t̄). Now since s̄ is linear, s̄_{1} is linear. Thus, to apply the inductive hypothesis to s̄_{1} and t̄_{1}, we have to show that

vars(s̄_{1}) ∩ nlvars(t̄_{1}) = ∅.  (14)

Suppose that u ∈ vars(s̄_{1}) so that u ∈ vars(s̄). Now, by hypothesis, we have vars(s̄) ∩ nlvars(t̄) = ∅. Thus s_{1}, u ∉ nlvars(t̄). If u ∈ vars((t_{2}, …, t_{n})) so that u ∉ vars(t_{1}), then u ∉ nlvars(t̄_{1}). On the other hand, if u ∉ vars((t_{2}, …, t_{n})), then, as s_{1} ∉ nlvars((t_{2}, …, t_{n})) and u ∉ nlvars(t_{1}), u ∉ nlvars(t̄_{1}). Thus, for all u ∈ vars(s̄_{1}), u ∉ nlvars(t̄_{1}). Hence (14) holds. It follows that the inductive hypothesis for s̄_{1} and t̄_{1} holds. Therefore there exists μ_{1} ∈ RSubst where

μ_{1} ∈ mgs(s̄_{1} = t̄_{1})

such that, for each z ∈ dom(μ_{1})\(vars(s̄_{1})∩vars(t̄_{1})), vars(zμ_{1})∩dom(μ_{1}) = ∅.

Let

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

We now show that μ ⊆ Eqs is in mgs(s̄ = t̄). First we show that μ is in rational solved form. By (13),

s_{1} ∉ vars(μ_{1}),  (16)

and, as s_{1} ∉ vars(t_{1}), we have

s_{1} ∉ vars(t_{1}μ_{1}).  (17)

Thus, as μ_{1} ∈ RSubst, μ has no identities or circular subsets so that μ ∈ RSubst. By Lemma 3, μ ∈ mgs(s̄ = t̄).

Let

z ∈ dom(μ) \ (vars(s̄) ∩ vars(t̄)).  (18)

Then we have to show that

vars(zμ) ∩ dom(μ) = ∅.  (19)

It follows from (15) and (18) that either z ∈ dom(μ_{1}) so that zμ = zμ_{1} or z = s_{1} and zμ = t_{1}μ_{1}. We consider these two cases separately.

Suppose first that z ∈ dom(μ_{1}). By (12), we have vars(s̄_{1}) ⊆ vars(s̄) and vars(t̄_{1}) ⊆ vars(t̄) so that vars(s̄_{1}) ∩ vars(t̄_{1}) ⊆ vars(s̄) ∩ vars(t̄). Therefore, z ∈ dom(μ_{1}) \ (vars(s̄_{1}) ∩ vars(t̄_{1})). Thus, by the inductive hypothesis, we have vars(zμ_{1}) ∩ dom(μ_{1}) = ∅. Now, as z ∈ dom(μ_{1}) and (16) holds, s_{1} ∉ vars(zμ_{1}). Thus, as dom(μ) = dom(μ_{1})∪{s_{1}}, vars(zμ_{1})∩dom(μ) = ∅. Hence, as zμ = zμ_{1},

(19) holds.

Secondly suppose that z = s_{1}. Then we have that s_{1} ∉ vars(s̄) ∩ vars(t̄). Hence t̄_{1} = (t_{2}, …, t_{n}). Let u be any variable in vars(t_{1}). Then we have that u ∉ vars(s̄_{1}) ∩ vars(t̄_{1}), since vars(s̄) ∩ nlvars(t̄) = ∅, If u ∈ dom(μ_{1}), then we can apply the inductive hypothesis to obtain vars(uμ_{1}) ∩ dom(μ_{1}) = ∅. On the other hand, if u ∉ dom(μ_{1}), we have u = uμ_{1} and vars(uμ_{1}) ∩ dom(μ_{1}) = ∅. Hence vars(t_{1}μ_{1}) ∩ dom(μ_{1}) = ∅. Thus, as dom(μ) = dom(μ_{1}) ∪ {s_{1}}, by (17), vars(t_{1}μ_{1}) ∩ dom(μ) = ∅. Therefore, as zμ = t_{1}μ_{1}, (19) holds.

Case c. t_{1} ∈ Vars \ vars(s_{1}).

Let

\begin{matrix}s̄_{1} & =^{def} (s_{2}[t_{1}/s_{1}], …, s_{n}[t_{1}/s_{1}]), \\ t̄_{1} & =^{def} (t_{2}[t_{1}/s_{1}], …, t_{n}[t_{1}/s_{1}]). \end{matrix}  (20)

All occurrences of t_{1} in s̄ and t̄ are replaced in s̄_{1} and t̄_{1} by s_{1} so that, as t_{1} ∉ vars(s_{1}),

t_{1} ∉ vars(s̄_{1}) ∪ vars(t̄_{1}).  (21)

Therefore vars(s̄_{1})∪vars(t̄_{1}) ⊂ vars(s̄)∪vars(t̄). Now, s̄_{1} is linear since s̄ is linear. Thus, to apply the inductive hypothesis to s̄_{1} and t̄_{1}, we have to show that

vars(s̄_{1}) ∩ nlvars(t̄_{1}) = ∅.  (22)

Suppose u is any variable in vars(s̄_{1}). Then either u ∈ vars((s_{2}, …, s_{n})) or u ∈ vars(s_{1}) and t_{1} ∈ vars((s_{2}, …, s_{n})). By hypothesis, vars(s̄) ∩ nlvars(t̄) = ∅, so that u ∉ nlvars(t̄). If u ∈ vars((s_{2}, …, s_{n})), then, as s̄ is linear, u ∉ vars(s_{1}). Thus, it follows from (20) that u ∉ nlvars(t̄_{1}). If t_{1} ∈ vars((s_{2}, …, s_{n})), then t_{1} ∉ vars((t_{2}, …, t_{n})) so that, again by (20), t̄_{1} = (t_{2}, …, t_{n}). Thus, for all u ∈ vars(s̄_{1}), u ∉ nlvars(t̄_{1}). Hence (22) holds. It follows that the inductive hypothesis for s̄_{1} and t̄_{1} holds. Therefore there exists μ_{1} ∈ RSubst where

μ_{1} ∈ mgs(s̄_{1} = t̄_{1})

such that, for each z ∈ dom(μ_{1})\(vars(s̄_{1})∩vars(t̄_{1})), vars(zμ_{1})∩dom(μ_{1}) = ∅.

Let

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

We now show that μ ⊆ Eqs is in mgs(s̄ = t̄). First we show that μ is in rational solved form. By (21),

t_{1} ∉ vars(μ_{1}),  (24)

and, as t_{1} ∉ vars(s_{1}), we have

t_{1} ∉ vars(s_{1}μ_{1}).  (25)

Thus, as μ_{1} ∈ RSubst, μ has no identities or circular subsets so that μ ∈ RSubst. By Lemma 3, μ ∈ mgs(s̄ = t̄).

Let

z ∈ dom(μ) \ (vars(s̄) ∩ vars(t̄)).  (26)

Then we have to show that

vars(zμ) ∩ dom(μ) = ∅.  (27)

It follows from (23) and (26) that either z ∈ dom(μ_{1}) so that zμ = zμ_{1} or z = t_{1} and zμ = s_{1}μ_{1}. We consider these two cases separately.

Suppose first that z ∈ dom(μ_{1}). To apply the inductive hypothesis to z, we need to show that,

vars(s̄_{1}) ∩ vars(t̄_{1}) ⊆ vars(s̄) ∩ vars(t̄).

To see this, let u ∈ vars(s̄_{1})∩vars(t̄_{1}). Then, by (20), either u ∈ vars((s_{2}, …, s_{n})) or u ∈ vars(s_{1}) and t_{1} ∈ vars((s_{2}, …, s_{n})). If u ∈ vars((s_{2}, …, s_{n})), then we have u ∈ vars(s̄) so that, as s̄ is linear, we have also u ∉ vars(s_{1}) and hence u ∈ vars((t_{2}, …, t_{n})). Alternatively, if u ∈ vars(s_{1}) and t_{1} ∈ vars((s_{2}, …, s_{n})), then u, t_{1} ∈ vars(s̄). Moreover, by hypothesis, vars(s̄) ∩ nlvars(t̄) = ∅, so that t_{1} ∉ vars((t_{2}, …, t_{n})). Thus t̄_{1} = (t_{2}, …, t_{n}) and hence u ∈ vars(t̄). Therefore, in both cases, u ∈ vars(s̄)∩vars(t̄). It follows that z ∈ dom(μ_{1})\(vars(s̄_{1})∩vars(t̄_{1})). Thus, by the inductive hypothesis, we have vars(zμ_{1}) ∩ dom(μ_{1}) = ∅. Now, as z ∈ dom(μ_{1}) and (24) holds, t_{1} ∉ vars(zμ_{1}). Thus, as dom(μ) = dom(μ_{1}) ∪ {t_{1}}, vars(zμ_{1}) ∩ dom(μ) = ∅. Hence, as zμ = zμ_{1}, (27) holds.

Secondly, suppose that z = t_{1}. Then t_{1} ∉ vars(s̄) ∩ vars(t̄) and, consequently, s̄_{1} = (s_{2}, …, s_{n}). Let u be any variable in vars(s_{1}). Then, as s̄ is linear, we have u ∉ vars(s̄_{1}) so that u ∉ vars(s̄_{1}) ∩ vars(t̄_{1}). Thus, if u ∈ dom(μ_{1}), we can apply the inductive hypothesis to u and obtain vars(uμ_{1}) ∩ dom(μ_{1}) = ∅. On the other hand, if u ∉ dom(μ_{1}), u = uμ_{1} and vars(uμ_{1}) ∩ dom(μ_{1}) = ∅. Hence vars(s_{1}μ_{1}) ∩ dom(μ_{1}) = ∅. Thus, as dom(μ) = dom(μ_{1}) ∪ {t_{1}}, by (25), vars(s_{1}μ_{1}) ∩ dom(μ) = ∅. Therefore, as zμ = s_{1}μ_{1}, (27) holds. ⊓ ⊔

Lemma 13. Suppose that the tuple of terms s̄ = (s_{1}, …, s_{n}) ∈ HTerms^{n} is linear, t̄ = (t_{1}, …, t_{n}) ∈ HTerms^{n} and mgs(s̄ = t̄) ≠ ∅. Then there exists μ ∈ mgs(s̄ = t̄) and, for each z ∈ dom(μ) \ vars(s̄), the following properties hold:

1. vars(zμ) ⊆ vars(s̄);

2. vars(zμ) ∩ dom(μ) = ∅.

Proof. We assume that the congruence and identity axioms hold. The proof is by induction on the number of variables in vars(s̄) ∪ vars(t̄).

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}) (m ≥ 0). Let

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

Then mvars(s̄′) = mvars(s̄) and mvars(t̄′) = mvars(t̄) so that, as s̄ is linear, s̄′ is linear. Moreover, by the congruence axiom (6), mgs(s̄′ = t̄′) = 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, for all i = 1, …, n, either s_{i} ∈ Vars or t_{i} ∈ Vars.

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 linear, s̄_{i} is linear. Therefore

dom(μ) \ vars(s̄) ⊆ dom(μ) \ vars(s̄_{i}).

Furthermore, by the congruence axiom (3), 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 either s_{i} ∈ Vars or t_{i} ∈ Vars, for all i = 1, …, n.

For the base case, we have vars(s̄) ∪ vars(t̄) = ∅ and the result holds.

For the inductive step, vars(s̄) ∪ vars(t̄) ≠ ∅ so that n > 0. As the order of the equations in s̄ = t̄ is not relevant to the hypothesis, we assume, without loss of generality that if, for some i = 1, …, n, vars(s_{i}) ∩ vars(t_{i}) = ∅ then, we have vars(s_{1}) ∩ vars(t_{1}) = ∅. There are four cases we consider separately: a. for all i = 1, …, n, vars(s_{i}) ∩ vars(t_{i}) ≠ ∅; b. s_{1} ∈ Vars \ vars(t_{1}); c. t_{1} ∈ Vars \ vars(s̄) and s_{1} ∉ Vars; d. t_{1} ∈ vars(s̄) \ vars(s_{1}) and s_{1} ∉ Vars.

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

For each i = 1, …, n, we are assuming that either s_{i} ∈ Vars or t_{i} ∈ Vars, 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} ∈ Vars if 1 ≤ i ≤ k and t_{i} ∈ Vars if k + 1 ≤ i ≤ n.

Let

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

We show that μ ⊆ Eqs is in mgs(s̄ = t̄). First we must show that μ ∈ RSubst. As s̄ is linear, (s_{1}, …, s_{k}) is linear. As s̄ is linear and t_{i} ∈ vars(s_{i}) if k + 1 ≤ i ≤ n, then (t_{k+1}, …, t_{n}) is linear and {s_{1}, …, s_{k}} ∩ {t_{k+1}, …, t_{n}} = ∅. As we are assuming that, for all i = 1, …, n, s_{i} ≠ t_{i} and 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 (4), μ ∈ mgs(s̄ = t̄).

As {t_{k+1}, …, t_{n}} ⊆ vars((s_{k+1}, …, s_{n})), dom(μ) \ vars(s̄) = ∅. Therefore the required result holds.

Case b. s_{1} ∈ Vars \ 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 linear, s̄_{1} is 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} ∉ vars(s̄_{1}) ∪ vars(t̄_{1}).  (28)

It follows that vars(s̄_{1}) ∪ vars(t̄_{1}) ⊂ vars(s̄) ∪ vars(t̄) so that the inductive hypothesis applies to s̄_{1} and t̄_{1}. Thus there exists μ_{1} ∈ RSubst where

μ_{1} ∈ mgs(s̄_{1} = t̄_{1})

such that, for each z ∈ dom(μ_{1}) \ vars(s̄_{1}), properties 1 and 2 hold using μ_{1} and s̄_{1}.

Let

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

We show that μ ⊆ Eqs is in mgs(s̄ = t̄). By (28), 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 3, μ ∈ mgs(s̄ = t̄).

Suppose that z ∈ dom(μ) \ vars(s̄). As

vars(s̄_{1}) ∪ {s_{1}} = vars(s̄)

and

dom(μ_{1}) ∪ {s_{1}} = dom(μ),

we have

dom(μ_{1}) \ vars(s̄_{1}) = dom(μ) \ vars(s̄).  (29)

Therefore z ∈ dom(μ_{1}) \ vars(s̄_{1}) and zμ_{1} = zμ. Thus the inductive properties 1 and 2 using μ_{1} and s̄_{1} can be applied to z. We show that properties 1 and 2 using μ and s̄ can be applied to z.

1. By property 1, vars(zμ) ⊆ vars(s̄_{1}) and hence, vars(zμ) ⊆ vars(s̄).

2. By property 2, we have vars(zμ) ∩ dom(μ_{1}) = ∅. Now s_{1} ∉ vars(zμ) because s_{1} ∉ vars(s̄_{1}) (since s̄ is linear) and vars(zμ) ⊆ vars(s̄_{1}) (by property 1). Thus, as dom(μ) = dom(μ_{1}) ∪ {s_{1}}, we have vars(zμ) ∩ dom(μ) = ∅.

Case c. Assume that t_{1} ∈ Vars \ 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 linear, s̄_{1} is linear. By the assumption for this case, t_{1} ∉ vars(s̄_{1}). Also, 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} ∉ vars(s̄_{1}) ∪ vars(t̄_{1}).  (30)

It follows that vars(s̄_{1}) ∪ vars(t̄_{1}) ⊂ vars(s̄) ∪ vars(t̄) so that we can apply the inductive hypothesis to s̄_{1} and t̄_{1}. Thus there exists μ_{1} ∈ RSubst where

μ_{1} ∈ mgs(s̄_{1} = t̄_{1})

such that, for each z ∈ dom(μ_{1}) \ vars(s̄_{1}), properties 1 and 2 hold using μ_{1} and s̄_{1}. Note that, by (30), t_{1} ∉ vars(μ_{1}) and, in particular, t_{1} ∉ dom(μ_{1}).

Let

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

As s_{1} ∉ Vars and μ_{1} ∈ RSubst, μ ∈ Eqs has no identities or circular subsets so that μ ∈ RSubst. By Lemma 3, μ ∈ mgs(s̄ = t̄).

As t_{1} ∈ dom(μ) (by (31)) and t_{1} ∉ vars(s̄) (by the assumption for this case), we have

dom(μ_{1}) \ vars(s̄_{1}) ∪ {t_{1}} = dom(μ) \ vars(s̄).

Suppose that z ∈ dom(μ) \ vars(s̄). Then either z ≠ t_{1} so that zμ = zμ_{1} and the inductive properties 1 and 2 using μ_{1} and s̄_{1} can be applied to z or z = t_{1} and zμ = s_{1}μ_{1}. We show that properties 1 and 2 using μ and s̄ can be applied to z.

1. Suppose z ≠ t_{1} so that zμ = zμ_{1}. Using property 1, vars(zμ_{1}) ⊆ vars(s̄_{1}). As vars(s̄_{1}) ⊆ vars(s̄), it follows that vars(zμ) ⊆ vars(s̄). Suppose that z = t_{1} so that zμ = s_{1}μ_{1}. Let u be any variable in s_{1}. As s̄ is linear, u ∉ vars(s̄_{1}). Thus, if u ∈ dom(μ_{1}), we can use property 1 to derive that vars(uμ_{1}) ⊆ vars(s̄_{1}). If u ∉ dom(μ_{1}), then uμ_{1} = u so that vars(uμ_{1}) ⊆ vars(s_{1}). Moreover vars(s_{1}) ∪ vars(s̄_{1}) = vars(s̄) so that

vars(s_{1}μ_{1}) ⊆ vars(s̄).  (32)

Hence vars(zμ) ⊆ vars(s̄).

2. Suppose z ≠ t_{1} so that zμ = zμ_{1}. Then, as property 2 holds, we have vars(zμ) ∩ dom(μ_{1}) = ∅. Now t_{1} ∉ vars(zμ) because vars(zμ) ⊆ vars(s̄_{1}) (by property 1) and t_{1} ∉ vars(s̄_{1}) (by (30)). Thus, as dom(μ) = dom(μ_{1}) ∪ {t_{1}}, we have vars(zμ) ∩ dom(μ) = ∅. Suppose that z = t_{1} so that zμ = s_{1}μ_{1}. Let u be any variable in vars(s_{1}). Then, as s̄ is linear, u ∉ vars(s̄_{1}). Then either u ∈ dom(μ_{1}), and we can apply property 2 to u to obtain vars(uμ_{1}) ∩ dom(μ_{1}) = ∅, or u = uμ_{1}, and vars(uμ_{1}) ∩ dom(μ_{1}) = ∅. Hence we have vars(s_{1}μ_{1}) ∩ dom(μ_{1}) = ∅. Now t_{1} ∉ vars(s_{1}μ_{1}) because vars(s_{1}μ_{1}) ⊆ vars(s̄) (by (32)) and t_{1} ∉ vars(s̄) (by the assumption for this case). Thus, as dom(μ) = dom(μ_{1}) ∪ {t_{1}}, we have vars(zμ) ∩ dom(μ) = ∅.

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

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

As s̄ is linear, there is only one occurrence of t_{1} in {s_{2}, …, s_{n}}, and, in s̄_{1}, this is replaced by s_{1} which is also linear. Thus s̄_{1} is linear, s̄_{1} ⊆ s̄ and t_{1} ∉ vars(s̄_{1}). Also, 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} ∉ vars(s̄_{1}) ∪ vars(t̄_{1}).  (33)

It follows that vars(s̄_{1}) ∪ vars(t̄_{1}) ⊂ vars(s̄) ∪ vars(t̄) so that we can apply the inductive hypothesis to s̄_{1} and t̄_{1}. Thus, there exists μ_{1} ∈ RSubst where

μ_{1} ∈ mgs(s̄_{1} = t̄_{1})

such that, for each z ∈ dom(μ_{1}) \ vars(s̄_{1}), properties 1 and 2 hold using μ_{1} and s̄_{1}.

Let

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

By (33), t_{1} ∉ vars(μ_{1}). Moreover μ_{1} ∈ RSubst and s_{1} ∉ Vars so that μ ∈ Eqs has no identities or circular subset. Thus μ ∈ RSubst. By Lemma 3, μ ∈ mgs(s̄ = t̄).

As vars(s̄_{1}) ∪ {t_{1}} = vars(s̄) and dom(μ_{1}) ∪ {t_{1}} = dom(μ), we have

dom(μ_{1}) \ vars(s̄_{1}) = dom(μ) \ vars(s̄).

Suppose z ∈ dom(μ) \ vars(s̄). Then z ≠ t_{1}, zμ = zμ_{1} and the inductive properties 1 and 2 using μ_{1} and s̄_{1} can be applied to z. We show that the properties 1 and 2 using μ and s̄ can be applied to z.

1. By property 1, vars(zμ) ⊆ vars(s̄_{1}) and hence, as s̄_{1} ⊆ s̄, vars(zμ) ⊆ vars(s̄).

2. By property 2, we have vars(zμ) ∩ dom(μ_{1}) = ∅. Now t_{1} ∉ vars(zμ) because t_{1} ∉ vars(s̄_{1}) (by (33)) and vars(zμ) ⊆ vars(s̄_{1}) (by property 1). As dom(μ_{1}) ∪ {t_{1}} = dom(μ), it follows that vars(zμ) ∩ dom(μ) = ∅. ⊓ ⊔

Proposition 5. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ MSubst and suppose that {r, r′} = {x, t}, vars(r) ⊆ hvars(σ) and rt(r, σ) ∈ GTerms. Then, for all τ ∈ mgs(σ∪{x = t}) in a syntactic equality theory T, we have

hvars(σ) ∪ vars(r′) ⊆ hvars(τ).  (34)

Proof. We assume that the congruence and identity axioms hold. If σ ∪ {x = t} is not satisfiable, the result is trivial. We therefore assume, for the rest of the proof, that σ ∪ {x = t} is satisfiable in T. It follows from Corollary 1 that we just have to show that

a vars(r′) ⊆ hvars(τ), for some τ ∈ mgs(σ ∪ {x = t}); b hvars(σ) ⊆ hvars(τ), for some τ ∈ mgs(σ ∪ {x = t}).

From these, we can then conclude that, for all τ ∈ mgs(σ ∪ {x = t}), (34) holds.

Note that, in both cases, since σ ∈ MSubst and vars(r) ⊆ hvars(σ), by Proposition 4 we have rt(r, σ) = rσ, so that rσ ∈ HTerms ∩ GTerms.

Case a. We must show that there exists τ ∈ mgs(σ ∪ {x = t}) such that vars(r′) ⊆ hvars(τ).

As mgs(σ ∪ {x = t}) ≠ ∅, by Theorem 5 and the definition of mgs we can assume that there exists τ ∈ MSubst ∩ mgs(σ ∪ {x = t}). Thus

τ ⟹ (σ ∪ {r = r′}).

By Lemma 2 and the congruence axioms, we have τ ⟹ {rσ = r′}. Since τ ∈ MSubst and rσ ∈ HTerms ∩ GTerms, Lemma 11 applies (with s = rσ) so that rσ = r′τ ∈ HTerms ∩GTerms. Thus, by Proposition 2, vars(r′) ⊆ hvars(τ).

Case b. In this case, we show that there exists τ ∈ mgs(σ ∪ {x = t}) such that hvars(σ) ⊆ hvars(τ).

Let

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

By Lemma 3 and the congruence axioms, σ ∪ {x = t} ⟹ s̄ = t̄. Thus, as σ ∪ {x = t} is satisfiable, mgs(s̄ = t̄) ≠ ∅. Then, by Theorem 5, there exists μ ∈ MSubst ∩ mgs(s̄ = t̄). Therefore, since rσ ∈ HTerms ∩ GTerms and μ ⟹ {rσ = r′σ}, Lemma 11 applies (with s = rσ) so that we have rσ = r′σμ ∈ HTerms ∩ GTerms. Hence, for all w ∈ dom(μ),

vars(wμ) = ∅.  (35)

Let

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

Then, as σ, μ ∈ RSubst, it follows from (35) that ν, τ ∈ Eqs have no identities or circular subsets so that ν, τ ∈ RSubst. By Lemma 3, τ ∈ mgs(σ ∪ {x = t}).

Suppose that y ∈ hvars(σ). Then we show that y ∈ hvars(τ). Using Proposition 4, rt(y, σ) = yσ and

vars(yσ) ∩ dom(σ) = ∅.  (36)

We show that vars(yτ) ∩ dom(τ) = ∅. Now, if y ∉ dom(τ), the result holds trivially. Suppose that y ∈ dom(ν), then yτ = yσμ and y ∈ dom(σ). Let w be any variable in vars(yσ) so that, by (36), w ∉ dom(σ). If w ∉ dom(μ), then w = wμ ∉ dom(τ). If w ∈ dom(μ), then, by (35), vars(wμ) = ∅. Therefore, vars(wμ) ∩ dom(τ) = ∅. It follows that vars(yν) ∩ dom(τ) = ∅. Finally, suppose y ∈ dom(μ). Then, by (35), vars(yμ) = ∅. Therefore vars(yμ) ∩ dom(τ) = ∅.

Therefore, using Definition 6, we have that y ∈ hvars(τ) as required. ⊓ ⊔

Proposition 6. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ MSubst and suppose that x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Suppose also that ind_{p}(x, t) and that or lin_{p}(x, t) hold. Then, for all τ ∈ mgs(σ ∪ {x = t}) in a syntactic equality theory T, we have

hvars(σ) ⊆ hvars(τ).  (37)

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

As x ∈ hvars(σ) and vars(t) ⊆ hvars(σ), we have, using Proposition 4, rt(x, σ) = xσ and rt(t, σ) = tσ. Also

vars(xσ) ∩ dom(σ) = ∅, vars(tσ) ∩ dom(σ) = ∅.  (38)

As ind_{p}(x, t) holds,

vars(xσ) ∩ vars(tσ) = ∅.  (39)

By hypothesis, or lin(x, t) holds so that, by Definition 4, for some r ∈ {x, t}, rσ is linear. Let r′ =^{def} {x, t} \ {r}.

By Lemma 3 and the congruence axioms, σ∪{x = t} ⟹ {rσ = r′σ}. Thus, as σ ∪ {x = t} is satisfiable, mgs(rσ = r′σ) ≠ ∅. Thus we can apply Lemma 12 (where s̄ = rσ and t̄ = r′σ) so that, using (39), there exists μ ∈ mgs(xσ = tσ) such that, for all w ∈ dom(μ),

vars(wμ) ∩ dom(μ) = ∅.  (40)

Note that, by (38),

dom(σ) ∩ vars(μ) = ∅.  (41)

Let

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

Then, as σ, μ ∈ RSubst, it follows from (41) that ν, τ ∈ Eqs have no identities or circular subsets so that ν, τ ∈ RSubst. By Lemma 3, τ ∈ mgs(σ ∪ {x = t}).

Suppose y ∈ hvars(σ). Then we show that y ∈ hvars(τ). As y ∈ HTerms, we have, using Proposition 4, rt(y, σ) = yσ and

vars(yσ) ∩ dom(σ) = ∅.  (42)

We show that vars(yτ) ∩ dom(τ) = ∅. Now, if y ∉ dom(τ), the result holds trivially. Suppose that y ∈ dom(ν), then yτ = yσμ. Let w be any variable in vars(yσ). Then, by (42), w ∉ dom(σ). If w ∉ dom(μ), then w = wμ ∉ dom(τ). If w ∈ dom(μ), then vars(wμ) ⊆ vars(μ) so that, by (41), vars(wμ) ∩ dom(ν) = ∅. Moreover (40) applies so that vars(wμ) ∩ dom(μ) = ∅. Therefore we have vars(wμ) ∩ dom(τ) = ∅. It follows that vars(yν) ∩ dom(τ) = ∅. Finally, suppose y ∈ dom(μ). Then yτ = yμ and, by (41), wehave vars(yμ) ∩ dom(ν) = ∅. Also (40) applies where w is replaced by y so that vars(yμ) ∩ dom(μ) = ∅. Thus vars(yμ) ∩ dom(τ) = ∅.

Therefore, using Definition 6, we have that y ∈ hvars(τ) as required. ⊓ ⊔

Proposition 7. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ MSubst and suppose that x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Suppose also that gfree_{p}(x) and gfree_{p}(t) hold. Then, for all τ ∈ mgs(σ∪{x = t}) in a syntactic equality theory T, we have

hvars(σ) ⊆ hvars(τ).  (43)

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

By Definition 4, gfree_{p}(x) and gfree_{p}(t) imply that rt(x, σ) ∈ GTerms or rt(x, σ) ∈ Vars, and that rt(t, σ) ∈ GTerms or rt(t, σ) ∈ Vars. Since we have rt(x, σ), rt(t, σ) ∈ HTerms and σ ∈ MSubst, as a consequence of Proposition 4, we have rt(x, σ) = xσ, rt(t, σ) = tσ and xσ, tσ ∉ dom(σ). There are three cases:

– vars(xσ) = ∅ ∨ vars(tσ) = ∅. Then the result follows from Proposition 5.

– xσ = tσ ∈ Vars. Then letting τ = σ gives the required result.

– xσ, tσ ∈ Vars are distinct variables. Let τ = σ ∪ {xσ = tσ}. Then, as xσ, tσ ∉ dom(σ), τ ∈ RSubst. Hence, by Lemma 3, τ ∈ mgs(σ ∪ {x = t}). Let y be any variable in hvars(σ). We show that y ∈ hvars(τ). Suppose first that y ≠ xσ. Then yτ = yσ. Thus using Proposition 4, rt(y, σ) = yτ and vars(yτ) ∩ dom(σ) = ∅. Thus vars(yτ) ∩ dom(τ) ⊆ {rσ}. However, rστ = tσ ∉ dom(τ) so that, by Definition 5, vars(yτ) ⊆ hvars_{1}(τ) and hence y ∈ hvars_{2}(τ). Therefore, by Lemma 6 and Definition 6, we have y ∈ hvars(τ). Secondly, suppose that y = xσ. Then yτ = tσ. So that, as tσ ∈ Vars \dom(σ) and xσ ≠ tσ, vars(yτ) ∩ dom(τ) = ∅. Therefore, using Definition 6, we have that y ∈ hvars(τ) as required. ⊓ ⊔

Proposition 8. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let σ ∈ γ_{P} (p) ∩ MSubst and suppose that x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Furthermore, suppose that or lin_{p}(x, t) and share lin_{p}(x, t) hold. Then, for all τ ∈ mgs(σ ∪ {x = t}) in a syntactic equality theory T, we have

hvars(σ) \ share same var_{p}(x, t) ⊆ hvars(τ).  (44)

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

As x ∈ hvars(σ) and vars(t) ⊆ hvars(σ), we have, using Proposition 4, rt(x, σ) = xσ and rt(t, σ) = tσ. Also

vars(xσ) ∩ dom(σ) = ∅, vars(tσ) ∩ dom(σ) = ∅.  (45)

By hypothesis, or lin_{p}(x, t) holds so that, by Definition 4, for some r ∈ {x, t}, rσ is linear. Also by hypothesis, share lin_{p}(x, t) holds so that, by Definition 4, if r′ = {x, t} \ {r}, for all z ∈ vars(rσ) ∩ vars(r′σ), occ lin(z, r′σ) holds. Therefore,

vars(rσ) ∩ nlvars(r′σ) = ∅.  (46)

By Lemma 3 and the congruence axioms, σ ∪ {x = t} ⟹ {rσ = r′σ}. Thus, as σ ∪ {x = t} is satisfiable, mgs(rσ = r′σ) ≠ ∅. Thus, as rσ is linear and (46) holds, we can apply Lemma 12 (where s̄ = rσ and t̄ = r′σ) so that there exists μ ∈ mgs(xσ = tσ) such that, for all w ∈ dom(μ) \ (vars(xσ) ∩ vars(tσ)),

vars(wμ) ∩ dom(μ) = ∅.  (47)

Note that, by (45),

dom(σ) ∩ vars(μ) = ∅.  (48)

Let

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

Then, as σ, μ ∈ RSubst, it follows from (48) that ν, τ ∈ Eqs have no identities or circular subsets so that ν, τ ∈ RSubst. By Lemma 3, τ ∈ mgs(σ ∪ {x = t}).

Suppose y ∈ hvars(σ) \ share same var_{p}(x, t). We show that y ∈ hvars(τ). As y ∈ hvars(σ), using Proposition 4, rt(y, σ) = yσ and

vars(yσ) ∩ dom(σ) = ∅.  (49)

As y ∉ share same var_{p}(x, t), by Definition 4,

vars(yσ) ∩ vars(xσ) ∩ vars(tσ) = ∅.  (50)

Therefore, using (50) if y ∉ dom(σ) and (45) if y ∈ dom(σ), it follows that

y ∉ vars(xσ) ∩ vars(tσ).  (51)

We show that vars(yτ) ∩ dom(τ) = ∅. Now, if y ∉ dom(τ), the result holds trivially. Suppose that y ∈ dom(ν), then yτ = yσμ. Let w be any variable in vars(yσ). Then, by (50), w ∉ (vars(xσ) ∩ vars(tσ)) and, by (49), w ∉ dom(σ). If w ∉ dom(μ), then w = wμ ∉ dom(τ). If w ∈ dom(μ), then vars(wμ) ⊆ vars(μ) so that, by (48), we also have vars(wμ) ∩ dom(ν) = ∅. Moreover (47) applies so that vars(wμ) ∩ dom(μ) = ∅. Therefore, vars(wμ) ∩ dom(τ) = ∅. It follows that vars(yν) ∩ dom(τ) = ∅. Finally, suppose y ∈ dom(μ). Then yτ = yμ and, by (48), vars(yμ) ∩ dom(ν) = ∅. As (51) holds, (47) applies where w is replaced by y so that vars(yμ) ∩ dom(μ) = ∅. Thus vars(yμ) ∩ dom(τ) = ∅.

Therefore, using Definition 6, we have that y ∈ hvars(τ) as required. ⊓ ⊔

Proposition 9. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ MSubst and suppose that {r, r′} = {x, t}, vars(r) ⊆ hvars(σ) and lin_{p}(r) holds. Then, for all τ ∈ mgs(σ ∪ {x = t}) in a syntactic equality theory T, we have

hvars(σ) \ share with_{p}(r) ⊆ hvars(τ).  (52)

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

By hypothesis, vars(r) ⊆ hvars(σ). Hence, by Proposition 4, rt(r, σ) = rσ and

vars(rσ) ∩ dom(σ) = ∅.  (53)

By hypothesis, lin_{p}(r) holds, so that, by Definition 4, rσ is linear.

Let

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

Since rσ is linear, it follows from (53) that s̄ is linear. By Lemma 3 and the congruence axioms, σ ∪ {x = t} ⟹ s̄ = t̄. Thus, as σ ∪ {x = t} is satisfiable, we have mgs(s̄ = t̄) ≠ ∅. Therefore, we can apply Lemma 13 so that there exists μ ∈ mgs(s̄ = t̄) such that, for all w ∈ dom(μ) \ vars(s̄),

vars(wμ) ∩ dom(μ) = ∅.  (54)

Note that, since σ ∈ MSubst, for each i = 1, …, l, we have

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

Thus

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

Let

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

Then, as σ, μ ∈ RSubst, it follows from (55) that ν, τ ∈ Eqs have no identities or circular subsets so that ν, τ ∈ RSubst. By Lemma 3, τ ∈ mgs(σ ∪ {x = t}).

Suppose y ∈ hvars(σ) \ share with_{p}(r). Then we show that y ∈ hvars(τ). As y ∈ hvars(σ), by Proposition 4, rt(y, σ) = yσ and

vars(yσ) ∩ dom(σ) = ∅.  (56)

As y ∉ share with_{p}(r), by Definition 4, y ∉ share same var_{p}(y, r) so that, using the same definition,

vars(yσ) ∩ vars(rσ) = ∅.  (57)

Therefore using (57) if y ∉ dom(σ) and (53) if y ∈ dom(σ), it follows that

y ∉ vars(rσ).  (58)

We show that vars(yτ) ∩ dom(τ) = ∅. Now, if y ∉ dom(τ), the result holds trivially. Suppose that y ∈ dom(ν). Then yτ = yσμ and y ∈ dom(σ). It follows from (56) and (57) that vars(yσ) ∩ vars(s̄) = ∅. Let w be any variable in vars(yσ) so that w ∉ vars(s̄). By (56), we have w ∉ dom(σ). If w ∉ dom(μ), then w = wμ ∉ dom(τ). If w ∈ dom(μ), then vars(wμ) ⊆ vars(μ) so that, by (55), vars(wμ) ∩ dom(ν) = ∅. Moreover (54) applies so that vars(wμ) ∩ dom(μ) = ∅. Therefore, vars(wμ) ∩ dom(τ) = ∅. It follows that vars(yν) ∩ dom(τ) = ∅. Finally, suppose y ∈ dom(μ). Then yτ = yμ and, by (55), vars(yμ) ∩ dom(ν) = ∅. As σ ∈ MSubst and y ∈ hvars(σ), y ∉ dom(σ) ∩ (vars(rσ) ∪ vars(r′σ)) and hence y ∉ vars(s̄). Therefore (54) applies and vars(yμ) ∩ dom(μ) = ∅. Thus vars(yμ) ∩ dom(τ) = ∅.

Therefore, using Definition 6, we have that y ∈ hvars(τ) as required. ⊓ ⊔ Proposition 10. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ MSubst. Then, for all τ ∈ mgs(σ ∪ {x = t}) in a syntactic equality theory T,

hvars(σ) \ (share with_{p}(x) ∪ share with_{p}(t)) ⊆ hvars(τ).  (59)

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

Let

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

Note that, since σ ∈ MSubst, for each i = 1, …, l, we have

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

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

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

Let

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

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

Suppose y ∈ hvars(σ) \ (share with_{p}(x) ∪ share with_{p}(t)). We show that y ∈ hvars(τ). As y ∈ hvars(σ), by Proposition 4, rt(y, σ) = yσ and

vars(yσ) ∩ dom(σ) = ∅.  (61)

As y ∉ share with_{p}(x) ∪ share with_{p}(t), it follows from Definition 4 that

y ∉ share same var_{p}(y, x) ∪ share same var_{p}(y, t)

so that, using the same definition with the result that rt(y, σ) = yσ, we obtain

vars(yσ) ∩ (vars(xσ) ∪ vars(tσ)) = ∅.  (62)

Therefore, using (62) if y ∉ dom(σ) and using the fact that σ ∈ MSubst, if y ∈ dom(σ), it follows that

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

We show that vars(yτ) ∩ dom(τ) = ∅. Now, if y ∉ dom(τ), the result holds trivially. Suppose that y ∈ dom(τ). Then, by (60) and (63), y ∉ vars(μ) so that y ∉ dom(μ) and vars(yμ) ∩ dom(μ) = ∅. Thus we must have y ∈ dom(ν) and yτ = yσ. Then, by (60) and (62), vars(yσ) ∩ dom(μ) = ∅. Moreover, by (61), vars(yσ) ∩ dom(σ) = ∅. It follows that vars(yσ) ∩ dom(τ) = ∅ and hence, as yσ = yτ, vars(yτ) ∩ dom(τ) = ∅.

Therefore, using Definition 6, we have that y ∈ hvars(τ) as required. ⊓ ⊔

Proof (Proof of Theorem 2).

By hypothesis, σ ∈ γ_{P} (p). By Theorem 5, there exists σ′ ∈ MSubst such that σ ⟺ σ′. By Lemma 10, we have hvars(σ) = hvars(σ′). By Definition 3, σ ∈ γ_{P} (p) if and only if σ′ ∈ γ_{P} (p). We therefore safely assume that σ ∈ MSubst.

By hypothesis, we have σ ∈ γ_{H}(h). Therefore, it follows from Definition 7 that h ⊆ hvars(σ). Similarly, by Definition 7, in order to prove τ ∈ γ_{H}(h′), we just need to show that h′ ⊆ hvars(τ) where h′ is as defined in Definition 8. There are eight cases that have to be considered.

1. hterm_{h}(x) ∧ ground_{p}(x) holds.

As hterm_{h}(x) holds, by Definition 8, x ∈ h. Hence, by Definition 7, we have x ∈ hvars(σ). As ground_{p}(x) holds, by Definition 4, rt(x, σ) ∈ GTerms. Therefore we can apply Proposition 5, where r is replaced by x and r′ by t, to conclude that

hvars(σ) ∪ vars(t) ⊆ hvars(τ).

2. hterm_{h}(t) ∧ ground_{p}(t) holds.

As hterm_{h}(t) holds, by Definition 8, vars(t) ⊆ h. Hence, by Definition 7, vars(t) ⊆ hvars(σ). As ground_{p}(t) holds, by Definition 4, rt(t, σ) ∈ GTerms. Therefore we can apply Proposition 5, where r is replaced by t and r′ by x, to conclude that

hvars(σ) ∪ {x} ⊆ hvars(τ).

3. hterm_{h}(x) ∧ hterm_{h}(t) ∧ ind_{p}(x, t) ∧ or lin_{p}(x, t) holds. As hterm_{h}(x) and hterm_{h}(t) hold, by Definition 8, x ∈ h and vars(t) ⊆ h. Hence, by Definition 7, x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 6 to conclude that

hvars(σ) ⊆ hvars(τ).

4. hterm_{h}(x) ∧ hterm_{h}(t) ∧ gfree_{p}(x) ∧ gfree_{p}(t) holds. As hterm_{h}(x) and hterm_{h}(t) hold, by Definition 8, x ∈ h and vars(t) ⊆ h. Hence, by Definition 7, x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 7 to conclude that

hvars(σ) ⊆ hvars(τ).

5. hterm_{h}(x) ∧ hterm_{h}(t) ∧ share lin_{p}(x, t) ∧ or lin_{p}(x, t) holds. As hterm_{h}(x) and hterm_{h}(t) hold, by Definition 8, x ∈ h and vars(t) ⊆ h. Hence, by Definition 7, x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 8 to conclude that

hvars(σ) \ share same var_{p}(x, t) ⊆ hvars(τ).

6. hterm_{h}(x) ∧ lin_{p}(x) holds.

As hterm_{h}(x) holds, by Definition 8, x ∈ h. Hence, by Definition 7, we have x ∈ hvars(σ). Therefore we can apply Proposition 9 where r is replaced by x and r′ by t, to conclude that

hvars(σ) \ share with_{p}(x) ⊆ hvars(τ).

7. hterm_{h}(t) ∧ lin_{p}(t) holds.

As hterm_{h}(t) holds, by Definition 8, vars(t) ⊆ h. Hence, by Definition 7, vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 9 where r is replaced by t and r′ by x, to conclude that

hvars(σ) \ share with_{p}(t) ⊆ hvars(τ).

8. For all (x ↦ t) ∈ Bind where {x} ∪ vars(t) ⊆ VI , Proposition 10 applies so

that

hvars(σ) \ (share with_{p}(x) ∪ share with_{p}(t)) ⊆ hvars(τ).
⊓ ⊔

Appendix References

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

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

[Cla78] K. L. Clark, Negation as failure, Logic and Databases (Toulouse, France) (H. Gallaire and J. Minker, eds.), Plenum Press, 1978, pp. 293–322.

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

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

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

[HBZ01] P. M. Hill, R. Bagnara, and E. Zaffanella, Soundness, idempotence and commutativity of set-sharing, Theory and Practice of Logic Programming (2001),

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

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