Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-20T09:28:13.275Z Has data issue: false hasContentIssue false
  • English
  • Français

An Improved Proof-Theoretic Compilation of Logic Programs

Published online by Cambridge University Press:  05 September 2012

ILIANO CERVESATO
ILIANO CERVESATO*
Affiliation:
Department of Computer Science, Carnegie Mellon University (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

CompilationAbstract Logic ProgrammingHereditary Harrop FormulasWell-Moded Logic Programs
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 12 , Issue 4-5: 28th International Conference on Logic Programming , July 2012 , pp. 639 - 657
Copyright
Copyright © Cambridge University Press 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aït-Kaci, H. 1991. Warren's Abstract Machine: a Tutorial Reconstruction. MIT Press.CrossRefGoogle Scholar
Börger, E. and Rosenzweig, D. 1995. The WAM — definition and compiler correctness. In Logic Programming: Formal Methods and Practical Applications, Beierle, C. and Pluemer, L., Eds. Computer Science and Artificial Intelligence, vol. 11. North-Holland, 21–90.Google Scholar
Cervesato, I. 1998. Proof-Theoretic Foundation of Compilation in Logic Programming Languages. In 1998 Joint International Conference and Symposium on Logic Programming — JICSLP'98, Jaffar, J., Ed. MIT Press, Manchester, UK, 115–129.Google Scholar
Cervesato, I. and Pfenning, F. 2002. A Linear Logical Framework. Information & Computation 179, 1, 19–75.CrossRefGoogle Scholar
Cervesato, I., Pfenning, F., Walker, D. and Watkins, K. 2003. A Concurrent Logical Framework II: Examples and Applications. Technical Report CMU-CS-02-102, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA. March 2002, revised May.CrossRefGoogle Scholar
Debray, S. K. and Warren, D. S. 1988. Automatic mode inference for logic programs. Journal of Logic Programming 5, 207–229.Google Scholar
Hodas, J. S. and Miller, D. 1994. Logic programming in a fragment of intuitionistic linear logic. Information and Computation 110, 2, 327–365.CrossRefGoogle Scholar
Jaffar, J., Michaylov, S., Stuckey, P. and Yap, R. 1992. An abstract machine for CLP(ℛ). In Proceedings of the SIGPLAN'92 Conference on Programming Language Design and Implementation — PLDI'92. San Francisco, CA.Google Scholar
Miller, D. and Nadathur, G. 1986. Higher-order logic programming. In Proceedings of the Third International Logic Programming Conference, Shapiro, E., Ed. London, 448–462.CrossRefGoogle Scholar
Miller, D., Nadathur, G., Pfenning, F. and Scedrov, A. 1991. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157.CrossRefGoogle Scholar
Nadathur, G. and Mitchell, D. J. 1999. System description: Teyjus — a compiler and abstract machine based implementation of lambda prolog. In Sixteenth Conference on Automated Deduction (CADE'99), Ganzinger, H., Ed. 287–291.Google Scholar
Pfenning, F. and Schürmann, C. 1999. System Description: Twelf — A Meta-Logical Framework for Deductive Systems. In Proceedings of the 16th International Conference on Automated Deduction — CADE-16. Springer-Verlag LNAI 1632, Trento, Italy, 202–206.CrossRefGoogle Scholar
Pientka, B. 2003. Tabled higher-order logic programming. Ph.D. thesis, Department of Computer Science, Carnegie Mellon University.Google Scholar
Russinoff, D. M. 1992. A verified Prolog compiler for the Warren abstract machine. Journal of Logic Programming 13, 367–412.Google Scholar
Sarnat, J. 2010. Syntactic finitism in the metatheory of programming languages. Ph.D. thesis, Department of Computer Science, Yale University.Google Scholar
Stirling, C. 2009. Decidability of higher-order matching. Logical Methods in Computer Science 5, 3.Google Scholar
Warren, D. H. D. 1983. An abstract Prolog instruction set. Technical Note 309, SRI International, Menlo Park, CA. Oct.Google Scholar
Watkins, K., Cervesato, I., Pfenning, F. and Walker, D. 2003. A Concurrent Logical Framework I: Judgments and Properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA. March 2002, revised May.Google Scholar