article

Modelling general recursion in type theory

Authors:

Venanzio CaprettaAuthors Info & Claims

Mathematical Structures in Computer Science, Volume 15, Issue 4

Pages 671 - 708

https://doi.org/10.1017/S0960129505004822

Published: 01 August 2005 Publication History

Abstract

Constructive type theory is an expressive programming language in which both algorithms and proofs can be represented. A limitation of constructive type theory as a programming language is that only terminating programs can be defined in it. Hence, general recursive algorithms have no direct formalisation in type theory since they contain recursive calls that satisfy no syntactic condition guaranteeing termination. In this work, we present a method to formalise general recursive algorithms in type theory. Given a general recursive algorithm, our method is to define an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm is then defined by structural recursion on the proof that the input values satisfy this predicate. The method separates the computational and logical parts of the definitions and thus the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Here, we give a formal definition of the method and discuss its power and its limitations.

References

[1]

Abel, A. (2004) Termination checking with types. In: Fix Points in Computer Science 2003 (FICS03). Special issue of Theoretical Informatics and Applications (RAIRO).

[2]

Aczel, P. (1977) An Introduction to Inductive Definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, North-Holland Publishing Company 739-782.

[3]

Balaa, A. and Bertot, Y. (2000) Fix-point equations for well-founded recursion in type theory. In: Harrison, J. and Aagaard, M. (eds.) Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000. Springer-Verlag Lecture Notes in Computer Science 1869 1-16.

[4]

Balaa, A. and Bertot, Y. (2002) Fonctions récursives générales par itération en théorie des types. Journées Francophones des Langages Applicatifs JFLA02, INRIA.

[5]

Barendregt, H. and Geuvers, H. (2001) Proof-assistants using dependent type systems. In: Robinson, A. and Voronkov, A. (eds.) Handbook of Automated Reasoning, Chapter 18, Elsevier 1149-1238.

[6]

Barendregt, H. P. (1992) Lambda calculi with types. In: Abramsky, S., Gabbay, D. M. and Maibaum, T. S. E. (eds.) Handbook of Logic in Computer Science 2, Oxford University Press, 117-309.

[7]

Barthe, G., Frade, M., Giménez, E., Pinto, L. and Uustalu, T. (2004) Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14 (1)97-141.

[8]

Bell, J. L. and Machover, M. (1977) A course in mathematical logic, North-Holland.

[9]

Bertot, Y., Capretta, V. and Barman, K. D. (2002) Type-theoretic functional semantics. In: Carreno, V. A., Munoz, C. A. and Tahar, S. (eds.) Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002. Springer-Verlag Lecture Notes in Computer Science 2410 83-97.

[10]

Bove, A. (1999) Programming in Martin-Löf type theory: Unification - A non-trivial example, Licentiate Thesis of the Department of Computer Science, Chalmers University of Technology. (Available at http://www.cs.chalmers.se/~bove/Papers/lic_thesis.ps.gz.)

[11]

Bove, A. (2001) Simple general recursion in type theory. Nordic Journal of Computing 8 (1) 22-42.

Digital Library

[12]

Bove, A. (2002a) General Recursion in Type Theory, Ph. D. thesis, Chalmers University of Technology, Department of Computing Science. (Available at http://www.cs.chalmers.se/ ~bove/Papers/phd_thesis.ps.gz.)

[13]

Bove, A. (2002b) Mutual general recursion in type theory. Technical Report, Chalmers University of Technology. (Available at http://www.cs.chalmers.se/~bove/Papers/mutual_rec.ps.gz.)

[14]

Bove, A. (2003) General recursion in type theory. In: Geuvers, H. and Wiedijk, F. (eds.) Types for Proofs and Programs, International Workshop TYPES 2002, The Netherlands. Springer-Verlag Lecture Notes in Computer Science 2646 39-58.

[15]

Bove, A. and Capretta, V. (2001) Nested general recursion and partiality in type theory. In: Boulton, R. J. and Jackson, P. B. (eds.) Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001. Springer-Verlag Lecture Notes in Computer Science 2152 121-135.

[16]

Bove, A. and Capretta, V. (2005) Recursive functions with higher order domains. In: Urzyczyn, P. (ed.) Typed Lambda Calculi and Applications. 7th International Conference, TLCA 2005, Nara, Japan. Springer-Verlag Lecture Notes in Computer Science 3461 116-130.

[17]

Bundy, A. (2001) The automation of proof by mathematical induction. In: Robinson, A. and Voronkov, A. (eds.) Handbook of Automated Reasoning 1, Elsevier Science and MIT Press 845- 912.

[18]

Capretta, V. (2002) Abstraction and Computation, Ph. D thesis, Computing Science Institute, University of Nijmegen.

[19]

Carreno, V. A., Munoz, C. A. and Tahar, S. (eds.) (2002) Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002. Springer-Verlag Lecture Notes in Computer Science 2410.

[20]

Coquand, T. and Huet, G. (1988) The Calculus of Constructions. Information and Computation 76 95-120.

Digital Library

[21]

Coquand, T., Nordström, B., Smith, J. M. and von Sydow, B. (1994) Type theory and programming. EATCS 52.

[22]

Coquand, T. and Paulin, C. (1990) Inductively defined types. In: Martin-Löf, P. (ed.) Proceedings of Colog'88. Springer-Verlag Lecture Notes in Computer Science 417.

[23]

de Mast, P., Jansen, J.-M., Bruin, D., Fokker, J., Koopman, P., Smetsers, S., van Eekelen, M. and Plasmeijer, R. (2001) Functional Programming in Clean, Computing Science Institute, University of Nijmegen.

[24]

Dubois, C. and Donzeau-Gouge, V. V. (1998) A step towards the mechanization of partial functions: Domains as inductive predicates. In: Kerber, M. (ed.) CADE-15, The 15th International Conference on Automated Deduction. WORKSHOP Mechanization of Partial Functions 53-62.

[25]

Dybjer, P. (2000) A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic 65 (2).

[26]

Finn, S., Fourman, M. and Longley, J. (1997) Partial functions in a total setting. Journal of Automated Reasoning 18 (1) 85-104.

[27]

Hagino, T. (1987) A Categorical Programming Language, Ph. D. thesis, University of Edinburgh.

[28]

Howard, W. A. (1980) The formulae-as-types notion of construction. In: Seldin, J. P. and Hindley, J. R. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press 479-490.

[29]

Hutter, D. (1992) Automatisierung der vollständigen Induktion, Oldenbourg Verlag.

[30]

Jones, S. P., (ed.) (2003) Haskell 98 Language and Libraries. The Revised Report, Cambridge University Press.

[31]

Manna, Z. and McCarthy, J. (1970) Properties of programs and partial function logic. Machine Intelligence 5 27-37.

[32]

Martin-Löf, P. (1984) Intuitionistic Type Theory, Bibliopolis, Napoli.

[33]

McBride, C. and McKinna, J. (2004) The view from the left. Journal of Functional Programming 14 (1) 69-111.

Digital Library

[34]

Milner, R., Tofte, M., Harper, R. and MacQueen, D. (1997) The Definition of Standard ML, MIT Press.

[35]

Nordström, B. (1988) Terminating General Recursion. BIT 28 (3) 605-619.

Digital Library

[36]

Nordström, B., Petersson, K. and Smith, J. M. (1990) Programming in Martin-Löf's Type Theory. An Introduction, Oxford University Press.

[37]

Paulson, L. C. (1986) Proving Termination of Normalization Functions for Conditional Expressions. Journal of Automated Reasoning 2 63-74.

Digital Library

[38]

Pfenning, F. and Paulin-Mohring, C. (1990) Inductively defined types in the Calculus of Constructions. In: Proceedings of Mathematical Foundations of Programming Semantics. Springer-Verlag Lecture Notes in Computer Science 442. (Also, Technical report CMU-CS-89- 209.)

[39]

Phillips, J. C. C. (1992) Recursion theory. Handbook of Logic in Computer Science 1 (Background: Mathematical Structures), Oxford University Press 79-187.

[40]

Sørensen, M. H. B. and Urzyczyn, P. (1998) Lectures on the Curry-Howard isomorphism. Available as DIKU Rapport 98/14.

[41]

Walther, C. (1992) Computing induction axioms. In: International Conference on Logic Programming and Automated Reasoning, LPAR 92. Springer-Verlag Lecture Notes in Artificial Intelligence 624.

[42]

Werner, B. (1994) Méta-théorie du Calcul des Constructions Inductives, Ph. D. thesis, Université Paris 7.

[43]

Wiedijk, F. and Zwanenburg, J. (2003) First order logic with domain conditions. In: Theorem Proving in Higher Order Logics, TPHOLs 2003. Springer-Verlag Lecture Notes in Computer Science 2758 221-237.

[44]

Winskel, G. (1993) The formal semantics of programming languages: An introduction, The MIT Press.

[45]

Zhang, X., Munro, M., Harman, M. and Hu, L. (2002) Weakest precondition for general recursive programs formalized in Coq. In: Carreno, V. A., Munoz, C. A. and Tahar, S. (eds.) Theorem Proving in Higher Order Logics: 15th International Conference, TPHOLs 2002. Springer-Verlag Lecture Notes in Computer Science 2410 332-347.

Cited By

Buchholtz USchipp von Branitz JSobocinski PLago UEsparza J(2024)Primitive Recursive Dependent Type TheoryProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662136(1-12)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662136
Liu YWeirich S(2023)Dependently-Typed Programming with Logical Equality ReflectionProceedings of the ACM on Programming Languages10.1145/36078527:ICFP(649-685)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607852
Abreu PDelaware BHubers AJenkins CMorris JStump A(2023)A Type-Based Approach to Divide-and-Conquer Recursion in CoqProceedings of the ACM on Programming Languages10.1145/35711967:POPL(61-90)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571196
Show More Cited By

Modelling general recursion in type theory
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
2. Theory of computation
  1. Semantics and reasoning

Recommendations

Simple general recursion in type theory

General recursive algorithms are such that the recursive calls are performed on arguments satisfying no condition that guarantees termination. Hence, there is no direct way of formalising them in type theory.The standard way of handling general ...
Nested General Recursion and Partiality in Type Theory
TPHOLs '01: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics

We extend Bove's technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in defining an inductive special-purpose accessibility predicate, that characterizes the ...
General recursion in type theory
TYPES'02: Proceedings of the 2002 international conference on Types for proofs and programs

In this work, a method to formalise general recursive algorithms in constructive type theory is presented throughout examples. The method separates the computational and logical parts of the definitions. As a consequence, the resulting type-theoretic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Mathematical Structures in Computer Science

Mathematical Structures in Computer Science Volume 15, Issue 4

August 2005

205 pages

ISSN:0960-1295

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 August 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Buchholtz USchipp von Branitz JSobocinski PLago UEsparza J(2024)Primitive Recursive Dependent Type TheoryProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662136(1-12)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662136
Liu YWeirich S(2023)Dependently-Typed Programming with Logical Equality ReflectionProceedings of the ACM on Programming Languages10.1145/36078527:ICFP(649-685)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607852
Abreu PDelaware BHubers AJenkins CMorris JStump A(2023)A Type-Based Approach to Divide-and-Conquer Recursion in CoqProceedings of the ACM on Programming Languages10.1145/35711967:POPL(61-90)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571196
Niu YSterling JGrodin HHarper R(2022)A cost-aware logical frameworkProceedings of the ACM on Programming Languages10.1145/34986706:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498670
Swierstra WBaanen T(2019)A predicate transformer semantics for effects (functional pearl)Proceedings of the ACM on Programming Languages10.1145/33417073:ICFP(1-26)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341707
Tomé Cortiñas CSwierstra WEisenberg RVazou N(2018)From algebra to abstract machine: a verified generic constructionProceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3240719.3241787(78-90)Online publication date: 27-Sep-2018
https://dl.acm.org/doi/10.1145/3240719.3241787
Abel AVezzosi AWinterhalter T(2017)Normalization by evaluation for sized dependent typesProceedings of the ACM on Programming Languages10.1145/31102771:ICFP(1-30)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110277
Weirich SVoizard Ade Amorim PEisenberg R(2017)A specification for dependent types in HaskellProceedings of the ACM on Programming Languages10.1145/31102751:ICFP(1-29)Online publication date: 29-Aug-2017
https://dl.acm.org/doi/10.1145/3110275
Larchey-Wendling D(2017)Typing Total Recursive Functions in CoqInteractive Theorem Proving10.1007/978-3-319-66107-0_24(371-388)Online publication date: 26-Sep-2017
https://dl.acm.org/doi/10.1007/978-3-319-66107-0_24
Christiansen DBrady E(2016)Elaborator reflection: extending Idris in IdrisACM SIGPLAN Notices10.1145/3022670.295193251:9(284-297)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951932
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents