# Term indexing

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Term_indexing
> Markdown URL: https://mediated.wiki/source/Term_indexing.md
> Source: https://en.wikipedia.org/wiki/Term_indexing
> Source revision: 1327487052
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

In [computer science](/source/computer_science), a '''term index''' is a [data structure](/source/data_structure) to facilitate fast lookup of terms and [clauses](/source/Clause_(logic)) in a [logic program](/source/logic_programming),<ref>{{Cite journal | doi = 10.1016/0743-1066(91)90004-9| title = Enhancing unification in PROLOG through clause indexing| journal = The Journal of Logic Programming| volume = 10| pages = 23–44| year = 1991| last1 = Colomb | first1 = Robert M. | doi-access = }}</ref> [deductive database](/source/deductive_database), or [automated theorem prover](/source/automated_theorem_prover).

== Overview ==
Many operations in automatic theorem provers require search in huge collections of terms and clauses. Such operations typically fall into the following scheme. Given a collection <math>S</math> of terms (clauses) and a query term (clause) <math>q</math>, find in <math>S</math> some/all terms <math>t</math> related to <math>q</math> according to a certain retrieval condition. Most interesting retrieval conditions are formulated as existence of a substitution that relates in a special way the query and the retrieved objects <math>t</math>. Here is a list of retrieval conditions frequently used in provers:

* term <math>q</math> is unifiable with term <math>t</math>, i.e., there exists a substitution <math> \theta </math>, such that <math>q\theta</math> = <math>t\theta</math>
* term <math>t</math> is an instance of <math>q</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>q\theta</math> = <math>t</math>
* term <math>t</math> is a generalisation of <math>q</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>q</math> = <math>t\theta</math>
* clause <math>q</math> [θ-subsumes](/source/Theta-subsumption) clause <math>t</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>q\theta</math> is a subset/submultiset of <math>t</math>
* clause <math>q</math> is [θ-subsumed](/source/Theta-subsumption) by <math>t</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>t\theta</math> is a subset/submultiset of <math>q</math>
 
More often than not, we are actually interested in finding the appropriate 
substitutions explicitly, together with the retrieved terms <math>t</math>,
rather than just in establishing existence of such substitutions. 

Very often the sizes of term sets to be searched are large, 
the retrieval calls are frequent and the retrieval condition test
is rather complex. In such situations [linear search](/source/linear_search) in <math>S</math>, when the retrieval
condition is tested on every term from <math>S</math>, becomes prohibitively costly. 
To overcome this problem, special data structures, called ''indexes'', are 
designed in order to support fast retrieval. Such data structures, 
together with the accompanying algorithms for index maintenance
and retrieval, are called ''term indexing techniques''.

== Classic indexing techniques ==

* [discrimination tree](/source/discrimination_tree)s
* [substitution tree](/source/substitution_tree)s
* [path indexing](/source/path_indexing)

Substitution trees outperform path indexing, discrimination tree indexing, and abstraction trees.<ref>
Peter Graf.
[http://pubman.mpdl.mpg.de/pubman/item/escidoc:1834191:2/component/escidoc:1857890/MPI-I-94-251.pdf "Substitution Tree Indexing"].
1994.
</ref>

A discrimination tree term index stores its information in a [trie](/source/trie) data structure.<ref>
John W. Wheeler; Guarionex Jordan.
[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.1789&rep=rep1&type=pdf "An Empirical Study of Term Indexing in the Darwin Implementation of the Model Evolution Calculus"].
2004.
p. 5.
</ref>

== Indexing techniques used in logic programming ==
First-argument indexing is the most common strategy where the first argument is used as index. It distinguishes atomic values and the principal [functor](/source/functor) of compound terms.

Nonfirst argument indexing is a variation of first-argument indexing that uses the same or similar techniques as first-argument indexing on one or more alternative arguments. For instance, if a predicate call uses variables for the first argument, the system may choose to use the second argument as the index instead.

Multiargument indexing creates a combined index over multiple instantiated arguments if there is not a sufficiently selective single argument index.

Deep indexing is used when multiple clauses use the same principal functor for some argument. It recursively uses the same or similar indexing techniques on the arguments of the compound terms.

[Trie](/source/Trie) indexing uses a prefix tree to find applicable clauses.<ref>{{Cite journal |last=Körner |first=Philipp |last2=Leuschel |first2=Michael |last3=Barbosa |first3=João |last4=Costa |first4=Vítor Santos |last5=Dahl |first5=Verónica |last6=Hermenegildo |first6=Manuel V. |last7=Morales |first7=Jose F. |last8=Wielemaker |first8=Jan |last9=Diaz |first9=Daniel |last10=Abreu |first10=Salvador |last11=Ciatto |first11=Giovanni |date=2022|title=Fifty Years of Prolog and Beyond |url=https://www.cambridge.org/core/product/identifier/S1471068422000102/type/journal_article |journal=Theory and Practice of Logic Programming |language=en |volume=22 |issue=6 |pages=776–858 |doi=10.1017/S1471068422000102 |issn=1471-0684|hdl=10174/33387 |hdl-access=free }}{{Creative Commons text attribution notice|from this source=yes|cc=by4}}</ref>

==References==
{{reflist}}

==Further reading==
* P. Graf, Term Indexing, Lecture Notes in Computer Science 1053, 1996 (slightly outdated overview)
* R. Sekar and I.V. Ramakrishnan and A. Voronkov, Term Indexing, in A. Robinson and A. Voronkov, editors, [Handbook of Automated Reasoning](/source/Handbook_of_Automated_Reasoning), volume 2, 2001 (recent overview)
* W. W. McCune, Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval, Journal of Automated Reasoning, 9(2), 1992
* P. Graf, Substitution Tree Indexing, Proc. of RTA, Lecture Notes in Computer Science 914, 1995
* M. Stickel, The Path Indexing Method for Indexing Terms, Tech. Rep. 473, [Artificial Intelligence Center](/source/Artificial_Intelligence_Center), [SRI International](/source/SRI_International), 1989
* S. Schulz, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Proc. of IJCAR-2004 workshop ESFOR, 2004
* A. Riazanov and A. Voronkov, Partially Adaptive Code Trees, Proc. JELIA, Lecture Notes in Artificial Intelligence 1919, 2000
* H. Ganzinger and R. Nieuwenhuis and P. Nivela, Fast Term Indexing with Coded Context Trees, Journal of Automated Reasoning, 32(2), 2004
* A. Riazanov and A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199(1–2), 2005

Category:Data structures
Category:Logic programming
Category:Theorem proving software systems

---
Adapted from the Wikipedia article [Term indexing](https://en.wikipedia.org/wiki/Term_indexing) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Term_indexing?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.