A data structure providing an eficient storage and retrieval of logical expressions is a necessary component of every automated reasoning system. Most theorem provers rely on term indexes tuned to unification. Tabled logic programming systems in contrast favour indexes tuned to the retrieval of variants or instances. This article proposes the versatile data structure Instance Trie which supports the unification of queries with stored expressions as well as the retrieval of variants, instances, and generalisations of queries. Instance tries are stable in the sense that their structure is independent of the order in which they are filled or updated. They give rise to an incremental expression retrieval.
Automated reasoning [
This article proposes instance tries primarily developed for tabled logic programming [
The article is structured as follows. Section 1 is this introduction. Section 2 is devoted to related work. Section 3 briefly recalls the concepts referred to, and introduces the notations used in this article. Section 4 describes the structure of an instance trie. Section 5 addresses various data retrieval modes for instance tries. Section 6 concludes the article.
The book [
Tries have been introduced in [
The Path-Indexing Method [
Dynamic Path Indexing [
Extended Path Indexing [
Discrimination Trees [
Deterministic Discrimination Trees [
Adaptive Discrimination Trees [
Abstraction Trees [
Substitution Trees [
Downward Substitution Trees [
Code Trees [
Coded Context Trees [
Tabling [
Dynamic Threaded Sequential Automata (DTSA) [
Time Stamped Tries [
Expressions Instance tries are defined in the following referring to expressions, a generalisation of first-order terms and first-order atomic formulas. 1 Expressions are defined from symbols as follows.
Finitely many non-variable symbols and infinitely many variables are considered. The nonvariable symbols are totally ordered by ≤ and the variables are totally ordered by ≤ .
A constructor is a pair / with a non-variable symbol and one of finitely many arities associated with the symbol .
An expression is either a variable or a non-variable expression. A non-variable expression is either a constructor of arity 0, or it has the form (1, . . . , ) where is a constructor of arity ≥ 1 and 1, . . . , are expressions.
Two expressions are variable-disjoint if none of the variables occurring in the one expression occur in the other.
1, . . ., and are the direct subexpressions of (1, . . . , ).
Observe that no proper prefix of an expression (in standard or prefix form) is an expression and that there are finitely many constructors.
cally [27, pp. 18–19] [28, pp. 88–89]) defined as follows on the variables and constructors from the orders ≤ , ≤ , and the order on the natural numbers: 1The distinction between terms and atomic formulas is irrelevant to storage and retrieval. • 1 < 2 if 1 and 2 are variables and 1 < 2. • < / if is a variable and is a non-variable symbol. • /1 < /2 if is a non-variable symbol and 1 < 2.
• 1/1 < 2/2 if 1 and 2 are non-variable symbols and 1 < 2.
A total order ≤ on expressions is lexicographically derived from the total order ≤ on constructors. Similarly, a total order ≤ on finite sequences of expressions is lexicographically derived from the total order ≤ on expressions.
Prefix notation An expression (1, . . . , ) is in standard notation. This expression can also be written without parentheses in prefix notation (also known as Polish or Łukasiewicz notation) as / 1/1 . . . / where is the arity of expression (1 ≤ ≤ ).
Notations In the following, the lower case letters , , , . . . , with the exception of denote the non-variable symbols and ≤ denotes the standard order on that set; 0, 1, 2, . . . (with subscripts) denote the variables and ≤ the order on variables: ≤ if ≤ . The notation 1, . . . , (with superscripts) denotes arbitrary variables.
Example 1.
• , () and (, ) are expressions in standard notation. Their counterparts in prefix notation are /0, /1 /0 and /2 /0 /0. • 2 and (, (5)) are expressions in standard notation. Their counterparts in prefix notations are 2 and /2 /0 /1 5. • < () < (, ) in standard notation and 2 < /2 /0 /1 5 in prefix notation. • 2 ≤ 5. • [6] < [6, (, ), (, (5))] < [(, ), (, (5))] < [(, (5)), (, )] where [1, 2, . . . , ] denotes the sequence of expressions 1, 2, . . ., and .
Substitutions Let ℰ denote the set of expressions and the set of variables. A substitution2 = {1 ↦→ 1, . . . , ↦→ } with ≥ 0 denotes a total function → ℰ such that • 1, . . . , are pairwise distinct variables, • () = for all = 1, . . . , , and • () = if ̸= for all = 1, . . . , .
The application of a substitution = {1 ↦→ 1, . . . , ↦→ } to an expression is the expression obtained from by simultaneously replacing for all = 1, . . . , every occurrence of each in by . The application of the empty substitution to an expression leaves it unchanged: For all expressions , = . If is an expression and if and are substitutions, then ( ) = ( ) where denotes the composition of and .
2The binding of a variable to an expression is denoted ↦→ because it reminds of the implementation of
variables as pointers. Another widespread notation for the same, used among others in [
Let = {1 ↦→ 1, . . . , ↦→ } be a substitution. The finite set of variables dom( ) = {1, . . . , } is the domain of . The set of variables modified by , that is, variables such that ̸= , map to the range of . The range of a substitution is finite.
A renaming substitution is a substitution which is a permutation of the set of variables.
Substitutions 1 and 2 are compatible if for all ∈ dom( 1) ∩ dom( 2) 1 = 2. If 1 and 2 are compatible substitutions, then 1 ∪ 2 is a well-defined substitution.
pression ′ such that ′ = for some renaming substitution .
An instance of an expression is an expression ′ such that ′ = for some substitution . An instance ′ of is said to match to . A strict instance of an expression is an instance of which is not a variant of .
A generalisation of an expression is an expression such that is an instance of , that is, = for some substitution . A strict generalisation of an expression is a generalisation of which is not a variant of .
A unifier of expressions 1 and 2 is a substitution such that 1 = 2 .
Matching and unification A (first-order syntactic) matching problem , short matching
problem, of an expression 1 in an expression 2 consists in finding substitutions such that
1 = 2 . Thus, a matching problem consists in finding substitutions establishing an instance,
or symmetrically generalisation, relationship between expressions [
A first-order syntactic unification problem , short unification problem , consists in finding uniifers for two expressions.
If the matching (unification, respectively) problem of 1 in 2 (1 and 2, respectively) has
solutions, then it has solutions most general matchers, short mgm, of 1 in 2 (most general
unifiers, short mgu, of 1 and 2), which are [
A matching problem is a strengthening of a unification problem: If 1 = 2 , then is a unifier of 1 and 2. The converse is false: Some solutions to unification problems of 1 and 2 are solutions neither of the matching problem of 1 in 2, nor of the matching problem of 2 in 1. As a consequence, matching problems can be solved with algorithms (called matching algorithms) which might be, in some cases, more eficient than algorithms for the unification problem (called unification algorithms ).
3Matching has also been called filtering , one-sided unification , and semi-unification.
An instance trie is a tree such that: • The root of carries, but does not store, a variable. • Every node of except the root stores an expression. • Every arc 1 → 2 of corresponds to non-renaming substitution such that if is the expression stored at node 1, then the instance of is the expression stored at node 2.
• The children of a node are ordered (in a manner described below).
Since the substitution corresponding to an arc of an instance trie is not a renaming substitution, the expression stored at a child of a node is a strict instance of the expression stored at . Example 2. Abstract depiction of an instance trie storing the expressions (, 1, 1), (, , ), (5, 3, 4, ), and (5, , , ):
v0 p(a,v1,v1) q(v5,v3,v4,c) p(a,b,b) {v0↦→p(a,v1,v1)} {v0↦→q(v5,v3,v4,c)} {v1↦→b} {v3↦→a,v4↦→b} Composing the substitutions along a path from the root to a node yields the expression stored at that node. (5, , , ) is for example obtained by 0{0 ↦→ (5, 3, 4, )}{3 ↦→ , 4 ↦→ }.
Instance tries do not store expressions in standard notation but instead in prefix notation and furthermore using a low-level representation. The following paragraphs successively address the representations of expressions, substitution application, substitutions, and finally instance tries.
Representation of expressions The representation of an expression in the memory of a run-time system is based on the expression’s prefix notation. Assuming that a constructor and a variable are stored in 4 bytes and storage begins at address 0, the representation of (, 1, , 1) is:4 4Recall that , , , . . . , except denote non-variable symbols and 0, 1, 2, . . . denote variables. The leftmost, or first, occurrence of the variable 1 is represented by the value nil which indicates that the variable is unbound. The second occurrence of the variable 1 is represented by an ofset: The address of this second occurrence’s representation, 16, minus the ofset, 8, is the address of the representation of the variable’s first occurrence, 8. Occurrences of (the representation of) a variable like the second occurrence of 1 in (, 1, , 1) and the cell representing such variables like the cell at address 16 in the above representation of (, 1, , 1) are called locally bound variables.
Three properties of an expression representation are worth stressing: 1. The variables’ names are irrelevant to expression representations. If is an expression and is a variable renaming, then and have exactly the same representation.5 For example, the expression (, 1, , 1) is represented exactly like (, 0, , 0) and the expression (5, 3, 4, ) is represented exactly like (0, 1, 3, ). However, this is not the case of the representation of substitution applications: As it is discussed below, (, 1, 2, 3){2 ↦→ , 3 ↦→ 1} is not represented like (, 1, , 1). 2. The representation of an expression is variable-linear, short linear, in the sense that a variable occurs at most once in an expression. Indeed, a non-linear expression (like (, 1, , 1)) is represented as the application of a substitution to a linear expression (like (, 1, , 2){2 ↦→ 1}). 3. In an instance trie, two distinct variables cannot be bound to two distinct expressions in which the same variable occurs. The bindings 1 ↦→ (3) and 2 ↦→ (3) for example cannot occur in an instance tree. In an instance trie, such bindings would be expressed for example as 1 ↦→ (3) and 2 ↦→ (4), 4 ↦→ 3.
Thus, expressions can be ordered as if their variables were, in the order of their first occurrence,
0, 1, 2, . . ., that is, as if they were standardized [
This representation of (, 1, , 1) given above is abstract in the sense that it is a simplification. Its implementation in the heap of a run-time system, that is, the concrete representation, difers from the abstract representation as follows: • A next-representation address is added at the beginning of a (connected) expression representation so as to ease garbage collecting (but not at the beginning of each subexpression). • Instead of cells, tokens are considered, each of which consists of one or several consecutive cells. • A three-valued flag at the beginning of every token indicates the type of its content:
Non-variable symbol, non-locally bound variable, or locally bound variable. • The token for a constructor / consists of three successive memory cells, the first of which contains the afore-mentioned type flag, the second the code of the symbol , and the third the arity .
5As a consequence, expressions can be considered standardized [
Assuming that there is no additional information, that and are represented by their ASCII codes 112 and 97 respectively, and that nil is represented as 9999997, the type flag takes the values 0, 1, and 2, and using decimal instead of binary numbers for better readability, the concrete representation of (, 1, 1) is as follows: 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
is stored at address 0 and the expression (, 3) at address 23, the substitution application (, 1, 1){1 ↦→ (, 3)} is represented as follows: Thus, binding a variable (like 1) to an expression (like (, 3)) is realised by storing the expression’s address (23) at the variable’s address (cell 8). Observe that the cell representing the second occurrence of the variable 1 (cell 12) keeps its ofset (4) unchanged. Thus, binding a variable which occurs in an expression to an expression ′ consists in storing at the leftmost occurrence of in the representation of the address of the representation of ′, leaving unchanged further occurrences of in the representation of . This approach to binding variables ensures that the representation of a substitution application is unique. Representation of substitutions In an instance trie, a substitution is applied at a node to the expression representation stored at the parent node of . The substitution’s domain consists of all variables with value nil, that is, the non-locally bound variables, of . Consider for example the arc : (5, 3, 4, ) → : (5, , , ) or, in a more faithful depiction, : {0 ↦→ (5, 3, 4, )} → : {3 ↦→ , 4 ↦→ }, of Example 3. The substitution {3 ↦→ , 4 ↦→ } is represented by two lists: • The sequence of addresses of nil variables (that is, non-locally bound variables) in the expression (5, 3, 4, ) at the parent node (in their order of occurrence): [5, 3, 4] • The sequence of the values assigned to each of these variables yielding the expression (5, , , ) at the child node : [, , ] 6Time stamps are needed by logic programming run-time systems for semi-naïve forward chaining and for tabling.
7nil can be represented by any other value outside the heap’s address space.
More generally, a substitution {1 ↦→ 1, . . . , ↦→ } at a node is represented by two lists: • The sequence of addresses of nil variables (that is, non-locally bound variables) in the expression representation at the parent node of . • The sequence of the expressions or variable addresses8 assigned to each of these variables at the child node .
• no variables occur in both lists since, as the expressions of second list are created, their variables are represented by so far unused memory cells, • the first list does not contain any variable which does not occur in the expression at the parent node.
Representation of instance tries The following example illustrates the representation of substitutions in an instance trie.
Example 3. Abstract depiction of an instance trie storing expressions (5, 3, 4, ), (5, , , ), (, 1, 1, 2), and (, , , ): Faithful depiction of the same instance trie with an abstract representation of substitutions: [] [v0] [f(a,v1,v1,v2)] [v1,v2] [q(v5,v3,v4,c)] [v5,v3,v4] [b,c] []
A substitution {1 ↦→ 1, . . . , ↦→ } at a node is represented by the expression sequence [1, . . . , ] for the variables [1, . . . , ] in the parent node’s variable sequence.
8Which turn nil variables in the parent node’s expression into locally bound variables in the child node’s expression. Faithful depiction of the same instance trie with a standard representation of substitutions: v0 v0 f(a,v1,v1,v2) q(v5,v3,v4,c) f(a,b,b,c) {v0↦→f(a,v1,v1,v2)} {v0↦→q(v5,v3,v4,c)} {v1↦→b,v2↦→c} {v3↦→a,v4↦→b} The children of a node are ordered after their expression sequences. For all expressions , ≤ , reflecting that as variable precedes every expression. The order on unbound variables is reflected by the positions of nil in expression sequences. The root of an instance trie has an empty expression sequence because it has no parent node. A node with an empty variable sequence [] (like the leftmost leaf in the above example) cannot have any children what reflects that the expression stored at such a node has no strict instance. The node of an instance trie carries two sequences: • A sequence of expressions or nil representing the bindings of its parent node’s variable. • The sequence of the addresses of the nil variables occurring in the node’s expression. The representations of the two kinds of sequences is as follows: • The first sequence, the sequence of variable bindings, is a sequence of representations of expressions. Since representations of expressions have variable lengths, the sequence is represented as a linked list. • The second sequence, the sequence of nil variables, is a sequence of representation of variables, that is, of addresses of memory cells representing variables. Since such cells all have the same length, the sequence can be represented as a memory block beginning with the number of variable addresses stored in the block.
In addition to the afore-mentioned two lists, the representation of the node of an instance tree includes a data structure storing, and giving a fast access to, the addresses of the children of . If this number is small, a linked list can be used. Otherwise, a binary tree, or a B-tree is convenient.
The expression stored at a node of an instance trie is obtained by successively applying to
the instance trie’s root variable the substitutions along the path from the root to . Because
of this, instance tries are a kind of substitution-based tries or substitution tree in [
Let be a query, that is, an expression to be evaluated against the expressions stored in an instance trie . Four query modes are considered:
2. Instance: Which expressions stored in are (strict) instances of ? 9Substitution-based tries are not expression-based tries because an expression stored at a child of a node is not a strict prefix of the expression stored at . Indeed, no strict prefix of an expression is an expression. 3. Generalisation: Which expressions stored in are (strict) generalisations of ? 4. Unification: With which expressions stored in does unify?
All four query modes are realized by both, a traversal of the instance trie and a test at each node whether that node’s expression is an answer to the query.
Dereferencing The tests are defined below referring to dereferenced representations of expressions.10 Consider the following two representations of (, 1, 2, 1, (1)): The first representations of (, 1, 2, 1, (1)) is dereferenced because, except for the representations of the second and third occurrences of the variable 1, the variables’ values are nil. The second and third occurrences of 1 cannot be dereferenced like a pointer, because this would result in the following representation of (, 1, 2, 3, (4)), not of (, 1, 2, 1, (1)): A dereferenced representation of an expression is generated from any representation of as follows: While traversing from left to right: • If the cell reached contains a constructor or nil, or the ofset of a locally bound variable, then copy its content to a new cell. • Otherwise (the token reached is a non-locally bound variable storing the address of an expression representation), (recursively) dereference the expression representation at address .
We assume that when an expression representation is dereferenced, the list of the addresses of its nil variables (that is, non-locally bound variables) is constructed. Constructing this list can be done while dereferencing the expression representation, that is, it does not require an additional traversal of the expression representation.
In implementing the algorithm sketch above, care must be given not to trespass expression representations’ ends in recursive calls. This is easily cared for in the same traversal of expression representations by using as follows the constructors’ arities during a left-to-right traversal of an expression representation :
Let denote the number of remaining (sub)expression representations; set := 1 before traversing , at each constructor / perform the update := − 1 + (− 1 for the (sub)expression beginning at that constructor and + for the subexpression representations 10Dereferencing a pointer means determining the value points to. now to be traversed), and at each variable perform the update := − 1. The expression representation’s end is reached when = 0.
Since dereferencing an expression copies that expression, dereferencing expressions comes at a cost. This cost is acceptable, though. Indeed, dereferencing speeds up the tests which anyway require to copy the stored expressions they are performed against because they bind variables. Binding variables directly in an instance trie would destroy it.11 Representation of a stored expression An expression stored at a node of an instance trie retrieved for comparison with a query has the form = ′ where ′ is the expression stored at the parent node of and is a non-renaming substitution, that is, is a strict instance of ′. As discussed in the previous paragraph, (the representation of) ′ is assumed to be dereferenced. Furthermore, and ′ as well as and are variable-disjoint.
The substitution is represented as described in Section 4, paragraph “Representation of substitutions” by two lists: A list of variables and a list of expressions or nil. It is also assumed that (the representation of) the expressions in that second list are dereferenced.
Useful information on ′, the nature of which depends on the query mode, can be assumed to be known: • If variants or instances of are searched for, then ′ is a strict generalisation of (or, equivalently, is a strict instance of ′). Indeed, otherwise the strict instance = ′ of ′ cannot be a variant or an instance of and the search through , which is described below, would not have led to . • If generalisations of are searched for, then ′ is already a generalisation of . Indeed, otherwise, the strict instance = ′ of which ′ is a strict generalisation cannot be a generalisation of and the search through , which is described below, woulds not have led to . • If expressions unifying with are searched for, then and ′ unify. Indeed, if and = ′ unify, then there exists a substitution such that = = ′ . Since the representations of and ′ are variable disjoint and the domain of the representation of contains only variables occurring in ′, = . Therefore = = ′ . That is, is as unifier of and ′. Thus, if and ′ do not unify, then and = ′ cannot unify, and the search through , which is described below, would not have led to . Retrieval Both a query and an expression stored in an instance tree at a node tested as a possible answer to are available as strict instances of the expression ′ stored at the parent node of . Indeed, by definition of an instance trie, is stored in that form, and during the instance tree traversal has been recognised as a strict instance of ′ for otherwise, and would not be compared.
Assume that = ′ and = ′ and recall that each of the representations of and is a list consisting of dereferenced expression representation, where is the number of nil variables in the representation of ′. The matching problems of in and of in therefore reduce to matching problems of these two lists:
11Copying the representation of the query is not necessary because, by using a log, bindings of query variables can be undone before the query is tested against another stored expression. • If the expressions in the list representing and are pairwise variant of each other, then and are variant of each other. • If every expression in the list representing is an instance of its counterpart in the list representing , then is an instance of , and if furthermore at least one of these expressions is a strict instance of its counterpart, then is a strict instance of . • If every expression in the list representing is a generalisation of its counterpart in the list representing , then is a generalisation of , and if furthermore at least one of these expressions is a strict generalisation of its counterpart, then is a strict generalisation of .
• If the lists representing and unify, then and unify.
Versatile unification algorithm Instance tries make use of a unification algorithm which determines in a single left-to-right traversal of dereferenced expression representations 1 and 2 whether the represented expressions 1 respectively 2 are variants of each other, or 1 is a strict instance of 2, or 1 is a strict generalisation of 2, or none of this hold but 1 and 2 are unifiable, or finally 1 and 2 are not unifiable. This algorithm is called “versatile” because it is both a matching and a unification algorithm and because it further qualifies how matching expressions do match.
This unification algorithm exploits the afore-mentioned representation of expressions in an instance trie for avoiding unnecessary occurs-checks in some cases: • on some ofset variables under certain conditions • as long as the left-to-right expression traversal is still in a matching mode (that is, one of variant, strict instance, or strict generalisation)
A description of this unification algorithm is beyond the scope of this paper and is given
in [
Traversal A left-to-right depth-first traversal of an instance trie is, like for any tree structure, the algorithm of choice, because it has a simple recursive definition and minimizes the space complexity. All query modes but the query mode Unification afect that traversal: • Variant: The traversal can be interrupted as soon as an answer is found because an instance tree does not contain distinct variant expressions. • Instance: Subtrees rooted at instances of the query do not have to be traversed because all expressions they store necessarily are answers to the query. • Generalisation: In a depth-first traversal of an instance tree, the first expression found which generalises and no children of which also generalise determines the answers to : Their set consists of and its ancestors (except the instance trie’s root). The subtree rooted at such a node is not traversed. Insertion and deletion The insertion of an expression in an instance trie is realised by ifrst searching with the matching algorithm mentioned above for a strict generalisation of in , which is always found because the root of an instance trie is a strict generalisation of every expression, second checking whether a child of is a instance of . If a child of is a variant of , then nothing is done. If a child of is a strict instance of , then is inserted between and (what requires no more than updating two pointers). Otherwise, is inserted in the instance trie as an as a new child of .
In order to maintain tree invariants (instances of an expression are always inserted below their first generalization in a tree), children of to the right of need to be searched for instances of and inserted below recursively.
The deletion of an expression from an instance trie is realised by searching with the matching algorithm mentioned above for a variant of in . If such a variant is found at a node , then this node is deleted (what requires no more than updating a pointer) and, after this deletion, each expression stored at children node of is inserted in the subtree rooted at the node which, before the deletion, was the parent node of . Otherwise nothing is done.
This article has introduced the data structure Instance Trie salient properties of which are: • Stability: Instance tries are stable in the sense that their structures are independent of the order in which they are filled or updated. • Versatility: Instance tries are versatile in the sense that they are well-suited to the retrieval of stored expressions in four query, or retrieval, modes: Variants, instances, generalisations and unification of expressions. • Incrementality: Instance tries’ storage based on the instance relationship gives rise to an incremental expression retrieval.
The companion article [