Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

A Productivity Checker for Logic Programming

verfasst von : Ekaterina Komendantskaya, Patricia Johann, Martin Schmidt

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators
Nächstes Kapitel Symbolic Abstract Contract Synthesis in a Rewriting Framework
Fußnoten
1
All proofs are in Appendix A, and corresponding pseudocode algorithms are in Appendix B, of the version of the paper at https://​arxiv.​org/​abs/​1608.​04415.
 
Literatur
1.
2.
3.
de Schreye, D., Decorte, S.: Termination of logic programs: the never-ending story. J. Logic Program. 19–20(Supplement 1), 199–260 (1994)MathSciNetCrossRefMATH
4.
5.
Endrullis, J., et al.: A coinductive framework for infinitary rewriting and equational reasoning. In: RTA, pp. 143–159 (2015)
6.
Fu, P., Komendantskaya, E.: Operational semantics of resolution and productivity in horn clause logic. Formal Aspects of Computing (2016)
7.
Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive logic programming and its applications. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 27–44. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-74610-2_​4 CrossRef
8.
9.
Johann, P., et al.: Structural resolution for logic programming. In: Technical Communications of ICLP (2015)
10.
Komendantskaya, E., et al.: Exploiting parallelism in coalgebraic logic programming. Electron. Notes Theor. Comput. Sci. 33, 121–148 (2014)CrossRefMATH
11.
Komendantskaya, E., et al.: Coalgebraic logic programming: from semantics to implementation. J. Logic Comput. 26(2), 745–783 (2016)MathSciNetCrossRefMATH
12.
Komendantskaya, E., Li, Y.: Productive corecursion in logic programming. In: Proceedings of ICLP 2017 (2017). arXiv:​1707.​01541. To appear in Journal of Theory and Practice of Logic Programming
13.
14.
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1988)MATH
15.
Nguyen, M.T., et al.: Termination analysis of logic programs based on dependency graphs. In: LPOSTR, pp. 8–22 (2007)
16.
Pfenning, F.: Types in Logic Programming. The MIT Press, Cambridge (1992)
17.
Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 197–213. Springer, Cham (2015). doi:10.​1007/​978-3-319-21401-6_​13 CrossRef
18.
Rohwedder, E., Pfenning, F.: Model and termination checking for higher-order logic programs. In: ESOP, pp. 296–310 (1996)
19.
20.
Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination analysis for logic programs by term rewriting. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 177–193. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-71410-1_​13 CrossRef
21.
Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: extending logic programming with coinduction. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 472–483. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-73420-8_​42 CrossRef
22.
Terese: Term Rewriting Systems. Cambridge University Press, New York (2003)
Metadaten
Titel
A Productivity Checker for Logic Programming
verfasst von
Ekaterina Komendantskaya
Patricia Johann
Martin Schmidt
Copyright-Jahr
2017
Buch
Logic-Based Program Synthesis and Transformation

Print ISBN: 978-3-319-63138-7

Electronic ISBN: 978-3-319-63139-4

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-63139-4_10