Abstract
Primitive recursion can be seen as the computational interpretation of induction through the Curry-Howard interpretation of propositions-as-types. In the present paper we discuss what happens if we apply this idea to possible non monotone inductive definitions. We start with a logical interpretation of a class of inductive definitions, thepartial inductive definitions. Then we internalise induction over such definitions as a rule of inference and consider a Curry-Howard interpretation of these definitions as type systems. As a basic example we discuss what meaning this interpretation gives to primitive recursion on a definition likeN=N→N.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
L. Hallnäs,Partial inductive definitions, TCS 87, 1991.
B. Nordström, K. Pettersson, J. Smith,Programming in Martin-Löf's Type Theory. An Introduction. Oxford University Press 1990.
P. Martin-Löf,Hauptsatz for the intuitionistic theory of iterated inductive definitions, in:Proceedings of the Second Scandinavian Logic Symposium, ed. J. E. Fenstad, North Holland, Amsterdam, 1971.
K. Pettersson, D. Synek,A set constructor for inductive sets in Martin-Löf's type theory, PMG Report 48, Department of Computer Science, Chalmers University of Technology and University of Göteborg, 1987.
D. Prawitz,Ideas and results in proof theory, in:Proceedings of the Second Scandinavian Logic Symposium, ed. J. E. Fenstad, North Holland, Amsterdam, 1971.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Hallnäs, L. On systems of definitions, induction and recursion. BIT 32, 45–63 (1992). https://doi.org/10.1007/BF01995107
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01995107