TY - GEN
T1 - Models and equality for logical programming
AU - Goguen, Joseph A.
AU - Meseguer, José
N1 - Funding Information:
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.
Publisher Copyright:
© 1987, Springer-Verlag.
PY - 1987
Y1 - 1987
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85034963820&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85034963820&partnerID=8YFLogxK
U2 - 10.1007/BFb0014969
DO - 10.1007/BFb0014969
M3 - Conference contribution
AN - SCOPUS:85034963820
SN - 9783540176114
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 22
BT - TAPSOFT 1987 - Proceedings of the International Joint Conference on Theory and Practice of Software Development
A2 - Ehrig, Hartmut
A2 - Levi, Giorgi
A2 - Montanari, Ugo
A2 - Kowalski, Robert
PB - Springer
T2 - 2nd International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1987
Y2 - 23 March 1987 through 27 March 1987
ER -