Abstract
Higher-order logic is known to be a good basis for meta-programming languages. Dale Miller's L λ is such a higher-order logic programming language, for which an interpreter extending the SLD-resolution used in Prolog has been provided.
No alternative to SLD-resolution is known however, and in particular no Bottom-Up strategy has been developed. Such a strategy would be interesting in domains such as natural language, databases, or software engineering. We present here a restriction of L λ, which we call L λ, providing λ-abstraction, quantification and function variables, and for which we prove it possible to define a very simple semi-naÏve Bottom-Up interpreter.
This work was partially supported by a grant from a European Software Factory (ESF) project.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
F. Bancilhon and R. Ramakrishnan. An amateur's introduction to recursive query processing strategies. In SIGMOD, invited paper, 1986.
F. Bancilhon and R. Ramakrishnan. Performance Evaluation of Data Intensive Logic Programs. Morgan Kaufman, 1988.
Jay Earley. An efficient context-free parsing algorithm. Communications A.C.M., 13(2):92–102, February 1970.
Amy Felty. Specifying theorem provers in a higher-order logic programming language. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction. Springer Verlag, May 1988.
Gérard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order logic. Acta Informatica, 11:31–55, 1978.
Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
Bernard Lang. Complete evaluation of Horn Clauses: an automata theoretic approach. Research Report 813, INRIA, November 1988.
Dale Miller. Unification under a mixed prefix, to appear in the Journal of Symbolic Computation.
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1:497–536, 1991.
Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24 th Annual Meeting of the Association for Computational Linguistics, 1986.
Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Proceedings of the 4 th Symposium on Logic Programming, pages 379–388. IEEE Press, 1987.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.
Gopalan Nadathur and Bharat Jarayaman. Implementation techniques for scoping constructs in logic programming. In Koichi Furukawa, editor, Proceedings of the Eighth International Conference on Logic Programming, pages 871–886, 1991.
Fernando C. N. Pereira. Semantic interpretation as higher-order deduction. In Springer-Verlag, editor, Lecture Notes in Artificial Intelligence, pages 78–96, 1990.
Remo Pareschi and Dale Miller. Extending definite clause grammars with scoping constructs. In Proceedings of the 7 th International Conference on Logic Programming, pages 373–389, 1990.
Fernando C.N. Pereira and Stuart M. Shieber. Prolog and Natural-Language Analysis, volume 10 of Lecture Notes, pages 178–185. CSLI, 1987.
F.C.N. Pereira and D.H.D. Warren. Parsing as deduction. In Proceedings of the 21st Annual Meeting of the Association for Computationnal Linguistic, pages 137–144, Cambridge (Massachussetts), 1983.
Raghu Ramakrishnan. Magic templates: A spellbounding approach to manipulating formulas and programs. In Proceedings of the 54 th International Conference/Symposium on Logic Programming, pages 140–159, 1988.
FranÇois Rouaix. Personal communication.
Anthony Rich and Marvin Solomon. A logic-based approach to system modelling. Extended Abstract, 1990.
Eugene J. Rollins and Jeannette M. Wing. Specifications as search keys for software libraries. In Koichi Furukawa, editor, Proceedings of the 84 th International Conference on Logic Programming, pages 173–187, 1991.
H. Tamaki and T. Sato. OLD-resolution with tabulation. In E. Shapiro, editor, Proc. of Third Int. Conf. on Logic Programming, pages 84–98, London, 1986. Springer-Verlag.
M. van Emden and R. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4), 1976.
D. H. Warren. Higher-order extensions to Prolog: Are they needed? Machine Intelligence, 10:441–454, 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoa, A.H.B. (1992). A bottom-up interpreter for a higher-order logic programming language. In: Bruynooghe, M., Wirsing, M. (eds) Programming Language Implementation and Logic Programming. PLILP 1992. Lecture Notes in Computer Science, vol 631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55844-6_145
Download citation
DOI: https://doi.org/10.1007/3-540-55844-6_145
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55844-6
Online ISBN: 978-3-540-47297-1
eBook Packages: Springer Book Archive