A productivity checker for logic programming

DOI10.1007/978-3-319-63139-4_10MaRDI QIDQ2409734zbMATH OpenOpenAlexFDO

Authors Ekaterina Komendantskaya, Patricia Johann, Martin Schmidt

Publication date 13 October 2017

Full work available at URL https://arxiv.org/abs/1608.04415

zbMATH Keywords

coinductioncorecursionlogic programmingproductivitytermination

Mathematics Subject Classification ID

Logic programming (68N17)

Abstract: Automated analysis of recursive derivations in logic programming is known to be a hard problem. Both termination and non-termination are undecidable problems in Turing-complete languages. However, some declarative languages offer a practical work-around for this problem, by making a clear distinction between whether a program is meant to be understood inductively or coinductively. For programs meant to be understood inductively, termination must be guaranteed, whereas for programs meant to be understood coinductively, productive non-termination (or "productivity") must be ensured. In practice, such classification helps to better understand and implement some non-terminating computations. Logic programming was one of the first declarative languages to make this distinction: in the 1980's, Lloyd and van Emden's "computations at infinity" captured the big-step operational semantics of derivations that produce infinite terms as answers. In modern terms, computations at infinity describe "global productivity" of computations in logic programming. Most programming languages featuring coinduction also provide an observational, or small-step, notion of productivity as a computational counterpart to global productivity. This kind of productivity is ensured by checking that finite initial fragments of infinite computations can always be observed to produce finite portions of their infinite answer terms. In this paper we introduce a notion of observational productivity for logic programming as an algorithmic approximation of global productivity, give an effective procedure for semi-deciding observational productivity, and offer an implemented automated observational productivity checker for logic programs.

Recommendations

• Productive corecursion in logic programming
• scientific article; zbMATH DE number 1670488
• PROVING PRODUCTIVITY IN INFINITE DATA STRUCTURES
• Infinite computation, co-induction and computational logic
• Automated Termination Analysis for Logic Programs by Term Rewriting

Cited in

(9)

• Logic programming: laxness and saturation
• Enhancing expressivity of checked corecursive streams
• Operational semantics of resolution and productivity in Horn clause logic
• Productive corecursion in logic programming
• scientific article; zbMATH DE number 7376040 (Why is no real title available?)
• Flexible coinductive logic programming
• Complexity of Fractran and Productivity
• Checked corecursive streams: expressivity and completeness
• Checking equivalence of corecursive streams: an inductive procedure

Describes a project that uses

Uses Software

• CoALP

This page was built for publication: A productivity checker for logic programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2409734)