A Method for Implementing Equational Theories as Logic Programs
M. H. M. Cheng, D. Scott Parker, M. H. van Emden · The MIT Press eBooks · 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 by means of a limited class of logic programs. We define regular equational theories, a useful class of theories, and show how our method can be used in obtaining efficient implementations for them. The programs obtained by our method have several advantages. Although executable, they maintain separation of concerns between specification and implementation. Prolog executes them efficiently. In addition, they permit interesting compilation and optimization techniques that can improve execution efficiency still further. Finally, the method offers perspectives on term rewriting and functional programming evaluation strategies, how such strategies can be compiled, and how they can be integrated effectively with logic programming. 1 Introduction Every scient...