Hostname: page-component-78c5997874-94fs2 Total loading time: 0 Render date: 2024-11-20T04:00:54.619Z Has data issue: false hasContentIssue false
  • English
  • Français

Flexible coinductive logic programming

Published online by Cambridge University Press:  22 September 2020

FRANCESCO DAGNINO ,
DAVIDE ANCONA Open the ORCID record for DAVIDE ANCONA [Opens in a new window]  and
ELENA ZUCCA
FRANCESCO DAGNINO
Affiliation:
DIBRIS, University of Genova (e-mail: [email protected], [email protected], [email protected])
DAVIDE ANCONA
Affiliation:
DIBRIS, University of Genova (e-mail: [email protected], [email protected], [email protected])
ELENA ZUCCA
Affiliation:
DIBRIS, University of Genova (e-mail: [email protected], [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

coinductionoperational semanticsdeclarative semanticssoundnesscompleteness
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 20 , Issue 6: 36th International Conference on Logic Programming Special Issue II , November 2020 , pp. 818 - 833
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

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.)

References

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.Google Scholar
Adámek, J., Milius, S., and Velebil, J. 2006. Iterative algebras at work. Mathematical Structures in Computer Scienc 16, 6, 1085–1131.CrossRefGoogle Scholar
Ancona, D. 2013. Regular corecursion in prolog. Comput. Lang. Syst. Struct. 39, 4, 142–162.Google Scholar
Ancona, D., Dagnino, F., Rot, J., and Zucca, E. 2020. A big step from finite to infinite computations. Science of Computer Programming 197, 102492.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
Ancona, D. and Dovier, A. 2015. A theoretical perspective of coinductive logic programming. Fundamenta Informaticae 140, 3-4, 221–246.CrossRefGoogle Scholar
Apt, K. R. 1997. From logic programming to Prolog . Prentice Hall International series in computer science. Prentice Hall.Google Scholar
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.Google Scholar
Courcelle, B. 1983. Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169.Google Scholar
Dagnino, F. 2017. Generalizing inference systems by coaxioms. M.S. thesis, DIBRIS, University of Genova. Best italian master thesis in Theoretical Computer Science 2018.Google Scholar
Dagnino, F. 2019. Coaxioms: flexible coinductive definitions by inference systems. Logical Methods in Computer Science 15, 1.Google Scholar
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.Google Scholar
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 in Computer Science, Corradini, A., Klin, B., and Crstea, C., Eds. Lecture Notes in Computer Science, vol. 6859. Springer, 40–54.Google Scholar
Komendantskaya, E. et al. 2016. Coalgebraic logic programming: from semantics to implementation. J. Logic and Computation 26, 2, 745.CrossRefGoogle Scholar
Komendantskaya, E. et al. 2017. A productivity checker for logic programming. Post-proc. LOPSTR’16.Google Scholar
Komendantskaya, E. and Li, Y. 2017. Productive corecursion in logic programming. Theory Pract. Log. Program. 17, 5-6, 906–923.CrossRefGoogle Scholar
Leroy, X. and Grall, H. 2009. Coinductive big-step operational semantics. Information and Computation 207, 2, 284–304.Google Scholar
Li, Y. 2017. Structural resolution with coinductive loop detection. In Post-proceedings of CoALP-Ty’16, Komendantskaya, E. and Power, J., Eds.Google Scholar
Lloyd, J. W. 1987. Foundations of Logic Programming, 2nd Edition. Springer.Google Scholar
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.Google Scholar
Mantadelis, T., Rocha, R., and Moura, P. 2014. Tabling, rational terms, and coinduction finally together! TPLP 14, 4-5, 429–443.Google Scholar
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.Google Scholar
Simon, L. 2006. Extending logic programming with coinduction. Ph.D. thesis, University of Texas at Dallas.Google Scholar
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 in Computer Science, vol. 4596. Springer, 472–483.Google Scholar
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.Google Scholar
Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 2, 285–309.CrossRefGoogle Scholar