Abstract
We argue that some standard tools from model theory provide a better semantic foundation than the more syntactic and operational approaches usually used in logic programming. In particular, we show how initial models capture the intended semantics of both functional and logic programming, as well as their combination, with existential queries having logical variables (for both functions and relations) in the presence of arbitrary user-defined abstract data types, and with the full power of constraint languages, having any desired built-in (computable) relations and functions, including disequality (the negation of the equality relation) as well as the usual ordering relations on the usual built-in types, such as numbers and strings. These results are based on a new completeness theorem for order-sorted Horn clause logic with equality, plus the use of standard interpretations for fixed sorts, functions and relations. Finally, we define “logical programming,” based on the concept of institution, and show how it yields a general framework for discussions of this kind. For example, this viewpoint suggests that the natural way to combine functional and logic programming is simply to combine their logics, getting Horn clause logic with equality.
Supported in part by Office of Naval Research Contracts N00014-85-C-0417 and N00014-86-C-0450, and a gift from the System Development Foundation.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Michael A. Arbib and Ernest Manes. Arrows, Structures and Functors. Academic Press, 1975.
John Backus. “Can Programming be Liberated from the von Neumann Style?”. Communications of the Association for Computing Machinery 21, 8 (1978), 613–641.
Jon Barwise. “Axioms for Abstract Model Theory”. Annals of Mathematical Logic 7 (1974), 221–265.
Robert Boyer and Moore, J. A Computational Logic. Academic Press, 1980.
Rod Burstall and Joseph Goguen. “Putting Theories together to Make Specifications”. Proceedings, Fifth International Joint Conference on Artificial Intelligence 5 (1977), 1045–1058.
Rod Burstall and Joseph Goguen. Lecture Notes in Computer Science. Volume 86: The Semantics of Clear, a Specification Language. In Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification, Springer-Verlag, 1980, pp. 292–332.
Rod Burstall and Joseph Goguen. Algebras, Theories and Freeness: An Introduction for Computer Scientists. In Proceedings, 1981 Marktoberdorf NATO Summer School, Reidel, 1982.
Hartmut Ehrig and Bernd Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer-Verlag, 1985.
Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud and José Meseguer. Principles of OBJ2. In Proceedings, Symposium on Principles of Programming Languages, Association for Computing Machinery, 1985, pp. 52–66.
Joseph Goguen and Rod Burstall. Institutions: Abstract Model Theory for Computer Science. CSLI-85-30, Center for the Study of Language and Information, Stanford University, 1985. Also submitted for publication; a preliminary version appears in Proceedings, Logics of Programming Workshop, edited by Edward Clarke and Dexter Kozen, Volume 164, Springer-Verlag Lecture Notes in Computer Science, pages 221–256, 1984.
Joseph Goguen and José Meseguer. Eqlog: Equality, Types, and Generic Modules for Logic Programming. In Functional and Logic Programming, Douglas DeGroot and Gary Lindstrom, Eds., Prentice-Hall, 1986, pp. 295–363. An earlier version appears in Journal of Logic Programming, Volume 1, Number 2, pages 179–210, September 1984.
Joseph Goguen and José Meseguer. Extensions and Foundations for Object-Oriented Programming. In preparation for Research Directions in Object-Oriented Programming, edited by Bruce Shriver and Peter Wegner. Preliminary version in SIGPLAN Notices, Volume 21, Number 10, pages 153–162, October 1986.
Joseph Goguen and José Meseguer. “Remarks on Remarks on Many-Sorted Equational Logic”. Bulletin of the European Association for Theoretical Computer Science 30 (October 1986), 66–73. Also to appear in SIGPLAN Notices.
Joseph Goguen and José Meseguer. Order-Sorted Algebra I: Partial and Overloaded Operations, Errors and Inheritance. To appear, SRI International, Computer Science Lab, 1987. Given as lecture at Seminar on Types, Carnegie-Mellon University, June 1983.
Joseph Goguen and José Meseguer. Order-Sorted Algebra Solves the Constructor-Selector Problem. In preparation.
Joseph Goguen, Jean-Pierre Jouannaud and José Meseguer. Operational Semantics of Order-Sorted Algebra. In Proceedings, 1985 International Conference on Automata, Languages and Programming, Springer-Verlag, 1985. Summary presented at IFIP WG2.2 (Boston MA) June 1984.
Joseph Goguen, James Thatcher and Eric Wagner. An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. RC 6487, IBM T. J. Watson Research Center, October, 1976. Appears in Current Trends in Programming Methodology, IV, edited by Raymond Yeh, Prentice-Hall, 1978, pages 80–149.
Joseph Y. Halpern, John H. Williams, Edward L. Wimmers and Timothy Winkler. Denotational Semantics and Rewrite Rules for FP. In Proceedings, Symposium on Principles of Programming Languages, Association for Computing Machinery, 1985, pp. 108–120.
Joxan Jaffar and Jean-Louis Lassez. Constraint Logic Programming. Monash University, Australia, 1986. Draft.
Joxan Jaffar and Spiro Michaylov. Methodology and Implementation of a Constraint Logic Programming System. Monash University, Australia, 1986. Draft.
Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.
José Meseguer and Joseph Goguen. Initiality, Induction and Computability. In Algebraic Methods in Semantics, Maurice Nivat and John C. Reynolds, Eds., Cambridge University Press, 1985, pp. 459–541. Also SRI CSL Technical Report 140, December 1983.
José Meseguer, Joseph Goguen and Gert Smolka. Order-Sorted Unification. SRI International, 1987. In preparation.
Michael O'Donnell. Equational Logic as a Programming Language. MIT Press, 1985.
J. Alan Robinson. “A Machine-oriented Logic Based on the Resolution Principle”. Journal of the Association for Computing Machinery 12 (1965).
Gert Smolka, Joseph Goguen and José Meseguer. Order-Sorted Equational Computation. SRI International, 1987. In preparation.
C. Walther. Unification in Many-sorted Theories. In Advances in Artificial Intelligence — Proceedings, Sixth European Conference on Artificial Intelligence, North-Holland, 1984, pp.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goguen, J.A., Meseguer, J. (1987). Models and equality for logical programming. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds) TAPSOFT '87. TAPSOFT 1987. Lecture Notes in Computer Science, vol 250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014969
Download citation
DOI: https://doi.org/10.1007/BFb0014969
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17611-4
Online ISBN: 978-3-540-47717-4
eBook Packages: Springer Book Archive