Towards Pre-Indexed Terms

ABSTRACT. Indexing of terms and clauses is a well-known technique used in Prolog implementations, as well as automated theorem provers, to speed up search. In this paper we show how the same mechanism can be used to implement efficient reversible mappings between term representations (which we will call pre-indexing). Based on user-provided term descriptions, this mapping allows us to use cheap data encodings internally (such as prefix trees). We found that for some classes of programs we can drastically improve the efficiency by carefully selecting the application of the mapping at specific program points.