Mantis H.M. Cheng, Maarten van Emden, D. Stott Parker
appeared in: Proceedings of the Intnl. Conf. on Logic Programming, Tokyo, MIT Press, June 1995.
Equational theories underly many fields of computing, including functional programming, symbolic algebra, theorem proving, term rewriting and constraint solving. In this paper we show a method for implementing many equational theories with a limited class of logic programs. We define regular equational theories, a useful class of theories, and illustrate with a number of examples how our method can be used in obtaining efficient implementations for them.The significance of our method is that:
- It is simple and easy to apply.
- Although executable, it supports separation of concerns between specification and implementation.
- Its class of logic programs execute with impressive efficiency using Prolog.
- It permits interesting compilation and optimization techniques that can improve execution efficiency still further.
- It offers perspectives on term rewriting and functional programming evaluation strategies, how they can be compiled, and how they can be integrated with logic programming effectively.
D. Stott Parker, Mantis H.M. Cheng, Maarten van Emden
Term rewriting is basic to a number of programming methods, including functional programming, symbolic mathematics, theorem proving, and constraint normalization. In this paper we approach term rewriting in the spirit of Stickel's Prolog Technology Theorem Prover (PTTP): to exploit the combination of high level programming and efficient implementation provided by Prolog.We show that there is an elegant and simple way to exploit Prolog technology in implementing term rewriting systems. The method is very flexible, permitting us to vary the rewriting strategy (from outermost to innermost to ad hoc), kinds of unification (reduction, narrowing, or higher-order rewriting), and the compilation techniques used (from partial evaluation to surgery on the underlying rewrite engine, which is specified in terms of axioms of equality). In this approach, innermost and outermost reduction, as well as many combinations of these, are obtained by merely rearranging the clauses that express equality axioms.
The approach also gives new perspective on Stickel's PTTP. In particular, using the approach we show how to declaratively reconstruct Stickel's PTTP system (a sizeable compiler) as an interpreter, in a way that permits essentially the same compiler to be obtained by partial evaluation. Also (and as a consequence), we show how PTTP can be extended from just a resolution theorem proving system to handle equational theorem proving as well.
Like Prolog, the strength of our approach lies in its interesting compromises between purity, flexibility, and performance. First, the simplicity of the method and its logical foundations permit reconsideration and reconstruction of term rewriting techniques. Second, its flexibility permits a wide variety of term rewriting methods to be implemented simultaneously (and be executed simultaneously). Third, although the method will not give the fastest possible implementation, it gives surprisingly good peformance.
Mantis H.M. Cheng, D. Stott Parker, Maarten van Emden
appeared in: Proceedings of the Intnl. Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA'93), 23rd-24th September 1993, CWI, Amsterdam, The Netherlands.
We explore Applicative Term Rewriting Systems, first-order term-rewriting systems that axiomatize function application. These systems are similar in flavor to Klop's higher order combinatory reduction systems, but involve only first-order terms.Applicative term-rewriting systems have several aspects that are interesting to us. First, they are simple, and their rules can be integrated directly with declarative, first-order axiomatizations of the equality relation. Second, they are easily implemented with Prolog, thereby making a basis for a Prolog Technology Term Rewriter in the sense of Stickel's ``Prolog Technology Theorem Prover'', and providing both easy implementation and efficient execution. Third, they permit specification of computationally useful fragments of higher order equality theories, by allowing selective omission of equality axioms. Finally, in this approach innermost and outermost reduction, as well as many combinations of these, are obtained by merely rearranging the clauses that express equality axioms.
A number of higher order term rewriting systems proposed recently rely on simplified lambda-term unification algorithms, implementing fragments of equality theories for lambda-terms. Our approach provides both a way to implement such schemes, and an alternative equality theory when the fragment required is limited (as is often the case).