An Improved Proof-Theoretic Compilation of Logic Programs

TL;DR

This paper refines proof-theoretic compilation methods for logic programming, removing unnecessary abstractions and enhancing efficiency for well-moded programs, thereby advancing the theoretical foundation and practical implementation of logic program compilation.

Contribution

It provides a more detailed logical justification for proof-theoretic compilation and introduces improvements for efficiently handling well-moded programs.

Findings

Eliminates spurious second-order abstractions in compilation

Provides a fully logical justification for previous techniques

Enhances efficiency for well-moded logic programs

Abstract

In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their linear variant. Compiled clauses were themselves logic formulas except for the presence of a second-order abstraction over the atomic goals matching their head. In this paper, we revisit our previous results into a more detailed and fully logical justification that does away with this spurious abstraction. We then refine the resulting technique to support well-moded programs efficiently.