Hostname: page-component-78c5997874-mlc7c Total loading time: 0 Render date: 2024-11-06T09:17:41.437Z Has data issue: false hasContentIssue false
  • English
  • Français

Productive corecursion in logic programming*

Published online by Cambridge University Press:  22 August 2017

EKATERINA KOMENDANTSKAYA  and
YUE LI Open the ORCID record for YUE LI [Opens in a new window]
EKATERINA KOMENDANTSKAYA
Affiliation:
Heriot-Watt University, Edinburgh, Scotland, UK (e-mails: [email protected], [email protected])
YUE LI
Affiliation:
Heriot-Watt University, Edinburgh, Scotland, UK (e-mails: [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental and important undecidable property is productivity. If a derivation is infinite and coinductively sound, we may ask whether the computed answer it determines actually computes an infinite formula. If it does, the infinite computation is productive. This intuition was first expressed under the name of computations at infinity in the 80s. In modern days of the Internet and stream processing, its importance lies in connection to infinite data structure processing. Recently, an algorithm was presented that semi-decides a weaker property – of productivity of logic programs. A logic program is productive if it can give rise to productive derivations. In this paper, we strengthen these recent results. We propose a method that semi-decides productivity of individual derivations for regular formulae. Thus, we at last give an algorithmic counterpart to the notion of productivity of derivations in logic programming. This is the first algorithmic solution to the problem since it was raised more than 30 years ago. We also present an implementation of this algorithm.

Keywords

Horn clauses(co)recursion(co)inductioninfinite term treesproductivity
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 17 , Special Issue 5-6: 33rd International Conference on Logic Programming , September 2017 , pp. 906 - 923
Copyright
Copyright © Cambridge University Press 2017 

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 has been partially supported by EPSRC grant EP/K031864/1-2.

References

Aczel, P. 1977. An introduction to inductive definitions. Studies in Logic and the Foundations of Mathematics 90, 739–782.CrossRefGoogle Scholar
Ancona, D. and Dovier, A. 2015. A theoretical perspective of coinductive logic programming. Fundamenta Informaticae 140, 3–4, 221–246.CrossRefGoogle Scholar
Colmerauer, A. 1982. Prolog and Infinite Trees. Academic Press.Google Scholar
Courcelle, B. 1983. Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169.Google Scholar
Davison, A. 2002. Logic programming languages for the internet. In Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part I, Kakas, A. C. and Sadri, F., Eds. Springer-Verlag, London, UK, 66–104.Google Scholar
Fu, P. and Komendantskaya, E. 2017. Operational semantics of resolution and productivity in Horn Clause logic. Journal on Formal Aspects of Computing 29, 3, 453–474.Google Scholar
Fu, P., Komendantskaya, E., Schrijvers, T. and Pond, A. 2016. Proof relevant corecursive resolution. In FLOPS'16. Lecture Notes in Computer Science, vol. 9613. Springer, 126–143.Google Scholar
Gupta, G., Bansal, A., Min, R., Simon, L. and Mallya, A. 2007. Coinductive logic programming and its applications. In ICLP, 27–44.Google Scholar
Heintze, N. and Jaffar, J. 1992. Semantic types for logic programs. In Types in Logic Programming, Pfening, F., ed. The MIT Press, 141–155.Google Scholar
Jaffar, J. and Stuckey, P. J. 1986. Semantics of infinite tree logic programming. Theoretical Computer Science 46, 3, 141–158.CrossRefGoogle Scholar
Johann, P., Komendantskaya, E. and Komendantskiy, V. 2015. Structural resolution for logic programming. In Proc. of Technical Communications of ICLP.Google Scholar
Komendantskaya, E., Johann, P. and Schmidt, M. 2017. A productivity checker for logic programming. Logic-Based Program Synthesis and Transformation, In Proc. of 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6–8, 2016, Revised Selected Papers. Hermenegildo, M. V. and Lopez-Garcia, P., Eds. Springer International Publishing, 168–186.Google Scholar
Komendantskaya, E., Power, J. and Schmidt, M. 2016. Coalgebraic logic programming: From semantics to implementation. Journal of Logic and Computation 26, 2, 745–783.Google Scholar
Li, Y. 2017. Structural resolution with coinductive loop detection. In Post-Proc. of CoALP-Ty'16, Komendantskaya, E. and Power, J., Eds. Open Publishing Association, to appear in.Google Scholar
Lloyd, J. 1988. Foundations of Logic Programming, 2nd ed. Springer-Verlag.Google Scholar
Proietti, M. and Pettorossi, A. 1995. Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142, 1, 89–124.CrossRefGoogle Scholar
Sangiorgi, D. 2011. Introduction to Bisimulation and Coinduction. Cambridge University Press.CrossRefGoogle Scholar
Senni, V., Pettorossi, A. and Proietti, M. 2008. A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs. Springer, Berlin, Heidelberg, 284–300.Google Scholar
Shen, Y.-D., You, J.-H., Yuan, L.-Y., Shen, S. S. P. and Yang, Q. 2003. A dynamic approach to characterizing termination of general logic programs. ACM Transactions on Computational Logic 4, 4, 417–430.CrossRefGoogle Scholar
Simon, L., Bansal, A., Mallya, A. and Gupta, G. 2007. Co-logic programming: Extending logic programming with coinduction. In Proc. of ICALP, 472–483.Google Scholar
Simon, L., Mallya, A., Bansal, A. and Gupta, G. 2006. Coinductive logic programming. In ICLP'06, 330–345.Google Scholar
van Emden, M. H. and Abdallah, M. A. N. 1985. Top-down semantics of fair computations of logic programs. Journal of Logic Programming 2, 1, 67–75.Google Scholar
Supplementary material: PDF

Komendantskaya and Li supplementary material

Online Appendix

Download Komendantskaya and Li supplementary material(PDF)
PDF 167.6 KB