Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Functional and Logic Programming

FLOPS 2016: Functional and Logic Programming pp 126–143Cite as

Proof Relevant Corecursive Resolution

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9613))

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.

P. Fu—This author is supported by EPSRC grant EP/K031864/1.

A. Pond—This author is supported by Carnegie Trust Scotland.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Note that here \( C \) is an eigenvariable.

  2. 2.

    The proof term can be type-checked with polymorphic recursion.

  3. 3.

    See the extended version for a detailed discussion.

  4. 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. 5.

    See the extended version for more examples and information about the implementation. Extended version is available from authors’ homepages.

  6. 6.

    See the extended version for a solution in Haskell using type family and more discussion.

References

  1. Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theor. Inf. Appl. 45(1), 3–33 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bird, R.S., Meertens, L.: Nested datatypes. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 52–67. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  4. Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  5. Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3, 69–115 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  6. Fu, P., Komendantskaya, E.: A type-theoretic approach to resolution. In: 25th International Symposium, LOPSTR 2015. Revised Selected Papers (2015)

    Google Scholar 

  7. Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundam. Inf. Spec. Issue Program Transform. 66(4), 353–366 (2005)

    MathSciNet  MATH  Google Scholar 

  8. Gimenez, C.E.: Un calcul de constructions infinies et son application a la vérification de systèmes communicants (1996)

    Google Scholar 

  9. Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types, vol. 7. Cambridge University Press, Cambridge (1989)

    MATH  Google Scholar 

  10. Hinze, R., Peyton-Jones, S.: Derivable type classes. Electron. Notes Theor. Comput. Sci. 41(1), 5–35 (2001)

    Article  MATH  Google Scholar 

  11. Hughes, J.: Restricted data types in Haskell. In: Haskell Workshop, vol. 99 (1999)

    Google Scholar 

  12. Johann, P., Ghani, N.: Haskell programming with nested types: a principled approach (2009)

    Google Scholar 

  13. Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications of ICLP 2015, July 2015

    Google Scholar 

  14. Jones, M.P.: Qualified Types: Theory and Practice, vol. 9. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  15. Jones, S.P., Jones, M., Meijer, E.: Type classes: an exploration of the design space. In: Haskell Workshopp (1997)

    Google Scholar 

  16. Komendantskaya, E., Johann, P. Structural resolution: a framework for coinductive proof search and proof construction in Horn clause logic. Submitted

    Google Scholar 

  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)

    Google Scholar 

  18. Lloyd, J.W.: Foundations of Logic Programming. Springer Science & Business Media, Heidelberg (1987)

    Book  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  20. Moss, L.S., Danner, N.: On the foundations of corecursion. Log. J. IGPL 5(2), 231–257 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  21. Plotkin, G.D.: A note on inductive generalization. Mach. Intell. 5, 153–163 (1970)

    MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Google Scholar 

  25. Zantema, H., Geser, A.: Non-looping rewriting. Universiteit Utrecht, Faculty of Mathematics & Computer Science (1996)

    Google Scholar 

Download references

Acknowledgements

We thank Patricia Johann and the FLOPS’16 reviewers for their helpful comments, and František Farka for many discussions. Part of this work was funded by the Flemish Fund for Scientific Research.

Author information

Authors and Affiliations

  1. Computer Science, University of Dundee, Dundee, UK

    Peng Fu, Ekaterina Komendantskaya & Andrew Pond

  2. Department of Computer Science, KU Leuven, Leuven, Belgium

    Tom Schrijvers

Authors
  1. Peng Fu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ekaterina Komendantskaya
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Tom Schrijvers
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Andrew Pond
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peng Fu .

Editor information

Editors and Affiliations

  1. Tohoku University, Sendai, Japan

    Oleg Kiselyov

  2. School of Computing, University of Kent, Canterbury, United Kingdom

    Andy King

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Fu, P., Komendantskaya, E., Schrijvers, T., Pond, A. (2016). Proof Relevant Corecursive Resolution. In: Kiselyov, O., King, A. (eds) Functional and Logic Programming. FLOPS 2016. Lecture Notes in Computer Science(), vol 9613. Springer, Cham. https://doi.org/10.1007/978-3-319-29604-3_9

Download citation

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

  • Published:

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-29604-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation