Fully abstract compositional semantics for logic programs

ABSTRACT

We propose a framework for discussing fully abstract compositional semantics, which exposes the interrelations between the choices of observables, compositions, and meanings. Every choice of observables and compositions determines a unique fully abstract equivalence. A semantics is fully abstract if it induces this equivalence. We study the semantics of logic programs within this framework. We find the classical Herbrand-base semantics of logic programs inadequate, since it identifies programs that should be distinguished and vice versa. We therefore propose alternative semantics, and consider the cases of no compositions, composition by program union, and composition of logic modules (programs with designated exported and imported predicates). Although equivalent programs can be in different vocabularies, we prove that our fully abstract semantics are always in a subvocabulary of that of the program. This subvocabulary, called the essential vocabulary, is common to all equivalent programs. The essential vocabulary is also the smallest subvocabulary in which an equivalent program can be written.

REFERENCES

• 1: Krzysztof R. Apt , M. H. van Emden, Contributions to the Theory of Logic Programming, Journal of the ACM (JACM), v.29 n.3, p.841-862, July 1982 [doi>10.1145/322326.322339]
• 2: G Berry , P L Curien , J J Lévy, Full abstraction for sequential algorithms: the state of the art, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 3: Clark, K.L., Predicate logic as a computational forrealism, Research Report DOC 79/59, Department of Computing, Imperi.al College, 1979.
• 4: Keith Clark , Steve Gregory, PARLOG: parallel programming in logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.1, p.1-49, Jan. 1986 [doi>10.1145/5001.5390]
• 5: Keith L. Clark , Steve Gregory, A relational language for parallel programming, Proceedings of the 1981 conference on Functional programming languages and computer architecture, p.171-178, October 18-22, 1981, Portsmouth, New Hampshire, United States [doi>10.1145/800223.806776]
• 6: W F. Clocksin , Christopher S. Mellish, Programming in Prolog (2nd ed.), Springer-Verlag New York, Inc., New York, NY, 1984
• 7: M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976 [doi>10.1145/321978.321991]
• 8: Gaifman, H., Mairson, H., Sagiv, Y. and Vardi, M.Y., Undecidable optimization problems for database logic programs, Proc. ~nd !EEE ~ympo- ~ium on Logic in Computer Science, pp. 106-115, Ithaca, 1987.
• 9: Gerth R., Codish M., Lichtenstein Y. and Shapiro E., Fully Abstract Denotational Semantics for Flat Concurrent Prolog, P'roc. 3rd IEEE Annual oOympo- 8ium on Logic in Computer Science, pp. 320-333, Edinburgh, 1988.
• 10: Goguen, J.A. and Meseguer, J., Equality, types, modules, and (why not?) generics for logic programming, J. Logic Programming 2, 179-210, 1984.
• 11: Hill, R., LUSH-resolution and its completeness, DCL Memo 78, Department of Artificial Intelligence, University of :Edinburgh, 1974.
• 12: Neil Immerman, Relational queries computable in polynomial time, Information and Control, v.68 n.1-3, p.86-104, Jan/Feb/March 1986 [doi>10.1016/S0019-9958(86)80029-8]
• 13: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 14: Maher, M.J., Semantics of Logic Programs, Ph.D. dissertation, University of Melbourne, 1985.
• 15: M. J. Maher, Equivalences of logic programs, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 16: Martelli, M., Falaschi, M., Levi, G. and Palarnidessi, G., A new declarative semantics for logic languages, To appeax in K. Bowen and R.A. Kowalski (eds.), Proc. 5th International Conference Symposium on Logic Programming, Seattle, MIT Press, 1988.
• 17: Meyer, A.R. and Cosmadakis, S.S., Semantical paradigms: notes for an invited lecture, Proc. 3rd IEEE Annual Symposium on Logic in Computer Science, pp. 236-253, Edinburgh, 1988.
• 18: O'Keefe, R.A., Towards an algebra for constructing logic programs, Proc. 1985 IEEE Symposium on Logic Programming, pp. 152-160, Boston, 1985.
• 19: Plotkin, G.D., LCF considered as a programming language, Theoretical Computer Science 5, 223- 256, 1977.
• 20: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 21: Y. Sagiv, Optimizing datalog programs, Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.349-362, March 23-25, 1987, San Diego, California, United States [doi>10.1145/28659.28696]
• 22: E. Shapiro, A subset of Concurrent Prolog and its interpreter, Concurrent Prolog, MIT Press, Cambridge, MA, 1988
• 23: Allen Stoughton, Fully abstract models of programming languages, Pitman Publishing, Inc., Marshfield, MA, 1988
• 24: Kazunori Ueda, Guarded horn clauses, Proceedings of the 4th conference on Logic programming '85, p.168-179, August 1986, Tokyo, Japan
• 25: Jeffrey D. Ullman, Implementation of logical query languages for databases, ACM Transactions on Database Systems (TODS), v.10 n.3, p.289-321, Sept. 1985 [doi>10.1145/3979.3980]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Algorithms, Design, Languages, Verification