Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-28T15:29:40.208Z Has data issue: false hasContentIssue false
  • English
  • Français

Checking termination of bottom-up evaluation of logic programs with function symbols*

Published online by Cambridge University Press:  13 August 2014

MARCO CALAUTTI ,
SERGIO GRECO ,
FRANCESCA SPEZZANO  and
IRINA TRUBITSYNA
MARCO CALAUTTI
Affiliation:
DIMES, Università della Calabria, 87036 Rende (CS), Italy (email: [email protected], [email protected], [email protected], [email protected])
SERGIO GRECO
Affiliation:
DIMES, Università della Calabria, 87036 Rende (CS), Italy (email: [email protected], [email protected], [email protected], [email protected])
FRANCESCA SPEZZANO
Affiliation:
DIMES, Università della Calabria, 87036 Rende (CS), Italy (email: [email protected], [email protected], [email protected], [email protected])
IRINA TRUBITSYNA
Affiliation:
DIMES, Università della Calabria, 87036 Rende (CS), Italy (email: [email protected], [email protected], [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Recently, there has been an increasing interest in the bottom-up evaluation of the semantics of logic programs with complex terms. The presence of function symbols in the program may render the ground instantiation infinite, and finiteness of models and termination of the evaluation procedure, in the general case, are not guaranteed anymore. Since the program termination problem is undecidable in the general case, several decidable criteria (called program termination criteria) have been recently proposed. However, current conditions are not able to identify even simple programs, whose bottom-up execution always terminates. The paper introduces new decidable criteria for checking termination of logic programs with function symbols under bottom-up evaluation, by deeply analyzing the program structure. First, we analyze the propagation of complex terms among arguments by means of the extended version of the argument graph called propagation graph. The resulting criterion, called acyclicity, generalizes most of the decidable criteria proposed so far. Next, we study how rules may activate each other and define a more powerful criterion, called safety. This criterion uses the so-called safety function able to analyze how rules may activate each other and how the presence of some arguments in a rule limits its activation. We also study the application of the proposed criteria to bound queries and show that the safety criterion is well-suited to identify relevant classes of programs and bound queries. Finally, we propose a hierarchy of classes of terminating programs, called k-safety, where the k-safe class strictly includes the (k-1)-safe class.

Keywords

Logic programming with function symbolsbottom-up executionprogram terminationstable models
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 15 , Issue 6 , November 2015 , pp. 854 - 889
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

This work refines and extends results from the conference paper (Greco et al. 2012).

References

Alviano, M., Faber, W. and Leone, N. 2010. Disjunctive asp with functions: Decidable queries and effective computation. Theory and Practice of Logic Programming 10, 4–6, 497–512.Google Scholar
Arts, T. and Giesl, J. 2000. Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 1–2, 133–178.Google Scholar
Baselice, S., Bonatti, P. A. and Criscuolo, G. 2009. On finitely recursive programs. Theory and Practice of Logic Programming 9, 2, 213–238.CrossRefGoogle Scholar
Beeri, C. and Ramakrishnan, R. 1991. On the power of magic. Journal of Logic Programming 10, 1–4, 255–299.CrossRefGoogle Scholar
Bonatti, P. A. 2004. Reasoning with infinite stable models. Artificial Intelligence 156, 1, 75–111.Google Scholar
Brockschmidt, M., Musiol, R., Otto, C. and Giesl, J. 2012. Automated termination proofs for java programs with cyclic data. In Proc. of 24th International Conference on Computer Aided Verification, Madhusudan, P. and Seshia, Sanjit A., Eds. Lecture Notes in Computer Science, vol. 7358. Springer-Verlag, Berlin, 105–122.Google Scholar
Bruynooghe, M., Codish, M., Gallagher, J. P., Genaim, S. and Vanhoof, W. 2007. Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems 29, 2.Google Scholar
Calimeri, F., Cozza, S., Ianni, G. and Leone, N. 2008. Computable functions in ASP: Theory and implementation. In Proc. of 24th International Conference on Logic Programming (ICLP), de la Banda, M. G. and Pontelli, E., Eds. Lecture Notes in Computer Science, vol. 5366. Springer-Verlag, Berlin, 407–424.Google Scholar
Codish, M., Lagoon, V. and Stuckey, P. J. 2005. Testing for termination with monotonicity constraints. In Proc. of 21st International Conference on Logic Programming (ICLP), Gabbrielli, M. and Gupta, G., Eds. Lecture Notes in Computer Science, vol. 3668. Springer-Verlag, Berlin, 326–340.Google Scholar
Endrullis, J., Waldmann, J. and Zantema, H. 2008. Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning 40, 2–3, 195–220.Google Scholar
Fagin, R., Kolaitis, P. G., Miller, R. J. and Popa, L. 2005. Data exchange: semantics and query answering. Theoretical Computer Science 336, 1, 89–124.Google Scholar
Ferreira, M. C. F. and Zantema, H. 1996. Total termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing 7, 2, 133–162.Google Scholar
Gebser, M., Kaufmann, B., Neumann, A. and Schaub, T. 2007a. clasp: A conflict-driven answer set solver. In Proc. of 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Baral, C., Brewka, G. and Schlipf, J., Eds. Lecture Notes in Computer Science, vol. 4483. Springer-Verlag, Berlin, 260–265.CrossRefGoogle Scholar
Gebser, M., Schaub, T. and Thiele, S. 2007b. Gringo: A new grounder for answer set programming. In Proc. of 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Baral, C., Brewka, G. and Schlipf, J., Eds. Lecture Notes in Computer Science, vol. 4483. Springer-Verlag, Berlin, 266–271.CrossRefGoogle Scholar
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proc. of 5th International Conference and Symposium on Logic Programming (ICLP/SLP), Kowalski, R. A. and Bowen, K. A., Eds. Series in Logic Programming, vol. 2. MIT Press, Cambridge, MA, 1070–1080.Google Scholar
Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New Generation Computing 9, 3/4, 365–386.CrossRefGoogle Scholar
Greco, G., Greco, S., Trubitsyna, I. and Zumpano, E. 2005. Optimization of bound disjunctive queries with constraints. Theory and Practice of Logic Programming 5, 6, 713–745.Google Scholar
Greco, S. 2003. Binding propagation techniques for the optimization of bound disjunctive queries. IEEE Transactions on Knowledge and Data Engineering 15, 2, 368–385.CrossRefGoogle Scholar
Greco, S. and Spezzano, F. 2010. Chase termination: A constraints rewriting approach. Proceedings of the VLDB Endowment (PVLDB) 3, 1, 93–104.CrossRefGoogle Scholar
Greco, S., Spezzano, F. and Trubitsyna, I. 2011. Stratification criteria and rewriting techniques for checking chase termination. Proceedings of the VLDB Endowment (PVLDB) 4, 11, 1158–1168.Google Scholar
Greco, S., Spezzano, F. and Trubitsyna, I. 2012. On the termination of logic programs with function symbols. In Proc. of International Conference on Logic Programming (Technical Communications), Dovier, A. and Santos Costa, V., Eds. LIPIcs, vol. 17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Budapest, Hungary, 323–333.Google Scholar
Krishnamurthy, R., Ramakrishnan, R. and Shmueli, O. 1996. A framework for testing safety and effective computability. Journal of Computer and System Sciences 52, 1, 100–124.Google Scholar
Leone, N., Pfeifer, G., Faber, W., Calimeri, F., Dell'Armi, T., Eiter, T., Gottlob, G., Ianni, G., Ielpa, G., Koch, K., Perri, S. and Polleres, A. 2002. The DLV system. In Proc. of 8th European Conference on Logics in Artificial Intelligence (JELIA), Flesca, S., Greco, S., Ianni, G. and Leonne, N., Eds. Lecture Notes in Computer Science, vol. 2424. Springer-Verlag, Berlin, 537–540.Google Scholar
Liang, S. and Kifer, M. 2013. A practical analysis of non-termination in large logic programs. Theory and Practice of Logic Programming 13, 4–5, 705–719.Google Scholar
Lierler, Y. and Lifschitz, V. 2009. One more decidable class of finitely ground programs. In Proc. of 25th International Conference on Logic Programming (ICLP), Hill, P. M. and Warren, D. S., Eds. Lecture Notes in Computer Science, vol. 5649. Springer-Verlag, Berlin, 489–493.Google Scholar
Marchiori, M. 1996. Proving existential termination of normal logic programs. In Proc. of 5th International Conference on Algebraic Methodology and Software Technology, Wirsing, M. and Nivat, M., Eds. Lecture Notes in Computer Science, vol. 1101. Springer-Verlag, Berlin, 375–390.CrossRefGoogle Scholar
Marnette, B. 2009. Generalized schema-mappings: From termination to tractability. In Proc. of 28th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS). Paredaens, J. and Su, J., Eds. ACM, New York, NY, 13–22.Google Scholar
Meier, M., Schmidt, M. and Lausen, G. 2009. On chase termination beyond stratification. CoRR abs/0906.4228.Google Scholar
Nguyen, M. T., Giesl, J., Schneider-Kamp, P. and Schreye, D. D. 2007. Termination analysis of logic programs based on dependency graphs. In Proc. of 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), King, A., Ed. Lecture Notes in Computer Science, vol. 4915. Springer-Verlag, Berlin, 8–22.Google Scholar
Nishida, N. and Vidal, G. 2010. Termination of narrowing via termination of rewriting. Applicable Algebra in Engineering, Communication and Computing 21, 3, 177–225.Google Scholar
Ohlebusch, E. 2001. Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing 12, 1/2, 73–116.Google Scholar
Schneider-Kamp, P., Giesl, J. and Nguyen, M. T. 2009b. The dependency triple framework for termination of logic programs. In Proc. of 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Schreye, D. D., Ed. Lecture Notes in Computer Science, vol. 6037. Springer-Verlag, Berlin, 37–51.Google Scholar
Schneider-Kamp, P., Giesl, J., Serebrenik, A. and Thiemann, R. 2009a. Automated termination proofs for logic programs by term rewriting. ACM Transactions on Computational Logic 11, 1.CrossRefGoogle Scholar
Schneider-Kamp, P., Giesl, J., Ströder, T., Serebrenik, A. and Thiemann, R. 2010. Automated termination analysis for logic programs with cut. Theory and Practice of Logic Programming 10, 4–6, 365–381.Google Scholar
Schreye, D. D. and Decorte, S. 1994. Termination of logic programs: The never-ending story. Journal of Logic Programming 19/20, 199–260.Google Scholar
Serebrenik, A. and De Schreye, D. 2005. On termination of meta-programs. Theory and Practice of Logic Programming 5, 3, 355–390.Google Scholar
Simons, P., Niemela, I. and Soininen, T. 2002. Extending and implementing the stable model semantics. Artificial Intelligence 138, 1–2, 181–234.CrossRefGoogle Scholar
Sternagel, C. and Middeldorp, A. 2008. Root-labeling. In Proc. of 19th International Conference on Rewriting Techniques and Applications, Voronkov, A., Ed. Lecture Notes in Computer Science, vol. 5117. Springer-Verlag, Berlin, 336–350.CrossRefGoogle Scholar
Ströder, T., Schneider-Kamp, P. and Giesl, J. 2010. Dependency triples for improving termination analysis of logic programs with cut. In Proc. of 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Alpuente, M., Ed. Lecture Notes in Computer Science, vol. 6564. Springer-Verlag, Berlin, 184–199.Google Scholar
Syrjänen, T. 2001. Omega-restricted logic programs. In Proc. of 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), Eiter, T., Faber, W. and Truszczynski, M. L., Eds. Lecture Notes in Computer Science, vol. 2173. Springer-Verlag, Berlin, 267–279.Google Scholar
Venturini Zilli, M. 1975. Complexity of the unification algorithm for first-order expressions. CALCOLO 12, 4, 361–371.Google Scholar
Voets, D. and Schreye, D. D. 2010. Non-termination analysis of logic programs using types. In Proc. of 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), Alpuente, M., Ed. Lecture Notes in Computer Science, vol. 6564. Springer-Verlag, Berlin, 133–148.Google Scholar
Zantema, H. 1995. Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 1/2, 89–105.CrossRefGoogle Scholar