Abstract
The subject of the paper is the connection between the typed λ-calculus and the cartesian closed categories, pointed out by several authors. Three languages and their theories, defined by equations, are shown to be equivalent: the typed λc-calculus (i.e. the λ-calculus with explicit products and projections) λc K , the free cartesian closed category CCC K , and a third intermediary language, the typed categorical combinatory logic CCL K , introduced by the author. In contrast to CCC K , CCL K has the same types as λc K , and roughly the terminal object in CCC K is replaced by the application and couple operators in CCL K . In CCL K β-reductions as well as evaluations w.r.t. environments (the basis of most practical implementations of λ-calculus based languages) may be simulated in the well-known framework of a same term rewriting system. Finally the introduction of CCL K allowed the author to understand the untyped underlying calculus, investigated in a companion paper. Another companion paper describes a general setting for equivalences between equational theories and their induced semantic equivalences, the equivalence between CCL K and CC K is an instance of which.
Chapter PDF
4. References
G. Berry, Some Syntactic and Categorical Constructions of Lambdacalculus models, Rapport INRIA 80 (1981).
N.G. De Bruijn, Lambda-calculus Notation without Nameless Dummies, a Tool for Automatic Formula Manipulation, Indag Math. 34, 381–392 (1972).
P-L. Curien, Algorithmes Séquentiels sur Structures de Données Concrètes, Thèse de Troisième Cycle, Université Paris VII (Mars 1979).
P-L. Curien, Combinateurs Catégoriques, Algorithmes Séquentiels et Programmation Applicative, Thèse d'Etat, Université Paris VII (Décembre 83), to be published in english as a monograph.
P-L. Curien, Categorical Combinatory Logic, submitted to ICALP 85.
Syntactic Equivalences Inducing Semantic Equivalences, submitted to EUROCAL 1985.
P. Dybjer, Category-Theoretic Logics and Algebras of Programs, PhD Thesis, Chalmers University of Technology, Goteborg (1983).
J. Lambek, From Lambda-calculus to Cartesian Closed Categories, in To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, ed. J.P. Seldin and J.R. Hindley, Academic Press (1980).
J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic, to be published by Cambridge University Press (1984).
P.J. Landin, The Mechanical Evaluation of Expressions, Computer Journal 6, 308–320 (1964).
K. Parsaye-Ghomi, Higher Order Abstract Algebras, PhD Thesis, UCLA (1981).
A. Poigné, Higher Order Data Structures, Cartesian Closure Versus λ-calculus, STACS 84, Lect. Notes in Comput. Sci.
G. Pottinger, The Church-Rosser Theorem for the Typed λ-calculus with Extensional Pairing, preprint, Carnegie-Mellon University, Pittsburgh (March 1979).
D. Scott, Relating Theories of the Lambda-calculus, cf. [Lam].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Curien, PL. (1985). Typed categorical combinatory logic. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds) Mathematical Foundations of Software Development. CAAP 1985. Lecture Notes in Computer Science, vol 185. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15198-2_10
Download citation
DOI: https://doi.org/10.1007/3-540-15198-2_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15198-2
Online ISBN: 978-3-540-39302-3
eBook Packages: Springer Book Archive