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 -