Unification Factoring for Efficient Evaluation of Logic Programs

Click on the title to obtain a gzip-ed PostScript version of the paper (86K).

Abstract:

The efficiency of resolution-based logic programming languages, such as Prolog, depends critically on selecting and executing sets of applicable clause heads to resolve against subgoals. Traditional approaches to this problem have focused on using indexing to determine the smallest possible applicable set. Despite their usefulness, these approaches ignore the non-determinism inherent in many programming languages to the extent that they do not attempt to optimize execution after the applicable set has been determined.

Unification factoring seeks to rectify this omission by regarding the indexing and unification phases of clause resolution as a single process. This paper formalizes that process through the construction of factoring automata. A polynomial-time algorithm is given for constructing optimal factoring automata which preserve the clause selection strategy of Prolog. More generally, when the clause selection strategy is not fixed, constructing such an optimal automaton is shown to be NP-complete, solving an open trie minimization problem.

Unification factoring is implemented through a source code transformation that preserves the full semantics of Prolog. This transformation is specified in the paper, and using it, several well-known programs show performance improvements of up to 100% across three different systems.