A productivity checker for logic programming

Ekaterina Komendantskaya, Patricia Johann, Martin Schmidt

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

Automated analysis of recursive derivations in logic programming is known to be a hard problem. Both termination and nontermination 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 nonterminating 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.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation. LOPSTR 2016
PublisherSpringer
Pages168-186
Number of pages19
ISBN (Electronic)9783319631394
ISBN (Print)9783319631387
DOIs
Publication statusPublished - 25 Jul 2017
Event26th International Symposium on Logic-Based Program Synthesis and Transformation 2016 - Edinburgh, United Kingdom
Duration: 6 Sep 20168 Sep 2016

Publication series

NameLecture Notes in Computer Science
Volume10184
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Symposium on Logic-Based Program Synthesis and Transformation 2016
Abbreviated titleLOPSTR 2016
Country/TerritoryUnited Kingdom
CityEdinburgh
Period6/09/168/09/16

Keywords

  • Coinduction
  • Corecursion
  • Logic programming
  • Productivity
  • Termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A productivity checker for logic programming'. Together they form a unique fingerprint.

Cite this