×

Flexible coinductive logic programming. (English) Zbl 1468.68054

Summary: Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched by coclauses, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels.

MSC:

68N17 Logic programming
68Q55 Semantics in the theory of computing

Software:

CoALP
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Aczel, P.1977. An introduction to inductive definitions. In Handbook of Mathematical Logic, J. Barwise, Ed. Studies in Logic and the Foundations of Mathematics, vol. 90. Elsevier, 739-782.
[2] Adámek, J., Milius, S., and Velebil, J.2006. Iterative algebras at work. Mathematical Structures in Computer Scienc 16, 6, 1085-1131. · Zbl 1112.18005
[3] Ancona, D.2013. Regular corecursion in prolog. Comput. Lang. Syst. Struct. 39,4, 142-162.
[4] Ancona, D., Dagnino, F., Rot, J., and Zucca, E.2020. A big step from finite to infinite computations. Science of Computer Programming 197, 102492.
[5] Ancona, D., Dagnino, F., and Zucca, E.2017a. Extending coinductive logic programming with co-facts. In First Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty’16, Komendantskaya, E. and Power, J., Eds. Electronic Proceedings in Theoretical Computer Science, vol. 258. Open Publishing Association, 1-18.
[6] Ancona, D., Dagnino, F., and Zucca, E.2017b. Generalizing inference systems by coaxioms. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, H. Yang, Ed. Notes, Lecture in Computer Science, vol. 10201. Springer, Berlin, 29-55. · Zbl 1485.68053
[7] Ancona, D., Dagnino, F., and Zucca, E.2018. Modeling infinite behaviour by corules. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018, T. D. Millstein, Ed. LIPIcs, vol. 109. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl, 21:1-21:31.
[8] Ancona, D. and Dovier, A.2015. A theoretical perspective of coinductive logic programming. Fundamenta Informaticae 140, 3-4, 221-246. · Zbl 1348.68028
[9] Apt, K. R.1997. From logic programming to Prolog. Prentice Hall International series in computer science. Prentice Hall.
[10] Basold, H., Komendantskaya, E., and Li, Y.2019. Coinduction in uniform: Foundations for corecursive proof search with horn clauses. In ESOP 2019, L. Caires, Ed. Notes, Lecture in Computer Science, vol. 11423. Springer, 783-813.
[11] Courcelle, B.1983. Fundamental properties of infinite trees. Theoretical Computer Science 25, 95-169. · Zbl 0521.68013
[12] Dagnino, F.2017. Generalizing inference systems by coaxioms. M.S. thesis, DIBRIS, University of Genova. Best italian master thesis in Theoretical Computer Science 2018. · Zbl 1485.68053
[13] Dagnino, F.2019. Coaxioms: flexible coinductive definitions by inference systems. Logical Methods in Computer Science 15, 1. · Zbl 1432.68251
[14] Dagnino, F.2020. Foundations of regular coinduction. Tech. rep., DIBRIS, University of Genova. May. Available at https://arxiv.org/abs/2006.02887. Submitted for journal publication.
[15] Gupta, G., Saeedloei, N., Devries, B. W., Min, R., Marple, K., and Kluzniak, F.2011. Infinite computation, co-induction and computational logic. In CALCO 2011 - Algebra and Coalgebra inComputer Science, Corradini, A., Klin, B., and Crstea, C., Eds. Lecture Notes in Computer Science, vol. 6859. Springer, 40-54. · Zbl 1344.68053
[16] Komendantskaya, E.et al.2016. Coalgebraic logic programming: from semantics to implementation. J. Logic and Computation 26, 2, 745. · Zbl 1344.68044
[17] Komendantskaya, E.et al.2017. A productivity checker for logic programming. Post-proc. LOPSTR’16. · Zbl 1485.68037
[18] Komendantskaya, E. and Li, Y.2017. Productive corecursion in logic programming. Theory Pract. Log. Program. 17,5-6, 906-923. · Zbl 1422.68025
[19] Leroy, X. and Grall, H.2009. Coinductive big-step operational semantics. Information and Computation 207, 2, 284-304. · Zbl 1165.68044
[20] Li, Y.2017. Structural resolution with coinductive loop detection. In Post-proceedings of CoALP-Ty’16, Komendantskaya, E. and Power, J., Eds.
[21] Lloyd, J. W.1987. Foundations of Logic Programming, 2nd Edition. Springer. · Zbl 0668.68004
[22] Löding, C. and Tollkötter, A.2016. Transformation between regular expressions and omega-automata. In 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, Faliszewski, P., Muscholl, A., and Niedermeier, R., Eds. LIPIcs, vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 88:1-88:13. · Zbl 1398.68319
[23] Mantadelis, T., Rocha, R., and Moura, P.2014. Tabling, rational terms, and coinduction finally together! TPLP 14, 4-5, 429-443. · Zbl 1307.68019
[24] Moura, P.2013. A portable and efficient implementation of coinductive logic programming. In Practical Aspects of Declarative Languages - 15th International Symposium, PADL 2013, Rome, Italy, January 21-22, 2013. Proceedings. 77-92.
[25] Simon, L.2006. Extending logic programming with coinduction. Ph.D. thesis, University of Texas at Dallas.
[26] Simon, L., Bansal, A., Mallya, A., and Gupta, G.2007. Co-logic programming: Extending logic programming with coinduction. In Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Arge, L., Cachin, C., Jurdzinski, T., and Tarlecki, A., Eds. Lecture Notes inComputer Science, vol. 4596. Springer, 472-483. · Zbl 1171.68404
[27] Simon, L., Mallya, A., Bansal, A., and Gupta, G.2006. Coinductive logic programming. In Logic Programming, 22nd International Conference, ICLP 2006, Etalle, S. and Truszczynski, M., Eds. Lecture Notes in Computer Science, vol. 4079. Springer, 330-345. · Zbl 1131.68400
[28] Tarski, A.1955. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 2, 285-309. · Zbl 0064.26004
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.