An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations. (English) Zbl 1051.68103
Summary: We extend the framework of M. Comini, G. Levi and M. C. Meo [Inf. Comput. 169, 23–80 (2001; Zbl 1007.68020)] in order to be able to reason on properties (of abstractions) of possibly infinite SLD-derivations. This issue is relevant since some important operational properties such as finite failure, infinite behavior can only be addressed as abstraction of finite and infinite SLD-derivations. The framework allows us to define new fixpoint semantics correctly modelling such properties and address problems such as compositionality w.r.t. various syntactic operators, correctness and minimality of the chosen denotations. In this paper we also apply the framework in order to obtain a new fixpoint semantics, based on a co-continuous operator, which correctly models finite failure and is compositional w.r.t. the syntactic operators.
MSC:
| 68Q55 | Semantics in the theory of computing |
Citations:
Zbl 1007.68020References:
| [1] | Abramsky, S.; Hankin, C., An introduction to abstract interpretation, (Abramsky, S.; Hankin, C., Abstract Interpretation of Declarative Languages (1987), Ellis-Horwood: Ellis-Horwood Chichester, UK), 9-31 |
| [2] | K.R. Apt, Introduction to logic programming, Vol. B: Formal Models and Semantics of Handbook of Theoretical Computer Science, Elsevier and The MIT Press, Amsterdam, Cambridge, MA, 1990, pp. 495-574.; K.R. Apt, Introduction to logic programming, Vol. B: Formal Models and Semantics of Handbook of Theoretical Computer Science, Elsevier and The MIT Press, Amsterdam, Cambridge, MA, 1990, pp. 495-574. · Zbl 0714.68001 |
| [3] | Apt, K. R.; van Emden, M. H., Contributions to the theory of logic programming, J. ACM, 29, 3, 841-862 (1982) · Zbl 0483.68004 |
| [4] | Bossi, A.; Gabbrielli, M.; Levi, G.; Martelli, M., The s-semantics approachtheory and applications, J. Logic Programming, 19-20, 149-197 (1994) · Zbl 0942.68527 |
| [5] | K.L. Clark, Predicate logic as a computational formalism, Res. Report DOC 79/59, Imperial College, Department of Computing, London, 1979.; K.L. Clark, Predicate logic as a computational formalism, Res. Report DOC 79/59, Imperial College, Department of Computing, London, 1979. |
| [6] | M. Comini, An abstract interpretation framework for semantics and diagnosis of logic programs, Ph.D. Thesis, Dipartimento di Informatica, Universitá di Pisa, 1998.; M. Comini, An abstract interpretation framework for semantics and diagnosis of logic programs, Ph.D. Thesis, Dipartimento di Informatica, Universitá di Pisa, 1998. |
| [7] | Comini, M.; Levi, G., An algebraic theory of observables, (Bruynooghe, M., Proc. 1994 Internat. Symp. on Logic Programming (1994), The MIT Press: The MIT Press Cambridge, MA), 172-186 |
| [8] | Comini, M.; Levi, G.; Meo, M. C., A theory of observables for logic programs, Inform. Comput., 169, 23-80 (2001) · Zbl 1007.68020 |
| [9] | Comini, M.; Meo, M. C., Compositionality properties of SLD-derivations, Theoret. Comput. Sci., 211, 1-2, 275-309 (1999) · Zbl 0912.68124 |
| [10] | Cousot, P., Semantic foundations of program analysis, (Muchnick, S.; Jones, N. D., Program Flow analysis: Theory and Applications (1981), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 303-342 · Zbl 0468.68002 |
| [11] | P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proc. 4th ACM Symp. Principles of Programming Languages, 1977, pp. 238-252.; P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proc. 4th ACM Symp. Principles of Programming Languages, 1977, pp. 238-252. |
| [12] | Cousot, P.; Cousot, R., Static determination of dynamic properties of recursive procedures, (Neuhold, E. J., IFIP Conf. on Formal Description of Programming Concepts (1977), Elsevier Science Publishers: Elsevier Science Publishers Amsterdam), 237-277 · Zbl 0788.68094 |
| [13] | Cousot, P.; Cousot, R., A constructive characterization of the lattices of all retracts, pre-closure, quasi-closure and closure operators on a complete lattice, Portugal. Math., 38, 2, 185-198 (1979) · Zbl 0503.06008 |
| [14] | Cousot, P.; Cousot, R., Constructive versions of Tarski’s fixed point theorems, Pacific J. Math., 82, 1, 43-57 (1979) · Zbl 0413.06004 |
| [15] | P. Cousot, R. Cousot, Systematic design of program analysis frameworks, in: Proc. 6th ACM Symp. Principles of Programming Languages, 1979, pp. 269-282.; P. Cousot, R. Cousot, Systematic design of program analysis frameworks, in: Proc. 6th ACM Symp. Principles of Programming Languages, 1979, pp. 269-282. · Zbl 1323.68356 |
| [16] | P. Cousot, R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Technical Report LIX/RR/92/09, LIX, Laboratoire d’Informatique École Polytechnique, 1991.; P. Cousot, R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Technical Report LIX/RR/92/09, LIX, Laboratoire d’Informatique École Polytechnique, 1991. · Zbl 1284.68173 |
| [17] | P. Cousot, R. Cousot, Inductive definitions, semantics and abstract interpretation, in: Proc. 19th Annu. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1992, pp. 83-94.; P. Cousot, R. Cousot, Inductive definitions, semantics and abstract interpretation, in: Proc. 19th Annu. ACM Symp. on Principles of Programming Languages, ACM Press, New York, 1992, pp. 83-94. · Zbl 0776.68024 |
| [18] | de Boer, F. S.; Di Pierro, A.; Palamidessi, C., Nondeterminism and infinite computations in constraint programming, Theoret. Comput. Sci., 151, 37-78 (1995) · Zbl 0872.68103 |
| [19] | Falaschi, M.; Levi, G., Finite failures and partial computations in concurrent logic languages, Theoret. Comput. Sci., 75, 45-66 (1990) · Zbl 0702.68079 |
| [20] | Falaschi, M.; Levi, G.; Martelli, M.; Palamidessi, C., Declarative modeling of the operational behavior of logic languages, Theoret. Comput. Sci., 69, 3, 289-318 (1989) · Zbl 0699.68113 |
| [21] | Falaschi, M.; Levi, G.; Martelli, M.; Palamidessi, C., A model-theoretic reconstruction of the operational semantics of logic programs, Inform. Comput., 102, 1, 86-113 (1993) · Zbl 0788.68088 |
| [22] | Ferrand, G., Error diagnosis in logic programming, an adaptation of E. Y. Shapiro’s method, J. Logic Programming, 4, 177-198 (1987) · Zbl 0623.68005 |
| [23] | Ferrand, G., The notions of symptom and error in declarative diagnosis of logic programs, (Fritzson, P. A., Automated and Algorithmic Debugging, Proceedings of AADEBUG ’93. Automated and Algorithmic Debugging, Proceedings of AADEBUG ’93, Lecture Notes in Computer Science, Vol. 749 (1993), Springer: Springer Berlin), 40-57 |
| [24] | Gabbrielli, M.; Levi, G.; Meo, M. C., Observable behaviors and equivalences of logic programs, Inform. Comput., 122, 1, 1-29 (1995) · Zbl 0834.68010 |
| [25] | Gabbrielli, M.; Levi, G.; Meo, M. C., Resultants semantics for PROLOG, J. Logic Comput., 6, 4, 491-521 (1996) · Zbl 0856.68038 |
| [26] | Giacobazzi, R., “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics, (Puech, C.; Reischuk, R., Proc. 13th Internat. Symp. on Theoretical Aspects of Computer Science (STACS’96). Proc. 13th Internat. Symp. on Theoretical Aspects of Computer Science (STACS’96), Lecture Notes in Computer Science, Vol. 1046 (1996), Springer: Springer Berlin), 503-514 · Zbl 1379.68065 |
| [27] | Golson, W. G., Toward a declarative semantics for infinite objects in logic programming, J. Logic Programming, 5, 151-164 (1988) · Zbl 0644.68025 |
| [28] | R. Gori, Reasoning about finite failure and infinite computations by abstract interpretation, Ph.D. Thesis, Dipartimento di Matematica, Università di Siena, 1999, http://www.di.unipi.it/ gori/gori.html; R. Gori, Reasoning about finite failure and infinite computations by abstract interpretation, Ph.D. Thesis, Dipartimento di Matematica, Università di Siena, 1999, http://www.di.unipi.it/ gori/gori.html |
| [29] | Gori, R., An abstract interpretation approach to termination of logic programs, (Parigot, M.; Voronkov, A., Proc. 7th Internat. Conf. on Logic for Programming and Automated Reasoning. Proc. 7th Internat. Conf. on Logic for Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, Vol. 1955 (2000), Springer: Springer Berlin), 362-380 · Zbl 0988.68033 |
| [30] | Gori, R.; Levi, G., Finite failure is and-compositional, J. Logic Comput., 7, 6, 753-776 (1997) · Zbl 0892.68016 |
| [31] | R. Gori, G. Levi, On the verification of finite failure, in: Proc. Internat. Conf. Principles and Practice of Declarative Programming, Lecture Notes in Computer Science, Springer, Berlin, 1999, pp. 311-327.; R. Gori, G. Levi, On the verification of finite failure, in: Proc. Internat. Conf. Principles and Practice of Declarative Programming, Lecture Notes in Computer Science, Springer, Berlin, 1999, pp. 311-327. · Zbl 0953.68083 |
| [32] | Kemp, R. S.; Ringwood, G. A., An algebraic framework for the abstract interpretation of logic programs, (Debray, S. K.; Hermenegildo, M., Proc. North American Conf. on Logic Programming’90 (1990), The MIT Press: The MIT Press Cambridge, MA), 506-520 |
| [33] | R.S. Kemp, G.A. Ringwood, Reynolds base, Clark models and Heyting semantics of logic programs, in: R. Momigliano, ICLP’94 Post-conference Workshop on Proof-Theoretical Extensions of Logic Programming.; R.S. Kemp, G.A. Ringwood, Reynolds base, Clark models and Heyting semantics of logic programs, in: R. Momigliano, ICLP’94 Post-conference Workshop on Proof-Theoretical Extensions of Logic Programming. |
| [34] | M.Z. Kwiatkowska, Infinite behaviour and fairness in concurrent constraint programming, in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (Eds.), Semantics: Foundations and Applications, Lecture Notes in Computer Science, Vol. 666, Beekbergen The Nederland, June 1992, REX Workshop, Springer, Berlin, pp. 348-383.; M.Z. Kwiatkowska, Infinite behaviour and fairness in concurrent constraint programming, in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (Eds.), Semantics: Foundations and Applications, Lecture Notes in Computer Science, Vol. 666, Beekbergen The Nederland, June 1992, REX Workshop, Springer, Berlin, pp. 348-383. |
| [35] | Lassez, J.-L.; Maher, M. J., Closures and fairness in the semantics of programming logic, Theoret. Comput. Sci., 29, 167-184 (1984) · Zbl 0547.68034 |
| [36] | B. Le Charlier, S. Rossi, P. Van Hentenryck, An abstract interpretation framework which accurately handles PROLOG search-rule and the cut, in: Proc. 1994 Internat. Logic Programming Symp., The MIT Press, Cambridge, MA, 1994.; B. Le Charlier, S. Rossi, P. Van Hentenryck, An abstract interpretation framework which accurately handles PROLOG search-rule and the cut, in: Proc. 1994 Internat. Logic Programming Symp., The MIT Press, Cambridge, MA, 1994. |
| [37] | Levi, G.; Martelli, M.; Palamidessi, C., Failure and success made symmetric, (Debray, S. K.; Hermenegildo, M., Proc. North American Conf. on Logic Programming’90 (1990), The MIT Press: The MIT Press Cambridge, MA), 3-22 |
| [38] | Lloyd, J. W., Foundations of Logic Programming (1987), Springer: Springer Berlin · Zbl 0547.68005 |
| [39] | Marriott, K.; Søndergaard, H., Semantics-based dataflow analysis of logic programs, (Ritter, G., Information Processing ’89 (1989), Elsevier Science Publishers: Elsevier Science Publishers Amsterdam) |
| [40] | NaitAbdallah, M. A., On the interpretation of infinite computations in logic programming, (Paredaens, J., Proc. Automata. Proc. Automata, Languages and Programming, Vol. 172 (1984), Springer: Springer Berlin), 374-381 · Zbl 0557.68030 |
| [41] | Nielson, F., A denotational framework for data flow analysis, Acta Inform., 18, 265-287 (1982) · Zbl 0479.68012 |
| [42] | Nyström, S. O.; Jonsson, B., Indeterminate concurrent constraint programminga fixpoint semantics for non-terminating computations, (Miller, D., Proc. 1993 Internat. Logic Programming Symp. Series on Logic Programming (1993), The MIT Press: The MIT Press Cambridge, MA), 335-352 |
| [43] | V.A. Saraswat, Concurrent constraint programming languages, Ph.D. Thesis, Carnegie-Mellon University, January 1989.; V.A. Saraswat, Concurrent constraint programming languages, Ph.D. Thesis, Carnegie-Mellon University, January 1989. |
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.
