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:
Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Proof Relevant Corecursive Resolution

verfasst von : Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond

Erschienen in: Functional and Logic Programming

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Resolution lies at the foundation of both logic programming and type class context reduction in functional languages. Terminating derivations by resolution have well-defined inductive meaning, whereas some non-terminating derivations can be understood coinductively. Cycle detection is a popular method to capture a small subset of such derivations. We show that in fact cycle detection is a restricted form of coinductive proof, in which the atomic formula forming the cycle plays the rôle of coinductive hypothesis.
This paper introduces a heuristic method for obtaining richer coinductive hypotheses in the form of Horn formulas. Our approach subsumes cycle detection and gives coinductive meaning to a larger class of derivations. For this purpose we extend resolution with Horn formula resolvents and corecursive evidence generation. We illustrate our method on non-terminating type class resolution problems.

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 Executable Relational Specifications of Polymorphic Type Systems Using Prolog
Nächstes Kapitel A Coq Library for Internal Verification of Running-Times
Fußnoten
1
Note that here \( C \) is an eigenvariable.
 
2
The proof term can be type-checked with polymorphic recursion.
 
3
See the extended version for a detailed discussion.
 
4
Note that we abuse notation here to denote contexts with multiple holes. Also we abbreviate identical instantiation of \(\mathcal {C}[D, \ldots , D]\) those multiple holes to \(\mathcal {C}[D]\).
 
5
See the extended version for more examples and information about the implementation. Extended version is available from authors’ homepages.
 
6
See the extended version for a solution in Haskell using type family and more discussion.
 
Literatur
1.
Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theor. Inf. Appl. 45(1), 3–33 (2011)MathSciNetCrossRefMATH
2.
Bird, R.S., Meertens, L.: Nested datatypes. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 52–67. Springer, Heidelberg (1998)CrossRef
3.
Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Gurevich Festschrift II 2015. LNCS, vol. 9300, pp. 24–51. Springer, Heidelberg (2015)CrossRef
4.
Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806. Springer, Heidelberg (1994)CrossRef
5.
6.
Fu, P., Komendantskaya, E.: A type-theoretic approach to resolution. In: 25th International Symposium, LOPSTR 2015. Revised Selected Papers (2015)
7.
Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundam. Inf. Spec. Issue Program Transform. 66(4), 353–366 (2005)MathSciNetMATH
8.
Gimenez, C.E.: Un calcul de constructions infinies et son application a la vérification de systèmes communicants (1996)
9.
Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types, vol. 7. Cambridge University Press, Cambridge (1989)MATH
10.
Hinze, R., Peyton-Jones, S.: Derivable type classes. Electron. Notes Theor. Comput. Sci. 41(1), 5–35 (2001)CrossRefMATH
11.
Hughes, J.: Restricted data types in Haskell. In: Haskell Workshop, vol. 99 (1999)
12.
Johann, P., Ghani, N.: Haskell programming with nested types: a principled approach (2009)
13.
Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications of ICLP 2015, July 2015
14.
Jones, M.P.: Qualified Types: Theory and Practice, vol. 9. Cambridge University Press, Cambridge (2003)MATH
15.
Jones, S.P., Jones, M., Meijer, E.: Type classes: an exploration of the design space. In: Haskell Workshopp (1997)
16.
Komendantskaya, E., Johann, P. Structural resolution: a framework for coinductive proof search and proof construction in Horn clause logic. Submitted
17.
Lämmel, R., Peyton-Jones, S.: Scrap your boilerplate with class: extensible generic functions. In: Proceedings of 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, pp. 204–215, New York, NY, USA. ACM (2005)
18.
Lloyd, J.W.: Foundations of Logic Programming. Springer Science & Business Media, Heidelberg (1987)CrossRefMATH
19.
Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Log. 51(1), 125–157 (1991)MathSciNetCrossRefMATH
20.
21.
22.
Simon, L., Gupta, G., Mallya, A., Bansal, A.: 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)CrossRef
23.
Sulzmann, M., Duck, G.J., Peyton Jones, S.L., Stuckey, P.J.: Understanding functional dependencies via constraint handling rules. J. Funct. Program. 17(1), 83–129 (2007)CrossRefMATH
24.
Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 60–76. ACM (1989)
25.
Zantema, H., Geser, A.: Non-looping rewriting. Universiteit Utrecht, Faculty of Mathematics & Computer Science (1996)
Metadaten
Titel
Proof Relevant Corecursive Resolution
verfasst von
Peng Fu
Ekaterina Komendantskaya
Tom Schrijvers
Andrew Pond
Copyright-Jahr
2016
Buch
Functional and Logic Programming

Print ISBN: 978-3-319-29603-6

Electronic ISBN: 978-3-319-29604-3

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-29604-3_9