Abstract
We present a general method for constructing extensional models for the polymorphic lambda calculus—the polymorphic extensional collapse. The method yields models that satisfy additional, computationally motivated constraints like having only two polymorphic booleans and having only the numerals as polymorphic integers. Moreover the method yields models that prove that the polymorphic lambda calculus can be conservatively added to arbitrary algebraic data type specifications, even with complete transfer of the computational power to the added data types.
The first author was supported in part by an IBM Graduate Fellowship and in part by NSF Grant DCR-8511190
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, second edition, 1984.
V. Breazu-Tannen. Ph.D. thesis, MIT. Expected Feb.1987.
V. Breazu-Tannen and A. R. Meyer. Computable values can be classical. In Proceedings of the 14th Symposium on Principles of Programming Languages, ACM, 1987. To appear.
V. Breazu-Tannen. Communication in the Types electronic forum (xx.lcs.mit.edu), July 29th. 1986. Unpublished.
K. B. Bruce and A. R. Meyer. The semantics of second order polymorphic lambda calculus. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, pages 131–144, Springer-Verlag, Berlin, June 1984.
R. M. Burstall, D.B. MacQueen, and D.T. Sanella. Hope: an experimental applicative language. In LISP Conference, pages 136–143, Stanford University Computer Science Department, 1980.
L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. Computing Surveys, 17(4):471–522, 1985.
L. Cardelli. Amber. In Combinators and functional programming languages, Proceedings of the 13th Summer School of the LITP, Le Val D'Ajol, Vosges, France, May 1985.
T. Coquand. Communication in the Types electronic forum (xx.lcs.mit.edu), April 14th. 1986. Unpublished.
J. Fairbairn. Ponder and its type system. Tech. Rep. 31, Computer Laboratory, Univ. of Cambridge, Cambridge, England, November 1982.
S. Fortune, D. Leivant, and M. O'Donnell. The expressiveness of simple and second-order type structures. Journal of the ACM, 30(1):151–185, January 1983.
R. O. Gandy. On the axiom of extensionality—Part I. Journal of Symbolic Logic, 21, 1956.
J.-Y. Girard. Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieure. Ph.D. thesis, Université Paris VII, 1972.
M. J. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1979.
R. Hindley and G. Longo. Lambda-calculus models and extensionality. Zeitschrift für Mathematische Logic und Grundlagen der Mathematik, 26:289–310, 1980.
J. W. Klop. Combinatory reduction systems. Tract 129, Mathematical Center, Amsterdam, 1980.
D. Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. In 24th Symposium on Foundations of Computer Science, pages 460–469, IEEE, 1983.
D. C. J. Matthews. Poly manual. Tech. Rep. 63, Computer Laboratory, Univ. of Cambridge, Cambridge, England, 1985.
A. R. Meyer, J. C. Mitchell, E. Moggi, and R. Statman. Empty types in polymorphic λ-calculus. In Proceedings of the 14th Symposium on Principles of Programming Languages, ACM, 1987. To appear.
Albert R. Meyer. What is a model of the lambda calculus? Information and Control, 52(1):87–122, January 1982.
A. R. Meyer. Communication in the Types electronic forum (xx.lcs.mit.edu), February 7th. 1986. Unpublished.
J. C. Mitchell and A.R. Meyer. Second-order logic relations (extended abstract). In R. Parikh, editor, Logics of Programs, pages 225–236, Springer-Verlag, Berlin, June 1985.
J. C. Mitchell. Personal communication, August. 1986. Unpublished.
J. C. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions. In LISP Conference, pages 308–319, ACM, New York, August 1986.
E. Moggi. Communication in the Types electronic forum (xx.lcs.mit.edu), February 10th. 1986. Unpublished.
E. Moggi. Communication in the Types electronic forum (xx.lcs.mit.edu), July 23rd. 1986. Unpublished.
R. S. Nikhil. An incremental, strongly typed database query language. Ph.D. thesis, Univ. of Pennsylvania, Philadelphia, August 1984. Available as tech. rep. MS-CIS-85-02.
J. C. Reynolds. Three approaches to type structure. In TAPSOFT advanced seminar on the role of semantics in software development, Springer-Verlag, Berlin, 1985.
A. Scedrov. Semantical methods for polymorphism. 1986. Unpublished manuscript, Univ. of Pennsylvania, July 1986.
R. Statman. On the existence of closed terms in the typed λ-calculus. In J. P. Seldin and R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 511–534, Academic Press, New York, 1980.
R. Statman. Number theoretic functions computable by polymorphic programs. In 22nd Symposium on Foundations of Computer Science, pages 279–282, IEEE, 1981.
R. Statman. λ-definable functionals and β η conversion. Arch. math. Logik, 23:21–26, 1983.
A. S. Troelstra (ed.). Metamathematical investigation of intuititionistic arithmetic and analysis. Volume 344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
D. A. Turner. Miranda: a non-strict functional language with polymorphic types. In J.-P. Jouannaud, editor, Functional programming languages and computer architecture, pages 1–16, Springer-Verlag, Berlin, September 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Breazu-Tannen, V., Coquand, T. (1987). Extensional models for polymorphism. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds) TAPSOFT '87. TAPSOFT 1987. Lecture Notes in Computer Science, vol 250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014987
Download citation
DOI: https://doi.org/10.1007/BFb0014987
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17611-4
Online ISBN: 978-3-540-47717-4
eBook Packages: Springer Book Archive