Abstract
We investigate, in a categorical setting, some completeness properties of beta-eta conversion between closed terms of the simplytyped lambda calculus. A cartesian-closed category is said to be complete if, for any two unconvertible terms, there is some interpretation of the calculus in the category that distinguishes them. It is said to have a complete interpretation if there is some interpretation that equates only interconvertible terms. We give simple necessary and sufficient conditions on the category for each of the two forms of completeness to hold. The classic completeness results of, e.g., Friedman and Plotkin are immediate consequences. As another application, we derive a syntactic theorem of Statman characterizing beta-eta conversion as a maximum consistent congruence relation satisfying a property known as typical ambiguity.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Y. Akama. On Mints' reduction for ccc-calculus. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, Proceedings of TLCA '93. LNCS 664, Springer Verlag, 1993.
H. P. Barendregt. The Lambda Calculus, its Syntax and Semantics. North Holland, Amsterdam, 1984. Second edition.
U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Proceedings of 6th Annual Symposium on Logic in Computer Science, pages 203–211, 1991.
D. Čubrić. Embedding of a free cartesian closed category into the category of sets. Journal of Pure and Applied Algebra, to appear, 1995.
H. Friedman. Equality between functionals. In R. Parikh, editor, Logic Colloquium, Springer-Verlag, New York, 1975.
N. Ghani. βη-equality for coproducts. This volume, 1995.
C. B. Jay and N. Ghani. The virtues of eta-expansion. Journal of Functional Programming, to appear, 1995.
J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Number 7 in Cambridge studies in advanced mathematics. Cambridge University Press, 1986.
E. Moggi. The Partial Lambda-Calculus. Ph.D. thesis, Department of Computer Science, University of Edinburgh, 1988. Available as LFCS report no. ECS-LFCS-88-63.
G. D. Plotkin. Lambda-definability and logical relations. Technical Report SAI-RM-4, School of Artificial Intelligence, University of Edinburgh, 1973.
G. D. Plotkin. Lambda-definability in the full type hierarchy. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980.
J. G. Riecke. Statman's 1-Section Theorem. Information and Computation, to appear, 1995.
S. Soloviev. The category of finite sets and CCCs. Journal of Soviet Mathematics, 22:1387–1400, 1983.
R. Statman. On the existence of closed terms in the typed λ-calculus I. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980.
R. Statman. Completeness, invariance and λ-definability. Journal of Symbolic Logic, 47:17–26, 1982.
R. Statman. λ-definable functionals and βη conversion. Archiv fur Math. Logik und Grund., 23:21–26, 1983.
R. Statman. Equality between functionals revisited. In L. A. Harrington et al, editors, Harvey Friedman's Research on the Foundations of Mathematics. Elsevier Science Publishers, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Simpson, A.K. (1995). Categorical completeness results for the simply-typed lambda-calculus. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014068
Download citation
DOI: https://doi.org/10.1007/BFb0014068
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59048-4
Online ISBN: 978-3-540-49178-1
eBook Packages: Springer Book Archive