Abstract
We extend Bove’s technique for formalising simple general recursive algrithms in constructive type theory to nested recursive algorithms. The method consists in defining an inductive special-purpose accessibility predicate, that characterizes the inputs on which the algorithm terminates. As a result, the type-theoretic version of the algorithm can be defined by structural recursion on the proof that the input values satisfy this predicate. This technique results in definitions in which the computational and logical parts are clearly separated; hence, the type-theoretic version of the algorithm is given by its purely functional content, similarly to the corresponding program in a functional programming language. In the case of nested recursion, the special predicate and the type-theoretic algorithm must be defined simultaneously, because they depend on each other. This kind of definitions is not allowed in ordinary type theory, but it is provided in type theories extended with Dybjer’s schema for simultaneous inductive-recursive definitions. The technique applies also to the formalisation of partial functions as proper type-theoretic functions, rather than relations representing their graphs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P. Aczel. An Introduction to Inductive Definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. North-Holland Publishing Company, 1977.
T. Altenkirch, V. Gaspes, B. Nordström, and B. von Sydow. A User’s Guide to ALF. Chalmers University of Technology, Sweden, May 1994. Available on the WWW ftp://ftp.cs.chalmers.se/pub/users/alti/alf.ps.Z.
P. Audebaud. Partial Objects in the Calculus of Constructions. In 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 86–95, July 1991.
Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In M. Aagaard, editors. Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science. Springer-Verlag, 2000. Harrison and Aagaard [HA00]}, pages 1–16.
A. Bove. Simple general recursion in type theory. Nordic Journal of Computing, 8(1):22–42, Spring 2001.
Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76:95–120, 1988.
R. L. Constable and N. P. Mendler. Recursive Definitions in Type Theory. In Logic of Programs, Brooklyn, volume 193 of Lecture Notes in Computer Science, pages 61–78. Springer-Verlag, June 1985.
R. L. Constable. Partial Functions in Constructive Type Theory. In Theoretical Computer Science, 6th GI-Conference, Dortmund, volume 145 of Lecture Notes in Computer Science, pages 1–18. Springer-Verlag, January 1983.
R. L. Constable and S. F. Smith. Partial Objects in Constructive Type Theory. In Logic in Computer Science, Ithaca, New York, pages 183–193, June 1987.
Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2), June 2000.
J. Giesl. Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning, 19:1–29, 1997.
J. Harrison and M. Aagaard, editors. Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
[JHe+99]_Simon Peyton Jones, John Hughes, (editors), Lennart Augustsson, Dave Barton, Brian Boutel, Warren Burton, Joseph Fasel, Kevin Hammond, Ralf Hinze, Paul Hudak, Thomas Johnsson, Mark Jones, John Launchbury, Erik Meijer, John Peterson, Alastair Reid, Colin Runciman, and Philip Wadler. Report on the Programming Language Haskell 98, a Non-strict, Purely Functional Language. Available from http://haskell.org, February 1999.
P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.
L. Magnusson and B. Nordström. The ALF proof editor and its proof engine. In Types for Proofs and Programs, volume 806 of LNCS, pages 213–237, Nijmegen, 1994. Springer-Verlag.
B. Nordström. Terminating General Recursion. BIT, 28(3):605–619, October 1988.
L. C. Paulson. Proving Termination of Normalization Functions for Conditional Expressions. Journal of Automated Reasoning, 2:63–74, 1986.
K. Slind. Another look at nested recursion. In M. Aagaard, editors. Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science. Springer-Verlag, 2000. Harrison and Aagaard [HA00]}, pages 498–518.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bove, A., Capretta, V. (2001). Nested General Recursion and Partiality in Type Theory. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_10
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive