Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 1996: Theorem Proving in Higher Order Logics pp 381–397Cite as

Function definition in higher-order logic

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1125))

Abstract

We use a formally proven wellfounded recursion theorem as the basis upon which to build a function definition facility for Higher Order Logic. This approach offers flexibility in the choice of wellfounded relations used, the deferral of termination arguments, and automatic isolation of termination conditions. Building on this platform, we provide the ability to define recursive functions via pattern matching. The system is parameterized and has been instantiated to quite different theorem provers.

Research supported by DFG grant Br 887/4-2, Deduktive Programmentwicklung

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Agerholm. LCF examples in HOL. The Computer Journal, 38(2):121–130, July 1995.

    Article  Google Scholar 

  2. S. Agerholm. Non-primitive recursive function definition. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications (LNCS 971), pages 17–31, Aspen Grove, Utah, September 1995. Springer Verlag.

    Google Scholar 

  3. Lennart Augustsson. Compiling pattern matching. In J.P. Jouannaud, editor, Conference on Functional Programming Languages and Computer Architecture (LNCS 201), pages 368–381, Nancy, France, 1985.

    Google Scholar 

  4. Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, 1979.

    Google Scholar 

  5. A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62:185–253, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  6. Simon Finn, Mike Fourman, and John Longley. Partial functions in a total setting. To appear in Journal of Automated Reasoning, 1996.

    Google Scholar 

  7. Juergen Giesl. Termination analysis for functional programs using term orderings. In Proceedings of the 2nd International Static Analysis Symposium, Glasgow, Scotland, 1995. Springer-Verlag.

    Google Scholar 

  8. H. Busch. Unification based induction. In L.J.M. Claesen and M.J.C. Gordon, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 97–116, Leuven, Belgium, September 1992. IFIP TC10/WG10.2, North-Holland. IFIP Transactions.

    Google Scholar 

  9. P. V. Homeier and D. F. Martin. A verified verification condition generator. The Computer Journal, 38(2):131–141, July 1995.

    Article  Google Scholar 

  10. Peter Johnstone. Notes on logic and set theory. Cambridge University Press, 1987.

    Google Scholar 

  11. Delia Kesner, Laurence Puel, and Val Tannen. A typed pattern calculus. Information and Computation, 124(4):32–61, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  12. Lena Magnusson and Bengt Nordstrom. The ALF proof editor and its proof engine. In Types for Proofs and Programs (LNCS 806), pages 213–237, Nijmegen, Netherlands, 1994. Springer-Verlag.

    Google Scholar 

  13. Pascal Manoury. A user's friendly syntax to define recursive functions as typed λ-terms. In Types for Proofs and Programs: International Workshop TYPES'94, number 996 in Lecture Notes in Computer Science, Baastad, Sweden, June 1995. Springer Verlag.

    Google Scholar 

  14. Pascal Manoury and Marianne Simonot. Automatizing termination proofs of recursively defined functions. Theoretical Computer Science, (135):319–343, 1994.

    Google Scholar 

  15. Tom Melham. Automating recursive type definitions in higher order logic. In Graham Birtwistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer-Verlag, 1989.

    Google Scholar 

  16. Tobias Nipkow. Term rewriting and beyond—theorem proving in Isabelle. Formal Aspects of Computing, 1:320–338, 1989.

    Article  Google Scholar 

  17. Bengt Nordstrom. Terminating general recursion. BIT, 28:605–619, 1988.

    Article  MathSciNet  Google Scholar 

  18. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, LNAI 607, pages 748–752, Saratoga Springs, New York, USA, June 15–18, 1992. Springer-Verlag.

    Google Scholar 

  19. Lawrence Paulson. A higher order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  20. Lawrence Paulson. Constructing recursion operators in intuitionistic type theory. Journal of Symoblic Computation, 2:325–355, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  21. Lawrence Paulson. Proving termination of normalization functions for conditional expressions. Journal of Automated Reasoning, 2:63–74, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  22. Franz Regensburger. HOLCF: Eine konservative Einbettung von LCF in HOL. PhD thesis, Institut für Informatik, Technische Universität München, 1994.

    Google Scholar 

  23. H. Schwichtenberg and S. Wainer. Ordinal bounds for programs. In Jeff Remmel, editor, Feasible Mathematics II, pages 387–406. Birkhäuser, 1994.

    Google Scholar 

  24. M. van der Voort. Introducing well-founded function definitions in HOL. Leuven, Belgium, September 1992. IFIP TC10/WG10.2, Elsevier Science Publishers.

    Google Scholar 

  25. Christoph Walther. On proving the termination of algorithms by machine. Artificial Intelligence, 71(1):101–157, 1994.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Technische Universität München, 80290, München, Germany

    Konrad Slind

Authors
  1. Konrad Slind
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gerhard Goos Juris Hartmanis Jan van Leeuwen Joakim von Wright Jim Grundy John Harrison

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Slind, K. (1996). Function definition in higher-order logic. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1996. Lecture Notes in Computer Science, vol 1125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0105417

Download citation

  • DOI: https://doi.org/10.1007/BFb0105417

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61587-3

  • Online ISBN: 978-3-540-70641-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation