Substitution Tree Indexing

Peter Graf

MPI–I–94–251 October 1994 Author’s Address

Peter Graf (graf@mpi-sb.mpg.de), Max–Planck–Institut für Informatik Im Stadtwald D-66123 Saarbrücken Germany

Publication Notes

This report has been submitted for publication elsewhere and will be copyrighted if accepted.

Acknowledgements

Thanks to Hans Jürgen Ohlbach for his comments on earlier versions of this report. I also like to thank William McCune for providing a part of the term sets.

This work was supported by the “Schwerpunkt Deduktion (Projekt: EDDS)” of the German Science Foundation (DFG).

Abstract

The performance of a theorem prover crucially depends on the speed of the basic retrieval operations, such as finding terms that are unifiable with (instances of, or more general than) a given query term. In this paper a new indexing method is presented, which outperforms traditional methods such as path indexing, discrimination tree indexing and abstraction trees. Additionally, the new index not only supports term indexing but also provides maintenance and efficient retrieval of substitutions. As confirmed in multiple experiments, substitution trees combine maximal search speed and minimal memory requirements.

Contents

1 Introduction 2

2 Preliminaries 3 2.1 Terms, Substitutions, and Unifiers . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Normalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

3 Indexing Techniques Related to Substitution Trees 5 3.1 Discrimination Tree Indexing . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Abstraction Tree Indexing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

4 Substitution Tree Indexing 7

5 Standard Retrieval 9 5.1 Theoretical Foundations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 5.2 Implementing Standard Retrieval . . . . . . . . . . . . . . . . . . . . . . . . 13 5.3 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

6 Merge 14 6.1 Theoretical Foundations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 6.2 Implementing the Merge . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 6.3 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

7 Insertion 19 7.1 Theoretical Foundations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 7.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 7.3 Computing the Most Specific Common Generalization . . . . . . . . . . . . 22 7.4 Reusing non–indicator Variables . . . . . . . . . . . . . . . . . . . . . . . . 24 7.5 Insertion Heuristics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

8 Deletion 26

9 Experiments 27 9.1 The Term Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 9.2 Memory Requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 9.3 Insertion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 9.4 Deletion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 9.5 Retrieval Times . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 9.6 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

10 Conclusion 32

1 Introduction

Searching for a proof, most automatic reasoning systems will accumulate enormous amounts of data – terms, substitutions, clauses, and sometimes also formulae [LO80]. These data must be stored and accessed in various ways. As in standard database technology, indexing is the key to efficiently retrieving data from large databases.

The structure of logical data, e.g. the structure of terms, is much more complicated than the structure of data stored in a relational database. Furthermore, queries to a logical database [BO94] are also more complex than queries to standard databases.

Typical queries which arise in the context of resolution theorem proving [Rob65] are: Given a database D containing terms (literals) and a query term t, find all terms in D which are unifiable with, instances of, or more general than t. Most deduction systems currently in use or under development employ sophisticated term indexing techniques in order to increase the speed of this access and thereby to accelerate the search as a whole. Hitherto, the most often applied strategies have been path–indexing [Sti89, McC92, Gra92, Gra94], discrimination tree indexing [McC92, Chr93, BCR93], and abstraction tree indexing [Ohl90a, Ohl90b].

In this paper substitution tree indexing is presented as a new indexing technique which combines the advantages of discrimination and abstraction tree indexing. Memory requirement and retrieval times being the main criteria for judging an indexing technique, this paper will show that substitution tree indexing is superior to all known strategies in these points. Substitution trees can represent any set of idempotent substitutions. In the simplest case all these substitutions have identical domains and consist of a single assignment, which implies that the substitution tree can be used as a term index as well. Figure 1 shows an index for the three substitutions {u ↦ f(a, b)}, {u ↦ f(y, b)}, and {u ↦ f(b, z)} which obviously represents a term index for the terms f(a, b), f(y, b), and f(b, z). As the name already indicates, the labels of substitution tree nodes are substitutions. Each branch in the tree therefore represents a binding chain for variables. Consequently, the substitutions of a branch from the root node down to a particular node can be composed and yield an instance of the root node’s substitution.

[figure: Σ_{2} = {x_{1} ↦ a}; Σ_{1} = {x_{2} ↦ b}; Σ_{3} = {x_{1} ↦ ∗_{1}}; Σ_{0} = {u ↦ f(x_{1}, x_{2})}; Σ_{4} = {x_{1} ↦ b, x_{2} ↦ ∗_{1}}]

Figure 1: Substitution tree

Before substitutions are inserted into the index, their codomain is renamed. This normalization changes all variables in the codomain of a substitution. Renamed variables are called indicator variables and are denoted by ∗_{i}. The substitutions inserted to the index in Fig. 1 therefore were {u ↦ f(a, b)}, {u ↦ f(∗_{1}, b)}, and {u ↦ f(b, ∗_{1})}. This renaming has two main reasons: There is more sharing in the index if the substitutions are normalized and, when searching for instances in the index, indicator variables must not be instantiated.

Consider the substitution Σ = {u ↦ f(a, b)} which is represented by the chain of substitutions Σ_{0} = {u ↦ f(x_{1}, x_{2})}, Σ_{1} = {x_{2} ↦ b}, and Σ_{2} = {x_{1} ↦ a}. The original substitution Σ can be reconstructed by simply applying the substitution Σ_{2}Σ_{1}Σ_{0} to u. The result of this application is Σ = {u ↦ Σ_{2}Σ_{1}Σ_{0}(u)} = {u ↦ Σ_{2}Σ_{1}(f(x_{1}, x_{2}))} = {u ↦ Σ_{2}(f(x_{1}, b))} = {u ↦ f(a, b)}.

The retrieval in a substitution tree is based on a backtracking algorithm in addition to an ordinary representation of substitutions as lists of variable–term pairs. This algorithm also needs a backtrackable variable binding mechanism, similar to the one used in PROLOG.

The search for substitutions compatible with {u ↦ f(a, x)} is presented, i.e. substitutions τ are searched such that τ(u) is unifiable with f(a, x). We begin with binding the variable u to the term f(a, x) and start the retrieval: The substitution tree is traversed by testing at each node marked with the substitution Σ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} whether under the current bindings all x_{i} are unifiable with their appropriate t_{i}. At the root node in our example we unify the terms f(a, x) and f(x_{1}, x_{2}) which yields the two bindings x_{1} ↦ a and x ↦ x_{2}. Consider the first son of the root node marked with Σ_{1} and unify x_{2} with b, because x_{2} hasn’t been bound yet. The resulting binding is x_{2} ↦ b and the leaf node Σ_{2} is the next node to be investigated. As x_{1} is bound to a, the unification problem is trivial and therefore the substitution represented by this leaf node is compatible with {u ↦ f(a, x)}. After backtracking node Σ_{3} is found to represent another solution, because the variable ∗_{1} is unifiable with a. Backtracking deletes the bindings of ∗_{1} and x_{2} and then proceeds with node Σ_{4}. Obviously, retrieval can be stopped at this point, because a, which is the binding of x_{1}, is not unifiable with b.

Substitution trees provide maximal search speed paired with minimal memory requirements. Additionally, they do not only work for term sets but also for sets of substitutions. These substitutions don’t even need to have identical domains. The structure is very simple, just a tree of substitutions has to be maintained.

2 Preliminaries

2.1 Terms, Substitutions, and Unifiers

The standard notions for first order logic are used. Let V and F be two disjoint sets of symbols. V denotes the set of variable symbols and V^{∗} ⊂ V is the set of indicator variables. The set of n-ary function symbols is F_{n} and F = ∪F_{i}. Furthermore, T is the set of terms with V ⊆ T and f(t_{1}, …, t_{n}) ∈ T if f ∈ F_{n} and t_{i} ∈ T. The variables occuring in a term or a set of terms are denoted by V (t). Function symbols with arity 0 are called constants . In our examples the symbols u, v, w, x, y, z ∈ V, ∗_{i} ∈ V^{∗}, f, g, h ∈ F \F_{0} and a, b, c ∈ F_{0} are used.

A substitution σ is a mapping from variables to terms represented by the set of assignments {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}. The set DOM(σ) = {x ∈ V | σ(x) ≠ x} is called domain of σ, the set COD(σ) = {σ(x) | x ∈ DOM(σ)} the codomain of σ, and I(σ) = V (COD(σ)) is the set of variables introduced by σ. The composition of substitutions σ = {x_{1} ↦ s_{1}, …, x_{n} ↦ s_{n}} and τ = {y_{1} ↦ t_{1}, …, y_{m} ↦ t_{m}} is defined as (στ)(x) := σ(τ(x)) for all x. It can be computed as στ = {y_{1} ↦ σ(t_{1}), …, y_{m} ↦ σ(t_{m})} ∪ {x_{i} ↦ s_{i} | x_{i} ∈ DOM(σ)\DOM(τ)}. The join of the substitutions σ and τ is defined as σ • τ := {y_{1} ↦ σ(t_{1}), …, y_{m} ↦ σ(t_{m})} ∪ {x_{i} ↦ s_{i} | x_{i} ∈ DOM(σ)\I(τ)}. Obviously, for σ = {x ↦ a, y ↦ c} and τ = {z ↦ f(x)} we have στ = {z ↦ f(a), x ↦ a, y ↦ c} and σ • τ = {z ↦ f(a), y ↦ c}.

A unifier for two terms s and t is a substitution σ such that σ(s) = σ(t). If such a unifier exists s and t are called unifiable. Terms may be non–unifiable for different reasons. Clashes occur when two non-variable symbols are not identical. In contrast to indirect clashes and failures resulting from occur–checks, a direct clash can be detected without considering partial substitutions. A direct clash is detected when unifying f(a, x) and f(b, y), an indirect clash when unifying f(x, x) and f(a, b), and the occur–check detects the failure when unifying f(x, x) and f(y, g(y)).

2.2 Normalization

A position in a term is a finite sequence of natural numbers or the empty position ε. The subterm of a term t at position p is denoted by t/p and t/ε = t. Note that ε∘p = p∘ε = p with the function ∘ representing the concatenation of positions. The set of positions of the term t = f(t_{1}, …, t_{n}) is recursively defined by O(t) = {ε}∪{i∘p | p ∈ O(t_{i}), t ∉ F_{0}, t ∉ V }. For example, O(h(a, g(b), x)) = {ε, 1, 2, 2∘1, 3}. For constants and variables the set of positions is {ε}, In order to properly define the normalization of terms, a total ordering ≺ on positions is needed.

Definition 2.1 (Total Ordering ≺ on Positions) Let p = p_{1}∘ … ∘p_{n} and q = q_{1}∘ … ∘q_{m} be two different positions with n, m > 0. Then

p ≺ q ⟺ ∃i.1 ≤ i ≤ min(n, m) : p_{i} < q_{i} ∧ ∀j.1 ≤ j < i : p_{j} = q_{j}

For example, 1∘1 ≺ 1∘2, 1∘1 ≺ 2, and 1∘2 ≺ 1∘2∘1. Finally, the notion of a normalized term \overline{s} for a term s is introduced. Normalization renames the variables of terms s and t such that for terms equal modulo variable renaming \overline{s} = \overline{t} holds.

Definition 2.2 (Normalization of Terms) Let s = f(s_{1}, …, s_{n}) be a term and F = { p | p ∈ O(s), s/p ∈ V (s), ∀q ∈ O(s). q ≺ p : s/q ≠ s/p} the set of first occurrences of variables in s. If p_{1}, …, p_{m} ∈ F and m = |F | and p_{i} ≺ p_{j} for 1 ≤ i < j ≤ m then the substitution σ = {s/p_{1} ↦ ∗_{1}, …, s/p_{m} ↦ ∗_{m}} is called normalization and

\overline{s} := \{s/p_{1} ↦ ∗_{1}, …, s/p_{m} ↦ ∗_{m}\}(s)

The condition m = |F | in Def. 2.2 ensures that all variables in the term are renamed. For example, \overline{f(x)} = \overline{f(y)} = f(∗_{1}) and \overline{h(x, x, y)} = \overline{h(z, z, x)} = h(∗_{1}, ∗_{1}, ∗_{2}). The next definition extends the normalization of terms to the normalization of substitutions.

Definition 2.3 (Normalization of Substitutions) Let σ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} be a substitution and f_{n} ∈ F_{n} an n–ary function symbol. Additionally, let < be a fixed total ordering on variables and x_{1} < … < x_{n}. The normalized substitution \overline{σ} is defined as

\overline{σ} := \{x_{1} ↦ \overline{f_{n}(t_{1}, …, t_{n})}/1, …, x_{n} ↦ \overline{f_{n}(t_{1}, …, t_{n})}/n\}

For example, if σ = \{x ↦ f(u, v), y ↦ f(a, v)\} and x < y then \overline{σ} = \{x ↦ f(∗_{1}, ∗_{2}), y ↦ f(a, ∗_{2})\}. However, if we had chosen y < x we would have normalized σ to \overline{σ} = \{x ↦ f(∗_{2}, ∗_{1}), y ↦ f(a, ∗_{1})}.

3 Indexing Techniques Related to Substitution Trees

It has been mentioned, that substitution trees combine features of discrimination and abstraction tree indexing. In this section a brief sketch of these fundamental techniques is presented. Discrimination trees contribute the idea of normalized terms and abstraction trees configurate the terms according to their instance relation. Indexing techniques which don’t serve as a perfect filter, like Path–Indexing and some versions of Discrimination tree indexing, are not discussed. These indexing techniques don’t check bindings of variables for failures resulting from occurs–check and indirect clashes.

3.1 Discrimination Tree Indexing

Structure. In this technique the index is a single tree representing the structure of the indexed terms. Pointers to these terms are stored in the leaves of the tree. Each path from the root to a leaf of the discrimination tree corresponds to a set of terms which are equal modulo variable renaming. All these terms are represented by the unique normalized form of the terms. Figure 2 shows a discrimination tree.

[figure: f; ∗_{1}; ∗_{2}; ∗_{1}; a; g; ∗_{1}; g; ∗_{1}; g; ∗_{1}; d; g; ∗_{1}; f(x,x); f(y,y); f(x,y); f(a,g(z)); f(g(x),g(x)); f(g(d),g(x))]

Figure 2: Discrimination tree Retrieval. To answer a query one has to traverse the tree using a backtracking algorithm. Let us take the retrieval of generalizations of a query term as an example: The query term is transformed into a structure which is compatible with the discrimination tree, a so–called query tree, by simply inserting the query term into an empty discrimination tree. The backtracking algorithm has to consider that a subterm of the query term can match the ∗_{i}–nodes and non–variable nodes in the discrimination tree. Both cases must be considered. Additionally, in case of a ∗_{i}–node the variable ∗_{i} is bound to the corresponding subterm of the query term. In case the variable ∗_{i} is processed again, the binding of ∗_{i} will be checked by testing whether the binding is equal to the current corresponding subterm of the query term.

Finding instances of a query term is also fairly simple: During retrieval of instances, a variable in the query term can match all children of a node in the discrimination tree. However, this time the variable occurs in the query term. Nevertheless, the test whether the bindings of identical variables in the query tree are identical still can’t be omitted.

The retrieval of unifiable terms searches for generalizations as well as for instances of subterms. Additionally, an occur check has to be performed and a regular unification routine has to be called in case a x_{i} has been bound.

Remarks. Since discrimination trees are deterministic, they don’t depend on the order of term insertion. Insertion of entries is very fast. The memory requirement depends on whether the target terms stored in the index share initial “substrings”. In our example there are three terms which end on g(∗_{1}). The whole tree consists of 14 nodes. Abstraction trees consist of less nodes due to a better configuration of the terms.

3.2 Abstraction Tree Indexing

Structure. Abstraction tree indexing [Ohl90a] exploits the lattice structure of terms. An abstraction tree is based on the usual instance relation on terms which forms a partial ordering.

The tree’s nodes are labeled with termlists so that the free variables of the termlists at node N and the termlists of N’s subnodes form the domain and codomain of a set of matchers. The abstraction tree in Fig. 3 contains several matchers like {x_{1} ↦ y, x_{2} ↦ y} and {x_{1} ↦ x_{3}, x_{2} ↦ g(x_{4})} which may be applied to f(x_{1}, x_{2}). If all matchers from the root to a leaf of the abstraction tree are applied to the termlist in the root of the tree the resulting term is the one which is represented by this path. Note that abstraction trees are not deterministic. Their structure depends on the order in which terms are inserted.

Retrieval. The procedure for accessing unifiable terms takes a node N and a termlist. It unifies the termlist with N’s label and applies the unifier to N’s variables yielding a new termlist. With each termlist the search for unifiable terms goes down recursively into all subnodes of N until the leaves of the tree are reached.

Generalizations of a query term are found in the same way, except that matching has to be used to prevent instantiation in the query terms.

[figure: f(x_{1}, x_{2}); [x_{1}, x_{2}]; x, x; y, y; x, y; x_{3}, g(x_{4}); [x_{3}, x_{4}]; a, z; g(x_{5}), x_{6}; [x_{5}, x_{6}]; x, x; d, x; f(x,x); f(y,y); f(x,y); f(a,g(z)); f(g(x),g(x)); f(g(d),g(x))]

Figure 3: Abstraction tree

Finding instances is also similar to finding unifiable terms. The only difference is that matching is used instead of unification at the leaf nodes. Note that it is not possible to use matching on all nodes.

Remarks. Compared to the discrimination tree in Fig. 2 the abstraction tree for the same indexed set consists of 9 nodes only. Additionally, the fact that there are three terms ending on g(∗_{1}) is represented in the tree. However, abstraction tree indexing has some disadvantages: First of all, the trees contain lots of variable renamings which are not necessary. In our example tree the variable x_{1} is renamed to x_{3} just to have a consistent tree. Secondly, variables of indexed terms may occur in leaf nodes of the tree only. This implies that an algorithm looking for instances of a query term at an inner node of the tree cannot exploit the fact that a variable in an indexed term must not be instantiated. The consequence is that it will have to use unification instead of matching at inner nodes – and visit more nodes. As a consequence of these disadvantages our abstraction tree contains 16 assignments.

4 Substitution Tree Indexing

Substitution trees were developed to increase the performance of indexing. The main difference compared to abstraction trees lies in the representation of variables of indexed substitutions. Additionally, variable renamings are avoided. To this end the structure of the nodes of trees was simplified such that substitutions are stored in contrast to termlists and lists of variables. Variables of indexed terms are represented by indicator variables just like in discrimination trees and may now occur at arbitrary positions in the substitution tree. Figure 4 shows our standard term set. We only need three auxiliary variables and the whole tree contains only 9 assignments in contrast to the 16 assignments of the abstraction tree in Fig. 3. However, the main advantages of abstraction trees are preserved. We can also perform a merge on two trees, for example. Essentially, substitution trees unify the advantages of abstraction and discrimination trees and result in an outstanding indexing technique.

[figure: u ↦ f(x_{1}, x_{2}); x_{1} ↦ ∗_{1}; x_{2} ↦ ∗_{1}; x_{2} ↦ ∗_{2}; x_{2} ↦ g(∗_{1}); x_{1} ↦ a; x_{1} ↦ g(x_{3}); x_{3} ↦ ∗_{1}; x_{3} ↦ d; u↦f(x,x); u↦f(y,y); u↦f(x,y); u↦f(a,g(z)); u↦f(g(x),g(x)); u↦f(g(d),g(x))]

Figure 4: Substitution tree

In our example, we have stored 6 substitutions in the substitution tree. The domains of all these substitutions are identical, but this is not necessary. Substitution trees may also contain substitutions with different domains, which is shown later. We use a backtracking algorithm to find substitutions in the tree with specific properties. All retrieval algorithms are based on backtrackable variable bindings and algorithms for unification and matching which take variable bindings into account. Insertion of a substitution into the index is a complex operation. In contrast to insertion, the deletion of entries is much more straight forward and even complex deletion operations, like the deletion of all compatible substitutions in a substitution tree, can easily be accomplished.

Definition 4.1 (Substitution Tree) A substitution tree is either an empty tree ε or it can be described by a tuple (Σ, Ω) where Σ is a substitution and Ω is a set of substitution trees. The following two conditions hold:

1. A node in the tree is either a leaf node (Σ, ∅) or an inner node (Σ, Ω) with |Ω| ≥ 2.

2. For every path (Σ_{1}, Ω_{1}), …, (Σ_{n}, Ω_{n}) from the root to a leaf of a non–empty tree we have

(a) I(Σ_{n} • … • Σ_{1}) ⊂ V^{∗}.

(b) DOM(Σ_{i}) ∩ (DOM(Σ_{0}) ∪ … ∪ DOM(Σ_{i−1})) = ∅.

Additionally, Subst(N) denotes the set of all substitutions contained in the substitution tree N. We define

Subst((Σ, Ω)) := {Σ} ∪ ⋃_{N′∈Ω} Subst(N′).

In the following we will need the definition of variables which are open at a specific node in the tree.

Definition 4.2 (Open and Closed Variables) A variable x is called open at node N_{n} in a substitution tree if (Σ_{0}, Ω_{0}), …, (Σ_{n}, Ω_{n}) is the path from the root of the tree to node N_{n} and

x ∈ ( ⋃_{0≤i≤n} I(Σ_{i}) \ ⋃_{0≤i≤n} DOM(Σ_{i})).

Variables which are not open are called closed .

The condition I(Σ_{n} • … • Σ_{1}) ⊂ V^{∗} in Def. 4.1 implies that all non–indicator variables are closed at leaf nodes in the tree.

5 Standard Retrieval

As stated in the introduction, the retrieval of substitutions providing specific properties is very important in the field of theorem proving. In this section a general approach to retrieval in substitution trees is presented. Such a retrieval is able to support the search for complementary literals in a large set of clauses for resolution, for example. Additionally, indexing can be used to support subsumption [WOL91, Vor94]. The retrieval of compatible substitutions as well as the search for instances or generalizations of substitutions have a very important feature in common: The search in the index is started for a single substitution which in this context is called query. In contrast to the merge which is introduced in Section 6 such a retrieval is called standard retrieval.

5.1 Theoretical Foundations

Retrieval in substitution trees is very simple. Generally, the retrieval algorithm checks each node of the tree for some special conditions. If the conditions are fulfilled the algorithm proceeds with the subnodes of the node that has been successfully tested. On its way down to the leaf nodes of the tree, the set of passed nodes is collected.

There are three different tests which have to be performed: Find more general substitutions, compatible substitutions, and instances. The functions G, I, and U support the tests at the nodes of the tree. For each assignment x_{i} ↦ t_{i} of the current node’s substitution the functions test whether the variable x_{i} or whatever it is bound to is more general, an instance of, or unifiable with t_{i}. Each of these functions can be used as a parameter for the retrieval function search.

Definition 5.1 (Substitution Functions) Let N = (Σ, Ω) be a substitution tree and ρ a substitution. Then

G(N, ρ) := { σ | ∀x_{i} ∈ DOM(Σ). σρΣ(x_{i}) = ρ(x_{i}) and σ is most general}
U(N, ρ) := { σ | ∀x_{i} ∈ DOM(Σ). σρΣ(x_{i}) = σρ(x_{i}) and σ is most general}
I(N, ρ) := { σ | σ ∈ U(N, ρ) and DOM(σ) ∩ V^{∗} = ∅}

The retrieval function search is defined. It takes the substitution Σ which is stored at node N = (Σ, Ω) in the tree and tests Σ against the current variable bindings ρ using one of the substitution functions. Although, one might only be interested in leaf nodes found in the substitution tree, the definition of search will produce a set of nodes which have successfully passed the test, no matter if they are leaf nodes or not.

Definition 5.2 (Retrieval Function) Let N = (Σ, Ω) be a node in a substitution tree, ρ a substitution, and X one of the functions U, I, or G. The retrieval function search is recursively defined as

search(N, ρ, X) := \{ \begin{matrix}\{N\} ∪ ⋃_{N′∈Ω} search(N′, σρ, X) & if ∃σ ∈ X(N, ρ) \\ ∅ & otherwise \end{matrix}

The next lemma is essential for the soundness of the retrieval operation for compatible substitutions. It states, that two unifiable terms remain unifiable even if a substitution is applied to one of them. However, this substitution has to fulfill some extra conditions.

Lemma 5.1 Let s and t be two unifiable terms, ρ an idempotent most general unifier such that ρ(s) = ρ(t), Σ a substitution with DOM(Σ) ∩ V (t) = ∅, and ∃τ∀x ∈ DOM(Σ). τρΣ(x) = τρ(x). Then

τρΣ(s) = τρ(t)

Proof: As the terms s and t are unifiable by applying the unifier ρ = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}, we have to show that for all assignments x_{i} ↦ ρ(x_{i}) of ρ the equation τρΣ(x_{i}) = τρΣρ(x_{i}) holds. Then τρΣ(s) = τρΣ(t) and as DOM(Σ) ∩ V (t) = ∅ we have τρΣ(s) = τρ(t). In order to prove that τρΣ(x_{i}) = τρΣρ(x_{i}), we have to distinguish four cases:

Case 1: (DOM(Σ) ∩ V (ρ(x_{i})) = ∅ ∧ x_{i} ∈ DOM(Σ))

As x_{i} ∈ DOM(Σ) we use the precondition ∃τ∀x ∈ DOM(Σ). τρΣ(x) = τρ(x) to simplify the equation τρΣ(x_{i}) = τρΣρ(x_{i}) to τρ(x_{i}) = τρΣρ(x_{i}). As DOM(Σ) ∩ V (ρ(x_{i})) = ∅ this is equivalent to τρ(x_{i}) = τρρ(x_{i}), which holds, because ρ is idempotent.

Case 2: (DOM(Σ) ∩ V (ρ(x_{i})) = ∅ ∧ x_{i} ∉ DOM(Σ))

As x_{i} ∉ DOM(Σ) we can simplify each occurrence of Σ(x_{i}) to x_{i}. Therefore the equation τρΣ(x_{i}) = τρΣρ(x_{i}) also simplifies to τρ(x_{i}) = τρΣρ(x_{i}). Proceed as in Case 1.

Case 3: (DOM(Σ) ∩ V (ρ(x_{i})) ≠ ∅ ∧ x_{i} ∈ DOM(Σ))

The equation τρΣ(x_{i}) = τρΣρ(x_{i}) simplifies to τρ(x_{i}) = τρΣρ(x_{i}), if the precondition ∃τ∀x ∈ DOM(Σ). τρΣ(x) = τρ(x) is used. The equation τρ(x_{i}) = τρΣρ(x_{i}) is equivalent to τρρ(x_{i}) = τρΣρ(x_{i}), because ρ is idempotent. We consider the variables y_{j} in ρ(x_{i}). Again we distinguish two cases: First, if y_{j} ∈ DOM(Σ) we may apply the precondition ∃τ∀x ∈ DOM(Σ). τρΣ(x) = τρ(x) to the variables y_{j} in ρ(x_{i}) and get τρ(x_{i}) = τρ(x_{i}). Second, if y_{j} ∉ DOM(Σ) the term Σρ(x_{i}) simplifies to ρ(x_{i}) and therefore τρρ(x_{i}) = τρρ(x_{i}). By induction on the structure of the terms the equation τρρ(x_{i}) = τρΣρ(x_{i}) holds.

Case 4: (DOM(Σ) ∩ V (ρ(x_{i})) ≠ ∅ ∧ x_{i} ∉ DOM(Σ))

Again, we can simplify each occurrence of Σ(x_{i}) to x_{i}, because x_{i} ∉ DOM(Σ). Therefore the equation τρΣ(x_{i}) = τρΣρ(x_{i}) also simplifies to τρ(x_{i}) = τρΣρ(x_{i}). Proceed as in Case 3. □

Theorem 5.1 (Compatible Substitutions) Let N_{0}, …, N_{n} be a path from the root N_{0} = (Σ_{0}, Ω_{0}) to a node N_{n} = (Σ_{n}, Ω_{n}) of a substitution tree and φ a query substitution. Then

N_{n} ∈ search(N_{0}, φ, U) ⟺ ∃σ∀x ∈ V. σΣ_{n} … Σ_{0}(x) = σφ(x)

Proof: Soundness is shown by induction on depth of the node in the tree and completeness is proved by contradiction.

⇒: \underline{n = 0:} In case N_{0} is a root node and N_{0} ∈ search(N_{0}, φ, U) the definition of search implies ∃σ = U(N_{0}, φ). The definition of U yields

∃σ∀x ∈ DOM(Σ_{0}). σφΣ_{0}(x) = σφ(x)

In substitution trees we always have DOM(φ) ∩ I(Σ_{0}) = ∅ and therefore

∃σ∀x ∈ V. σΣ_{0}(x) = σφ(x)

\underline{n > 0:} In case N_{n+1} ∈ search(N_{0}, φ, U) and N_{n+1} ≠ N_{0} we can directly conclude from the definition of search that for the father node N_{n} of N_{n+1} we have N_{n} ∈ search(N_{0}, φ, U) and by the induction hypothesis

∃ρ∀x ∈ V. ρΣ_{n} … Σ_{0}(x) = ρφ(x)

As N_{n+1} ∈ search(N_{0}, φ, U) we can conclude that ∃τ = U(N_{n+1}, ρ) which is equivalent to

∃τ∀x_{i} ∈ DOM(Σ_{n+1}). τρΣ_{n+1}(x_{i}) = τρ(x_{i})

Application of Lemma 5.1 to the induction hypothesis yields

∃ρ, τ∀x ∈ V. τρΣ_{n+1} … Σ_{0}(x) = τρφ(x)

The induction is finished by setting σ = τρ which yields

∃σ∀x ∈ V. σΣ_{n+1} … Σ_{0}(x) = σφ(x)

⇐: Assume that N_{n} ∉ search(N_{0}, φ, U) and ∃σ∀x ∈ V. σΣ_{n} … Σ_{0}(x) = σφ(x). Then there is a path N_{0}, …, N_{i−1}, N_{i}, … N_{n} such that either N_{i} ∉ search(N_{0}, φ, U) and ∀j. 0 ≤ j < i : N_{j} ∈ search(N_{0}, φ, U) or N_{n} is the root node. The case that N_{n} is the root node can directly be excluded as it contradicts the definition of U. We consider the first case: N_{i} ∉ search(N_{0}, φ, U) and ∀j. 0 ≤ j < i : N_{j} ∈ search(N_{0}, φ, U) implies that

U(N_{i}, σ_{i−1} … σ_{0}φ) = ∅

This is equivalent to U(N_{i}, σφ) = ∅, because one can set σ_{i} = σ and for idempotent σ we have σσ = σ. Thus,

¬∃σ∀x ∈ DOM(Σ_{i}). σφΣ_{i}(x) = σφ(x)

which yields

¬∃σ∀x ∈ DOM(Σ_{i}). σφΣ_{i} … Σ_{0}(x) = σφ(x)

because the definition of substitution trees states that DOM(Σ_{i}) ∩ (DOM(Σ_{0}) ∪ … ∪ DOM(Σ_{i−1})) = ∅. Additionally, DOM(φ) ∩ I(Σ_{i}) = ∅ and therefore

¬∃σ∀x ∈ DOM(Σ_{i}). σΣ_{i} … Σ_{0}(x) = σφ(x)

As the variables x ∈ DOM(Σ_{i}) don’t occur in the substitutions of the nodes N_{i+1}, … N_{n} this is equivalent to

¬∃σ∀x ∈ DOM(Σ_{i}). σΣ_{n} … Σ_{0}(x) = σφ(x)

which contradicts our assumptions. □

The proof of the soundness and completeness of the retrieval of more general substitutions is very similar to the one for compatible substitutions. Again a lemma is presented first.

Lemma 5.2 Let s and t be two terms, ρ a matcher such that ρ(s) = t, Σ a substitution with DOM(Σ) ∩ V (t) = ∅, and ∃τ∀x ∈ DOM(Σ). τρΣ(x) = ρ(x). Then

τρΣ(s) = t

Proof: It has to be shown that for all variables x ∈ V (s) the condition τρΣ(x) = ρ(x) holds, because ρ doesn’t instantiate t and DOM(Σ) ∩ V (t) = ∅. Two different cases have to be considered. In the first case x ∈ DOM(Σ) we can use the condition ∃τ∀x ∈ DOM(Σ). τρΣ(x) = ρ(x) to prove τρΣ(x) = ρ(x). In the second case x ∉ DOM(Σ) which implies that Σ(x) simplifies to x. However, the equation τρ(x) = ρ(x) is fulfilled if τ is set to the empty substitution. □

Theorem 5.2 (More General Substitutions) Let N_{0}, …, N_{n} be a path from the root N_{0} = (Σ_{0}, Ω_{0}) to a node N_{n} = (Σ_{n}, Ω_{n}) of a substitution tree and φ a query substitution. Then

N_{n} ∈ search(N_{0}, φ, G) ⟺ ∃σ∀x ∈ V. σΣ_{n} … Σ_{0}(x) = φ(x)

Proof: Using Lemma 5.2 the theorem can be proved in analogy to Theorem 5.1. □

The definitions of the functions U and I are identical except for I doesn’t bind indicator variables. This fact is employed by the next theorem.

Theorem 5.3 (Instances) Let N_{0}, …, N_{n} be a path from the root N_{0} = (Σ_{0}, Ω_{0}) to a leaf node N_{n} = (Σ_{n}, Ω_{n}) of a substitution tree and φ a query substitution. Then

N_{n} ∈ search(N_{0}, φ, I) ⟺ ∃σ∀x ∈ V. Σ_{n} … Σ_{0}(x) = σφ(x)

Proof: We have N_{n} ∈ search(N_{0}, φ, I) if and only if N_{n} ∈ search(N_{0}, φ, U) and DOM(σ) ∩ V^{∗} = ∅ where ∃σ∀x ∈ V. σΣ_{n} … Σ_{0}(x) = σφ(x) if and only if ∃σ∀x ∈ V. Σ_{n} … Σ_{0}(x) = σφ(x) and DOM(σ) ∩ V^{∗} = ∅, because the definition of substitution trees contains I(Σ_{n} • … • Σ_{0}) ⊂ V^{∗}. □

Note that the theorem is valid only for leaf nodes N_{n}.

5.2 Implementing Standard Retrieval

Now that soundness and correctness of the definition of the retrieval have been shown, we can describe an efficient implementation. In our implementations we used the following technique: The algorithm is based on a stack of variable bindings. Variables are pushed on the stack by the function unify(N,STACK,BINDINGS), for example. This function checks for each assignment x_{i} ↦ t_{i} of N’s substitution Σ = {…, x_{i} ↦ t_{i}, …} whether x_{i} is unifiable with t_{i}. The bindings of variables to terms which are necessary to make the terms identical are pushed on the STACK and counted in BINDINGS. Obviously, this unification has to consider variable bindings in the terms to be unified. All occurrences of a variable can easily be changed if the variable is stored just once and shared in all occurrences. Additionally, the function backtrack(STACK, BINDINGS) pops BINDINGS bindings from the STACK. Therefore, this function resets the stack to the state before the unification. A retrieval algorithm based on these functions is presented in Fig. 5.

algorithm search (input N, STACK; output HITS) begin

HITS = ∅;

if (unify(N, STACK, BINDINGS)) HITS = HITS ∪{N}; forall (N′ ∈ Ω^{N})

HITS = HITS ∪ search(N′, STACK); backtrack(STACK, BINDINGS); return HITS;

end;

Figure 5: Algorithm for retrieval function search

5.3 Example

Figure 6 depicts a sequence of stacks resulting from the search for substitutions compatible with {u ↦ f(a, y)}. Originally, the stack is empty. Before we start the retrieval algorithm, all variables in the domain of the query substitution are bound to their corresponding codomain, i.e. the bindings are pushed on the stack (compare stack “Init”). The recursive retrieval algorithm starts with the root node. In case it succeeds, the resulting stack is marked with “Success”. If the corresponding node in the tree is a leaf node, “Success” is written boldface.

Empty

\begin{matrix}u ↦ f(a, y) \\ Init \end{matrix}

Success

x_{2} ↦ y x_{1} ↦ a u ↦ f(a, y) Node 1

Success

∗_{1} ↦ a x_{2} ↦ y x_{1} ↦ a u ↦ f(a, y) Node 2 Success y ↦ a ∗_{1} ↦ a x_{2} ↦ y x_{1} ↦ a u ↦ f(a, y) Leaf 3 BackTrack 3 Success ∗_{2} ↦ y ∗_{1} ↦ a x_{2} ↦ y x_{1} ↦ a u ↦ f(a, y) Leaf 4

BackTrack 4,2

Success

y ↦ g(∗_{1}) x_{2} ↦ y x_{1} ↦ a u ↦ f(a, y) Node 5 Success

y ↦ g(∗_{1}) x_{2} ↦ y x_{1} ↦ a u ↦ f(a, y) Leaf 6 BackTrack 6

Fail

y ↦ g(∗_{1}) x_{2} ↦ y x_{1} ↦ a u ↦ f(a, y) Node 7 BackTrack 7,5,1

\begin{matrix}u ↦ f(a, y) \\ Init \end{matrix}

Reset Init

Empty

Figure 6: Stack of bindings during retrieval for {u ↦ f(a, y)}

In the example the three leaf nodes 3, 4, and 6 are found. They correspond to the substitutions {u ↦ f(x, x)}, {u ↦ f(y, y)},{u ↦ f(x, y)}, and {u ↦ f(a, g(z))}. Due to the renaming of the variables in the substitutions inserted the retrieval in substitution trees does not identify the variable y in the query substitution {u ↦ f(a, y)} with the y occurring in the inserted substitutions.

6 Merge

An advanced operation on substitution trees is merging. The merge computes the set of compatible substitutions stored in two different trees. Substitutions are compatible if the codomains of identical variables in the two substitutions are simultaneously unifiable. For example, the substitutions {x ↦ f(u, b), z ↦ h(w)} and {x ↦ f(a, v), y ↦ g(v)} are compatible and the result of the merge of the two substitutions is {x ↦ f(a, b), y ↦ g(b), z ↦ h(w)}.

An application of the merge operation is hyperresolution. In this context a simultaneous unifier has to be found for a set of literals. To this end we maintain a substitution tree for each literal of the nucleus which contains all unifiers with literals of the electrons. By merging the substitution trees attached to the literals of the nucleus a simultaneous unifier can be computed efficiently.

6.1 Theoretical Foundations

The merge operation is very similar to an ordinary retrieval except that two trees are traversed in parallel. To this end we alternately test nodes in both of the trees.

Definition 6.1 (Merge) Let M = (Σ^{M}, Ω^{M}) and N = (Σ^{N}, Ω^{N}) be two substitution trees, ρ a substitution. The retrieval function merge is recursively defined as follows:

merge(M, N, ρ) := \{ \begin{matrix}\{(M, N′) | N′ ∈ search(N, σρ, U)\} \\ if Ω^{M} = ∅ and Ω^{N} ≠ ∅ and ∃σ ∈ U(M, ρ) \\ \{(M′, N) | M′ ∈ search(M, σρ, U)\} \\ if Ω^{M} ≠ ∅ and Ω^{N} = ∅ and ∃σ ∈ U(N, ρ) \\ \{(M, N)\} ∪ ⋃_{M′∈Ω^{M}} ⋃_{N′∈Ω^{N}} merge(M′, N′, τσρ) \\ if ∃σ ∈ U(M, ρ) and ∃τ ∈ U(N, σρ) \end{matrix}

Theorem 6.1 (merge is Sound and Complete) Let M_{0}, …, M_{m} be a path from the root M_{0} = (Σ_{0}^{M}, Ω_{0}^{M}) to a node M_{m} = (Σ_{m}^{M}, Ω_{m}^{M}) of a substitution tree and N_{0}, …, N_{n} be a path from the root N_{0} = (Σ_{0}^{N}, Ω_{0}^{N}) to a node N_{n} = (Σ_{n}^{N}, Ω_{n}^{N}) of another tree. Additionally, I(Subst(M_{0})) ∩ I(Subst(N_{0})) = ∅. Then

(M_{m}, N_{n}) ∈ merge(M_{0}, N_{0}, ∅) ⟺ ∃σ∀x ∈ V. σΣ_{m}^{M} … Σ_{0}^{M}(x) = σΣ_{n}^{N} … Σ_{0}^{N}(x)

Proof: We proof soundness by nested induction on m and n. Completeness is shown by contradiction.

⇒: \underline{m = 0:}

\underline{n = 0:} We have (M_{0}, N_{0}) ∈ merge(M_{0}, N_{0}, ∅) if ∃ρ ∈ U(M_{0}, ∅) and ∃τ ∈ U(N_{0}, ρ). ∃ρ ∈ U(M_{0}, ∅) implies ρ = Σ_{0}^{M}. As ∃τ ∈ U(N_{0}, Σ_{0}^{M}) we have

∃σ∀x ∈ V. σΣ_{0}^{M}(x) = σΣ_{0}^{N}(x)

\underline{n > 0:} We have (M_{0}, N_{n}) ∈ merge(M_{0}, N_{0}, ∅) if ∃ρ ∈ U(M_{0}, ∅) and additionally N_{n} ∈ search(N_{0}, ρ, U). Again ∃ρ ∈ U(M_{0}, ∅) implies ρ = Σ_{0}^{M}. Theorem 5.1 yields the equivalence of N_{n} ∈ search(N_{0}, Σ_{0}^{M}, U) and

∃σ∀x ∈ V. σΣ_{0}^{M}(x) = σΣ_{n}^{N} … Σ_{0}^{N}(x)
\underline{m > 0:}

\underline{n = 0:} We have (M_{m}, N_{0}) ∈ merge(M_{0}, N_{0}, ∅) if ∃ρ ∈ U(N_{0}, ∅) and additionally M_{m} ∈ search(M_{0}, ρ, U). Again ∃ρ ∈ U(N_{0}, ∅) implies ρ = Σ_{0}^{N}. Theorem 5.1 yields the equivalence of M_{m} ∈ search(M_{0}, Σ_{0}^{N}, U) and

∃σ∀x ∈ V. σΣ_{m}^{M} … Σ_{0}^{M}(x) = σΣ_{0}^{N}(x)

\underline{n > 0:} The fact that (M_{m+1}, N_{n+1}) ∈ merge(M_{0}, N_{0}, ∅) implies that the father nodes (M_{m}, N_{n}) ∈ merge(M_{0}, N_{0}, ∅). The induction hypothesis therefore yields ∃ρ∀x ∈ V. ρΣ_{m}^{M} … Σ_{0}^{M}(x) = ρΣ_{n}^{N} … Σ_{0}^{N}(x). Additionally, (M_{m+1}, N_{n+1}) ∈ merge(M_{0}, N_{0}, ∅) implies that ∃ρ′ ∈ U(M_{m+1}, ρ) and ∃τ ∈ U(N_{n+1}, ρ′ρ). We apply Lemma 5.1 twice to the induction hypothesis and finally get

∃σ∀x ∈ V. σΣ_{m+1}^{M} … Σ_{0}^{M}(x) = σΣ_{n+1}^{N} … Σ_{0}^{N}(x)

⇐: Assume that (M_{m}, N_{n}) ∉ merge(M_{0}, N_{0}, ∅) and

∃σ∀x ∈ V. σΣ_{m}^{M} … Σ_{0}^{M}(x) = σΣ_{n}^{N} … Σ_{0}^{N}(x).

Then there is a path M_{0}, …, M_{i_{j−1}}, M_{i_{j}}, … M_{m} in the tree M_{0} and a path N_{0}, …, N_{i_{j−1}}, N_{i_{j}}, … N_{n} in the tree N_{0} such that (M_{i_{j}}, N_{i_{j}}) ∉ merge(M_{0}, N_{0}, ∅) and (M_{i_{j−1}}, N_{i_{j−1}}) ∈ merge(M_{0}, N_{0}, ∅). This implies that either U(M_{i_{j}}, σ) = ∅ or U(N_{i_{j}}, σ) = ∅.

Case 1: (U(M_{i_{j}}, σ) = ∅)

We have

¬∃σ∀x ∈ DOM(Σ_{i_{j}}^{M}). σΣ_{i_{j}}^{M}(x) = σ(x)

which is equivalent to

¬∃σ∀x ∈ DOM(Σ_{i_{j}}^{M}). σΣ_{m}^{M} … Σ_{0}^{M}(x) = Σ_{n}^{N} … Σ_{0}^{N}σ(x)

as I(Subst(M_{0})) ∩ I(Subst(N_{0})) = ∅ and DOM(Σ_{i_{j}}^{M}) ∩ (DOM(Σ_{0}^{M}) ∪ … ∪ DOM(Σ_{i_{j−1}}^{M})) = ∅ in substitution trees.

Case 2: (U(N_{i_{j}}, σ) = ∅)

Then

¬∃σ∀x ∈ DOM(Σ_{i_{j}}^{N}). σΣ_{i_{j}}^{N}(x) = σ(x)

which corresponds to

¬∃σ∀x ∈ DOM(Σ_{i_{j}}^{N}). σΣ_{m}^{M} … Σ_{0}^{M}(x) = Σ_{n}^{N} … Σ_{0}^{N}σ(x)

for analogous reasons.

In both cases we have a contradiction to our assumptions. □

6.2 Implementing the Merge

An efficient implementation for the merge of two substitution trees is presented. It is based on the same functions and ideas as the algorithm for standard retrieval. The algorithm presented in Fig. 7 has some very special features. First of all, the substitutions of M are tested before each call of the function merge(M,N,STACK). This approach minimizes backtracking on bindings made in context with node M. As a consequence, however, the first unification of the root of M has to be done before merge is called. Second, the roles of the trees M and N are swapped in case N is a leaf node and M is not. Third, in case one of the trees is a leaf node, the function merge does a retrieval identical to the one performed by search.

In Def. 6.1 the result of the merge operation is a set of tuples. In many applications, however, the user is interested in the common instances which are produced during unification of the substitutions. These instances can easily be stored in another substitution tree which then represents the result of the merge. The procedure in order to compute this resulting tree is straight forward: The common instance found by the merge is normalized and inserted. Note that the variable bindings done in context with the renaming have to be reset before the merge is continued. algorithm merge (input M, N, STACK; output HITS) begin

HITS = ∅;

if (unify(N, STACK, BINDINGS^{N})) HITS = HITS ∪ {(M, N)}; if (is leaf(M) and not is leaf(N))

forall (N′ ∈ Ω^{N})

HITS = HITS ∪ merge(M, N′,STACK); else if (is leaf(N) and not is leaf(M))

forall (M′ ∈ Ω^{M})

HITS = HITS ∪ merge(N, M′,STACK); else

forall (M′ ∈ Ω^{M})

if (unify(M′, STACK, BINDINGS^{M}))

forall (N′ ∈ Ω^{M})

HITS = HITS ∪ merge(M′, N′,STACK); backtrack(STACK, BINDINGS^{M});

backtrack(STACK, BINDINGS^{N}); return HITS;

end;

Figure 7: Algorithm for retrieval function merge

6.3 Example

This example shows how an implementation of the merge function computes all pairs of compatible substitutions in the two substitution trees depicted in Fig. 8.

[figure: 1: u ↦ f(x_{1}, x_{2}); 2: x_{1} ↦ ∗_{1}; 3: x_{2} ↦ ∗_{1}; 4: x_{2} ↦ ∗_{2}; 5: x_{2} ↦ g(∗_{1}); 6: x_{1} ↦ a; 7: x_{1} ↦ g(x_{3}); 8: x_{3} ↦ ∗_{1}; 9: x_{3} ↦ d; u↦f(x,x); u↦f(y,y); u↦f(x,y); u↦f(a,g(z)); u↦f(g(x),g(x)); u↦f(g(d),g(x)); A: u ↦ f(y_{1}, y_{2}); B: y_{2} ↦ g(y_{3}); C: y_{1} ↦ ∗_{3}; y_{3} ↦ b; u↦f(z,g(b)); u↦f(y,g(b)); D: y_{1} ↦ c; y_{3} ↦ d; u↦f(c,g(d)); E: y_{1} ↦ a; y_{2} ↦ b; u↦f(a,b)]

Figure 8: Trees to be merged

Note that all variables introduced in the codomains of the substitutions in the trees are disjoint. The tree in Fig. 4 uses the variables x_{i} and the indicator variables ∗_{1} and ∗_{2}. The tree in Fig. 8 uses y_{i} and the indicator variable ∗_{3}.

The merge in our example finds the following compatible substitutions: The substitutions represented by leaf 3 are compatible with the substitutions represented by leaf C.

18 6 MERGE

Empty

Success

u ↦ f(x_{1}, x_{2}) Node 1

Success

x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Node A

Success

y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Node 2

Success

y_{2} ↦ g(y_{3}) y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Node B

Success ∗_{1} ↦ g(y_{3}) y_{2} ↦ g(y_{3}) y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf 3

Success y_{3} ↦ b ∗_{3} ↦ g(y_{3}) ∗_{1} ↦ g(y_{3}) y_{2} ↦ g(y_{3}) y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2})

Leaf C BackTrack C

Fail

∗_{1} ↦ g(y_{3}) y_{2} ↦ g(y_{3}) y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf D BackTrack D,3

Success

∗_{2} ↦ g(y_{3}) y_{2} ↦ g(y_{3}) y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf 4

Success y_{3} ↦ b ∗_{3} ↦ ∗_{1} ∗_{2} ↦ g(y_{3}) y_{2} ↦ g(y_{3}) y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf C BackTrack C

Success y_{3} ↦ a ∗_{1} ↦ b ∗_{2} ↦ g(y_{3}) y_{2} ↦ g(y_{3}) y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf D

BackTrack D,4,B Success ∗_{1} ↦ a y_{2} ↦ b y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf E Fail ∗_{2} ↦ b ∗_{1} ↦ a y_{2} ↦ b y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf 3 BackTrack 3 Success ∗_{2} ↦ b ∗_{1} ↦ a y_{2} ↦ b y_{1} ↦ ∗_{1} x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Leaf 4 BackTrack 4,E,2 Success y_{2} ↦ g(∗_{1}) x_{2} ↦ y_{2} x_{1} ↦ y_{1} u ↦ f(x_{1}, x_{2}) Node 5 • • • Empty

Figure 9: Stack of bindings during merge of two substitution trees Additionally, we have the pairs 4–C, 4–D, 4–E, 6–C, 8–C, and 9–D.

7 Insertion

The insertion of new entries to a substitution tree is more difficult than the retrieval or the deletion of entries. In this section the insertion function and the central notion of the most specific common generalization are introduced. These generalizations are needed if the insertion of new entries produces a new inner node in the tree.

7.1 Theoretical Foundations

Definition 7.1 (Most Specific Common Generalization) Let Σ_{1} and Σ_{2} be two substitutions. If there exist substitutions μ, σ_{1}, and σ_{2} such that σ_{1} • μ = Σ_{1} and σ_{2} • μ = Σ_{2} and there is no substitution λ such that λμ has these properties, then

mscg(Σ_{1}, Σ_{2}) := (μ, σ_{1}, σ_{2})

The substitution μ is called the most specific common generalization (mscg). The substitutions σ_{1} and σ_{2} are called specializations.

The definition is illustrated by the following example: Suppose Σ = {x ↦ g(b), y ↦ a} and ρ = {x ↦ g(a), y ↦ b}. Then mscg(Σ, ρ) := ({x ↦ g(x_{1})}, {x_{1} ↦ b, y ↦ a}, {x_{1} ↦ a, y ↦ b}). The original substitution Σ can be reconstructed by {x_{1} ↦ b, y ↦ a} • {x ↦ g(x_{1})} and ρ = {x_{1} ↦ a, y ↦ b} • {x ↦ g(x_{1})}, respectively. Note that x_{1} is a new auxiliary variable . Obviously, these auxiliary variables represent the parts of the substitutions which differ from each other.

Generally spoken, the insertion process is very similar to finding variant entries in the tree. To this end we define the function V which tries to match the codomain of the substitutions of a tree to the terms which have to be inserted.

Definition 7.2 (Variant Nodes) Let N = (Σ, Ω) be a substitution tree and ρ a substitution. Then

V(N, ρ) := { σ | ∀x_{i} ∈ DOM(Σ). σ(ρ(Σ(x_{i}))) = ρ(x_{i}) ∧ DOM(σ) ∩ V^{∗} = ∅}

When looking for variant nodes, indicator variables are not bound. However, since the substitution which is inserted has to be normalized before adding it to the substitution tree, the test for variant nodes will succeed in matching two identical indicator variables, because no binding will have to be made.

A heuristic select subnode is used for descending into the tree instead of traversing all possible subnodes of a node in the tree. This heuristic has to cope with three different situations: First of all, the heuristic has to select a variant subnode of the current node for descending if such a variant exists. Second, the heuristic selects a non–variant subnode which will yield a non–empty mscg if a variant couldn’t be found. Third, if neither a variant nor a subnode which yields a non–empty common generalization could be found, the heuristic has to select the empty tree for insertion. In this case our insertion function will create a new leaf node.

The insertion function ins returns a tuple (N, M) where N is the modified tree and M is the leaf node which has been found or inserted, respectively. We chose this approach for the following purpose: Usually, people don’t just want to store substitutions, but use the index as a means for accessing data. To this end it has to be possible to store additional information at the leaf nodes of the search tree. Therefore, we also return the leaf node M to enable the user to perform some extra operations on this node.

Definition 7.3 (Insertion Function ins) Let N = (Σ, Ω) be a substitution tree, ρ a substitution which is supposed to be inserted and OV the set of open variables at node N. Then

ins(N, ρ, OV) := \{ \begin{matrix}(M, M) \\ if N = ε and M = (ρ|_{OV} , ∅) & (1) \\ (N, N) \\ if ∃σ ∈ V(Σ, ρ) and Ω = ∅ & (2) \\ ((μ, \{(σ_{1}, Ω), M\}), M) \\ if ¬∃σ ∈ V(Σ, ρ) and mscg(Σ, ρ) = (μ, σ_{1}, σ_{2}) \\ and M = (σ_{2} ∪ ρ|_{OV \DOM(Σ)}, ∅) & (3) \\ ((Σ, Ω\N′ ∪ M′), M) \\ if ∃σ ∈ V(Σ, ρ) and Ω ≠ ∅ and \\ N′ = select subnode(N) and \\ (M′, M) = ins(N′, σρ, OV \DOM(Σ) ∪ I(Σ)) & (4) \end{matrix}

To insert a substitution ρ into a tree (N, M) = ins(N, \overline{ρ}, DOM(ρ)) is called. Note that the substitution ρ has to be normalized in advance. Rule (1) creates a new leaf node in case a substitution is inserted into an empty tree, while Rule (2) returns a leaf node which corresponds to a variant substitution which has been inserted yet. Rule (3) creates a new inner node and a new leaf in case the substitution in the tree is not a variant of the substitution which has to be inserted. The set of open variables OV is needed for completely describing the inserted substitution in case a new leaf node is created. Finally, Rule (4) uses a heuristic to find a subnode of the current node where the insertion will be continued. Depending on the subnode selected by the heuristic Rule (4) can cause different insertions.

7.2 Examples

Consider the exemplifying insertion sequence in Fig. 10. Rule (1) works on empty trees and the insertion of \{x ↦ \overline{f(z, g(b))}\} into an empty tree yields leaf A marked with \{x ↦ f(∗_{1}, g(b))}.

The substitution \{x ↦ \overline{f(y, g(b))}\} is inserted into tree A. The tree is non–empty and f(∗_{1}, g(b)) is a variation of the substitution in the root node. In this case no new leaf is created and tree B is identical to tree A.

The substitution \{x ↦ \overline{f(a, b)}\} is inserted into tree B yielding tree C. As f(∗_{1}, g(b)) is not a variant of f(a, b), Rule (3) adds a new root and a new leaf node to the tree. The new root represents the common parts of f(∗_{1}, g(b)) and f(a, b). Such a most specific common generalization contains auxiliary variables at the positions where the original terms are different. In our example the root is marked with {x ↦ f(x_{1}, x_{2})}. Additionally, the new leaf contains the bindings which are needed to completely represent the substitution being inserted.

Insertion of the substitution \{x ↦ \overline{f(c, g(d))}\} to tree C employs the heuristic mentioned in Rule (4). As the substitution to be inserted is a variant of the root of the tree, the heuristic has to select the subnode of the tree where the insertion process will be continued. Assume that the node marked with {x_{1} ↦ ∗_{1}, x_{2} ↦ g(b)} is selected. Again Rule (3) is applied; the resulting tree D contains a new leaf node and a new inner node marked with {x_{2} ↦ g(x_{3})}. This substitution is the most specific common generalization for the substitutions {x_{1} ↦ ∗_{1}, x_{2} ↦ g(b)} and {x_{1} ↦ c, x_{2} ↦ g(d)}.

Eventually, \{x ↦ \overline{f(b, g(a))}\} is inserted into tree D, thus yielding tree E. In this case Rule (4) is applied two times in a row. Assume that the heuristic in the first application selects node {x_{2} ↦ g(x_{3})} for insertion. However, the heuristic applied to this node cannot find a subnode which is either a variant or at least would produce a non–empty mscg if Rule (3) was applied. Therefore, our heuristic selects the empty tree, and Rule (1) produces a single leaf which then is added to the leaf nodes of the current node by Rule (4).

[figure: A: x ↦ f(∗_{1}, g(b)); x↦f(z,g(b)); B: x ↦ f(∗_{1}, g(b)); x↦f(z,g(b)); x↦f(y,g(b)); C: x ↦ f(x_{1}, x_{2}); x_{1} ↦ ∗_{1}; x_{2} ↦ g(b); x↦f(z,g(b)); x↦f(y,g(b)); x_{1} ↦ a; x_{2} ↦ b; x↦f(a,b); D: x ↦ f(x_{1}, x_{2}); x_{2} ↦ g(x_{3}); x_{1} ↦ ∗_{1}; x_{3} ↦ b; x↦f(z,g(b)); x↦f(y,g(b)); x_{1} ↦ c; x_{3} ↦ d; x↦f(c,g(d)); x_{1} ↦ a; x_{2} ↦ b; x↦f(a,b); E: x ↦ f(x_{1}, x_{2}); x_{2} ↦ g(x_{3}); x_{1} ↦ ∗_{1}; x_{3} ↦ b; x↦f(z,g(b)); x↦f(y,g(b)); x_{1} ↦ b; x_{3} ↦ a; x↦f(b,g(a)); x_{1} ↦ c; x_{3} ↦ d; x↦f(c,g(d)); x_{1} ↦ a; x_{2} ↦ b; x↦f(a,b)]

Figure 10: Insertion sequence for substitutions with identical domains

So far, all nodes in our substitution trees have been marked with non–empty substitutions, which is not the case in general! The insertion of the substitutions {x ↦ a} and {x ↦ b} into an empty tree, for instance, will yield a root node marked with the empty substitution, as the constants a and b actually have very little in common. The same thing happens if substitutions with non–identical domains are inserted into our index. The insertion sequence in Fig. 11 shows more details: First, the substitution {x ↦ g(a), y ↦ b} is inserted into the empty tree and a single leaf is created. Insertion of {x ↦ g(b), z ↦ b} produces a root marked with {x ↦ g(x_{1})}. The substitution {z ↦ a} is neither a variant of {x ↦ g(x_{1})} nor is there a non–empty common generalization for the two substitutions; an empty root is created. Finally, {x ↦ g(a)} is added to the tree. However, this substitution is part of a substitution which has been inserted. As a consequence the new leaf node is also marked with an empty substitution. Note that inner nodes never have empty substitutions.

[figure: A: x ↦ g(a), y ↦ a; x↦g(a),y↦a; B: x ↦ g(x_{1}); x_{1} ↦ a; y ↦ a; x↦g(a),y↦a; x_{1} ↦ b; z ↦ b; x↦g(b),z↦b; C: ∅; x ↦ g(x_{1}); x_{1} ↦ a; y ↦ a; x↦g(a),y↦a; x_{1} ↦ b; z ↦ b; x↦g(b),z↦b; z ↦ a; z↦a; D: ∅; x ↦ g(x_{1}); x_{1} ↦ a; y ↦ a; x↦g(a),y↦a; ∅; x↦g(a); x_{1} ↦ b; z ↦ b; x↦g(b),z↦b; z ↦ a; z↦a]

Figure 11: Insertion sequence for substitutions with different domains

7.3 Computing the Most Specific Common Generalization

The next two definitions 7.4 and 7.5 are rather technical. They show how the mscg is derived in detail. In Def. 7.4 the function mscg^{t} which computes the mscg for two terms is defined. Definition 7.5 extends mscg^{t} to substitutions.

Definition 7.4 (MSCG for Terms) Let s and t be two terms and σ_{1} and σ_{2} be two substitutions. Then

mscg^{t}(s, t, σ_{1}, σ_{2}) := \{ \begin{matrix}(f(cg_{1}, …, cg_{n}), σ_{1}, σ_{2}) \\ if s = f(s_{1}, …, s_{n}) and t = f(t_{1}, …, t_{n}) and \\ ∀_{1≤i≤n} (cg_{i}, σ_{1}, σ_{2}) = mscg^{t}(s_{i}, t_{i}, σ_{1}, σ_{2}) & (1) \\ (s, σ_{1}, σ_{2}) \\ if s ∈ V^{∗} and s = t & (2) \\ (s, σ_{1}, σ_{2} ∪ \{s ↦ t\}) \\ if s ∈ V \V^{∗} and s ≠ t & (3) \\ (y, σ_{1}, σ_{2}) \\ if ∃y ∈ DOM(σ_{1}) ∩ DOM(σ_{2}) and \\ σ_{1}(y) = s and σ_{2}(y) = t & (4) \\ (x_{j}, σ_{1} ∪ \{x_{j} ↦ s\}, σ_{2} ∪ \{x_{j} ↦ t\}) \\ where x_{j} is a new auxiliary variable. & (5) \end{matrix}

Rules (1) and (2) extract identical symbols from the two terms with Rule (1) handling constant and function symbols and Rule (2) treating indicator variables as if they were constants. Note that the substitutions σ_{1} and σ_{2} in Rule (1) are changed by every call of mscg^{t}. In case there is a non–indicator variable in term s it can also be used in the specialization for the new leaf node, which is stated by Rule (3). Rule (4) describes how the assignments will be reused in the found specializations, resulting in a non–linear mscg. However, to achieve generalizations this rule may be omitted. The effect on the substitution tree is minimal, because most of the non–linear generalizations in a tree are changed to linear generalizations by further insertions. Changes in memory requirements and retrieval times are minimal. Finally, Rule (5) introduces new non–indicator variables in case none of the other rules could be applied.

When solving mscg^{t}(f(a, ∗_{2}, x_{1}, ∗_{1}, ∗_{1}), f(a, ∗_{2}, c, b, b), ∅, ∅), for instance, all five Rules of the definition of mscg^{t} are applied. The result is (f(a, ∗_{2}, x_{1}, x_{2}, x_{2}), {x_{2} ↦ ∗_{1}}, {x_{1} ↦ c, x_{2} ↦ b}).

Definition 7.5 (MSCG for Substitutions) Let Σ be a substitution in a substitution tree, ρ the current variable bindings. The most specific common generalization μ and the specializations σ_{1} and σ_{2} are computed using the following recursive definition.

mscg^{σ}(Σ, ρ, μ, σ_{1}, σ_{2}) := \{ mscg^{σ}(Σ\\{x_{i} ↦ t_{i}\}, ρ, μ, σ_{1} ∪ \{x_{i} ↦ t_{i}\}, σ_{2}) if x_{i} ↦ t_{i} ∈ Σ and x_{i} = ρ(x_{i})  (1) mscg^{σ}(Σ\\{x_{i} ↦ t_{i}\}, ρ, μ ∪ \{x_{i} ↦ t_{i}\}, σ_{1}, σ_{2}) if x_{i} ↦ t_{i} ∈ Σ and t_{i} = ρ(x_{i})  (2) \begin{matrix}mscg^{σ}(Σ\\{x_{i} ↦ t_{i}\}, ρ, μ, σ_{1} ∪ \{x_{i} ↦ t_{i}\}, \\ σ_{2} ∪ \{x_{i} ↦ ρ(x_{i})\}) \end{matrix} if x_{i} ↦ t_{i} ∈ Σ and top(t_{i}) ≠ top(ρ(x_{i})) (3) mscg^{σ}(Σ\\{x_{i} ↦ t_{i}\}, ρ, μ ∪ \{x_{i} ↦ cg\}, σ_{1}, σ_{2}) if x_{i} ↦ t_{i} ∈ Σ and top(t_{i}) = top(ρ(x_{i})) and t_{i} ≠ ρ(x_{i}) and (cg, σ_{1}, σ_{2}) = mscg^{t}(t_{i}, ρ(x_{i}), σ_{1}, σ_{2})  (4) (μ, σ_{1}, σ_{2}) if Σ = ∅  (5)

The function mscg^{σ} considers every assignment x_{i} ↦ t_{i} ∈ Σ. We have seen, that during the insertion variable bindings are established by the function V. These current bindings are stored in ρ. Rule (1) handles assignments in Σ which map variables that don’t occur in the substitution which is inserted. Rule (2) detects assignments where the binding of x_{i} is identical to what it has to be bound. In case the terms under consideration don’t even have the same top symbol, Rule (3) completely splits the information to the specializations. Finally, Rule (4) initiates calls to mscg^{t} in all other cases.

For example, we have mscg^{σ}({y ↦ a, x_{1} ↦ a, x_{2} ↦ b, x_{3} ↦ f(c)}, {x_{1} ↦ a, x_{2} ↦ c, x_{3} ↦ f(a)}, ∅, ∅, ∅) = ({x_{1} ↦ a, x_{3} ↦ f(x_{4})}, {y ↦ a, x_{2} ↦ b, x_{4} ↦ c}, {x_{2} ↦ c, x_{4} ↦ a}).

7.4 Reusing non–indicator Variables

In Rule (5) of Def. 7.4 we introduced new auxiliary variables for representing the differences of the terms in the mscg. However, such a non–indicator variable doesn’t really have to be a new variable: In tree D in Fig. 10 we introduced the new variable x_{3}. Obviously, the variable x_{3} could be used again if we had to create another mscg in the right subtree of the root. Generally spoken, let N_{0} = (Σ_{0}, Ω_{0}), …, N_{i} = (Σ_{i}, Ω_{i}) be a path in a substitution tree and N_{i} a node which has to be extended. In this situation the set of non–indicator variables which can be reused is the set of all non–indicator variables in the tree minus the domain variables on the path from N_{0} to N_{i} minus the domain variables that occur in the subtree N_{i}. More formally, this set can also be described as

DOM(Subst(N_{0})) \ ⋃_{0≤j<i} DOM(Σ_{j}) \ DOM(Subst(N_{i})).

Reusing non–indicator variables is an advantage both for memory requirements and for the speed of the retrieval. Using the above definition the reusable variables can easily be computed during insertion if the set DOM(Subst(N_{0})) is maintained, which implies that it doesn’t have to be recomputed for each insertion. In our implementation of substitution tree indexing, this technique of variable reusing was able to reduce the number of variables by a factor of 40 in the average case.

7.5 Insertion Heuristics

As mentioned, an insertion heuristic is used for descending into the tree and the heuristic has to cope with three different situations: Either it selects a variant subnode of the current node for descending or it selects a non–variant subnode which will yield a non– empty mscg if a variant couldn’t be found. If such a node doesn’t exist either, the empty tree is selected. In this case the insertion function will create a new leaf node. In our implementation we used a very simple first–fit heuristic: We chose the first^{1} variant son for descending. If such a son doesn’t exist the first non–variant son which produces a non–empty mscg is selected.

In general, using a more complex insertion heuristic implies the necessity of traversing the tree finding all possible insertion positions. Finally, the different positions found are rated by the insertion heuristic and the substitution is inserted at the best position. However, this technique has some disadvantages compared to the first–fit technique:

• The whole tree has to be traversed.

• The variable bindings found in the traversal either have to be stored for each insertion position or have to be recomputed for the insertion position that was considered to be best.

• Further insertions to the index are not known at the moment the selection of the best node is taken. This implies that the decision to insert the substitution at a specific position could be “wrong”.

• Most insertion heuristics cause the computation or the storage of additional information like the depth of a subtree and such.

For all these reasons using insertion heuristics doesn’t guarantee best results. Trying several heuristics which minimize

• size of the index,

• number of auxiliary variables x_{i} in the index,

• number of sons for inner nodes of the tree, or

• depth of indicator variables ∗_{i} in the tree

when inserting new substitutions confirmed our suspicion: Insertion was very slow and, although the resulting trees were a little smaller with some heuristics, the retrieval times didn’t change significantly. Due to this experience, using a complex insertion heuristic cannot be recommended.

1In the definition of substitution trees the subtrees of an inner node are represented by a set of subtrees.

A real implementation, however, will store these subtrees in some order.

8 Deletion

The deletion of entries in a substitution tree is based on two facts. First, the substitution which has to be deleted from the index doesn’t need to be normalized if we keep on looking for variants until we find a leaf node in the tree. Second, just like the insertion function, the deletion has to cope with additional information which is stored in the leaf nodes of the tree, if the tree is used to access a database by substitutions. To this end, the deletion uses a predicate Δ in order to determine whether a specific node really has to be deleted. Assume the user stores different pointers at the leaf nodes of the tree. If a leaf only contains the pointer which was searched, the whole leaf node has to be deleted. If the leaf contains more than this pointer, the pointer has to be deleted from the list of pointers stored at the leaf node, but the node itself is left unchanged.

Definition 8.1 (Deletion Function del) Let N be a substitution tree and ρ a substitution which is supposed to be deleted. Function del deletes nodes which represent variants of ρ if the predicate Δ evaluates to true at specific leaf nodes in the tree.

del(N, ρ, Δ) := \{ \begin{matrix}ε & if ∃σ ∈ V(Σ, ρ) and either Ω = ∅ and Δ(N) \\ or Ω ≠ ∅ and ⋃_{N_{i}∈Ω} del(N_{i}, σρ, Δ) = ∅ & (1) \\ N & if ∃σ ∈ V(Σ, ρ) and Ω = ∅ and ¬Δ(N) & (2) \\ (Σ, ⋃_{N_{i}∈Ω} del(N_{i}, σρ, Δ)) \\ if ∃σ ∈ V(Σ, ρ) and Ω ≠ ∅ \\ and | ⋃_{N_{i}∈Ω} del(N_{i}, σρ, Δ)| ≥ 2 & (3) \\ (Σ′ • Σ, Ω′) \\ if ∃σ ∈ V(Σ, ρ) and Ω ≠ ∅ \\ and ⋃_{N_{i}∈Ω} del(N_{i}, σρ, Δ) = \{(Σ′, Ω′)\} & (4) \\ N & otherwise & (5) \end{matrix}

Rule (1) is applied either if N is a leaf node and Δ decides to delete the leaf or if all subtrees of an inner node are deleted by recursive calls of del. Leaf nodes where Δ(N) evaluates^{2} to false are left unchanged, as stated by Rule (2). Rule (3) describes the deletion of subnodes of an inner node where at least two subtrees remain. The join in Rule (4) is needed in case just one subtree is left over, because our definition of substitution trees demands that every inner node has to have at least two subtrees. In case the current node N is not a variant of the current variable bindings ρ the node is left unchanged, which is stated by Rule (5). Obviously, Fig. 10 and Fig. 11 also represent deletion sequences if the trees are read in reverse order.

Deleting the Results of a Retrieval. The function del can easily be modified so it will delete all instances, generalizations, or unifiable entries from the index. Simply change all occurrences of V(Σ, ρ) to I(Σ, ρ), G(Σ, ρ), or U(Σ, ρ), respectively. Additionally, Δ(N) has to be true for all nodes N.

2Maybe after having performed some side effects on the data stored at the leaf.

9 Experiments

In this section substitution trees are compared to other indexing methods. As most of the other techniques don’t serve as an indexing mechanism for substitutions, we use our implementation of substitution trees as a term index.

9.1 The Term Sets

For the experiments special term sets were used. Part of them have been introduced in [McC92]. These sets were taken from typical OTTER applications. As the sets are paired, there is a set of positive literals and a set of negative literals in each pair. Unifiable terms are searched in order to find resolution partners and to detect unit conflicts. The sets EC– pos and EC–neg consist of 500 terms each and are derived from a theorem in equivalential calculus. Two representative members of EC–pos and EC–neg are

P (e(e(x, e(y, e(z, e(e(u, e(v, z)), e(v, u))))), e(y, x)))

and

¬P (e(e(x, e(e(y, e(z, x)), e(z, y))), e(e(u, e(e(v, e(w, u)), e(w, v))), e(e(v6,
e(e(v7, e(v8, v6)), e(v8, v7))), e(e(v9, e(e(e(b, a),
e(e(e(a, e(b, c)), c), v9)), v10)), v10))))).

The sets CL–pos and CL–neg have 1000 members and are derived from a theorem in combinatory logic. Two representative members of CL–pos and CL–neg are

g(x, g(g(g(g(g(B, B), y), z), u), v)) = g(g(g(B, x), g(y, z)), g(u, v)

and

g(f(g(g(N, x), y)), g(g(g(N, x), y), f(g(g(N, x), y)))) ≠
g(g(g(x, f(g(g(N, x), y))), y), f(g(g(N, x), y))).

The sets BOOL–pos and BOOL–neg are derived from a theorem in the relational formulation of Boolean algebra and consist of 6000 terms each. Two representative members of BOOL–pos and BOOL–neg are

Sum(x, p(x, y), p(x, s(x, y)))

and

¬Sum(p(c2, n(x)), p(c2, x), c4).

The other part of the term sets was produced randomly. All of these sets contain 10000 terms. Three different function symbols with varying arities and three different constants have been used. The terms contain at most three different variables with possibly multiple occurrences.

The set WIDE-10000 contains function symbols with an arity of at least 3. In the other sets the maximal arity of function symbols is 2.

The maximal depth of all terms is 3 except for the set DEEP-10000 where the maximal term depth is 6.

Terms in LIN–10000 contain each variable at most once and the set GND-10000 contains no variables at all. All other sets contain linear as well as non–linear terms.

For example, a representative member of the set AVG-10000 which contains linear and non–linear terms with a maximal depth of 3 and a maximal arity of 2 is

g(f(g(x14, a), g(a, c)), g(h(x14), f(b, c))).

9.2 Memory Requirements

In Fig. 12 the memory requirements of discrimination trees (DT), abstraction trees (AT), and substitution trees (ST) are compared. Additionally, a survey on the times needed to build the index and the times needed to delete all entries of the index one by one is presented.

Memory Requirements [KBytes]

Indexed Set  DT  AT  ST
EC–pos  108  153  \underline{88}
EC–neg  539  483  \underline{252}
CL–pos  612  505  \underline{318}
CL–neg  2113  1116  \underline{797}
BOOL–pos  685  780  \underline{610}
BOOL–neg  958  1090  \underline{858}
AVG–10000  969  1278  \underline{935}
WIDE–10000 13402  9312  \underline{8056}
GND–10000  846  1015  \underline{831}
LIN–10000  1020  1265  \underline{950}
DEEP–10000  6191  4312  \underline{3766}
100% ^{97%} ^{70%} DT AT ST

Figure 12: Memory requirements

First of all, our experiments show that substitution trees require the least memory space. This result was expected, because the information sharing is best in this index. In the average case a substitution tree consumes 70% of the memory occupied by the worst of the three techniques. This fact is illustrated in Fig. 12. For each of the three indexing techniques we have three bars. The white bar represents the average behavior, for example discrimination tree indexing is most greedy in memory consumption. The gray bar shows the best result of the experiments and the black bar the worst behavior. Consider the bars for abstraction tree indexing: In the average case, the trees need 97% of the memory needed by the most greedy technique. However, there was an experiment where abstraction trees occupied just 53% of the memory occupied by the worst technique. Nevertheless, the black bar tells us that abstraction trees also have at least once been the most memory consuming index.

9.3 Insertion

The creation of discrimination trees is fastest, because these indexes are deterministic. To insert a term we just have to normalize it and to insert it at the only possible position in the index. The other two indexing techniques are slower at adding entries to the index, because these indexes are non-deterministic and a position for insertion has to be found using a more or less complex algorithm. In contrast to substitution trees the abstraction tree technique doesn’t require a normalization of the entries to be inserted, and therefore abstraction trees are faster at inserting new entries as shown in Fig. 13.

Insertion [Seconds]

Indexed Set DT AT  ST
EC–pos  \underline{0.3} \underline{0.3} \underline{0.3}
EC–neg  1.0 \underline{0.9}  1.3
CL–pos  \underline{0.8}  0.9  1.3
CL–neg  \underline{2.4} \underline{2.4}  3.2
BOOL–pos  \underline{1.1}  1.6  2.4
BOOL–neg  \underline{1.7}  2.3  3.6
AVG–10000  \underline{1.7}  6.4  4.2
WIDE–10000 \underline{9.0} 13.6 17.7
GND–10000  \underline{1.5}  2.6  4.0
LIN–10000  \underline{1.8}  6.0  4.3
DEEP–10000 \underline{5.3} 11.3  9.3
41% ^{68%} ^{100%} DT AT ST

Figure 13: Experiments with insertion

9.4 Deletion

Figure 14 shows, that substitution trees are appropriate also for dynamic data, because entries are deleted most quickly although insertion is slow.

Deletion [Seconds]

Indexed Set DT AT  ST
EC–pos  0.4  0.2  \underline{0.1}
EC–neg  1.6  1.2  \underline{0.2}
CL–pos  1.6  1.0  \underline{0.1}
CL–neg  4.1  3.1  \underline{1.5}
BOOL–pos  \underline{1.9}  2.2  2.7
BOOL–neg  2.7 \underline{2.1}  3.0
AVG–10000  \underline{2.7}  6.6  4.7
WIDE–10000 19.2 16.9 \underline{13.3}
GND–10000  \underline{2.4} \underline{2.4}  4.0
LIN–10000  \underline{2.7}  6.2  4.6
DEEP–10000  9.9 11.0  \underline{7.6}
100% ^{96%} ^{80%} DT AT ST

Figure 14: Experiments with deletion

The wide range of the values for deletion in substitution trees is striking; the best deletion takes just 6% of the time of the worst while there are examples where the deletion in substitution trees itself is slowest. When no indicator variables occur in the terms, as in GND–10000, deletion of entries is slow, because the treatment of indicator variables is the main advantage of substitution tree indexing. Deletion in substitution trees performs extremely well in case the terms are deep as in EC–neg, CL–pos, and DEEP–10000.

9.5 Retrieval Times

The experiments were run on a Sun SPARCstation SLC computer with 16 MBytes of RAM. In all but the merge experiments the set in column Index was stored in an index. Then for all members of the set Query we were looking for more general substitutions, instances, and compatible substitutions. Similar tests using discrimination tree indexing and path–indexing have been reported in [McC92].

Generalizations [Seconds]

Index  Query  DT  AT  ST
EC–pos  EC–pos  0.6  0.4  \underline{0.3}
EC–pos  EC–neg  1.7  0.8  \underline{0.4}
EC–neg  EC–pos  0.4  \underline{0.1}  \underline{0.1}
EC–neg  EC–neg  2.1  0.7  \underline{0.6}
CL–pos  CL–pos  3.4  \underline{0.8}  \underline{0.8}
CL–pos  CL–neg  4.0  \underline{0.2}  0.3
CL–neg  CL–pos  1.3  \underline{0.1}  \underline{0.1}
CL–neg  CL–neg  5.6  1.7  \underline{1.5}
BOOL–pos  BOOL–pos  \underline{3.3}  3.5  3.4
BOOL–pos  BOOL–neg  3.6  3.1  \underline{3.0}
BOOL–neg  BOOL–pos  1.7  0.9  \underline{0.8}
BOOL–neg  BOOL–neg  3.6  2.3  \underline{2.1}
AVG–10000  AVG–10000  13.5 28.0 \underline{13.3}
WIDE-10000 WIDE-10000 27.9 \underline{16.2} 18.0
GND–10000  GND–10000  4.6  4.1  \underline{3.7}
LIN–10000  LIN–10000  13.0 25.5 \underline{12.8}
DEEP–10000 DEEP–10000 22.7 28.2 \underline{14.8}

100% ^{66%} ^{53%} DT AT ST

Figure 15: Retrieval of more general terms

By the way, in all experiments path–indexing was much slower than substitution tree indexing. For the merge experiments an index for the set Index and an index for the Query set was created. Then the two indexes were merged. The retrieval times exclude the time for the creation of indexes. First of all, in the average case substitution tree indexing is the fastest of the techniques. Discrimination trees are slowest. Abstraction trees seem to work well on “wide” terms. The merge of discrimination trees is not defined.

There are only three experiments in which substitution tree indexing is not the fastest technique for the retrieval of more general entries. Due to the introduction of indicator variables, the search for instances using substitution trees takes just 1% of the time of discrimination or abstraction trees in case of the sets EC–neg and EC–pos which contain lots of variables. Substitution trees provide fastest retrieval of instances in all examples.

There are only two experiments where substitution trees don’t find unifiable entries most quickly. In eight experiments, the retrieval time using abstraction trees for the merge 9.5 Retrieval Times 31

Instances [Seconds]

Index  Query  DT AT  ST
EC–pos  EC–pos  6.5  6.0  \underline{1.0}
EC–pos  EC–neg  3.8  6.0  \underline{0.8}
EC–neg  EC–pos  42.8 14.9  \underline{0.3}
EC–neg  EC–neg  76.4 18.6  \underline{1.4}
CL–pos  CL–pos  17.9  4.6  \underline{1.7}
CL–pos  CL–neg  3.2  3.5  \underline{0.1}
CL–neg  CL–pos  100.0 11.9  \underline{6.7}
CL–neg  CL–neg  5.2  5.1  \underline{3.1}
BOOL–pos  BOOL–pos  6.1  7.5  \underline{5.2}
BOOL–pos  BOOL–neg  2.6  4.2  \underline{2.3}
BOOL–neg  BOOL–pos  18.7  2.4  \underline{1.8}
BOOL–neg  BOOL–neg  3.7  3.5  \underline{2.6}
AVG–10000  AVG–10000  60.8 50.6 \underline{32.2}
WIDE-10000 WIDE-10000 550.3 60.0 \underline{46.7}
GND–10000  GND–10000  5.0  5.5  \underline{4.3}
LIN–10000  LIN–10000  49.0 44.3 \underline{30.0}
DEEP–10000 DEEP–10000 643.1 70.4 \underline{52.8}

100% ^{67%} ^{33%} DT AT ST

Figure 16: Retrieval of instances

Unifiable Terms [Seconds]

Index  Query  DT  AT  ST
EC–pos  EC–pos  27.9  32.1  \underline{11.8}
EC–pos  EC–neg  28.6  60.6  \underline{21.8}
EC–neg  EC–pos  99.9  89.2  \underline{5.8}
EC–neg  EC–neg  308.8 211.1  \underline{46.1}
CL–pos  CL–pos  50.2  12.7  \underline{6.8}
CL–pos  CL–neg  42.7  17.6  \underline{4.8}
CL–neg  CL–pos  309.4  22.5  \underline{16.9}
CL–neg  CL–neg  19.1  7.3  \underline{6.8}
BOOL–pos  BOOL–pos  11.1  10.0  \underline{9.2}
BOOL–pos  BOOL–neg  \underline{4.9}  5.5  5.3
BOOL–neg  BOOL–pos  23.9  2.4  \underline{2.3}
BOOL–neg  BOOL–neg  4.0  3.5  \underline{3.3}
AVG–10000  AVG–10000  100.2  86.5  \underline{61.5}
WIDE-10000 WIDE-10000 672.7 \underline{84.3} 110.3
GND–10000  GND–10000  4.6  5.1  \underline{4.5}
LIN–10000  LIN–10000  74.7  71.1  \underline{52.2}
DEEP–10000 DEEP–10000 736.6 142.3 \underline{138.6}

100% ^{67%} ^{42%} DT AT ST

Figure 17: Retrieval of unifiable terms

Merge [Seconds]

Index  Query  AT  ST
EC–pos  EC–pos  34.9 \underline{12.1}
EC–pos  EC–neg  89.1  \underline{8.9}
EC–neg  EC–pos  88.5  \underline{6.1}
EC–neg  EC–neg  226.3 \underline{25.9}
CL–pos  CL–pos  11.7  \underline{4.3}
CL–pos  CL–neg  19.7  \underline{9.5}
CL–neg  CL–pos  19.2  \underline{8.3}
CL–neg  CL–neg  5.8  \underline{4.4}
BOOL–pos  BOOL–pos  9.7  \underline{8.7}
BOOL–pos  BOOL–neg  \underline{3.0}  3.9
BOOL–neg  BOOL–pos  \underline{3.7}  5.0
BOOL–neg  BOOL–neg  1.7  \underline{1.6}
AVG–10000  AVG–10000  93.6 \underline{57.9}
WIDE-10000 WIDE-10000 \underline{173.4} 290.0
GND–10000  GND–10000  \underline{2.8}  3.8
LIN–10000  LIN–10000  76.3 \underline{48.0}
DEEP–10000 DEEP–10000 184.9 \underline{99.7}

100% ^{65%} AT ST

Figure 18: Retrieval of unifiable terms using the merge operation

is slower as the standard retrieval for compatible substitutions. With substitution trees this happened just four times.

9.6 Implementation

Substitution trees, abstraction trees, discrimination trees, and (extended) path–indexing are implemented in C and are available via anonymous ftp. They are as well as implementations of other indexing techniques part of “A Collection of Indexing Data Structures (ACID)” developed at MPI. Some of the techniques support subterm retrieval. In the future ACID which is a library for efficient data structures and algorithms for theorem provers will be further improved. Our implementations do not depend on term data structures and can very easily be embedded into other software. For more information send e-mail to acid@mpi-sb.mpg.de.

10 Conclusion

The new data structure of substitution trees for indexing substitutions was presented. Substitution trees are based on a simple data structure. Experiments showed, that substitution trees perform very well on completely different tasks. They are stable also for large sets of entries and memory requirements are low. Additionally, retrieval is fastest. The disadvantage of relatively slow insertion is compensated by a very fast and powerful deletion procedure.

References

[BCR93] L. Bachmair, T. Chen, and I.V. Ramakrishnan. Associative-commutative discrimination nets. In Proceedings TAPSOFT ’93, LNCS 668, pages 61–74. Springer Verlag, 1993.

[BO94] R. Butler and R. Overbeek. Formula databases for high–performance resolution/paramodulation systems. Journal of Automated Reasoning, 12:139–156, 1994.

[Chr93] J. Christian. Flatterms, discrimination nets, and fast term rewriting. Journal of Automated Reasoning, 10(1):95–113, February 1993.

[Gra92] P. Graf. Path indexing for term retrieval. Technical Report MPI-I-92-237, Max-Planck-Institut für Informatik, Saarbrücken, Germany, December 1992.

[Gra94] P. Graf. Extended path–indexing. In 12th Conference on Automated Deduction, pages 514–528. Springer LNAI 814, 1994.

[LO80] E. Lusk and R. Overbeek. Data structures and control architectures for the implementation of theorem proving programs. In 5th International Conference on Automated Deduction, pages 232–249. Springer Verlag, 1980.

[McC92] W. McCune. Experiments with discrimination-tree indexing and path-indexing for term retrieval. Journal of Automated Reasoning, 9(2):147–167, October 1992.

[Ohl90a] H.J. Ohlbach. Abstraction tree indexing for terms. In Proceedings of the 9th European Conference on Artificial Intelligence, pages 479–484. Pitman Publishing, London, August 1990.

[Ohl90b] H.J. Ohlbach. Compilation of recursive two-literal clauses into unification algorithms. In Proc. of AIMSA 1990. Bulgaria, 1990.

[Rob65] J.A. Robinson. A machine–oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, 1965.

[Sti89] M. Stickel. The path–indexing method for indexing terms. Technical Note 473, Artificial Intelligence Center, SRI International, Menlo Park, CA, October 1989.

[Vor94] A. Voronkov. The anatomy of vampire: Implementing bottom–up procedures with code trees. Submitted to Journal of Automated Reasoning, 1994.

[WOL91] L. Wos, R. Overbeek, and E. Lusk. Subsumption, a sometimes undervalued procedure. In J.L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 3–40. MIT Press, Cambridge, Massachusetts,

Index

Symbols COD . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 DOM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 I . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 V . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 V^{∗} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Δ. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .26 Ω . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Σ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 •. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4 del. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .26 ins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 merge . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 mscg^{σ} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 mscg^{t} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .22 search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Subst . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 G . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 I . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 U . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

A abstraction tree indexing. . . . . . . . . . . .2, 6 auxiliary variable . . . . . . . . . . . . . 19, 23, 24

C closed variable . . . . . . . . . . . . . . . . . . . . . . . . 9 codomain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 compatible substitution . . . . . . . . . . . . . . . 3 composition of substitutions . . . . . . . . . . . 4 constant . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

D discrimination tree indexing. . . . . . . . .2, 5 domain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

H heuristic . . . . . . . . . . . . . . . . . . . . . . . . . 19, 25 hyperresolution . . . . . . . . . . . . . . . . . . . . . . 14

I indicator variable . . . . . . . . . . . . . . . . . . . . . 3

J join of substitutions . . . . . . . . . . . . . . . . . . . 4

M

most specific common generalization. .19

N

normalization of substitutions . . . . . . . . . 5 normalization of terms . . . . . . . . . . . . . . . . 4

O

open variable . . . . . . . . . . . . . . . . . . . . . . . . . 9

P

path–indexing . . . . . . . . . . . . . . . . . . . . . . 2, 5 position . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

R

resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

S

substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 substitution tree . . . . . . . . . . . . . . . . . . . . . . 8 subsumption . . . . . . . . . . . . . . . . . . . . . . . . . . 9

T

term . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

U

unifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

V

variant nodes . . . . . . . . . . . . . . . . . . . . . . . . 19

[figure: I N F O R M A T I K]

Below you find a list of the most recent technical reports of the research group Logic of Programming at the Max-Planck-Institut für Informatik. They are available by anonymous ftp from our ftp server ftp.mpi-sb.mpg.de under the directory pub/papers/reports. Most of the reports are also accessible via WWW using the URL http://www.mpi-sb.mpg.de. If you have any questions concerning ftp or WWW access, please contact reports@mpi-sb.mpg.de. Paper copies (which are not necessarily free of charge) can be ordered either by regular mail or by e-mail at the address below.

Max-Planck-Institut für Informatik Library attn. Regina Kraemer Im Stadtwald D-66123 Saarbrücken GERMANY

e-mail: kraemer@mpi-sb.mpg.de

MPI-I-94-246 M. Hanus On Extra Variables in (Equational) Logic Programming

MPI-I-94-241 J. Hopf Genetic Algorithms within the Framework of Evolutionary Computation: Proceedings of the KI-94 Workshop

MPI-I-94-240 P. Madden Recursive Program Optimization Through Inductive Synthesis Proof Transformation

MPI-I-94-239 P. Madden, I. Green A General Technique for Automatically Optimizing Programs Through the Use of Proof Plans

MPI-I-94-238 P. Madden Formal Methods for Automated Program Improvement

MPI-I-94-235 D. A. Plaisted  Ordered Semantic Hyper-Linking
MPI-I-94-234 S. Matthews, A. K. Simpson  Reflection using the derivability conditions

MPI-I-94-233 D. A. Plaisted The Search Efficiency of Theorem Proving Strategies: An Analytical Comparison

MPI-I-94-232 D. A. Plaisted  An Abstract Program Generation Logic
MPI-I-94-230 H. J. Ohlbach  Temporal Logic: Proceedings of the ICTL Workshop
MPI-I-94-229 Y. Dimopoulos  Classical Methods in Nonmonotonic Reasoning

MPI-I-94-228 H. J. Ohlbach Computer Support for the Development and Investigation of Logics

MPI-I-94-226 H. J. Ohlbach, D. Gabbay, D. Plaisted  Killer Transformations

MPI-I-94-225 H. J. Ohlbach Synthesizing Semantics for Extensions of Propositional Logic

MPI-I-94-224 H. Aït-Kaci, M. Hanus, J. J. M. Navarro Integration of Declarative Paradigms: Proceedings of the ICLP’94 Post-Conference Workshop Santa Margherita Ligure, Italy

MPI-I-94-223 D. M. Gabbay LDS – Labelled Deductive Systems: Volume 1 — Foundations

MPI-I-94-218 D. A. Basin  Logic Frameworks for Logic Programs
MPI-I-94-216 P. Barth  Linear 0-1 Inequalities and Extended Clauses
MPI-I-94-209 D. A. Basin, T. Walsh  Termination Orderings for Rippling