Abstract
In this paper we consider the problem of extending Prolog to include predicate and function variables and typed λ-terms. For this purpose, we use a higher-order logic to describe a generalization to first-order Horn clauses. We show that this extension possesses certain desirable computational properties. Specifically, we show that the familiar operational and least fixpoint semantics can be given to these clauses. A language, λProlog that is based on this generalization is then presented, and several examples of its use are provided. We also discuss an interpreter for this language in which new sources of branching and backtracking must be accommodated. An experimental interpreter has been constructed for the language, and all the examples in this paper have been tested using it.
This work has been supported by NSF grants MCS8219196-CER, MCS-82-07294, AI Center grants NSF-MCS-83-05221, US Army Research office grant ARO-DAA29-84-9-0027, and DARPA N000-14-85-K-0018.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Section 7: References
Krzysztof R. Apt and M. H. van Emden, “Contributions to the Theory of Logic Programming” JACM, Vol 29 (1982), 841–862.
Alonzo Church, “A Formulation of the Simple Theory of Types,” Journal of Symbolic Logic 5 (1940), 56–68.
Steven Fortune, Daniel Leivant, and Michael O'Donnell, “The Expressiveness of Simple and Second-Order Type Structures”, J.ACM Vol. 30(1), January 1983, pp. 151–185.
Warren D. Goldfarb, “The Undecidability of the Second-Order Unification Problem,” Theoretical Computer Science 13 (1981), 225–230.
Gérard P. Huet, “A Unification Algorithm for Typed λ-calculus,” Theoretical Computer Science 1 (1975), 27–57.
Gérard P. Huet, Bernard Lang, “Proving and Applying Program Transformations Expressed with Second-Order Patterns” Acta Informatica 11 (1978), 31–55.
Dale A. Miller, “Proofs in Higher-order Logic,” Ph. D. Dissertation, Carnegie-Mellon University, August 1983.
Dale A. Miller, “A Theory of Modules for Logic Programming,” University of Pennsylvania Technical Report, 1986.
Dale A. Miller, Gopalan Nadathur, “A Computational Logic Approach to Syntax and Semantics,” 10th Annual Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985.
Dale A. Miller, Gopalan Nadathur, “An Abstract Interpreter for a Higher Order Extension of Prolog,” forthcoming UPenn technical report, December 1985.
Robin Milner, “A Theory of Type Polymorphism in Programming,” Journal of Computer and System Sciences 17, 348–375, 1978.
A. Mycroft and R. A. O'Keefe, “A Polymorphic Type System for Prolog,” Artificial Intelligence, Vol. 23(3), August 1984.
J. C. Reynolds, “Three Approaches to Type Structure”, Proceedings of the International Joint Conference on Theory and Practice of Software Development, March 1985.
M. H. van Emden, R. A. Kowalski, “The semantics of predicate logic as a programming language,” J.ACM 23 4 (Oct. 1976), 733–742.
D. H. D. Warren, “Higher-order extension to PROLOG: are they needed?”, Machine Intelligence 10, 1982, pp. 441–454.
David Scott Warren, “Using λ-Calculus to Repressent Meaning in Logic Grammars” in the Proceedings of the 21st Annual Meeting of the Association for Computational Linguistics, June 1983, 51–56.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miller, D.A., Nadathur, G. (1986). Higher-order logic programming. In: Shapiro, E. (eds) Third International Conference on Logic Programming. ICLP 1986. Lecture Notes in Computer Science, vol 225. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16492-8_94
Download citation
DOI: https://doi.org/10.1007/3-540-16492-8_94
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16492-0
Online ISBN: 978-3-540-39831-8
eBook Packages: Springer Book Archive