Run-time and compile-time improvements to equational programs
David James Sherman · 1994
This thesis shows how to use compile-time transformations and run-time caching of congruence information to improve the running time of equational logic programs. We base our work on the term-rewriting implementation of equational logic programming of Christoph Hoffmann and Michael O'Donnell, the definition of directed congruence closure by Paul Chew, and the compiler for forward-branching sets of equations developed by Robert Strandh. Our first two contributions provide frameworks for reasoning about and implementing term-rewriting systems for equational logic. The first is a definition of a logical representation of the state of a rewriting system, capturing existing notions of addressable memory and associative memoization tables. The second is the developement of an abstract pattern-matching machine for term rewriting, offering an assembly language EM code that is amenable to semantics-based analysis, compilation, and optimization. We present a standard optimizing compiler for EM code, appropriately extended to implement the logic tables and all of their transformations. Our third contribution is the definition of analyses and transformations for performing compile-time partial evaluation of EM code programs. We present an implementation of our partial evaluator that removes significant inefficiencies in EM code programs used for equational logic programming. Our partial evaluator uses a novel unfolding strategy driven by node construction that is particularly adapted to term-rewriting. Our fourth contribution is the definition and implementation of run-time improvements based on congruence. Such improvements discover term equivalencies during execution, and can lead to exponential savings in running time. Using our logic representation, we define and characterize four congruence-based methods, and prove that their separations are supralinear. Using our EM code compiler, we implement the three most practical of these methods, and experimentally demonstrate their separations.