Proof-Theoretic Foundation of Compilation in Logic Programming Languages

Commercial implementations of logic programming languages are engineered Appeared in the Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming --- JICSLP'98 (J. Jaffar editor), pp ??--??, MIT Press, Manchester, UK, 16--19 June 1998. around a compiler based on Warren's Abstract Machine (WAM) or a variant of it. In spite of various correctness proofs, the logical machinery relating the proof-theoretic specification of a logic programming language and its compiled form is still poorly understood. In this paper, we propose a logicindependent definition of compilation for logic programming languages. We apply this methodology to derive the first cut of a compiler and the corresponding abstract machine for the language of hereditary Harrop formulas and then for its linear refinement. 1 Introduction Compiled logic programs run over an order of magnitude faster than their interpreted source and constitute therefore a key step to combining the advantages of..