An Efficient and Precise Finite-Tree Analysis for Constraint Logic-Based Languages^{1}

Roberto Bagnara and Enea Zaffanella Department of Mathematics University of Parma, Italy E-mail: bagnara@cs.unipr.it, zaffanella@cs.unipr.it

and

Roberta Gori Department of Computer Science University of Pisa, Italy E-mail: gori@di.unipi.it

and

Patricia M. Hill School of Computing University of Leeds, U.K. E-mail: hill@comp.leeds.ac.uk

Version: April 10, 2002

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 safe omission of the occurs-check) and increased expressivity (cyclic terms can provide very efficient representations 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 widely-used program analysis and manipulation techniques are correct only for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of the 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, in the style of the open product construction of Cortesi et al., 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. This finite-tree analysis domain is further enhanced by coupling it with a domain of Boolean functions, called finite-tree dependencies, that precisely captures how the finiteness of some variables influences the finiteness of other variables. We also summarize our experimental results showing how finite-tree analysis, enhanced with finite-tree dependencies, is a practical means of obtaining precise finiteness information.

1This work has been partly supported by MURST projects “Certificazione automatica di programmi mediante interpretazione astratta” and “Interpretazione astratta, sistemi di tipo e analisi control-flow”. Some of this work was done during visits of the second author to Leeds, funded by EPSRC under grant M05645.

1. INTRODUCTION

The intended computation domain of most logic-based languages^{2} includes the algebra (or structure) of finite trees. Other (constraint) logic-based languages, such as Prolog II and its successors [18, 20], SICStus Prolog [63], and Oz [59], refer to a computation domain of rational trees.^{3} A rational tree is a possibly infinite tree with a finite number of distinct subtrees and where each node has a finite number of immediate descendants. These properties 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 [32], parser generation and grammar manipulation [18, 35], and computing with finite-state automata [18]. Other applications are described in [34] and [37]. Going from Prolog to CLP, [53] combines constraints on rational trees and record structures, while the logic-based language Oz allows constraints over rational and feature trees [59]. 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) [55], in the ALE system (Attribute Logic Engine) [12], and in the ProFIT system (Prolog with Features, Inheritance and Templates) [33].

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^{4} and for complexity analysis^{5} 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 interrupting the program. 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 with a finiteness analysis providing the precondition for the applicability of the other techniques.

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

3Support for rational trees is also provided as an option by the YAP Prolog system [56].

4Such as TerminWeb [16, 17], TermiLog [49], cTI [54], and LPTP [61, 62].

5Systems like GAIA [21], CASLOG [31], and the Ciao-Prolog preprocessor [38].

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. Builtins 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:^{6} failing, raising an exception, answering Y = [a] (if duplicates are deleted) and answering Y = [a|Y] (if duplicates are kept) can all 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.^{7} 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 could be used 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 ensuring that such a predicate is never called with an illegal argument, will result in a robuster system. With the appropriate data-flow analyses, safe libraries do not have to be inefficient libraries.

Another serious problem is the following: the standard term ordering dictated by ISO Prolog [43] 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 is obtained by assuming B @< A. As a consequence, applying any Prolog term-ordering predicate to terms where one or both of them is infinite 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.

6Even though sort/2 is not required to be a built-in by the ISO Prolog standard, it is offered as such by several implementations.

7SICStus 3.9.0 still loops on ?- X = [97|X], name(Y, X).

Still on efficiency, it is worth noting that even for built-ins whose definition on rational trees is not problematic, there is often a performance penalty in catering for the possibility of infinite trees. Thus, for such predicates, a compile-time knowledge of term finiteness can also be beneficial. For instance, rational-tree implementa-

tions of the built-ins ground/1, term_variables/2, copy_term/2, subsumes/2,

variant/2 and numbervars/3 need to use some sort of marking to ensure they do not enter an infinite loop. With finiteness information it is possible to avoid this overhead.

In this paper, we present a parametric abstract domain for finite-tree analysis, denoted by H ×P. This domain combines a simple component H (written with the initial of Herbrand and called 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 [6] for an account of some of them). By giving a generic specification for this parameter component, in the style of the open product construct proposed in [25], 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 information encoded by H is attribute independent [27], which means that each variable is considered in isolation. What this lacks is information about how finiteness of one variable affects the finiteness of other variables. This kind of information, usually called relational information, is not captured at all by H and is only partially captured by the composite domain H × P. Moreover, H × P is designed to capture the “negative” aspect of term-finiteness, that is, the circumstances under which finiteness can be lost. However, term-finiteness has also a “positive” aspect: there are cases where a variable is granted 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, besides those explicitly provided to test for term-finiteness such as the acyclic_term/1 predicate of SICStus Prolog. For these reasons H × P is coupled with a domain of Boolean functions that precisely captures how the finiteness of some variables influences the finiteness of other variables. This domain of finite-tree dependencies provides relational information that is important for the precision of the overall finite-tree analysis.

The domain H × P also has obvious similarities, interesting differences and somewhat unexpected connections with classical domains for groundness dependencies. Finite-tree and groundness dependencies are similar in that they both track covering information (a term s covers t if all the variables in t also occur in s) and share several abstract operations. However, they are different because covering does not tell the whole story. Suppose x and y are free variables before either the unification x = f(y) or the unification x = f(x, y) are executed. In both cases, x will be ground if and only if y will be so. However, when x = f(y) is the performed unification, this equivalence will also carry over to finiteness. In contrast, when the unification is x = f(x, y), x will never be finite and will be totally independent, as far as finiteness is concerned, from y. Among the unexpected connections is the fact that finite-tree dependencies can improve the groundness information obtained by the usual approaches to groundness analysis.

The paper is structured as follows. The required notations and preliminary concepts are given in Section 2. The concrete domain for the analysis is presented in Section 3. The finite-tree domain is then introduced in Section 4: Section 4.1 provides the specification of the parameter domain P; Section 4.2 defines some computable operators that extract, from substitutions in rational solved form, properties of the denoted rational trees; Section 4.3 defines the abstraction function for the finiteness component H; Section 4.4 defines the abstract unification operator for H ×P. Section 5 introduces the use of Boolean functions for tracking finite-tree dependencies, whereas Section 6 illustrates the interaction between groundness and finite-tree dependencies. Our experimental results are presented in Section 7. We conclude the main body of the paper in Section 8.

Appendix A specifies the sharing domain SFL defined in [41, 64] as a possible instance of the parameter P. All the results are then proved in Appendix B.

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 one function symbol having rank 0 and one having rank greater than 0. Let Vars denote a denumerable set of variables disjoint from Sig and Terms denote 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 non-leaf 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.

Suppose s, t ∈ Terms: s and t are independent if vars(s) ∩ vars(t) = ∅; t is said to be ground if vars(t) = ∅; t is free if t ∈ Vars; if y ∈ vars(t) occurs exactly once in t, then we say that variable y occurs linearly in t, more briefly written using the predication occ lin(y, t); t is linear if we have occ lin(y, t) for all y ∈ vars(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. As we have specified that Sig contains function symbols of rank 0 and rank greater than 0, GTerms ∩ HTerms ≠ ∅ and GTerms \ HTerms ≠ ∅.

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

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

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

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

If t ∈ HTerms, we write tσ to denote σ(t) and tστ to denote (tσ)τ.

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

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

We denote by vars(σ) the set of variables occurring in the bindings of σ. 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.

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

(τ ∘ σ)(t) = τ(σ(t)) = tστ

and has the formulation

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

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

Consider an infinite sequence of terms t_{0}, t_{1}, t_{2}, … with t_{i} ∈ HTerms for each i ∈ ℕ. Suppose there exists t ∈ Terms such that, for each n ∈ ℕ, there exists m_{0} ∈ ℕ such that, for each m ∈ ℕ with m ≥ m_{0}, the trees corresponding to the terms t and t_{m} coincide up to the first n levels. Then we say that the sequence t_{0}, t_{1}, t_{2}, … converges to t and we write t = lim_{i→∞} t_{i} [8].

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

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

converges [8, 48]. Therefore, the function rt: HTerms ×RSubst → Terms such that

rt(t, σ) =^{def} lim_{i→∞} σ^{i}(t)

is well defined.

2.2. Equations

An equation is a statement 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).

Languages such as Prolog II, SICStus and Oz are based on RT , the theory of rational trees [18, 19]. 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 non-domain 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 . Equality theories and, in particular, RT are presented in more detail in Section B.1.1. 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. For instance, {x = y, y = z} and {x = f(y), y = f(x)} are in rational solved form. We refer the interested reader to [46, 47, 50] 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), i.e., if theory RT entails the first order formula ∀(σ → 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).

In the sequel, in order to model the constraint accumulation process of logicbased languages, we will need to characterize those sets of equations that are stronger than (that can be obtained by adding equations to) a given set of equations.

Definition 1. (↓(·)) The function ↓(·): RSubst → ℘(RSubst) is defined, for each σ ∈ RSubst, by

↓ σ =^{def} { τ ∈ RSubst | ∃σ′ ∈ RSubst . τ ∈ mgs(σ ∪ σ′) }.

The next result shows that ↓(·) corresponds to the closure by entailment in RT .

Proposition 2. Let σ ∈ RSubst. Then

↓ σ = { τ ∈ RSubst | RT ⊢ ∀(τ → σ) }.

2.3. Boolean Functions

Boolean functions have already been extensively used for data-flow analysis of logic-based languages. An important class of these functions used for tracking groundness dependencies is Pos [1]. This domain was introduced in [51] under the name Prop and further refined and studied in [23, 52].

Boolean functions are based on the notion of Boolean valuation.

Definition 3. (Boolean valuation.) Let VI ∈ ℘_{f}(Vars) and Bool =^{def} {0, 1}. The set of Boolean valuations over VI is given by

Bval =^{def} VI → Bool.

For each a ∈ Bval, each x ∈ VI , and each c ∈ Bool the valuation a[c/x] ∈ Bval is given, for each y ∈ VI , by

a[c/x](y) =^{def} \begin{cases}c, & if x = y; \\ a(y), & otherwise. \end{cases}

If X = {x_{1}, …, x_{k}} ⊆ VI , then a[c/X] denotes a[c/x_{1}] ⋯ [c/x_{k}].

The distinguished elements 0, 1 ∈ Bval are given by

0 =^{def} λx ∈ VI . 0,
1 =^{def} λx ∈ VI . 1.

Definition 4. (Boolean function.) The set of Boolean functions over VI is

Bfun =^{def} Bval → Bool.

Bfun is partially ordered by the relation ⊧ where, for each ϕ, ψ ∈ Bfun,

ϕ ⊧ ψ ⟺^{def} (∀a ∈ Bval : ϕ(a) = 1 ⟹ ψ(a) = 1).

The distinguished elements ⊥, ⊤ ∈ Bfun are the functions defined by

⊥ =^{def} λa ∈ Bval . 0,
⊤ =^{def} λa ∈ Bval . 1.

For ϕ ∈ Bfun, x ∈ VI , and c ∈ Bool, the Boolean function ϕ[c/x] ∈ Bfun is given, for each a ∈ Bval, by

ϕ[c/x](a) =^{def} ϕ(a[c/x]).

When X ⊆ VI , ϕ[c/X] is defined in the expected way. If ϕ ∈ Bfun and x, y ∈ VI the function ϕ[y/x] ∈ Bfun is given, for each a ∈ Bval, by

ϕ[y/x](a) =^{def} ϕ(a[a(y)/x]).

Boolean functions are constructed from the elementary functions corresponding to variables and by means of the usual logical connectives. Thus, for each x ∈ VI , x also denotes the Boolean function ϕ such that, for each a ∈ Bval, ϕ(a) = 1 if and only if a(x) = 1. For ϕ_{1}, ϕ_{2} ∈ Bfun, we write ϕ_{1} ∧ ϕ_{2} to denote the function ϕ such that, for each a ∈ Bval, ϕ(a) = 1 if and only if both ϕ_{1}(a) = 1 and ϕ_{2}(a) = 1. A variable is restricted away using Schröder’s elimination principle [57]:

∃x . ϕ =^{def} ϕ[1/x] ∨ ϕ[0/x].

Note that existential quantification is both monotonic and extensive on Bfun. The other Boolean connectives and quantifiers are handled similarly. For notational convenience, when X ⊆ VI , we inductively define

⋀ X =^{def} \begin{cases}⊤, & if X = ∅; \\ x ∧ ⋀(X \ \{x\}) & if x ∈ X. \end{cases}

Pos ⊂ Bfun consists precisely of those functions assuming the true value under the everything-is-true assignment, i.e.,

Pos =^{def} { ϕ ∈ Bfun | ϕ(1) = 1 }.

For each ϕ ∈ Bfun, the positive part of ϕ, denoted pos(ϕ), is the strongest Pos formula that is entailed by ϕ. Formally,

pos(ϕ) =^{def} ϕ ∨ ⋀ VI .

For each ϕ ∈ Bfun, the set of variables necessarily true for ϕ and the set of variables necessarily false for ϕ are given, respectively, by

true(ϕ) =^{def} { x ∈ VI | ∀a ∈ Bval : ϕ(a) = 1 ⟹ a(x) = 1 },
false(ϕ) =^{def} { x ∈ VI | ∀a ∈ Bval : ϕ(a) = 1 ⟹ a(x) = 0 }.

3. THE CONCRETE DOMAIN

A knowledge of the basic concepts of abstract interpretation theory [26, 28] is assumed. In this paper, the concrete domain consists of 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 5. (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.

The operation of projecting x ∈ Vars away from (Σ, V) ∈ D^{♭} is defined as follows:

∃∃ x . (Σ, V) =^{def} \{ σ′ ∈ RSubst | \begin{matrix}σ ∈ Σ, \overline{V} = Vars \ V, \\ RT ⊢ ∀(∃\overline{V} . (σ′ ↔ ∃x . σ)) \end{matrix} \}.

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 [3] 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.^{8} As a consequence, when the context makes it clear, we will write Σ ∈ D^{♭} as a shorthand for (Σ, VI ) ∈ D^{♭}.

8This 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.

4. 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 [29, 60] 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.^{9} 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 6. (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 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 finitetree 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 [6, 9, 36]. However, this would tie our specification to a particular sharing analysis domain, whereas the overall approach is inherently more general. For this reason, we will define a finite-tree analysis based on the abstract domain schema H × P, where the generic sharing component P is a parameter of the abstract domain construction. This approach can be formalized as an application of the open product operator [25].

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

9Such a requirement is typically obtained by replacing the unification with a call to the standard predicate unify with occurs 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.

The interface between H and P is provided by a set of abstract operators that satisfy suitable correctness criteria. We only specify those that are useful for defining abstract unification and projection on the combined domain H × P. Other operations needed for a full description of the analysis, such as renaming and upper bound, are very simple and, as usual, do not pose any problems.

Definition 8. (Abstract operators on P.) Let s, t ∈ HTerms be finite terms. For each p ∈ P, we specify 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 is linear in p if and only if lin_{p}: HTerms → Bool holds for s, where

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

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;

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 pair of terms 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′).

The function proj_{P} : P × VI → P correctly captures the operation of projecting away a variable from an element of P. For each x ∈ VI , p ∈ P and σ ∈ γ_{P} (p), if τ ∈ ∃∃ x . {σ}, then τ ∈ γ_{P} (proj_{P} (p, x)).

As it will be shown in Section A, some of these generic operators can be directly mapped to the corresponding abstract operators defined for well-known sharing analysis domains. However, the specification given in Definition 8, besides being more general than a particular implementation, also allows for a modular approach when proving correctness results.

4.2. Operators on Substitutions in Rational Solved Form

There are cases when an analysis tries to capture properties of the particular substitutions computed by a specific (ordinary or rational) unification algorithm. This is the case, for example, when the analysis needs to track structure sharing for the purpose of compile-time garbage collection, or provide upper bounds on the amount of memory needed to perform a given computation. More often the interest is on properties of the (finite or rational) trees that are denoted by such substitutions.

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 (as usual, this is modulo the possible renaming of variables). 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 to 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 function

σ^{∞} =^{def} λt ∈ HTerms . rt(t, σ),

obtained by fixing the substitution parameter of ‘rt’. The problem is that, in general, σ^{∞} is not a substitution: while having a finite domain, its “bindings” x ↦ lim_{i→∞} σ^{i}(x) can map a domain variable x to an infinite rational term. 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. Of course, it is important that the properties under investigation are exactly captured, so as to avoid any unnecessary precision loss. Pursuing this goal requires an ability to observe properties of (infinite) rational trees while just dealing with one of their finite representations. This is not always an easy task since even simple properties can be “hidden” when using non-idempotent substitutions. For instance, when σ^{∞} maps variable x to an infinite and ground rational tree (i.e., when rt(x, σ) ∈ GTerms\HTerms), all of its finite representations in RSubst (i.e., all the τ ∈ RSubst such that RT ⊧ ∀(σ ↔ τ)) will map the variable x into a finite term that is not ground. These are the motivations behind the introduction of the following computable operators on substitutions.

The groundness operator ‘gvars’ captures the set of variables that are mapped to ground rational trees by rt. We define it by means of the occurrence operator ‘occ’. This was introduced in [40] as a replacement for the sharing-group operator ‘sg’ of [44]. In [40] the occ operator is used to define a new abstraction function for set-sharing analysis that, differently from the classical ones [22, 44], maps equivalent substitutions in rational solved form to the same abstract element.

Definition 9. (Occurrence and groundness operators.) For each n ∈ ℕ, the occurrence function occ_{n}: RSubst × Vars → ℘_{f}(Vars) is defined, for each σ ∈ RSubst and each v ∈ Vars, by

occ_{n}(σ, v) =^{def} \begin{cases}\{v\} \ dom(σ), & if n = 0; \\ \{ y ∈ Vars | vars(yσ) ∩ occ_{n−1}(σ, v) ≠ ∅ \}, & if n > 0. \end{cases}

The occurrence operator occ: RSubst × Vars → ℘_{f}(Vars) is given, for each substitution σ ∈ RSubst and v ∈ Vars, by occ(σ, v) =^{def} occ_{ℓ}(σ, v), where ℓ = # σ.

The groundness operator gvars: RSubst → ℘_{f}(Vars) is given, for each substitution σ ∈ RSubst, by

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

Example 10. Let

σ = {x ↦ f(y, z), y ↦ g(z, x), z ↦ f(a)}.

Then gvars(σ) = {x, y, z}, although vars(xσ^{i}) ≠ ∅ and vars(yσ^{i}) ≠ ∅, for all 0 ≤ i < ∞.

The finiteness operator is defined, like occ, by means of a fixpoint construction.

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

For each σ ∈ RSubst and each i ≥ 0, we have hvars_{i}(σ) ⊆ hvars_{i+1}(σ) and also that Vars \ hvars_{i}(σ) ⊆ dom(σ) is a finite set. By these two properties, the chain hvars_{0}(σ) ⊆ hvars_{1}(σ) ⊆ ⋯ is stationary and finitely computable. In particular, if ℓ = # σ, then, for all n ≥ ℓ, hvars_{ℓ}(σ) = hvars_{n}(σ).

Definition 12. (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 13. If σ ∈ RSubst and x ∈ Vars then

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

Example 14. 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(σ), although vars(x_{1}σ) ⊆ dom(σ).

The following proposition states how ‘gvars’ and ‘hvars’ behave with respect to the further instantiation of variables.

Proposition 15. Let σ, τ ∈ RSubst, where τ ∈ ↓ σ. Then

hvars(σ) ⊇ hvars(τ),  (15a)
gvars(σ) ∩ hvars(σ) ⊆ gvars(τ) ∩ hvars(τ).  (15b)

4.3. The Abstraction Function for H

A Galois connection between ℘(RSubst) and H can now be defined naturally.

Definition 16. (The Galois connection between ℘(RSubst) and 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 [26]: whenever h ∈ H,

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

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

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

4.4. Abstract Unification and Projection 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 18. (Abstract unification on H × P.) A term t ∈ HTerms is a finite tree in h ∈ 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′ is given by the first case that applies in

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 variables which may be possibly bound to cyclic terms 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 [29, 60]. Accordingly, it is required that both x and t describe finite terms that do not share. 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 [29], this may happen when the component P embeds the domain Pos for groundness analysis.^{10}

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 [6] is a safe, more precise 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, only the shared variables can introduce cycles.

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.

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

Theorem 19. 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′).

Abstract projection on the composite domain H × P is much simpler than abstract unification, because in this case there is no interaction between the two components of the abstract domain.

Definition 20. (Abstract projection on H ×P.) The function proj_{H}: H × VI → H captures the effects, on the H component, of projecting away a variable. For each h ∈ H and x ∈ VI ,

proj_{H}(h, x) =^{def} h ∪ {x}.

10Let t be y. Let also P be Pos. Then, given the Pos formula ϕ =^{def} (x ∨ y), both ind_{ϕ}(x, y)

and or lin_{ϕ}(x, y) satisfy the conditions in Definition 4. Note that from ϕ we cannot infer that x is definitely linear and neither that y is definitely linear.

The abstract variable projection function proj: (H × P) × VI → H × P, for any ⟨h, p⟩ ∈ H × P and x ∈ VI , is given by

proj(⟨h, p⟩, x) =^{def} ⟨proj_{H}(h, x), proj_{P} (p, x)⟩.

As a consequence, as far as the H component is concerned, the correctness of the projection function does not depend on the assumption on proj_{P} as specified in Definition 8.

Theorem 21. Let x ∈ VI , h ∈ H and σ ∈ γ_{H}(h). Then

τ ∈ ∃∃ x . {σ} ⟹ τ ∈ γ_{H}(proj_{H}(h, x)).

Several abstract domains for sharing analysis can be used to implement the parameter component P. As a basic implementation, one could consider the wellknown set-sharing domain of Jacobs and Langen [44]. In such a case, most of the required correctness results have already been established in [40]. Note however that, since no freeness and linearity information is recorded in the plain set-sharing domain, some of the predicates of Definition 8 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. Another possibility would be to use the domain based on pair-sharing, definite groundness and definite linearity described in [48]. A more precise choice is constituted by the SFL domain (an acronym standing from Set-sharing plus Freeness plus Linearity) introduced in [42, 64]. Even in this case, all the non-trivial correctness results have already been proved. In particular, in [41, 64] it is shown that the abstraction function satisfies the requirement of Definition 7 and that the abstract unification operator is correct with respect to rational-tree unification. In order to better highlight the generality of our specification of the sharing component P, the instantiation of P to SFL is presented in Appendix A. Notice that the quest for more precision does not end with SFL: a number of possible precision improvements are presented and discussed in [6].

5. FINITE-TREE DEPENDENCIES

The precision of the finite-tree analysis based on H × P is highly dependent on the precision of the generic component P. As explained before, the information provided by P on groundness, freeness, linearity, and sharing of variables is exploited, in the combination H ×P, to circumscribe as much as possible the creation and propagation of cyclic terms. However, finite-tree analysis can also benefit from other kinds of relational information. In particular, we now show how finite-tree dependencies allow a positive propagation of finiteness information.

Let us consider the finite terms t_{1} = f(x), t_{2} = g(y), and t_{3} = 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}).^{11} 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.

11The introduction of such Boolean formulas, called dependency formulas, is originally due to P. W. Dart [30].

2. vars(t_{3}) ⊇ vars(t_{1}) ∪ vars(t_{2}), that is, t_{3} covers both t_{1} and t_{2}; this means that, if an assignment to the variables of t_{3} produces a finite instance of t_{3}, that very 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 this dependency will keep holding for any further simultaneous instantiation of t_{1}, t_{2}, and t_{3}. In other words, such dependencies are preserved by forward computations (which proceed by consistently instantiating program variables).

Consider x ↦ t ∈ Bind where t ∈ HTerms and vars(t) = {y_{1}, …, y_{n}}. After this binding has been successfully applied, the destinies of x and t concerning termfiniteness are tied together: forever. This tie can be described by the dependency formula

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

meaning that x will be bound to a finite term if and only if y_{i} is bound to a finite term, for each i = 1, …, n. While the dependency expressed by (2) 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 (2) is logically equivalent to

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

Although this is correct —whenever x is bound to a finite term, all the other variables will be bound to finite terms— it misses the point that x has just been bound, irrevocably, to a non-finite term: no forward computation can change this. Thus, the implication (3) holds vacuously. A more 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.”

We are building an abstract domain for finite-tree dependencies where we are making the deliberate choice of including only information that cannot be withdrawn by forward computations. The reason for this choice is that we want the concrete constraint accumulation process to be paralleled, at the abstract level, by another constraint accumulation process: logical conjunction of Boolean formulas. For this reason, it is important to distinguish between permanent and contingent information. Permanent information, once established for a program point p, maintains its validity in all points that follow p in any forward computation. Contingent information, instead, does not carry its validity beyond the point where it is established. An example of contingent information is given by the h component of H ×P: having x ∈ h in the description of some program point means that x is definitely bound to a finite term at that point; nothing is claimed about the finiteness of x at later program points and, in fact, unless x is ground, x can still be bound to a non-finite term. However, if at some program point x is finite and ground, then x will remain finite. In this case we will ensure our Boolean dependency formula entails the positive atom x.

At this stage, we already know something about the abstract domain we are designing. In particular, we have positive and negated atoms, the requirement of describing program predicates of any arity implies that arbitrary conjunctions of these atomic formulas must be allowed and, finally, it is not difficult to observe that the merge-over-all-paths operation [26] will be logical disjunction, so that the domain will have to be closed under this operation. This means that the carrier of our domain must be able to express any Boolean function: Bfun is the carrier.

Definition 22. (γ_{F} : Bfun → ℘(RSubst).) The function hval: RSubst → Bval is defined, for each σ ∈ RSubst and each x ∈ VI , by

hval(σ)(x) = 1 ⟺^{def} x ∈ hvars(σ).

The concretization function γ_{F} : Bfun → ℘(RSubst) is defined, for ϕ ∈ Bfun, by

γ_{F} (ϕ) =^{def} { σ ∈ RSubst | ∀τ ∈ ↓ σ : ϕ(hval(τ)) = 1 }.

The domain of positive Boolean functions Pos used, among other things, for groundness analysis is so popular that our use of the domain Bfun deserves some further comments. For the representation of finite-tree dependencies, the presence in the domain of negative functions such as ¬x, meaning that x is bound to an infinite term, is an important feature. One reason why it is so is that knowing about definite non-finiteness can improve the information on definite finiteness. The easiest example goes as follows: if we know that either x or y is finite (i.e., x ∨ y) and we know that x is not finite (i.e., ¬x), then we can deduce that y must be finite (i.e., y). It is important to observe that this reasoning can be applied, verbatim, to groundness: a knowledge of non-groundness may improve groundness information. The big difference is that non-finiteness is information of the permanent kind while non-groundness is only contingent. As a consequence, a knowledge of finiteness and non-finiteness can be monotonically accumulated along computation paths by computing the logical conjunction of Boolean formulae. An approach where groundness and non-groundness information is represented by elements of Bfun would need to use a much more complex operation and significant extra information to correctly model the constraint accumulation process.

The other reason why the presence of negative functions in the domain is beneficial is efficiency. The most efficient implementations of Pos and Bfun, such as the ones described in [1, 5], are based on Reduced Ordered Binary Decision Diagrams (ROBDD) [10]. While an ROBDD representing the imprecise information given by the formula (3) has a worst case complexity that is exponential in n, the more precise formula ¬x has constant complexity.

The following theorem shows how most of the operators needed to compute the concrete semantics of a logic program can be correctly approximated on the abstract domain Bfun. Notice how the addition of equations is modeled by logical conjunction and projection of a variable is modeled by existential quantification.

Theorem 23. Let Σ, Σ_{1}, Σ_{2} ∈ ℘(RSubst) and ϕ, ϕ_{1}, ϕ_{2} ∈ Bfun be such that γ_{F} (ϕ) ⊇ Σ, γ_{F} (ϕ_{1}) ⊇ Σ_{1}, and γ_{F} (ϕ_{2}) ⊇ Σ_{2}. Let also (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Then the following hold:

γ_{F} (x ↔ ⋀ vars(t)) ⊇ {{x ↦ t}};  (23a)
γ_{F} (¬x) ⊇ {{x ↦ t}}, if x ∈ vars(t);  (23b)
γ_{F} (x) ⊇ { σ ∈ RSubst | x ∈ gvars(σ) ∩ hvars(σ) };  (23c)
γ_{F} (ϕ_{1} ∧ ϕ_{2}) ⊇ { mgs(σ_{1} ∪ σ_{2}) | σ_{1} ∈ Σ_{1}, σ_{2} ∈ Σ_{2} };  (23d)
γ_{F} (ϕ_{1} ∨ ϕ_{2}) ⊇ Σ_{1} ∪ Σ_{2};  (23e)
γ_{F} (∃x . ϕ) ⊇ ∃∃ x . Σ.  (23f)

Cases (23a), (23b), and (23d) of Theorem 23 ensure that the following definition of amgu_{F} provides a correct approximation on Bfun of the concrete unification of rational trees.

Definition 24. The function amgu_{F} : Bfun×Bind → Bfun captures the effects of a binding on a finite-tree dependency formula. Let ϕ ∈ Bfun and (x ↦ t) ∈ Bind be such that {x} ∪ vars(t) ⊆ VI . Then

amgu_{F} (ϕ, x ↦ t) =^{def} \begin{cases}ϕ ∧ (x ↔ ⋀ vars(t)), & if x ∉ vars(t); \\ ϕ ∧ ¬x, & otherwise. \end{cases}

Other semantic operators, such as the consistent renaming of variables, are very simple and omitted for the sake of brevity.

The next result shows how finite-tree dependencies may improve the finiteness information encoded in the h component of the domain H × P.

Theorem 25. Let h ∈ H and ϕ ∈ Bfun. Let also h′ =^{def} true(ϕ ∧ ⋀ h). Then

γ_{H}(h) ∩ γ_{F} (ϕ) = γ_{H}(h′) ∩ γ_{F} (ϕ).

Example 26. Consider the following program, where it is assumed that the only “external” query is ‘?- r(X, Y)’:

           p(X, Y) :- X = f(Y,  ).
           q(X, Y) :- X = f( , Y).
           r(X, Y) :- p(X, Y), q(X, Y), acyclic term(X).

Then the predicate p/2 in the clause defining r/2 will called with X and Y both unbound. Computing on the abstract domain H ×P gives us the finiteness description h_{p} = {x, y}, expressing the fact that both X and Y are bound to finite terms. Computing on the finite-tree dependencies domain Bfun, gives us the Boolean formula ϕ_{p} = x → y (Y is finite if X is so).

Considering now the call to the predicate q/2, we note that, since variable X is already bound to a non-variable term sharing with Y, all the finiteness information encoded by H will be lost (i.e., h_{q} = ∅). So, both X and Y are detected as possibly cyclic. However, the finite-tree dependency information is preserved, since we have ϕ_{q} = (x → y) ∧ (x → y) = x → y.

Finally, consider the effect of the abstract evaluation of acyclic_term(X). On the H × P domain we can only infer that variable X cannot be bound to an infinite term, while Y will be still considered as possibly cyclic, so that h_{r} = {x}. On the domain Bfun we can just confirm that the finite-tree dependency computed so far still holds, so that ϕ_{r} = x → y (no stronger finite-tree dependency can be inferred, since the finiteness of X is only contingent). Thus, by applying the result of Theorem 25, we can recover the finiteness of Y:

h′_{r} = true(ϕ_{r} ∧ ⋀ h_{r}) = true((x → y) ∧ x) = true(x ∧ y) = {x, y}.

Information encoded in H × P and Bfun is not completely orthogonal and the following result provides a kind of consistency check.

Theorem 27. Let h ∈ H and ϕ ∈ Bfun. Then

γ_{H}(h) ∩ γ_{F} (ϕ) ≠ ∅ ⟹ h ∩ false(ϕ) = ∅.

Note however that, provided the abstract operators are correct, the computed descriptions will always be mutually consistent, unless ϕ = ⊥.

6. GROUNDNESS DEPENDENCIES

Since information about the groundness of variables is crucial for many applications, it is natural to consider a static analysis domain including both a finite-tree and a groundness component. In fact, any reasonably precise implementation of the parameter component P of the abstract domain specified in Section 4 will include some kind of groundness information.^{12} We highlight similarities, differences and connections relating the domain Bfun for finite-tree dependencies to the abstract domain Pos for groundness dependencies. Note that these results also hold when considering a combination of Bfun with the groundness domain Def [1].

We first define how elements of Pos represent sets of substitutions in rational solved form.

Definition 28. (γ_{G}: Pos → ℘(RSubst).) The function gval: RSubst → Bval is defined as follows, for each σ ∈ RSubst and each x ∈ VI :

gval(σ)(x) = 1 ⟺^{def} x ∈ gvars(σ).

The concretization function γ_{G}: Pos → ℘(RSubst) is defined, for each ψ ∈ Pos,

γ_{G}(ψ) =^{def} { σ ∈ RSubst | ∀τ ∈ ↓ σ : ψ(gval(τ)) = 1 }.

The following is a simple variant of the standard abstract unification operator for groundness analysis over finite-tree domains: the only difference concerns the case of cyclic bindings [2].

Definition 29. The function amgu_{G}: Pos × Bind → Pos captures the effects of a binding on a groundness dependency formula. Let ψ ∈ Pos and (x ↦ t) ∈ Bind be such that {x} ∪ vars(t) ⊆ VI . Then

amgu_{G}(ψ, x ↦ t) =^{def} ψ ∧ (x ↔ ⋀(vars(t) \ {x})).

The next result shows how, by exploiting the finiteness component H, the finitetree dependencies (Bfun) component and the groundness dependencies (Pos) component can improve each other.

Theorem 30. Let h ∈ H, ϕ ∈ Bfun and ψ ∈ Pos. Let also ϕ′ ∈ Bfun and ψ′ ∈ Pos be defined as ϕ′ = ∃VI \ h . ψ and ψ′ = ∃VI \ h . pos(ϕ). Then

γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ) = γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ ∧ ψ′);  (30a)
γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ) = γ_{H}(h) ∩ γ_{F} (ϕ ∧ ϕ′) ∩ γ_{G}(ψ).  (30b)

Moreover, even without any knowledge of the H component, combining Theorem 25 and Eq. (30a), the groundness dependencies component can be improved.

Corollary 31. Let ϕ ∈ Bfun and ψ ∈ Pos. Then

γ_{F} (ϕ) ∩ γ_{G}(ψ) = γ_{F} (ϕ) ∩ γ_{G}(ψ ∧ true(ϕ)).

12One could define P so that it explicitly contains the abstract domain Pos. Even when this is not the case, it should be noted that, as soon as the parameter P includes the set-sharing domain of Jacobs and Langen [45], then it will subsume the groundness information captured by the domain Def [15, 24].

The following example shows that, when computing on rational trees, finite-tree dependencies may provide groundness information that is not captured by the usual approaches.

Example 32. Consider the program:

                 p(a, Y).
                 p(X, a).
                 q(X, Y) :- p(X, Y), X = f(X, Z).

The abstract semantics of p/2, for both finite-tree and groundness dependencies, is ϕ_{p} = ψ_{p} = x ∨ y. The finite-tree dependency for q/2 is ϕ_{q} = (x ∨ y) ∧ ¬x = ¬x ∧ y. Using Definition 29, the groundness dependency for q/2 is

ψ_{q} = ∃z . ((x ∨ y) ∧ (x ↔ z)) = x ∨ y.

This can be improved, using Corollary 31, to

ψ′_{q} = ψ_{q} ∧ ⋀ true(ϕ_{q}) = y.

It is worth noticing that the groundness information can be improved regardless of whether, like Pos, the groundness domain captures disjunctive information: groundness information represented by the less expressive domain Def [1] can be improved as well. The next example illustrates this point.

Example 33. Consider the following program:

                   p(a, a).
                   p(X, Y) :- X = f(X,  ).
                   q(X, Y) :- p(X, Y), X = a.

Consider first the predicate p/2. Concerning finite-tree dependencies, the abstract semantics of p/2 is expressed by the Boolean formula ϕ_{p} = x → y (y is finite if x is so). In contrast, the Pos-groundness abstract semantics of p/2 is a plain “don’t know”: the Boolean formula ψ_{p} = ⊤. In fact, the groundness of X and Y can be completely decided by the call-pattern of p/2.

Consider now the predicate q/2. The finiteness semantics of q/2 is given by ϕ_{q} = (x → y) ∧ x = x ∧ y, whereas the Pos formula expressing groundness dependencies is ψ_{q} = ⊤ ∧ x = x. By applying the reduction process of Theorem 80, we obtain

ψ′_{q} = ψ_{q} ∧ ⋀ true(ϕ_{q}) = x ∧ y,

therefore recovering the groundness of variable y.

Since better groundness information, besides being useful in itself, may also improve the precision of many other analyses such as sharing [6, 15], the reduction steps given by Theorem 30 and Corollary 31 can trigger improvements to the precision of other components. Theorem 30 can also be exploited to recover precision after the application of a widening operator on either the groundness dependencies or the finite-tree dependencies component.

7. EXPERIMENTAL RESULTS

The work described here has been experimentally evaluated in the framework provided by the China analyzer [2]. We implemented and compared the three domains Pattern(P), Pattern(H × P) and Pattern(Bfun × H × P),^{13} where the parameter component P has been instantiated to the domain Pos × SFL_{2} [6, 41, 64] for tracking groundness, freeness, linearity and (non-redundant) set-sharing information. The Pattern(·) operator [3] further upgrades the precision of its argument by adding explicit structural information.

Concerning the Bfun component, the implementation was straightforward, since all the techniques described in [5] (and almost all the code, including the widenings) was reused unchanged, obtaining comparable efficiency. As a consequence, most of the implementation effort was in the coding of the abstract operators on the H component and in the reduction processes between the different components. A key choice, in this sense, is ‘when’ the reduction steps given in Theorems 25 and 30 should be applied. When striving for maximum precision, a trivial strategy is to perform reductions immediately after any application of any abstract operator. This is how predicates like acyclic_term/1 should be handled: after adding the variables of the argument to the H component, the reduction process is applied to propagate the new information to all domain components. However, such an approach turns out to be unnecessarily inefficient. In fact, the next result shows that Theorems 25 and 30 cannot lead to a precision improvement if applied just after the abstract evaluation of the merge-over-all-paths or the existential quantification operations (provided the initial descriptions are already reduced).

Theorem 34. Let x ∈ VI , h, h′ ∈ H ϕ, ϕ′ ∈ Bfun and ψ, ψ′ ∈ Pos. Let

h_{1} =^{def} h ∩ h′,  ϕ_{1} =^{def} ϕ ∨ ϕ′,  ψ_{1} =^{def} ψ ∨ ψ′,
h_{2} =^{def} proj_{H}(h, x),  ϕ_{2} =^{def} ∃x . ϕ,  ψ_{2} =^{def} ∃x . ψ.

Let also

h ⊇ true(ϕ ∧ ⋀ h),  ϕ ⊧ (∃VI \ h . ψ),  ψ ⊧ (∃VI \ h . pos(ϕ)),
h′ ⊇ true(ϕ′ ∧ ⋀ h′), ϕ′ ⊧ (∃VI \ h′ . ψ′), ψ′ ⊧ (∃VI \ h′ . pos(ϕ′)).

Then, for i = 1, 2,

h_{i} ⊇ true(ϕ_{i} ∧ ⋀ h_{i}), ϕ_{i} ⊧ (∃VI \ h_{i} . ψ_{i}), ψ_{i} ⊧ (∃VI \ h_{i} . pos(ϕ_{i})).

A goal-dependent analysis was run for all the programs in our benchmark suite and the results (with respect to the precision) are summarized in Table 1. Here, the precision is measured as the percentage of the total number of variables that the analyser can show to be finite. Two alternative views are provided.

In the first view, each column is labeled by an analysis domain and each row is labeled by a precision interval. For instance, the value ‘31’ at the intersection of column ‘H’ and row ‘80 ≤ p < 100’ is to be read as “for 31 benchmarks, the percentage p of the total number of variables that the analyzer can show to be finite using the domain H is between 80% and 100%.”

13For ease of notation, the domain names are shortened to P, H and Bfun, respectively.

Prec. class  P H Bfun
p = 100  2 84  86
80 ≤ p < 100  1 31  36
60 ≤ p < 80  7 26  23
40 ≤ p < 60  6 41  40
20 ≤ p < 40  47 47  46
0 ≤ p < 20 185 19  17

Prec. improvement P → H H → Bfun
i > 20  185  4
10 < i ≤ 20  31  3
5 < i ≤ 10  11  6
2 < i ≤ 5  4  10
0 < i ≤ 2  2  24
no improvement  15  201

TABLE 1: The precision on finite variables when using P, H and Bfun.

The second view provides a better picture of the precision improvements obtained when moving from P to H (in the column ‘P → H’) and from H to Bfun (in the column ‘H → Bfun’). For instance, the value ‘10’ at the intersection of column ‘H → Bfun’ and row ‘2 < i ≤ 5’ is to be read as “when moving from H to Bfun, for 10 benchmarks the improvement i in the percentage of the total number of variables shown to be finite was between 2% and 5%.”

It can be seen from Table 1 that, even though the H domain is remarkably precise, the inclusion of the Bfun component allows for a further, and sometimes significant, precision improvement for a number of benchmarks. It is worth noting that the current implementation of China does not yet fully exploit the finite-tree dependencies arising when evaluating many of the built-in predicates, therefore incurring an avoidable precision loss. We are working on this issue and we expect that the specialized implementation of the abstract evaluation of some built-ins will result in more and better precision improvements. The experimentation has also shown that, in practice, the Bfun domain does not improve the groundness information.

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

As a consequence, those applications that exploit rational trees tend to do so in a very controlled way, that is, most program variables can only be bound to finite terms. By detecting the program variables that may be bound to infinite terms with a good degree of accuracy, we can significantly reduce the disadvantages of using rational trees.

In this paper we have proposed an abstract-interpretation based solution to this problem, where the composite abstract domain H × P allows to track the creation and propagation of infinite terms. Even though this information is crucial to any finite-tree analysis, propagating the guarantees of finiteness that come from several built-ins (including those that are explicitly provided to test term-finiteness) is also important. Therefore, we have introduced a domain of Boolean functions Bfun for finite-tree dependencies which, when coupled to the domain H × P, can enhance its expressive power. Since Bfun has many similarities with the domain Pos used for groundness analysis, we have investigated how these two domains relate to each other and, in particular, the synergy arising from their combination in the “global” domain of analysis.

REFERENCES

[1] T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Two classes of Boolean functions for dependency analysis. Science of Computer Programming, 31(1):3–45, 1998.

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

[3] 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 Artificial Intelligence, pages 189–206, Réunion Island, France, 2000. Springer-Verlag, Berlin.

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

[5] R. Bagnara and P. Schachte. Factorizing equivalent variable pairs in ROBDDbased implementations of Pos. In A. M. Haeberer, editor, Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (AMAST’98)”, volume 1548 of Lecture Notes in Computer Science, pages 471–485, Amazonia, Brazil, 1999. Springer-Verlag, Berlin.

[6] 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.

[7] R. Bagnara, E. Zaffanella, and P. M. Hill. Enhanced sharing analysis techniques: A comprehensive evaluation. Submitted for publication. Available at

http://www.cs.unipr.it/~bagnara/, 2001.

[8] A. Berarducci and M. Venturini Zilli. Generalizations of unification. Journal of Symbolic Computation, 15:479–491, 1993.

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

[10] R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.

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

[12] 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.

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

[14] 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.

[15] M. Codish, H. Søndergaard, and P. J. Stuckey. Sharing and groundness dependencies in logic programs. ACM Transactions on Programming Languages and Systems, 21(5):948–976, 1999.

[16] M. Codish and C. Taboch. A semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints. In M. Hanus, J. Heering, and K. Meinke, editors, Algebraic and Logic Programming, 6th International Joint Conference, volume 1298 of Lecture Notes in Computer Science, pages 31–45, Southampton, U.K., 1997. Springer-Verlag, Berlin.

[17] M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming, 41(1):103–123, 1999.

[18] 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.

[19] 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.

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

[21] A. Cortesi, B. Le Charlier, and S. Rossi. Specification-based automatic verification of Prolog programs. In J. P. Gallagher, editor, Logic Programming Synthesis and Transformation: Proceedings of the 6th International Workshop, volume 1207 of Lecture Notes in Computer Science, pages 38–57, Stockholm, Sweden, 1997. Springer-Verlag, Berlin.

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

[23] A. Cortesi, G. Filé, and W. Winsborough. Prop revisited: Propositional formula as abstract domain for groundness analysis. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 322–327, Amsterdam, The Netherlands, 1991. IEEE Computer Society Press.

[24] A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation for comparing static analyses. Theoretical Computer Science, 202(1&2):163–192, 1998.

[25] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming: Open product and generic pattern construction. Science of Computer Programming, 38(1–3):27–71, 2000.

[26] 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.

[27] P. Cousot and R. Cousot. Abstract interpretation and applications to logic programs. Journal of Logic Programming, 13(2&3):103–179, 1992.

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

[29] L. Crnogorac, A. D. Kelly, and H. Søndergaard. A comparison of three occurcheck 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.

[30] P. W. Dart. On derived dependencies and connected databases. Journal of Logic Programming, 11(1&2):163–188, 1991.

[31] S. Debray and N.-W. Lin. Cost analysis of logic programs. ACM Transactions on Programming Languages and Systems, 15(5):826–875, 1993.

[32] 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.

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

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

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

[36] 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.

[37] S. Haridi and D. Sahlin. Efficient implementation of unification of cyclic structures. In Campbell [11], pages 234–249.

[38] M. Hermenegildo, F. Bueno, G. Puebla, and P. López. Program analysis, debugging, and optimization using the ciao system preprocessor. In D. De Schreye, editor, Logic Programming: The 1999 International Conference, MIT Press Series in Logic Programming, pages 52–66, Las Cruces, New Mexico, 1999. The MIT Press.

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

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

[41] P. M. Hill, E. Zaffanella, and R. Bagnara. A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages. Submitted for publication. Available at http://www.

cs.unipr.it/~bagnara/.

[42] P. M. Hill, E. Zaffanella, and R. Bagnara. A correct, precise and efficient integration of set-sharing, freeness and linearity for the analysis of finite and rational tree languages. Quaderno 273, Dipartimento di Matematica, Univer-

sità di Parma, 2001. Available at http://www.cs.unipr.it/Publications/.

Also published as technical report No. 2001.22, School of Computing, University of Leeds, U.K.

[43] ISO/IEC. ISO/IEC 13211-1: 1995 Information technology — Programming languages — Prolog — Part 1: General core. International Standard Organization, 1995.

[44] 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.

[45] D. Jacobs and A. Langen. Static analysis of logic programs for independent AND parallelism. Journal of Logic Programming, 13(2&3):291–314, 1992.

[46] 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.

[47] 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.

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

[49] N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. TermiLog: A system for checking termination of queries to logic programs. In O. Grumberg, editor, Computer Aided Verification: Proceedings of the 9th International Conference, volume 1250 of Lecture Notes in Computer Science, pages 444–447, Haifa, Israel, 1997. Springer-Verlag, Berlin.

[50] 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.

[51] K. Marriott and H. Søndergaard. Notes for a tutorial on abstract interpretation of logic programs. North American Conference on Logic Programming, Cleveland, Ohio, USA, 1989.

[52] K. Marriott and H. Søndergaard. Precise and efficient groundness analysis for logic programs. ACM Letters on Programming Languages and Systems, 2(1–4):181–196, 1993.

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

[54] U. Neumerkel and F. Mesnard. Localizing and explaining reasons for nonterminating logic programs with failure-slices. In G. Nadathur, editor, Principles and Practice of Declarative Programming, volume 1702 of Lecture Notes in Computer Science, pages 328–341, Paris, France, 1999. Springer-Verlag, Berlin.

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

[56] V. Santos Costa, L. Damas, R. Reis, and R. Azevedo. YAP User’s Manual. Universidade do Porto, version 4.3.20 edition, 2001.

[57] E. Schröder. Der Operationskreis des Logikkalkuls. B. G. Teubner, Leibzig, 1877.

[58] 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.

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

[60] 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.

[61] R. F. Stärk. Total correctness of pure Prolog programs: A formal approach. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Extensions of Logic Programming: Proceedings of the 5th International Workshop, volume 1050 of Lecture Notes in Computer Science, pages 237–254, Leipzig, Germany, 1996. Springer-Verlag, Berlin.

[62] R. F. Stärk. The theoretical foundations of LPTP (a Logic Program Theorem Prover). Journal of Logic Programming, 36(3):241–269, 1998.

[63] Swedish Institute of Computer Science, Intelligent Systems Laboratory. SIC-Stus Prolog User’s Manual, release 3.9 edition, 2002.

[64] E. Zaffanella. Correctness, Precision and Efficiency in the Sharing Analysis of Real Logic Languages. PhD thesis, School of Computing, University of Leeds,

    Leeds, U.K., 2001. Available at http://www.cs.unipr.it/~zaffanella/.

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

APPENDIX A: AN INSTANCE OF THE PARAMETER DOMAIN P

As discussed in Section 4, several abstract domains for sharing analysis can be used to implement the parameter component P. We here consider the abstract domain SFL [41, 64], integrating the set-sharing domain of Jacobs and Langen with definite freeness and linearity information.

Definition 35. (The set-sharing domain SH .) The set SH is defined by SH =^{def} ℘(SG), where SG =^{def} ℘(VI ) \ {∅} is the set of sharing groups. SH is ordered by subset inclusion.

The information about definite freeness and linearity is encoded by two sets of variables, one for each property.

Definition 36. (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; the bottom element is ⊥_{S} =^{def} ⟨∅, VI , VI ⟩.

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

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

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

For each sh ∈ SH and each x ∈ VI , the function proj_{SH} : SH × VI → SH projects away variable x from sh:

proj_{SH} (sh, x) =^{def} {{x}} ∪ { S \ {x} | S ∈ sh, S ≠ {x} }.

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

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

ind_{d}(s, t) =^{def} (sh_{s} ∩ sh_{t} = ∅);
ground_{d}(t) =^{def} (vars(t) ⊆ VI \ vars(sh));
occ lin_{d}(y, t) =^{def} ground_{d}(y) ∨ (occ lin(y, t) ∧ (y ∈ l)
∧ ∀z ∈ vars(t) : (y ≠ z ⟹ ind_{d}(y, z)));
share lin_{d}(s, t) =^{def} ∀y ∈ vars(sh_{s} ∩ sh_{t}) :
y ∈ vars(s) ⟹ occ lin_{d}(y, s)
∧ y ∈ vars(t) ⟹ occ lin_{d}(y, t);
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 ∈ vars(t) : occ lin_{d}(y, t);
or lin_{d}(s, t) =^{def} lin_{d}(s) ∨ lin_{d}(t);
share same var_{d}(s, t) =^{def} vars(sh_{s} ∩ sh_{t});
share with_{d}(t) =^{def} vars(sh_{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 {x} ∪ vars(t) ⊆ VI . Let also

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

where

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

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

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

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

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

where

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

Then

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

The function proj_{S}: SFL × VI → SFL correctly captures the operation of projecting away a variable from an element of SFL. For each d ∈ SFL and x ∈ VI ,

proj_{S}(d, x) =^{def} \begin{cases}⊥_{S}, & if d = ⊥_{S}; \\ ⟨proj_{SH} (sh, x), f ∪ \{x\}, l ∪ \{x\}⟩, & if d = ⟨sh, f, l⟩ ≠ ⊥_{S}. \end{cases}

Observe that a set-sharing domain such as SFL is strictly more precise for term finiteness information than a pair-sharing domain such as SFL_{2} [41, 64] (where the set-sharing component SH in SFL is replaced by the domain PSD as defined in [4, 65]). To see this, consider the abstract evaluation of the binding x ↦ y and the description ⟨h, d⟩ ∈ H×SFL, where h = {x, y, z} and d = ⟨sh, f, l⟩ is such that sh = {{x, y}, {x, z}, {y, z}}, f = ∅ and l = {x, y, z}. Then z ∉ share same var_{d}(x, y) so that we have h′ = {z}. In contrast, when using a pair sharing domain such as SFL_{2} the element d is equivalent to d′ = ⟨sh′, f, l⟩, where sh′ = sh ∪{{x, y, z}}. Hence we have z ∈ share same var_{d′}(x, y) and h′ = ∅. Thus, in sh the information provided by the sharing group {x, y, z} is redundant for the pair-sharing and groundness properties, but not redundant for term finiteness. Note that the above observation holds regardless of the pair-sharing variant considered, so that similar examples can be obtained for ASub [14, 60] and Sh^{PSh} [58].

Although the domain SFL described here is very precise and used to implement the parameter component P for computing our experimental results, it is not intended as the target of the generic specification given in Definition 8; more powerful sharing domains can also satisfy this schema, including all the enhanced combinations considered in [6, 7]. For instance, as the predicate gfree_{d} defined on SFL does not fully exploit the disjunctive nature of its generic specification gfree_{p}, the precision of the analysis may be improved by adding a domain component explicitly tracking ground-or-freeness, as proposed in [6, 7]. The same argument applies to the predicate or lin_{d}, with respect to or lin_{p}, when considering the combination with the groundness domain Pos.

APPENDIX B: PROOFS OF THE STATED RESULTS

This appendix 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. In Section B.2 we recall few general results holding for (syntactic) equality theories and provide the proof of Proposition 2. 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 some general results on operators on substitutions in RSubst, Propositions 13 and 15. Section B.4 is propaedeutic to Section B.5, where we prove Theorem 17 and to Section B.6, where we provide the proofs of Theorems 19 and 21. Results in Section B.4 are then used in Section B.7 to prove Theorems 23, 25 and 27, and in Section B.8 to prove Theorems 30 and 34.

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 an explicit quantifier is assumed to be universally quantified.

A path p ∈ (ℕ \ {0})^{⋆} is any finite sequence of non-zero natural numbers. The empty path is denoted by ϵ, whereas i.p denotes the path obtained by concatenating the sequence formed by the natural number i ≠ 0 with the sequence of the path p. Given a path p and a (possibly infinite) term t ∈ Terms, we denote by t[p] the subterm of t found by following path p. Formally,

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

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

The 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̄) = ∅.

B.1.1. 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,  (6)
s = t ↔ t = s,  (7)
r = s ∧ s = t → r = t,  (8)
s_{1} = t_{1} ∧ ⋯ ∧ s_{n} = t_{n} → f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n}).  (9)

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

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

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

An alternative approach used in some implementations of Prolog, does not require the occurs-check axioms. This approach is based on the theory of rational trees RT [18, 19]. 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.^{14} 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).

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. Properties of Equality Theories

Lemma 39. Let σ ∈ RSubst and {x ↦ t} ∈ RSubst be both satisfiable in the equality theory T, where x ∉ dom(σ) and vars(t) ∩ dom(σ) = ∅. Define also σ′ =^{def} σ ∪ {x ↦ t}. Then σ′ ∈ RSubst and σ′ is satisfiable in T.

Proof. Note that σ′ is a substitution, since σ ∈ RSubst and x ∉ dom(σ). Moreover, as vars(t) ∩ dom(σ) = ∅, σ′ cannot contain circular subsets. Hence, σ′ ∈ RSubst.

Since both σ and {x ↦ t} are satisfiable in T, we have

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

Letting V = Vars \ (dom(σ) ∪ {x}), we can rewrite these as

T ⊢ ∀V : ∀x : ∃ dom(σ) . σ,  (13)
T ⊢ ∀V : ∀ dom(σ) : ∃x . {x = t}.  (14)

Then, as vars(x = t) ∩ dom(σ) = ∅, it follows from (14) that

T ⊢ ∀V : ∃x . {x = t}.

Combining this with (13) gives

T ⊢ ∀V : ((∀x : ∃ dom(σ) . σ) ∧ (∃x . {x = t})).

14Note that, as a consequence of axiom (11) 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}.

Thus we have

T ⊢ ∀V : ∃x . (∃ dom(σ) . σ ∧ {x = t}),

and hence, as vars(x = t) ∩ dom(σ) = ∅,

T ⊢ ∀V : ∃x . ∃ dom(σ) . (σ ∧ {x = t}).

Therefore,

T ⊢ ∀V : ∃(dom(σ) ∪ {x}) . σ ∪ {x = t}.

Thus σ′ is satisfiable in T.

Corollary 40. 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.

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

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

Proof. Proved in [40, Lemma 2].

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

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

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

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

Using these results, we obtain

T ⊢ ∀(σ ∪ {s = t} ↔ σ ∪ {s = t, t = tσ}),  [by (16)]
T ⊢ ∀(σ ∪ {s = t} ↔ σ ∪ {s = tσ, t = tσ}),  [by (15)]
T ⊢ ∀(σ ∪ {s = t} ↔ σ ∪ {s = tσ}).  [by (16)]

Lemma 43. Let σ ∈ RSubst and s, t ∈ HTerms, where RT ⊢ ∀(σ → (s = t)). Then rt(s, σ) = rt(t, σ).

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

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

r = rt(s, σ)[p] ∉ Vars and x = rt(t, σ)[p] ∈ Vars \ dom(σ); or

c. r_{1} = rt(s, σ)[p] ∉ Vars, r_{2} = rt(t, σ)[p] ∉ Vars and r_{1} and r_{2} have different principal functors.

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

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

2. x = sσ^{i}[p] ∈ Vars \ dom(σ) and r = tσ^{i}[p] ∉ Vars or, in a symmetrical way, r = sσ^{i}[p] ∉ Vars and x = tσ^{i}[p] ∈ Vars \ dom(σ); or

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

By Lemma 41, we have RT ⊢ ∀(σ → (sσ^{i} = tσ^{i})); from this, since RT is a syntactic equality theory, we obtain that

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

We now prove that each case leads to a contradiction.

Consider case 1. Let r_{1}, r_{2} ∈ GTerms ∩ HTerms be two terms having different principal functors, so that RT ⊢ ∀(r_{1} ≠ r_{2}). Then, by Lemma 39, we have that σ′ = σ ∪ {x ↦ r_{1}, y ↦ r_{2}} ∈ RSubst is satisfiable and also RT ⊢ ∀(σ′ → σ), RT ⊢ ∀(σ′ → (x = r_{1})), RT ⊢ ∀(σ′ → (y = r_{2})). This is a contradiction, since, by (17), we have RT ⊢ ∀(σ → (x = y)).

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

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

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

Proof of Proposition 2 on page 7. We have the following chain of double implications

τ ∈ ↓ σ ⟺ ∃σ′ ∈ RSubst . τ ∈ mgs(σ ∪ σ′)
⟺ ∃σ′ ∈ RSubst . RT ⊢ ∀(τ ↔ (σ ∪ σ′))
⟺ ∃σ′ ∈ RSubst .
RT ⊢ (∀(τ → σ) ∧ ∀(τ → σ′)
∧ ∀((σ ∪ σ′) → τ))
⟺ RT ⊢ ∀(τ → σ).

Note that the left implication in the last step is obtained by taking σ′ = τ.

B.3. Variable-Idempotence

In [40], (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. In [39] 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 (e.g., when linearity is a property of interest). In the following we consider this stronger definition, also adopted in [41, 64].

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

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

The set of variable-idempotent substitutions is denoted VSubst.

Note that we have ISubst ⊂ VSubst ⊂ RSubst.

Definition 46. (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 VSubst is not a restrictive hypothesis.

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

Proof. Proved in [40, Theorem 1].

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

Proof. The proof is the same given for [40, Theorem 2], where a weaker result, using weak variable-idempotence, was stated.

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

Proof. The result easily follows from Theorems 47 and 48.

B.4. Some Results on Operators on Substitutions in RSubst

When computing hvars(σ) by means of the fixpoint computation given in Definition 11 on page 13, the fixpoint is reached after a single iteration if σ ∈ VSubst.

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

Proof. We show that hvars_{2}(σ) ⊆ hvars_{1}(σ). Let y ∈ hvars_{2}(σ). By Definition 11, 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 11, 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σ) ∩ dom(σ) = ∅. Let z ∈ V so that z ∈ vars(yσ). By hypothesis, we have σ ∈ VSubst 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 σ ∈ VSubst.

Proposition 51. For each σ ∈ VSubst, we have

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

Proof. The result is obtained by applying Lemma 50 and then unfolding Definition 11.

Proposition 52. Let σ ∈ VSubst and r ∈ HTerms, where vars(r) ⊆ hvars(σ). Then

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

Proof. Suppose y ∈ vars(r). Then, by Proposition 51, 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(σ) = ∅.

Proposition 53. Let σ ∈ RSubst and t ∈ HTerms. Then

vars(rt(t, σ))∩ dom(σ) = ∅,  (53a)
rt(t, σ) ∈ HTerms ⟺ ∃i ∈ ℕ . rt(t, σ) = tσ^{i}.  (53b)

Proof.

(53a) Let x ∈ dom(σ) and, towards a contradiction, suppose x ∈ vars(rt(t, σ)). Thus, there exists a finite path p such that x = rt(t, σ)[p]. Thus, by definition of ‘rt’, there exists an index i ∈ ℕ such that x = σ^{i}(t)[p]. Since x ∈ dom(σ), then x ≠ xσ, so that x ≠ σ^{i+1}(t)[p]. Also note that, being σ ∈ RSubst, σ contains no circular subsets, so that we have x ≠ σ^{j}(t)[p], for each index j > i. This implies x ≠ rt(t, σ)[p], which is a contradiction. Since no such finite path p can exist, we can conclude x ∉ vars(rt(t, σ)).

(53b) Since substitutions map finite terms into finite terms, a finite number of applications cannot produce an infinite term, so that the left implication holds. Proving the right implication by contraposition, suppose that rt(t, σ) ≠ tσ^{i}, for all i ∈ ℕ. Then, by definition of ‘rt’, we have tσ^{i} ≠ tσ^{i+1}, for all i ∈ ℕ. Letting n ∈ ℕ be the number of bindings in σ ∈ RSubst, for all i ∈ ℕ we have that size(tσ^{i}) < size(tσ^{i+n}), because σ has no circular subsets. Thus rt(t, σ) ∉ HTerms, because there is no finite upper bound to the number of function symbols occurring in rt(t, σ).

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

Proposition 54. Let σ ∈ VSubst and y ∈ Vars. Then

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

Proof. Since σ ∈ VSubst, by Proposition 51 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. By Proposition 53, there exists an i ∈ ℕ such that rt(y, σ) = yσ^{i} and vars(yσ^{i}) ∩ dom(σ) = ∅. Since σ ∈ V Subst, we have vars(yσ^{i}) = vars(yσ), so that vars(yσ)∩dom(σ) = ∅.

The following proposition is proved in [40], and shows that the function ‘gvars’ precisely captures the intended property.

Proposition 55. Let σ ∈ RSubst and x ∈ Vars. Then

y ∈ gvars(σ) ⟺ rt(y, σ) ∈ GTerms.

The following results is a consequence of Proposition 54 and Proposition 55.

Corollary 56. Let σ ∈ RSubst and t ∈ HTerms. Then

vars(t) ⊆ gvars(σ) ⟺ rt(t, σ) ∈ GTerms,  (56a)
vars(t) ⊆ hvars(σ) ⟺ rt(t, σ) ∈ HTerms.  (56b)

Proof of Proposition 15 on page 14. We prove the two statements (15a) and (15b), one at a time.

(15a). Suppose x ∈ hvars(τ) \ hvars(σ). Then, by Proposition 54, we have that rt(x, τ) ∈ HTerms. By Proposition 53, there exists i ∈ ℕ such that rt(x, τ) = xτ^{i} and also vars(xτ^{i}) ∩ dom(τ) = ∅. Let t ∈ GTerms ∩ HTerms and

υ =^{def} { y ↦ t | y ∈ vars(xτ^{i}) }.

Then, by Lemma 39, τ′ =^{def} τ ∪ υ ∈ RSubst is satisfiable. Moreover, we have that xτ^{i}τ′ ∈ GTerms ∩ HTerms. Define now n =^{def} size(xτ^{i}τ′). Note that, since x ∉ hvars(σ), rt(x, σ) ∉ HTerms, then there exists j ∈ ℕ such that size(xσ^{j}) > n. Therefore, by Lemma 44,

RT ⊢ ∀(xτ^{i}τ′ ≠ xσ^{j}).  (20)

Also, by Lemma 41, RT ⊢ ∀(σ → (x = xσ^{j})) and RT ⊢ ∀(τ → (x = xτ^{i})). By definition, τ′ ∈ ↓ τ and, by hypothesis, τ ∈ ↓ σ, so that τ′ ∈ ↓ σ. Thus, by Proposition 2 and transitivity, we have RT ⊢ ∀(τ′ → (xτ^{i} = xσ^{j})). Applying Lemma 41, we obtain RT ⊢ ∀(τ′ → (xτ^{i}τ′ = xσ^{j})), which contradicts (20).

(15b). Suppose x ∈ hvars(σ) ∩ gvars(σ). Then, by Propositions 54 and 55, rt(x, σ) ∈ GTerms ∩ HTerms. Thus, by case (53b) of Proposition 53, there exists i ∈ ℕ such that rt(x, σ) = xσ^{i} and also vars(xσ^{i}) = ∅. Thus rt(xσ^{i}, τ) = xσ^{i}. Since by hypothesis we have τ ∈ ↓ σ, by Lemma 41 and transitivity we obtain that RT ⊢ ∀(τ → (x = xσ^{i})). Thus, by Lemma 43, rt(x, τ) = rt(xσ^{i}, τ) = xσ^{i}. Therefore, by Propositions 54 and 55, x ∈ gvars(τ) ∩ hvars(τ).

In order to prove Proposition 13, 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 57. For each m > 0, we have hvars_{m−1}(σ) ⊆ hvars_{m}(σ).

Proof. Straightforward by Definition 11.

Lemma 58. 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 47 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 11, 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 47 and the inductive hypothesis we have

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

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

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

Since, by hypothesis, 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 11 and Lemma 57,

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 57 and Theorem 47 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 11, we have two cases: if z ∈ hvars_{m−1}(σ′) then the result follows by the inductive hypothesis and Lemma 57; otherwise, we have

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

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

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

so that, by Definition 11, z ∈ hvars_{m+1}(σ). Otherwise, if z = y, by definition of σ′, the inductive hypothesis and Lemma 57, 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 11 we have

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

The result follows by observing that

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

Lemma 59. 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 58.

Proof of Proposition 13 on page 14. By Theorem 49, there exists σ′ ∈ VSubst such that σ ⟼^{∗}^{S} σ′ and, for all equality theories T, T ⊢ ∀(σ ↔ σ′). Thus, by Lemma 59, we have hvars(σ) = hvars(σ′). The thesis then follows by applying Proposition 54.

Lemma 60. Let σ, τ ∈ VSubst 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 51, vars(yσ) ∩ dom(σ) = ∅. We will show that rt(y, τ) ∈ HTerms so that, by Proposition 54, y ∈ hvars(τ).

Take t ∈ HTerms ∩ GTerms and let

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

Note that yσσ′ ∈ HTerms ∩ GTerms, so that size(yσσ′) = n ∈ ℕ. Also, by Lemma 40, we have σ′ ∈ RSubst is satisfiable in T.

By contraposition, suppose that rt(y, τ) ∉ HTerms. Then, there exists an index i ∈ ℕ such that size(yτ^{i}) > n. By Lemma 41, we have σ′ ⟹ {y = yσσ′} and

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

so that, by the congruence axioms, σ′ ⟹ {yσσ′ = yτ^{i}}. However, by Lemma 44, T ⊢ ∀(yσσ′ ≠ yτ^{i}), therefore obtaining a contradiction. Thus rt(y, τ) ∈ HTerms.

Proposition 61. Let σ, τ ∈ RSubst. Let also W ⊆ Vars, where

RT ⊢ ∀(∃W . σ ↔ ∃W . τ).

Then hvars(σ) \ W = hvars(τ) \ W.

Proof. Consider a variable z ∈ hvars(σ) \ W. We assume that z ∉ hvars(τ) to obtain a contradiction.

By Proposition 54, rt(z, σ) ∈ HTerms. By Proposition 53, there exists i ∈ ℕ such that rt(z, σ) = zσ^{i} and vars(zσ^{i}) ∩ dom(σ) = ∅.

Take t ∈ GTerms ∩ HTerms and let

υ =^{def} { y ↦ t | y ∈ vars(zσ^{i}) }.

By Lemma 39, σ′ =^{def} σ ∪ υ ∈ ↓ σ is satisfiable. Thus, by Proposition 2, we have

RT ⊢ ∀(σ′ → σ).  (21)

By the definition of σ′, zσ^{i}σ′ ∈ GTerms ∩ HTerms. As z ∉ hvars(τ), there exists j ∈ ℕ such that size(zτ^{j}) > size(zσ^{i}σ′). Thus, by Lemma 44,

RT ⊢ ∀(zσ^{i}σ′ ≠ zτ^{j}).  (22)

From the application of Lemma 41, we obtain that RT ⊢ ∀(σ → (z = zσ^{i})) and RT ⊢ ∀(σ′ → (zσ^{i} = zσ^{i}σ′)). Thus, by (21),

RT ⊢ ∀(σ′ → (z = zσ^{i}σ′)).  (23)

Using (21), the hypothesis and the logically true statement ∀(σ → ∃W . σ), we obtain RT ⊢ ∀(σ′ → ∃W . τ). By Lemma 41, we have RT ⊢ ∀(τ → (z = zτ^{j})); thus, as RT is a first-order theory, RT ⊢ ∀(∃W . τ → ∃W . (z = zτ^{j})). Therefore, by transitivity, we obtain

RT ⊢ ∀(σ′ → ∃W . (z = zτ^{j})).  (24)

Observe now that vars(z = zσ^{i}σ′) = {z} and, as a consequence, we have vars(z = zσ^{i}σ′) ∩ W = ∅. Therefore, by (23) and (24), we obtain

RT ⊢ ∀(σ′ → (z = zσ^{i}σ′ ∧ ∃W . z = zτ^{j}))
⟺ RT ⊢ ∀(σ′ → ∃W . (z = zσ^{i}σ′ ∧ z = zτ^{j}))
⟺ RT ⊢ ∀(σ′ → ∃W . (zσ^{i}σ′ = zτ^{j})).

But this contradicts (22), so that the assumption was false and z ∈ hvars(τ). As the choice of z was arbitrary, we have

hvars(σ) \ W ⊆ hvars(τ) \ W.

The reverse inclusion follows by symmetry.

B.5. Abstracting Finiteness

Lemma 62. 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 48 and Lemma 59, there exists σ′, τ′ ∈ VSubst such that σ ⟺ σ′, hvars(σ) = hvars(σ′), τ ⟺ τ′ and hvars(τ) = hvars(τ′). By hypothesis, σ ⟺ τ so that σ′ ⟺ τ′. By Lemma 60, hvars(σ′) = hvars(τ′). Therefore hvars(σ) = hvars(τ).

Corollary 63. 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 62.

Proof of Theorem 17 on page 15. By Definition 16, we have α_{H}(σ) = hvars(σ)∩ VI and α_{H}(σ′) = hvars(σ′) ∩ VI . The result is a simple consequence of Lemma 62, since RT is a syntactic equality theory and RT ⊢ ∀(σ ↔ σ′).

B.6. Correctness of Abstract Unification on H × P

Lemma 64. Let σ ∈ VSubst 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 we have, by the identity axioms, T ⊢ ∀(r ≠ s). Note also that, by Lemma 41 and the congruence axioms, we have T ⊢ ∀(σ → s = tσ).

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

First we show that tσ is not a variable. In order to prove this, we suppose that tσ = y ∈ Vars and derive a contradiction. If y ∉ dom(σ) then, by Lemma 40, σ′ = σ ∪ {y ↦ r} ∈ RSubst and σ′ is satisfiable in T. Therefore, using the congruence axioms, T ⊢ ∀(σ′ → r = s), which is a contradiction. If otherwise tσ = y ∈ dom(σ) then, since σ ∈ VSubst, we have y ∈ vars(yσ) so that, for all i > 0, size(tσ^{i+1}) > size(tσ^{i}). Thus, by Lemma 44, there exists an index j > 0 such that T ⊢ ∀(s ≠ tσ^{j}). However, by the hypothesis and Lemma 41, 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 that T ⊢ ∀(σ → s_{i} = t_{i}), for each i = 1, …, m. 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 σ ∈ VSubst, we have vars(tσ) = ∅ so that tσσ = tσ. Hence s = tσ.

Lemma 65. 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 (9), mgs(s̄′ = t̄′) = mgs(s̄ = t̄). We repeat this process until all terms in s̄′ and t̄′ can not be decomposed any further. (Note that in the case that s_{i} and t_{i} are identical constants, we can remove them from s̄′ and t̄′, since the corresponding equation s_{i} = t_{i} holds vacuously.) 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, for all μ ∈ mgs(s̄ = t̄), we have s_{i} ∉ dom(μ). Therefore

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

Furthermore, by the congruence axiom (6), 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 (7), μ ∈ 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}  (25)

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

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}) = ∅.  (27)

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

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

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

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

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

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

Let

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

Then we have to show that

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

It follows from (28) and (31) 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 (25), we have both vars(s̄_{1}) ⊆ vars(s̄) and vars(t̄_{1}) ⊆ vars(t̄), so that vars(s̄_{1}) ∩ vars(t̄_{1}) ⊆ vars(s̄) ∩ vars(t̄). Hence we have z ∈ dom(μ_{1}) \ (vars(s̄_{1}) ∩ vars(t̄_{1})). Thus we obtain, by the inductive hypothesis, vars(zμ_{1}) ∩ dom(μ_{1}) = ∅. Now, as z ∈ dom(μ_{1}) and (29) holds, s_{1} ∉ vars(zμ_{1}). Thus, as dom(μ) = dom(μ_{1}) ∪ {s_{1}}, vars(zμ_{1}) ∩ dom(μ) = ∅. Hence, as zμ = zμ_{1},

(32) 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 (30), vars(t_{1}μ_{1}) ∩ dom(μ) = ∅. Therefore, as zμ = t_{1}μ_{1}, (32) 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}  (33)

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

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

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}) = ∅.  (35)

Suppose u is any variable in vars(s̄_{1}). Then either u ∈ vars((s_{2}, …, s_{n})) or we have 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 (33) that u ∉ nlvars(t̄_{1}). If t_{1} ∈ vars((s_{2}, …, s_{n})), then we have t_{1} ∉ vars((t_{2}, …, t_{n})) so that, again by (33), t̄_{1} = (t_{2}, …, t_{n}). Thus, for all u ∈ vars(s̄_{1}), u ∉ nlvars(t̄_{1}). Hence (35) 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})), we have vars(zμ_{1}) ∩ dom(μ_{1}) = ∅.

Let

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

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

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

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

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

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

Let

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

Then we have to show that

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

It follows from (36) and (39) 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 (33), 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 (37) holds, t_{1} ∉ vars(zμ_{1}). Thus, as dom(μ) = dom(μ_{1}) ∪ {t_{1}}, vars(zμ_{1}) ∩ dom(μ) = ∅. Hence, as zμ = zμ_{1}, (40) 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 (38), vars(s_{1}μ_{1}) ∩ dom(μ) = ∅. Therefore, as zμ = s_{1}μ_{1}, (40) holds.

Lemma 66. Suppose that the tuple of terms s̄ =^{def} (s_{1}, …, s_{n}) ∈ HTerms^{n} is linear, t̄ =^{def} (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 (9), mgs(s̄′ = t̄′) = mgs(s̄ = t̄). We repeat this process until all terms in s̄′ and t̄′ can not be decomposed any further. (Note that in the case that s_{i} and t_{i} are identical constants, we can remove them from s̄′ and t̄′, since the corresponding equation s_{i} = t_{i} holds vacuously.) 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 (6), 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 (7), μ ∈ mgs(s̄ = t̄).

As {t_{k+1}, …, t_{n}} ⊆ vars((s_{k+1}, …, s_{n})), we have 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}).  (41)

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 (41), 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 42, μ ∈ 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̄).  (42)

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

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 (43), t_{1} ∉ vars(μ_{1}) and, in particular, t_{1} ∉ dom(μ_{1}).

Let

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

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

As t_{1} ∈ dom(μ) (by (44)) 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̄).  (45)

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 (43)). 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 (45)) 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}).  (46)

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 (46), t_{1} ∉ vars(μ_{1}). Moreover μ_{1} ∈ RSubst and s_{1} ∉ Vars so that μ ∈ Eqs has no identities or circular subset. Thus μ ∈ RSubst. By Lemma 42, μ ∈ 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 (46)) and vars(zμ) ⊆ vars(s̄_{1}) (by property 1). It follows that vars(zμ) ∩ dom(μ) = ∅, since dom(μ_{1}) ∪ {t_{1}} = dom(μ).

Proposition 67. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ VSubst 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(τ).  (47)

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 63 that we just have to show that 1. vars(r′) ⊆ hvars(τ), for some τ ∈ mgs(σ ∪ {x = t});

2. hvars(σ) ⊆ hvars(τ), for some τ ∈ mgs(σ ∪ {x = t}).

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

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

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

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

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

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

We now prove statement 2. 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 42 and the congruence axioms, σ ∪ {x = t} ⟹ s̄ = t̄. Thus, as σ ∪ {x = t} is satisfiable, mgs(s̄ = t̄) ≠ ∅. Then, by Theorem 49, there exists μ ∈ VSubst ∩ mgs(s̄ = t̄). Therefore, since rσ ∈ HTerms ∩ GTerms and μ ⟹ {rσ = r′σ}, Lemma 64 applies (with s = rσ) so that we can conclude rσ = r′σμ ∈ HTerms ∩ GTerms. Hence, for all w ∈ dom(μ),

vars(wμ) = ∅.  (48)

Let

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

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

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

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

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 (49), w ∉ dom(σ). If w ∉ dom(μ), then w = wμ ∉ dom(τ). If w ∈ dom(μ), then, by (48), vars(wμ) = ∅. Therefore, vars(wμ) ∩ dom(τ) = ∅. It follows that vars(yν) ∩ dom(τ) = ∅. Finally, suppose y ∈ dom(μ). Then, by (48), vars(yμ) = ∅. Therefore vars(yμ) ∩ dom(τ) = ∅.

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

Proposition 68. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ VSubst 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 substitutions τ ∈ mgs(σ ∪ {x = t}) in a syntactic equality theory T,

hvars(σ) ⊆ hvars(τ).  (50)

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 63 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (50) holds.

As x ∈ hvars(σ) and vars(t) ⊆ hvars(σ), by using Proposition 52 we obtain rt(x, σ) = xσ and rt(t, σ) = tσ. Also

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

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

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

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

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

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

Note that, by (51),

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

Let

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

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

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

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

We show that vars(yτ) ∩ dom(τ) = ∅. If y ∉ dom(τ), the result holds trivially. Suppose that y ∈ dom(ν), then yτ = yσμ. Let w be any variable in vars(yσ). Then, by (55), w ∉ dom(σ). If w ∉ dom(μ), then w = wμ ∉ dom(τ). If w ∈ dom(μ), then vars(wμ) ⊆ vars(μ) so that, by (54), vars(wμ) ∩ dom(ν) = ∅. Moreover (53) 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 (54), we have vars(yμ)∩dom(ν) = ∅. Also (53) applies where w is replaced by y so that vars(yμ) ∩ dom(μ) = ∅. Thus vars(yμ) ∩ dom(τ) = ∅.

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

Proposition 69. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ VSubst 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(τ).  (56)

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 63 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (56) holds.

By Definition 8, gfree_{p}(x) and gfree_{p}(t) imply that either rt(x, σ) ∈ GTerms or rt(x, σ) ∈ Vars, and either rt(t, σ) ∈ GTerms or rt(t, σ) ∈ Vars. Since we have rt(x, σ), rt(t, σ) ∈ HTerms and σ ∈ VSubst, as a consequence of Proposition 52, 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 67.

• 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 42, τ ∈ 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 52, rt(y, σ) = yτ and vars(yτ) ∩ dom(σ) = ∅. Thus vars(yτ) ∩ dom(τ) ⊆ {xσ}. However, xστ = tσ ∉ dom(τ) so that, by Definition 11, vars(yτ) ⊆ hvars_{1}(τ) and hence y ∈ hvars_{2}(τ). Therefore, by Lemma 57 and Definition 12, 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 12, we have that y ∈ hvars(τ) as required.

Proposition 70. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let σ ∈ γ_{P} (p) ∩ VSubst 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 substitutions τ ∈ mgs(σ ∪ {x = t}) in a syntactic equality theory T, we have

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

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 63 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (57) holds.

As x ∈ hvars(σ) and vars(t) ⊆ hvars(σ), by using Proposition 52 we obtain rt(x, σ) = xσ and rt(t, σ) = tσ. Also

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

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

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

By Lemma 42 and the congruence axioms, σ ∪ {x = t} ⟹ {rσ = r′σ}. Thus, as σ ∪ {x = t} is satisfiable, mgs(rσ = r′σ) ≠ ∅. Thus, as rσ is linear and (59) holds, we can apply Lemma 65 (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(μ) = ∅.  (60)

Note that, by (58),

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

Let

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

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

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

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

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

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

Therefore, using (63) if y ∉ dom(σ) and (58) if y ∈ dom(σ), it follows that

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

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 (63), w ∉ (vars(xσ) ∩ vars(tσ)) and, by (62), w ∉ dom(σ). If w ∉ dom(μ), then w = wμ ∉ dom(τ). If w ∈ dom(μ), then vars(wμ) ⊆ vars(μ) so that, by (61), we also have vars(wμ) ∩ dom(ν) = ∅. Moreover (60) 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 (61), vars(yμ) ∩ dom(ν) = ∅. As (64) holds, (60) applies where w is replaced by y so that vars(yμ) ∩ dom(μ) = ∅. Thus vars(yμ) ∩ dom(τ) = ∅.

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

Proposition 71. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ VSubst 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(τ).  (65)

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 63 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (65) holds.

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

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

By hypothesis, lin_{p}(r) holds, so that, by Definition 8, 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 (66) that s̄ is linear. By Lemma 42 and the congruence axioms, σ ∪ {x = t} ⟹ s̄ = t̄. Thus, as σ ∪ {x = t} is satisfiable, we have mgs(s̄ = t̄) ≠ ∅. Therefore, we can apply Lemma 66 so that there exists μ ∈ mgs(s̄ = t̄) such that, for all w ∈ dom(μ) \ vars(s̄),

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

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

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

Thus

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

Let

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

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

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

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

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

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

Therefore using (70) if y ∉ dom(σ) and (66) if y ∈ dom(σ), it follows that

y ∉ vars(rσ).  (71)

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 (69) and (70) that vars(yσ) ∩ vars(s̄) = ∅. Let w be any variable in vars(yσ) so that w ∉ vars(s̄). By (69), we have w ∉ dom(σ). If w ∉ dom(μ), then we have w = wμ ∉ dom(τ). If w ∈ dom(μ), then vars(wμ) ⊆ vars(μ) so that, by (68), vars(wμ) ∩ dom(ν) = ∅. Moreover (67) 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 (68), vars(yμ) ∩ dom(ν) = ∅. Since σ ∈ VSubst and y ∈ hvars(σ), we have y ∉ dom(σ) ∩ (vars(rσ) ∪ vars(r′σ)) and hence y ∉ vars(s̄). Therefore (67) applies and vars(yμ) ∩ dom(μ) = ∅. Thus vars(yμ) ∩ dom(τ) = ∅.

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

Proposition 72. Let p ∈ P and (x ↦ t) ∈ Bind, where {x} ∪ vars(t) ⊆ VI . Let also σ ∈ γ_{P} (p) ∩ VSubst. Then, for all τ ∈ mgs(σ ∪ {x = t}) in a syntactic equality theory T,

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

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 63 that we just have to show that there exists τ ∈ mgs(σ ∪ {x = t}) such that (72) 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 σ ∈ VSubst, 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σ).  (73)

Let

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

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

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

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

As y ∉ share with_{p}(x) ∪ share with_{p}(t), it follows from Definition 8 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σ)) = ∅.  (75)

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

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

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

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

Proof of Theorem 19 on page 16. By hypothesis, σ ∈ γ_{P} (p). By Theorem 49, there exists σ′ ∈ VSubst such that σ ⟺ σ′. By Lemma 62, we have that hvars(σ) = hvars(σ′). By Definition 7, σ ∈ γ_{P} (p) if and only if σ′ ∈ γ_{P} (p). We therefore safely assume that σ ∈ VSubst.

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

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

As hterm_{h}(x) holds, by Definition 18, x ∈ h. Hence, by Definition 16, we have x ∈ hvars(σ). As ground_{p}(x) holds, by Definition 8, rt(x, σ) ∈ GTerms. Therefore we can apply Proposition 67, 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 18, vars(t) ⊆ h. Hence, by Definition 16, vars(t) ⊆ hvars(σ). As ground_{p}(t) holds, by Definition 8, rt(t, σ) ∈ GTerms. Therefore we can apply Proposition 67, 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 18, x ∈ h and vars(t) ⊆ h. Hence, by Definition 16, x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 68 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 18, x ∈ h and vars(t) ⊆ h. Hence, by Definition 16, x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 69 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 18, x ∈ h and vars(t) ⊆ h. Hence, by Definition 16, x ∈ hvars(σ) and vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 70 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 18, x ∈ h. Hence, by Definition 16, we have x ∈ hvars(σ). Therefore we can apply Proposition 71 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 18, vars(t) ⊆ h. Hence, by Definition 16, vars(t) ⊆ hvars(σ). Therefore we can apply Proposition 71 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 72 applies so

that

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

Proof of Theorem 21 on page 17. Suppose that τ ∈ ∃∃ x . {σ}. We need to show that τ ∈ γ_{H}(proj_{H}(h, x)).

Let \overline{V} = Vars \ VI . Then, by Definition 5, RT ⊢ ∀(∃\overline{V} . (τ ↔ ∃x . σ)). Thus we have

RT ⊢ ∀((∃\overline{V} . τ) ↔ (∃\overline{V} ∪ \{x\} . σ)).  (77)

Suppose v ∈ \overline{V} \ vars(σ). As we assumed that Vars is denumerable and that VI is finite, such a v will exist. Moreover, as x ∈ VI , we have x ≠ v. Let σ′ ∈ RSubst be obtained from σ by replacing every occurrence of x by v. Formally, if ρ = {x ↦ v}, let

σ′ =^{def} { y ↦ yσρ | y ∈ dom(σ) \ {x} } ∪ σ′′,

where σ′′ = {v ↦ xσρ} if x ∈ dom(σ) and ∅ otherwise. Then σ′ ∈ RSubst and

RT ⊢ ∀((∃\overline{V} . σ′) ↔ (∃\overline{V} ∪ \{x\} . σ)).

Thus, by (77), RT ⊢ ∀((∃\overline{V} . τ) ↔ (∃\overline{V} . σ′)). Therefore, by Proposition 61,

hvars(τ) ∩ VI = hvars(σ′) ∩ VI .  (78)

As σ′ ∈ RSubst and x ∉ dom(σ′), rt(x, σ′) = x so that, by Proposition 12, x ∈ hvars(σ′). Also, as σ′ is obtained from σ by renaming x to the new variable v, hvars(σ′) ⊇ hvars(σ) \ {v}. Since v ∉ VI , we have

hvars(σ′) ∩ VI ⊇ (hvars(σ) ∪ {x}) ∩ VI .

Therefore, by (78),

hvars(τ) ∩ VI ⊇ (hvars(σ) ∪ {x}) ∩ VI .  (79)

By hypothesis, σ ∈ γ_{H}(h), so that, by Definition 16, hvars(σ) ⊇ h. Therefore, by (79), hvars(τ) ∩ VI ⊇ (h ∪ {x}) ∩ VI . Thus, by applying Definition 16, we can conclude that τ ∈ γ_{H}(h ∪ {x}).

B.7. Finite-Tree Dependencies

Proposition 73. Let σ, τ ∈ RSubst and ϕ ∈ Bfun, where σ ∈ γ_{F} (ϕ) and τ ∈ ↓ σ. Then τ ∈ γ_{F} (ϕ).

Proof. By the hypothesis, τ ∈ ↓ σ, so that, for each υ ∈ ↓ τ, υ ∈ ↓ σ. Therefore, as σ ∈ γ_{F} (ϕ), it follows from Definition 22 that, for all υ ∈ ↓ τ, ϕ(hval(υ)) = 1 and hence τ ∈ γ_{F} (ϕ).

Lemma 74. Let ϕ_{1}, ϕ_{2} ∈ Bfun. Then

γ_{F} (ϕ_{1} ∧ ϕ_{2}) = γ_{F} (ϕ_{1}) ∩ γ_{F} (ϕ_{2}).

Proof.

γ_{F} (ϕ_{1} ∧ ϕ_{2}) = { σ ∈ RSubst | ∀τ ∈ ↓ σ : (ϕ_{1} ∧ ϕ_{2})(hval(τ)) = 1 }
= { σ ∈ RSubst | ∀τ ∈ ↓ σ : ∀i ∈ {1, 2} : ϕ_{i}(hval(τ)) = 1 }
= { σ ∈ RSubst | ∀τ ∈ ↓ σ : ϕ_{1}(hval(τ)) = 1 }
∩ { σ ∈ RSubst | ∀τ ∈ ↓ σ : ϕ_{2}(hval(τ)) = 1 }
= γ_{F} (ϕ_{1}) ∩ γ_{F} (ϕ_{2}).

Proof of Theorem 23 on page 19. Assuming the hypothesis of the theorem, we will prove each relation separately.

(23a). Let σ = {x ↦ t} and suppose that τ ∈ ↓ σ. Then, by Proposition 2, RT ⊢ ∀(τ → σ). It follows from Lemma 43 that rt(x, τ) = rt(t, τ) and thus, by case (56b) of Corollary 56, x ∈ hvars(τ) if and only if vars(t) ⊆ hvars(τ). This is equivalent to (x ↔ ⋀ vars(t))(0[1/ hvars(τ)]) = 1 and, by Definition 22, to (x ↔ ⋀ vars(t))(hval(τ)) = 1. As this holds for all τ ∈ ↓ σ, by Definition 22, σ ∈ γ_{F} (x ↔ ⋀ vars(t)).

(23b). Let σ = {x ↦ t}, where x ∈ vars(t). By Definition 12, x ∉ hvars(σ). By case (15a) of Proposition 15, for all τ ∈ ↓ σ, we have hvars(τ) ⊆ hvars(σ). Thus x ∉ hvars(τ) and (¬x)(hval(τ)) = 1. Therefore, by Definition 22, σ ∈ γ_{F} (¬x).

(23c). Let σ ∈ RSubst such that x ∈ gvars(σ) ∩ hvars(σ). By case (15b) of Proposition 15, we have x ∈ hvars(τ) for all τ ∈ ↓ σ. So (x)(hval(τ)) = 1. Therefore, by Definition 22, σ ∈ γ_{F} (x).

(23d). Let σ_{1} ∈ Σ_{1} and σ_{2} ∈ Σ_{2}. Then, by hypothesis σ_{1} ∈ γ_{F} (ϕ_{1}) and σ_{2} ∈ γ_{F} (ϕ_{2}). Let τ ∈ mgs(σ_{1} ∪ σ_{2}). By definition of mgs, RT ⊢ ∀(τ → σ_{1}) and RT ⊢ ∀(τ → σ_{2}). Thus, by Proposition 2, we have τ ∈ ↓ σ_{1} ∩ ↓ σ_{2}. Therefore, by Proposition 73, τ ∈ γ_{F} (ϕ_{1}) ∩ γ_{F} (ϕ_{2}). The result then follows by Lemma 74.

(23e). We have

γ_{F} (ϕ_{1} ∨ ϕ_{2}) = { σ ∈ RSubst | ∀τ ∈ ↓ σ : (ϕ_{1} ∨ ϕ_{2})(hval(τ)) = 1 }
= { σ ∈ RSubst | ∀τ ∈ ↓ σ : ∃i ∈ {1, 2} . ϕ_{i}(hval(τ)) = 1 }
⊇ { σ ∈ RSubst | ∀τ ∈ ↓ σ : ϕ_{1}(hval(τ)) = 1 }
∪ { σ ∈ RSubst | ∀τ ∈ ↓ σ : ϕ_{2}(hval(τ)) = 1 }
= γ_{F} (ϕ_{1}) ∪ γ_{F} (ϕ_{2})
⊇ Σ_{1} ∪ Σ_{2}.

(23f). Let σ ∈ Σ and let σ′ ∈ ∃∃ x . {σ}. We will show that σ′ ∈ γ_{F} (∃x . ϕ). Let τ′ ∈ ↓ σ′. Then there exists σ′_{1} ∈ RSubst such that RT ⊢ ∀(τ′ ↔ (σ′ ∪ σ′_{1})).

Let σ_{1} ∈ ∃∃ x . {σ′_{1}} and let W =^{def} (Vars \ VI ) ∪ {x}. Then, by Definition 5, it follows RT ⊢ ∀(∃W . (σ′ ↔ σ)) and RT ⊢ ∀(∃W . (σ′_{1} ↔ σ_{1})). As a consequence

RT ⊢ ∀(∃W . (σ′ ∪ σ′_{1}) ↔ ∃W . (σ ∪ σ_{1})).

Therefore σ ∪ σ_{1} is satisfiable so that, for some τ ∈ RSubst, RT ⊢ ∀(τ ↔ (σ ∪ σ_{1})). Thus RT ⊢ ∀(∃W . τ ↔ ∃W . τ′). By Proposition 61, hvars(τ′) \ W = hvars(τ) \ W so that

(hvars(τ′) ∩ VI ) ∪ {x} = (hvars(τ) ∩ VI ) ∪ {x}.  (80)

Let c =^{def} hval(τ)(x). Then, since τ ∈ ↓ σ and, by hypothesis, σ ∈ γ_{F} (ϕ), we have the following chain of implications:

ϕ(hval(τ)) = 1  [by Defn. 22]
ϕ(hval(τ)[c/x]) = 1  [by Defn. 3]
ϕ(0[1/ hvars(τ) ∩ VI ][c/x]) = 1  [by Defn. 22]
ϕ(0[1/(hvars(τ) ∩ VI ) ∪ {x}][c/x]) = 1  [by Defn. 3]
ϕ(0[1/(hvars(τ′) ∩ VI ) ∪ {x}][c/x]) = 1  [by (80)]
ϕ(0[1/ hvars(τ′) ∩ VI ][c/x]) = 1  [by Defn. 3]
ϕ(hval(τ′)[c/x]) = 1  [by Defn. 22]
ϕ[c/x](hval(τ′)) = 1.  [by Defn. 4]

From this last relation, since ϕ[c/x] ⊧ ∃x . ϕ, it follows that (∃x . ϕ)(hval(τ′)) = 1. As this holds for all τ′ ∈ ↓ σ′, by Definition 22, σ′ ∈ γ_{F} (∃x . ϕ).

Proof of Theorem 25 on page 20. Since h ⊆ h′, by the monotonicity of γ_{H} we have γ_{H}(h) ⊇ γ_{H}(h′), whence one of the inclusions: γ_{H}(h)∩γ_{F} (ϕ) ⊇ γ_{H}(h′)∩γ_{F} (ϕ).

In order to establish the other inclusion, we now prove that σ ∈ γ_{H}(h′) assuming σ ∈ γ_{H}(h) ∩ γ_{F} (ϕ). To this end, by Definition 16, it is sufficient to prove that h′ ⊆ hvars(σ).

Let z ∈ h′ and let ψ = (ϕ∧⋀ h), so that, by hypothesis, h′ = true(ψ). Therefore, we have ψ ⊧ z. Consider now ψ′ = (ϕ ∧ ⋀ hvars(σ)). Since σ ∈ γ_{H}(h), by Definition 16 we have h ⊆ hvars(σ), so that ψ′ ⊧ ψ and thus ψ′ ⊧ z.

Since σ ∈ γ_{F} (ϕ), by Definition 22 we have ϕ(hval(σ)) = 1. Also note that (⋀ hvars(σ))(hval(σ)) = 1. From these, by the definition of conjunction for Boolean formulas, we obtain ψ′(hval(σ)) = 1. Thus we can observe that

ψ′(hval(σ)) = 1 ⟺ (ψ′ ∧ z)(hval(σ)) = 1
⟹ z ∈ hvars(σ).

Theorem 75. Let x ∈ VI , h, h′ ∈ H and ϕ, ϕ′ ∈ Bfun, where h ⊇ true(ϕ∧⋀ h) and h′ ⊇ true(ϕ′ ∧ ⋀ h′). Let also

h_{1} =^{def} h ∩ h′,  h_{2} =^{def} h ∪ {x},
ϕ_{1} =^{def} ϕ ∨ ϕ′,  ϕ_{2} =^{def} ∃x . ϕ.

Then, for i = 1, 2,

h_{i} ⊇ true(ϕ_{i} ∧ ⋀ h_{i}).

Proof. We assume the hypotheses and prove each statement in turn. For the case where i = 1 we have:

h_{1} =^{def} h ∩ h′
⊇ true(ϕ ∧ ⋀ h) ∩ true(ϕ′ ∧ ⋀ h′)
⊇ true(ϕ ∧ ⋀(h ∩ h′)) ∩ true(ϕ′ ∧ ⋀(h ∩ h′))
= true(ϕ ∧ ⋀(h ∩ h′) ∨ ϕ′ ∧ ⋀(h ∩ h′))
= true((ϕ ∨ ϕ′) ∧ ⋀(h ∩ h′))
= true(ϕ_{1} ∧ ⋀ h_{1}).

For the case where i = 2 we have:

h_{2} =^{def} h ∪ {x}
⊇ true(ϕ ∧ ⋀ h) ∪ {x}
⊇ true((∃x . ϕ) ∧ ⋀ h) ∪ {x}
= true((∃x . ϕ) ∧ ⋀(h ∪ {x}))
= true(ϕ_{2} ∧ ⋀ h_{2}).

Proof of Theorem 27 on page 20. Suppose that there exists σ ∈ γ_{H}(h)∩γ_{F} (ϕ). By Definition 22, since σ ∈ ↓ σ, we have ϕ(hval(σ)) = 1; therefore, we also have

hvars(σ) ∩ false(ϕ) = ∅;

by Definition 16, we have h ⊆ hvars(σ), so that we can conclude h∩false(ϕ) = ∅.

B.8. Relation Between Groundness Dependencies and Finite-Tree Dependencies

As was the case for finite-tree dependencies, groundness dependencies only capture permanent information, therefore preserving the equivalence relation induced by RT . Moreover, the γ_{G} function is meet-preserving.

Proposition 76. Let σ, τ ∈ RSubst and ψ ∈ Pos, where we have σ ∈ γ_{G}(ψ) and τ ∈ ↓ σ. Then τ ∈ γ_{G}(ψ).

Proof. By the hypothesis, τ ∈ ↓ σ, so that, for each υ ∈ ↓ τ, υ ∈ ↓ σ. Therefore, as σ ∈ γ_{G}(ϕ), it follows from Definition 28 that, for all υ ∈ ↓ τ, ψ(gval(υ)) = 1 and hence τ ∈ γ_{G}(ϕ).

Corollary 77. Let σ, τ ∈ RSubst and ψ ∈ Pos, where we have σ ∈ γ_{G}(ψ) and RT ⊢ ∀(σ ↔ τ). Then τ ∈ γ_{G}(ψ).

Lemma 78. Let ψ_{1}, ψ_{2} ∈ Pos. Then

γ_{G}(ψ_{1} ∧ ψ_{2}) = γ_{G}(ψ_{1}) ∩ γ_{G}(ψ_{2}).

Proof.

γ_{G}(ψ_{1} ∧ ψ_{2}) = { σ ∈ RSubst | ∀τ ∈ ↓ σ : (ψ_{1} ∧ ψ_{2})(gval(τ)) = 1 }

= \{ σ ∈ RSubst | \begin{matrix}∀τ ∈ ↓ σ : ∀i ∈ \{1, 2\} : \\ ψ_{i}(gval(τ)) = 1 \end{matrix} \}

= { σ ∈ RSubst | ∀τ ∈ ↓ σ : ψ_{1}(gval(τ)) = 1 }

∩ { σ ∈ RSubst | ∀τ ∈ ↓ σ : ψ_{2}(gval(τ)) = 1 }

= γ_{G}(ψ_{1}) ∩ γ_{G}(ψ_{2}).

Since non-ground terms can be made cyclic by instantiating their variables, those terms detected as definitely finite on Bfun are also definitely ground.

Lemma 79. Let x ∈ VI . Then γ_{F} (x) ⊆ γ_{G}(x).

Proof. Suppose that σ ∈ γ_{F} (x). Then, by Definition 22, (x)(hval(τ)) = 1 for all τ ∈ ↓ σ, so that x ∈ hvars(τ); in particular, x ∈ hvars(σ). We prove x ∈ gvars(σ) by contradiction. That is, we show that if x ∈ hvars(σ) \ gvars(σ), then there exists τ ∈ ↓ σ for which x ∉ hvars(τ).

Suppose that x ∈ hvars(σ) \ gvars(σ). Then, by Propositions 54 and 55, rt(x, σ) ∈ HTerms \ GTerms. Hence, by Proposition 53, there exists i ∈ ℕ such that rt(x, σ) = xσ^{i} and there exists y ∈ vars(xσ^{i}) \ dom(σ). As we assumed that Sig contains a function symbol of non-zero arity, there exists t ∈ HTerms \ {y} for which {y} = vars(t). It follows that σ′ = {y ↦ t} ∈ RSubst and, by Definition 12, y ∉ hvars(σ′). Since y ∉ dom(σ), by Lemma 39, τ = σ∪σ′ ∈ RSubst. Since τ ∈ ↓ σ′ then, by case (15a) of Proposition 15, we have y ∉ hvars(τ).

By Lemma 41, we have RT ⊢ ∀(σ → (x = xσ^{i})). Thus, since we also have τ ∈ ↓ σ, we obtain RT ⊢ ∀(τ → (x = xσ^{i})). By applying Lemma 43, we have that rt(x, τ) = rt(xσ^{i}, τ) and thus, by case (56b) of Corollary 56, we obtain x ∈ hvars(τ) if and only if vars(xσ^{i}) ⊆ hvars(τ). However, as observed before, we know that y ∈ vars(xσ^{i}) \ hvars(τ), so that we also have x ∉ hvars(τ).

Therefore x ∈ gvars(σ) ∩ hvars(σ) and, by case (15b) of Proposition 15, for all τ ∈ ↓ σ, x ∈ gvars(τ)∩hvars(τ). As a consequence, for all τ ∈ ↓ σ, (x)(gval(τ)) = 1, so that, by Definition 28, we can conclude that σ ∈ γ_{G}(x).

Theorem 80. Let ϕ ∈ Bfun and ψ ∈ Pos. Let also ν ∈ Pos be defined as ν =^{def} ⋀ true(ϕ). Then

γ_{F} (ϕ) ∩ γ_{G}(ψ) = γ_{F} (ϕ) ∩ γ_{G}(ψ ∧ ν).

Proof. Since ψ ∧ ν ⊧ ψ, the inclusion

γ_{F} (ϕ) ∩ γ_{G}(ψ) ⊇ γ_{F} (ϕ) ∩ γ_{G}(ψ ∧ ν)

follows by the monotonicity of γ_{G}. To prove the inclusion

γ_{F} (ϕ) ∩ γ_{G}(ψ) ⊆ γ_{F} (ϕ) ∩ γ_{G}(ψ ∧ ν)

we will show that γ_{F} (ϕ) ⊆ γ_{G}(ν). The thesis will follow as, by Lemma 78, we have γ_{G}(ψ ∧ ν) = γ_{G}(ψ) ∩ γ_{G}(ν). We have

γ_{F} (ϕ) ⊆ γ_{F} (ν)  [since ϕ ⊧ ν]
= ⋂{ γ_{F} (x) | x ∈ true(ϕ) }  [by Lemma 74]
⊆ ⋂{ γ_{G}(x) | x ∈ true(ϕ) }  [by Lemma 79]
= γ_{G}(ν).  [by Lemma 78]

Theorem 81. Let ϕ, ϕ′ ∈ Bfun and ψ, ψ′ ∈ Pos, where ψ ⊧ ⋀ true(ϕ) and ψ′ ⊧ ⋀ true(ϕ′). Let also

ϕ_{1} =^{def} ϕ ∨ ϕ′,  ϕ_{2} =^{def} ∃x . ϕ,
ψ_{1} =^{def} ψ ∨ ψ′,  ψ_{2} =^{def} ∃x . ψ.

Then, for i = 1, 2, we have ψ_{i} ⊧ ⋀ true(ϕ_{i}).

Proof. Let us assume the hypotheses hold and prove each statement in turn. For the case where i = 1 we have:

ψ_{1} =^{def} ψ ∨ ψ′

⊧ ⋀ true(ϕ) ∨ ⋀ true(ϕ′)

⊧ ⋀ true(ϕ ∨ ϕ′)

=^{def} ⋀ true(ϕ_{1}).

Since by hypothesis we have that ψ ⊧ ⋀ true(ϕ) and existential quantification is a monotonic operation, for the case where i = 2 we have:

ψ_{2} =^{def} ∃x . ψ

⊧ ∃x . ⋀ true(ϕ)

= ⋀(true(ϕ) \ {x})

= ⋀ true(∃x . ϕ)

=^{def} ⋀ true(ϕ_{2}).

Proof of Theorem 30 on page 21.

Proof of (30a). Since ψ ∧ ν ⊧ ψ, the inclusion

γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ) ⊇ γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ ∧ ν)

follows by the monotonicity of γ_{G}.

We now prove the reverse inclusion. Let us assume σ ∈ γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ). By Lemma 78 we have that γ_{G}(ψ ∧ ν) = γ_{G}(ψ) ∩ γ_{G}(ν). Therefore it is enough to show that σ ∈ γ_{G}(ν). By hypothesis, ν = ∃VI \ h . pos(ϕ). Moreover, by Definition 22, h ⊆ hvars(σ). Thus, to prove the result, we will show, by contradiction, that σ ∈ γ_{G}(∃VI \ hvars(σ) . pos(ϕ)).

Suppose therefore that σ ∉ γ_{G}(∃VI \ hvars(σ) . pos(ϕ)). Then there exists τ ∈ ↓ σ such that

(∃VI \ hvars(σ) . pos(ϕ))(gval(τ)) = 0.  (81)

Let z ∈ hvars(σ) ∩ VI . By Proposition 54, rt(z, σ) ∈ HTerms. By Proposition 53, there exists i ∈ ℕ such that rt(z, σ) = zσ^{i} and vars(zσ^{i}) ∩ dom(σ) = ∅. Therefore, by Definition 12, vars(zσ^{i}) ⊆ hvars(σ). Thus, we have

vars(zσ^{i}) ⊆ hvars(σ) \ dom(σ).  (82)

By Lemma 41, as τ ∈ ↓ σ, RT ⊢ ∀(τ → (z = zσ^{i})). By Lemma 43, we have rt(z, τ) = rt(zσ^{i}, τ) so that, by case (56a) of Corollary 56,

z ∈ gvars(τ) ⟺ vars(zσ^{i}) ⊆ gvars(τ).  (83)

Take t ∈ GTerms ∩ HTerms and let

υ_{1} =^{def} { y ↦ t | y ∈ (hvars(σ) ∩ gvars(τ)) \ dom(σ) }.

As we assumed that Sig contains a function symbol of non-zero arity, for each y ∈ Vars there exists t_{y} ∈ HTerms \ {y} such that vars(t_{y}) = {y}. Thus let

υ_{2} =^{def} \{ y ↦ t_{y} | \begin{matrix}y ∈ (VI ∪ vars(σ)) ∩ hvars(σ) \\ y ∉ gvars(τ) ∪ dom(σ) \end{matrix} \}.

Note that υ_{1}, υ_{2} ∈ RSubst, vars(υ_{1}) ∩ vars(υ_{2}) = ∅ and vars(υ_{i}) ∩ dom(σ) = ∅, for i = 1, 2. Thus, by Lemma 39, τ′ =^{def} (σ ∪ υ_{1} ∪ υ_{2}) ∈ RSubst is satisfiable in RT .

We now show that

z ∈ gvars(τ) ⟺ z ∈ hvars(τ′).  (84)

First, assume that z ∈ gvars(τ). Then, by (83), we have vars(zσ^{i}) ⊆ gvars(τ). From this, since also (82) holds, we obtain vars(zσ^{i}) ⊆ dom(υ_{1}) so that, by Definitions 9 and 12, vars(zσ^{i}) ⊆ gvars(υ_{1}) ∩ hvars(υ_{1}). Since τ′ ∈ ↓ υ_{1}, by case (15b) of Proposition 15, vars(zσ^{i}) ⊆ gvars(τ′) ∩ hvars(τ′). Thus, by Corollary 56, rt(zσ^{i}, τ′) ∈ GTerms ∩ HTerms. Now τ′ ∈ ↓ σ so that, by Lemma 41, RT ⊢ ∀(τ′ → (z = zσ^{i})). By Lemma 43, rt(zσ^{i}, τ′) = rt(z, τ′) ∈ GTerms∩HTerms so that, by Proposition 54 and Proposition 55, z ∈ hvars(τ′).

We prove the other direction by contraposition, assuming that z ∉ gvars(τ). By (83), there exists y ∈ vars(zσ^{i}) \ gvars(τ). Also note that y ∈ VI ∪ vars(σ) and, by (82), y ∉ dom(σ) so that y ∈ dom(υ_{2}). By Definition 12, we have y ∉ hvars(υ_{2}) and, since τ′ ∈ ↓ υ_{2}, by case (15a) of Proposition 15, y ∉ hvars(τ′). Thus, by case (56b) of Corollary 56, we have that rt(zσ^{i}, τ′) ∉ HTerms. Moreover, as RT ⊢ ∀(τ′ → (z = zσ^{i})), by Lemma 43 we have rt(zσ^{i}, τ′) = rt(z, τ′) ∉ HTerms and therefore, by Proposition 54, z ∉ hvars(τ′).

Since z was an arbitrary variable in hvars(σ) ∩ VI , it follows from (81) and (84) that,

(∃VI \ hvars(σ) . pos(ϕ))(hval(τ′)) = 0.  (85)

We have by hypothesis that σ ∈ γ_{F} (ϕ), so that, as τ′ ∈ ↓ σ, by Definition 22 we have ϕ(hval(τ′)) = 1. Therefore, as ϕ ⊧ ∃VI \ hvars(σ) . pos(ϕ), (∃VI \ hvars(σ) . pos(ϕ))(hval(τ′)) = 1, which contradicts (85).

Proof of (30b). Since ϕ ∧ ν ⊧ ϕ, the inclusion

γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ) ⊇ γ_{H}(h) ∩ γ_{F} (ϕ ∧ ν) ∩ γ_{G}(ψ)

follows by the monotonicity of γ_{G}.

We now prove the reverse inclusion. Assume that σ ∈ γ_{H}(h) ∩ γ_{F} (ϕ) ∩ γ_{G}(ψ). By Lemma 74 we have that γ_{F} (ϕ ∧ ν) = γ_{F} (ϕ) ∩ γ_{F} (ν). Therefore it is enough to show that σ ∈ γ_{F} (ν). By hypothesis, ν = ∃VI \ h . ψ. Moreover, by Definition 16, h ⊆ hvars(σ). Thus, to prove the result, we will show, by contradiction, that σ ∈ γ_{F} (∃VI \ hvars(σ) . ψ).

Suppose therefore that σ ∉ γ_{F} (∃VI \ hvars(σ) . ψ). Then there exists τ ∈ ↓ σ such that

(∃VI \ hvars(σ) . ψ)(hval(τ)) = 0.  (86)

Take t ∈ GTerms ∩ HTerms and let

υ =^{def} { y ↦ t | y ∈ vars(σ) ∩ (hvars(τ) \ dom(σ)) }.  (87)

By Lemma 39, τ′ =^{def} σ ∪ υ ∈ RSubst is satisfiable in RT .

Let z be any variable in hvars(σ). By Proposition 54, we have rt(z, σ) ∈ HTerms. Then, by Proposition 53, there must exists i ∈ ℕ such that rt(z, σ) = zσ^{i} and vars(zσ^{i}) ∩ dom(σ) = ∅. Therefore, by Definition 12, vars(zσ^{i}) ⊆ hvars(σ). Thus, we have

vars(zσ^{i}) ⊆ hvars(σ) \ dom(σ).  (88)

By Lemma 41, as τ ∈ ↓ σ, RT ⊢ ∀(τ → (z = zσ^{i})). By Lemma 43, we have rt(z, τ) = rt(zσ^{i}, τ) so that, by case (56b) of Corollary 56,

z ∈ hvars(τ) ⟺ vars(zσ^{i}) ⊆ hvars(τ).  (89)

We now show that

hvars(τ) = hvars(σ) ∩ gvars(τ′).  (90)

Since τ ∈ ↓ σ, it follows from case (15a) of Proposition 15 that hvars(τ) ⊆ hvars(σ). Thus, as z ∈ hvars(σ), either z ∈ hvars(τ) or z ∈ hvars(σ) \ hvars(τ). We consider these cases separately.

First, assume that z ∈ hvars(τ). Then, by (89), we have vars(zσ^{i}) ⊆ hvars(τ). Also, by case (15a) of Proposition 15, we have z ∈ hvars(σ), so that we can apply (88) to derive vars(zσ^{i}) ∩ dom(σ) = ∅. Therefore, vars(zσ^{i}) ⊆ dom(υ) and, by Definitions 9 and 12, vars(zσ^{i}) ⊆ gvars(υ) ∩ hvars(υ). Since τ′ ∈ ↓ υ, by case (15b) of Proposition 15, we have vars(zσ^{i}) ⊆ gvars(τ′) ∩ hvars(τ′). Thus, by Corollary 56, rt(zσ^{i}, τ′) ∈ GTerms ∩ HTerms. Now τ′ ∈ ↓ σ so that, by Lemma 41, we have RT ⊢ ∀(τ′ → (z = zσ^{i})). Thus, by Lemma 43, rt(zσ^{i}, τ′) = rt(z, τ′) ∈ GTerms ∩ HTerms so that, by Propositions 54 and 55, z ∈ hvars(τ′) ∩ gvars(τ′). Hence, by case (15a) of Proposition 15, we can conclude z ∈ hvars(σ) ∩ gvars(τ′). Thus hvars(τ) ⊆ hvars(σ) ∩ gvars(τ′).

Secondly, we assume that z ∈ hvars(σ) \ hvars(τ). Since z ∉ hvars(τ), by (89), there exists y ∈ vars(zσ^{i}) \ hvars(τ). Also, since z ∈ hvars(σ), by (88), we have y ∈ hvars(σ) \ dom(σ) so that, by Definition 9, we have y ∉ gvars(σ). By (87), since y ∉ dom(σ) ∪ hvars(τ), we have y ∉ dom(υ) so that y ∉ gvars(τ′). Thus, by case (56a) of Corollary 56, we have rt(zσ^{i}, τ′) ∉ GTerms. Moreover, since we have RT ⊢ ∀(τ′ → (z = zσ^{i})), we obtain, by Lemma 43, rt(zσ^{i}, τ′) = rt(z, τ′) ∉ GTerms and thus, by Proposition 55, z ∉ gvars(τ′). Thus hvars(τ) ⊇ hvars(σ) ∩ gvars(τ′).

It follows from (86) and (90) that,

(∃VI \ hvars(σ) . ψ)(gval(τ′)) = 0.  (91)

We have by hypothesis that σ ∈ γ_{G}(ψ), so that, as τ′ ∈ ↓ σ, by Definition 28 we have ψ(gval(τ′)) = 1. Therefore, as ψ ⊧ ∃VI \ hvars(σ) . ψ,

(∃VI \ hvars(σ) . ψ)(gval(τ′)) = 1.

which contradicts (91).

Proof of Theorem 34 on page 23. Let us assume the hypotheses. For the case where i = 1 we have:

ϕ_{1} =^{def} ϕ ∨ ϕ′

⊧ (∃VI \ h . ψ) ∨ (∃VI \ h′ . ψ′)

⊧ (∃VI \ (h ∩ h′) . ψ)∨(∃VI \ (h ∩ h′) . ψ′)

= ∃VI \ (h ∩ h′) . ψ ∨ ψ′

=^{def} ∃VI \ h_{1} . ψ_{1}.

Since by hypothesis we have that ϕ ⊧ ∃VI \ h . ψ and existential quantification is a monotonic operation, for the case where i = 2 we have:

ϕ_{2} =^{def} ∃x . ϕ

⊧ ∃x . ∃VI \ h . ψ = ∃VI \ h . ∃x . ψ

= ∃VI \ (h ∪ {x}) . ∃x . ψ

=^{def} ∃VI \ h_{2} . ψ_{2}.