×

S-semantics for logic programming: a retrospective look. (English) Zbl 1187.68122

Summary: The paper provides an overview of the s-semantic approach to the semantics of logic programs which had been developed about twenty years ago. The aim of such an approach was that of providing a suitable base for program analysis by means of a semantics which really captures the operational behavior of logic programs, and thus offers useful notions of observable program equivalences. The semantics is given in terms of extended interpretations, which are more expressive than Herbrand interpretations, extends the standard Herbrand semantics, and can be obtained as a result of both top-down and bottom-up constructions. The approach has been applied to several extensions of positive logic programs and used to develop semantic-based techniques for program analysis, verification and transformation.

MSC:

68N17 Logic programming
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Apt, K. R., Introduction to logic programming, (van Leeuwen, J., Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (1990), Elsevier, Amsterdam and The MIT Press: Elsevier, Amsterdam and The MIT Press Cambridge), 495-574
[2] Aravindan, Chandrabose; Dung, Phan Minh, On the correctness of unfold/fold transformation of normal and extended logic programs, Journal of Logic Programming, 24, 3, 201-217 (1995) · Zbl 0866.68018
[3] Barbuti, Roberto; Codish, Michael; Giacobazzi, Roberto; Maher, Michael J., Oracle semantics for Prolog, Information and Computation, 122, 2, 178-200 (1995) · Zbl 1096.68583
[4] Barbuti, Roberto; Giacobazzi, Roberto; Levi, Giorgio, A general framework for semantics-based bottom-up abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), 15, 1, 133-181 (1993)
[5] Bossi, Annalisa; Bugliesi, Michele; Fabris, Massimo, A new fixpoint semantics for Prolog, (Warren, D. S., ICLP’93: Proceedings of the Tenth Int’l Conference on Logic Programming, Cambridge, MA, USA (1993), The MIT Press), 374-389
[6] Bossi, Annalisa; Bugliesi, Michele; Gabbrielli, Maurizio; Levi, Giorgio; Meo, Maria Chiara, Differential logic programming, (POPL’93: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA (1993), ACM Press), 359-370
[7] Bossi, Annalisa; Cocco, Nicoletta, Basic transformation operations which preserve computed answer substitutions of logic programs, Journal of Logic Programming, 16, 1-2, 47-87 (1993) · Zbl 0778.68020
[8] Bossi, Annalisa; Gabbrielli, Maurizio; Levi, Giorgio; Martelli, Maurizio, The s-semantics approach: Theory and applications, Journal of Logic Programming, 19/20, 149-197 (1994) · Zbl 0942.68527
[9] Bossi, Annalisa; Gabbrielli, Maurizio; Levi, Giorgio; Meo, Maria Chiara, A compositional semantics for logic programs, Theoretical Computer Science, 122, 1-2, 3-47 (1994) · Zbl 0801.68110
[10] Annalisa Bossi, Marina Menegus, Una semantica composizionale per programmi logici aperti, in: P. Asirelli (Ed.), Sesto convegno sulla programmazione logica, in: Proc. Sixth Italian Conference on Logic Programming, GULP, Pisa, Italy, June 1991, pp. 95-109; Annalisa Bossi, Marina Menegus, Una semantica composizionale per programmi logici aperti, in: P. Asirelli (Ed.), Sesto convegno sulla programmazione logica, in: Proc. Sixth Italian Conference on Logic Programming, GULP, Pisa, Italy, June 1991, pp. 95-109
[11] Bruscoli, Paola; Levi, Francesca; Levi, Giorgio; Meo, Maria Chiara, Compilative constructive negation in constraint logic programs, (CAAP’94: Proc. of the 19th Int’l Colloquium on Trees in Algebra and Programming, London, UK (1994), Springer-Verlag), 52-67 · Zbl 0938.68571
[12] Bruynooghe, Maurice, A practical framework for the abstract interpretation of logic programs, Journal of Logic Programming, 10, 2, 91-124 (1991) · Zbl 0717.68010
[13] Codish, Michael; Dams, Dennis; Yardeni, Eyal, Bottom-up abstract interpretation of logic programs, Theoretical Computer Science, 124, 1, 93-125 (1994) · Zbl 0795.68038
[14] Michael Codish, Saumya K. Debray, Roberto Giacobazzi, Compositional analysis of modular logic programs, in: Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, 1993, pp. 451-464; Michael Codish, Saumya K. Debray, Roberto Giacobazzi, Compositional analysis of modular logic programs, in: Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, 1993, pp. 451-464
[15] Codish, Michael; Søndergaard, Harald, Meta-Circular Abstract Interpretation in Prolog (2002), pp. 109-134 · Zbl 1026.68505
[16] Comini, Marco; Levi, Giorgio; Meo, Maria Chiara; Vitiello, Giuliana, Proving properties of logic programs by abstract diagnosis, (Selected Papers from the 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages, London, UK (1997), Springer-Verlag), 22-50 · Zbl 0947.68024
[17] Comini, Marco; Levi, Giorgio; Meo, Maria Chiara; Vitiello, Giuliana, Abstract diagnosis, Journal of Logic Programming, 39, 1-3, 43-93 (1999) · Zbl 0947.68024
[18] Comini, Marco; Levi, Giorgio; Vitiello, Giuliana, Abstract debugging of logic program, (LOPSTR’94/META’94: Proceedings of the 4th Int’l Workshops on Logic Programming Synthesis and Transformation — Meta-Programming in Logic, London, UK (1994), Springer-Verlag), 440-450
[19] Cousot, Patrick, Program analysis: The abstract interpretation perspective, ACM Computing Surveys, 28, 4es, 165 (1996) · Zbl 0676.68004
[20] Delzanno, Giorgio; Martelli, Maurizio, A bottom-up characterization of finite success, (ILPS’93: Proceedings of the 1993 Int’l Symposium on Logic Programming, Cambridge, MA, USA (1993), The MIT Press), 676
[21] Denis, Francois; Delahaye, Jean-Paul, Unfolding, procedural and fixpoint semantics of logic programs, (Eighth Annual Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany. Eighth Annual Symposium on Theoretical Aspects of Computer Science, Hamburg, Germany, Lecture Notes in Computer Science (February 1991)), 511-522 · Zbl 0776.68079
[22] Dung, P. M.; Kanchanasut, K., A fixpoint approach to declarative semantics of logic programs, (Lusk, E. L.; Overbeek, R. A., Logic Programming: Proc. of the North American Conference 1989, vol. 1 (1989), The MIT Press: The MIT Press Cambridge, MA), 604-625
[23] Van Emden, M. H.; Kowalski, R. A., The semantics of predicate logic as a programming language, Journal of the ACM, 23, 4, 733-742 (1976) · Zbl 0339.68004
[24] Etalle, Sandro; Gabbrielli, Maurizio, Transformations of CLP modules, Theoretical Computer Science, 166, 1-2, 101-146 (1996) · Zbl 0872.68021
[25] Fages, Francois; Gori, Roberta, A hierarchy of semantics for normal constraint logic programs, (Algebraic and Logic Programming (1996)), 77-91 · Zbl 1355.68034
[26] Falaschi, Moreno; Levi, Giorgio; Martelli, Maurizio; Palamidessi, Catuscia, Declarative modeling of the operational behaviour of logic languages, Theoretical Computer Science, 69, 289-318 (1989) · Zbl 0699.68113
[27] Falaschi, Moreno; Levi, Giorgio; Martelli, Maurizio; Palamidessi, Catuscia, A model-theoretic reconstruction of the operational semantics of logic programs, Information and Computation, 102, 1, 86-113 (1993) · Zbl 0788.68088
[28] Ferrand, Gèrard, Error diagnosis in logic programming, an adaptation of E.Y. Shapiro’s method, Journal of Logic Programming, 4, 3, 177-198 (1987) · Zbl 0623.68005
[29] Maurizio Gabbrielli, The semantics of logic programming as a programming language, Ph.D. Thesis, Dipartimento di Informatica, Università di Pisa, 1992; Maurizio Gabbrielli, The semantics of logic programming as a programming language, Ph.D. Thesis, Dipartimento di Informatica, Università di Pisa, 1992 · Zbl 0757.68074
[30] Maurizio Gabbrielli, Roberto Giacobazzi, Goal independency and call patterns in the analysis of logic programs, in: ACM Symposium on Applied Computing, 1994, pp. 394-399; Maurizio Gabbrielli, Roberto Giacobazzi, Goal independency and call patterns in the analysis of logic programs, in: ACM Symposium on Applied Computing, 1994, pp. 394-399
[31] Gabbrielli, Maurizio; Levi, Giorgio, Unfolding and fixpoint semantics of concurrent constraint logic programs, (Proc. of the Second Int’l Conference on Algebraic and Logic Programming, London, UK (1990), Springer-Verlag), 204-216 · Zbl 0757.68074
[32] Gabbrielli, Maurizio; Levi, Giorgio; Meo, Maria Chiara, Observational equivalences for logic programs, (Apt, K., Logic Programming, Proceedings of the Joint Int’l Conference and Symposium on Logic Programming, Washington, DC (November 1992), The MIT Press), 131-145 · Zbl 0834.68010
[33] Maurizio Gabbrielli, Giorgio Levi, Daniele Turi, A two steps semantics for logic programs with negation, in: LPAR’92: Proceedings of the Int’l Conference on Logic Programming and Automated Reasoning, 1992, pp. 297-308; Maurizio Gabbrielli, Giorgio Levi, Daniele Turi, A two steps semantics for logic programs with negation, in: LPAR’92: Proceedings of the Int’l Conference on Logic Programming and Automated Reasoning, 1992, pp. 297-308
[34] Gabbrielli, Maurizio; Meo, Maria Chiara, Fixpoint semantics for partial computed answer substitutions and call patterns, (Kirchner, H.; Levi, G., Algebraic and Logic Programming: Proc. of the Third Int’l Conference (1992), Springer: Springer Berlin, Heidelberg), 84-99
[35] Gaifman, H.; Shapiro, E., Fully abstract compositional semantics for logic programs, (POPL’89: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA (1989), ACM Press), 134-142
[36] Gaifman, H.; Shapiro, E., Proof theory and semantics of logic programs, (Proceedings of the Fourth Annual Symposium on Logic in Computer Science, Piscataway, NJ, USA (1989), IEEE Press), 50-62
[37] Giacobazzi, Roberto; Debray, Saumya K.; Levi, Giorgio, A generalized semantics for constraint logic programs, (Proceedings of the Int’l Conference on Fifth Generation Computer Systems, ICOT, Japan (1992), Association for Computing Machinery), 581-591 · Zbl 0862.68072
[38] Gori, Roberta, An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations, Theoretical Computer Science, 290, 1, 863-936 (2003) · Zbl 1051.68103
[39] Gori, Roberta; Levi, Giorgio, On the verification of finite failure, Journal of Computer and System Sciences, 71, 4, 535-575 (2005) · Zbl 1105.68016
[40] Jacobs, Dean; Langen, Anno, Static analysis of logic programs for independent AND parallelism, Journal of Logic Programming, 13, 2-3, 291-314 (1992) · Zbl 0776.68026
[41] Janssens, G.; Bruynooghe, M., Deriving descriptions of possible values of program variables by means of abstract interpretation, Journal of Logic Programming, 13, 2-3, 205-258 (1992) · Zbl 0776.68027
[42] Kanchanasut, Kanchana; Stuckey, Peter J., Transforming normal logic programs to constraint logic programs, Theoretical Computer Science, 105, 1, 27-56 (1992) · Zbl 0757.68029
[43] Lassez, Jean-Louis; Maher, Michael J., Closures and fairness in the semantics of programming logic, Theoretical Computer Science, 29, 167-184 (1984) · Zbl 0547.68034
[44] Levi, Giorgio, Models, unfolding rules and fixpoint semantics, (Kowalski, R. A.; Bowen, K. A., Logic Programming: Proc. of the Fifth Int’l Conference and Symposium, vol. 2 (1991), The MIT Press: The MIT Press Cambridge, MA), 1649-1665
[45] Levi, Giorgio; Martelli, Maurizio; Palamidessi, Catuscia, Failure and success made symmetric, (Debray, S.; Hermenegildo, M., Logic Programming: Proc. of the 1990 North American Conference (1990), The MIT Press: The MIT Press Cambridge, MA), 3-22
[46] Levi, Giorgio; Ramundo, Davide, Formalization of metaprogramming for real, (ICLP’93: Proceedings of the Tenth Int’l Conference on Logic Programming, Cambridge, MA, USA (1993), The MIT Press), 354-373
[47] Lloyd, J. W., Foundations of Logic Programming (1984), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. New York, NY, USA · Zbl 0547.68005
[48] Lloyd, John W., Declarative error diagnosis, New Generation Computing, 5, 2, 133-154 (1987) · Zbl 0624.68018
[49] Lloyd, J. W.; Shepherdson, J. C., Partial evaluation in logic programming, Journal of Logic Programming, 11, 217-242 (1991) · Zbl 0741.68030
[50] Marriott, Kim; Søndergaard, Harald, Bottom-up abstract interpretation of logic programs, (Kowalski, R. A.; Bowen, K. A., Proc. Fifth Int’l Conf. on Logic Programming, Cambridge, MA (1988), The MIT Press), 733-748 · Zbl 0776.68025
[51] Marriott, Kim; Søndergaard, Harald, Semantics-based dataflow analysis of logic programs, (Ritter, G., IFIP Congress (1989), North-Holland), 601-606 · Zbl 0776.68025
[52] De Schreye, Danny; Martens, Bern, A sensible least herbrand semantics for untyped vanilla meta-programming and its extension to a limited form of amalgamation, (Pettorossi, A., Meta-Programming in Logic: Proc. of the Third Int’l Workshop META-92 (1992), Springer: Springer Berlin, Heidelberg), 192-204
[53] Shapiro, Ehud Y., Algorithmic Program Debugging (1983), The MIT Press: The MIT Press Cambridge, MA, USA · Zbl 0589.68003
[54] Hisao Tamaki, Taisuke Sato, Unfold/fold transformation of logic programs, in: Second Int. Conf. on Logic Programming, 1984, pp. 127-138; Hisao Tamaki, Taisuke Sato, Unfold/fold transformation of logic programs, in: Second Int. Conf. on Logic Programming, 1984, pp. 127-138 · Zbl 0985.68554
[55] Turi, Daniele, Extending s-models to logic programs with negation, (Furukawa, Koichi, Logic Programming, Proceedings of the Eighth International Conference, Cambridge, MA, USA (June 1991), The MIT Press), 397-411
[56] Wim Vanhoof, Techniques for online and offline specialisation of logic programs, Ph.D. Thesis, Katholieke Universiteit Leuven, June 2001; Wim Vanhoof, Techniques for online and offline specialisation of logic programs, Ph.D. Thesis, Katholieke Universiteit Leuven, June 2001
[57] Vanhoof, Wim; De Schreye, Danny; Martens, Bern, Bottom-up partial deduction of logic programs, Journal Functional and of Logic Programming, 2 (1999), (special issue) · Zbl 0946.68012
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.