Abstract
This paper introduces an extension of a typed λ-calculus with local recursive definitions, that is, a language combining higher types and recursion. In contrast to the Gödel's calculus of recursive functionals, the reduction presented arranges local definitions to a normal form. Essential properties of the reduction are soundness with respect to the outlined categorical semantics, confluence, and strong normalization. Suitability of the language to be a basis for higher order specification languages is discussed.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Abadi M., L.Cardelli, P.-L.Curien, J.-J.Levy. Explicit Substitutions. Research report 54 of Systems Research Center of DEC, 1990.
Barr M. Fixed Points in Cartesian Closed Categories. Theoretical Computer Science, Vol.70, 1990.
Bergstra J.A., J.Heering, P.Klint. Module Algebra. Journal of the ACM, Vol. 37(2), 1990.
Ershov Yu.L. The language of Σ-Expressions. In Vychislitelnye Sistemy, Vol.114, Novosibirsk, 1986 (in Russian).
Feijs L.M.G. The Calculus λπ. Lecture Notes in Computer Science, Vol.394, Springer-Verlag, 1989.
Feijs L.M.G. Transformations of Designs. Lecture Notes in Computer Science, Vol.490, Springer-Verlag, 1991.
Gray J.W. Semantics of the Typed λ-Calculus with Substitution in a Cartesian Closed Category. INRIA Rapports de Recherche 1261, 1990.
Gödel K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, 1958.
Huwig H., A.Poigné. A note on Inconsistencies Caused by Fixpoints in a Cartesian Closed Category. Theoretical Computer Science, Vol.73, 1990.
Johnsson H.B.M. Lambda Lifting: Transforming Programs to Recursive Equations. Lecture Notes in Computer Science, Vol.201, Springer-Verlag, 1985.
Jonkers H.B.M. An Introduction to COLD-K. Lecture Notes in Computer Science, Vol.394, Springer-Verlag, 1989.
Lambek J. From λ-Calculus to Cartesian Closed Categories. in: To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
Lambek J., Scott P. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986.
MacLane S. Categories for the Working Mathematician. Springer-Verlag, 1971.
Moschovakis Y.N. The Formal Language of Recursion. Journal of Symbolic Logic, Vol.55, 1990.
Poigné A. On Specifications, Theories, and Models with Higher Types. Information and Control, Vol.68, 1986.
Sannella D., A. Tarlecki. Towards Formal Development of Programs from Algebraic Specifications: Implementation Revisited. Acta Informatica, Vol.25(3), 1988.
Scott D. Continuous Lattices. Lecture Notes in Mathematics 274, Springer-Verlag, 1972.
Scott D. Relating Theories to the Lambda Calculus. in: To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
Stenlund S. Combinators, Lambda Terms, and Proof Theory. D.Reidel, Dordrecht, Holland, 1972.
Wirsing M. Structured Algebraic Specifications: a Kernel Language. Theoretical Computer Science, Vol.42, 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kotov, S.V. (1992). Typed λ-calculus with recursive definitions. In: Nerode, A., Taitslin, M. (eds) Logical Foundations of Computer Science — Tver '92. LFCS 1992. Lecture Notes in Computer Science, vol 620. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023879
Download citation
DOI: https://doi.org/10.1007/BFb0023879
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55707-4
Online ISBN: 978-3-540-47276-6
eBook Packages: Springer Book Archive