×

Type checking and typability in domain-free lambda calculi. (English) Zbl 1241.03011

Summary: This paper shows (1) the undecidability of type checking and the typability problems in the domain-free lambda calculus with negation, product, and existential types, (2) the undecidability of the typability problem in the domain-free polymorphic lambda calculus, and (3) the undecidability of type checking and the typability problems in the domain-free lambda calculus with function and existential types. The first and the third results are proved by the second result and CPS translations that reduce those problems in the domain-free polymorphic lambda calculus to those in the domain-free lambda calculi with existential types. The key idea is the conservativity of the domain-free lambda calculi with existential types over the images of the translations.

MSC:

03B40 Combinatory logic and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barthe, G.; Sørensen, M. H., Domain-free pure type systems, Journal of Functional Programming, 10, 412-452 (2000) · Zbl 0979.03013
[2] Danvy, O.; Filinski, A., Representing control: a study of the CPS translation, Mathematical Structures in Computer Science, 2, 4, 361-391 (1992) · Zbl 0798.68102
[3] Fujita, K., Explicitly typed \(\lambda \mu \)-calculus for polymorphism and call-by-value, (Proceedings of 4th International Conference on Typed Lambda Calculi and Applications. Proceedings of 4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999. Proceedings of 4th International Conference on Typed Lambda Calculi and Applications. Proceedings of 4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999, LNCS, vol. 1581 (1999)), 162-177 · Zbl 0933.03009
[4] Fujita, K.; Schubert, A., Partially typed terms between Church-style and Curry-style, (International Conference IFIP TCS 2000. International Conference IFIP TCS 2000, LNCS, vol. 1872 (2000)), 505-520 · Zbl 0998.03009
[5] Fujita, K., Galois embedding from polymorphic types into existential types, (Proceedings of 7th International Conference on Typed Lambda Calculi and Applications. Proceedings of 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005. Proceedings of 7th International Conference on Typed Lambda Calculi and Applications. Proceedings of 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005, LNCS, vol. 3461 (2005)), 194-208 · Zbl 1114.03009
[6] Fujita, K.; Schubert, A., Existential type systems with no types in terms, (Proceedings of 9th International Conference on Typed Lambda Calculi and Applications. Proceedings of 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009. Proceedings of 9th International Conference on Typed Lambda Calculi and Applications. Proceedings of 9th International Conference on Typed Lambda Calculi and Applications, TLCA 2009, LNCS, vol. 5608 (2009)), 112-126 · Zbl 1246.03028
[7] J.Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse de doctorat d’Etat, Université de Paris VII, 1972.; J.Y. Girard, Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse de doctorat d’Etat, Université de Paris VII, 1972.
[8] Harper, R.; Lillibridge, M., Polymorphic type assignment and CPS conversion, Lisp and Symbolic Computation, 6, 361-380 (1993)
[9] Hasegawa, M., Relational parametricity and control, Logical Methods in Computer Science, 2, 3:3, 1-22 (2006) · Zbl 1126.68023
[10] M. Hasegawa, 2007 (unpublished manuscript).; M. Hasegawa, 2007 (unpublished manuscript).
[11] Mitchell, J. C.; Plotkin, G. D., Abstract types have existential type, ACM Transactions on Programming Languages and Systems, 10, 3, 470-502 (1988)
[12] E. Moggi, Computational lambda-calculus and monads, in: Proceedings of 4th Annual Symposium on Logic in Computer Science, LICS 1989, 1989, pp. 14-23.; E. Moggi, Computational lambda-calculus and monads, in: Proceedings of 4th Annual Symposium on Logic in Computer Science, LICS 1989, 1989, pp. 14-23. · Zbl 0716.03007
[13] Nakazawa, K., An isomorphism between cut-elimination procedure and proof reduction, (Proceedings of 8th International Conference on Typed Lambda Calculi and Applications. Proceedings of 8th International Conference on Typed Lambda Calculi and Applications, TLCA 2007. Proceedings of 8th International Conference on Typed Lambda Calculi and Applications. Proceedings of 8th International Conference on Typed Lambda Calculi and Applications, TLCA 2007, LNCS, vol. 4583 (2007)), 336-350 · Zbl 1215.03067
[14] Nakazawa, K.; Tatsuta, M.; Kameyama, Y.; Nakano, H., Undecidability of type-checking in domain-free typed lambda-calculi with existence, (The 17th EACSL Annual Conference on Computer Science Logic. The 17th EACSL Annual Conference on Computer Science Logic, CSL 2008. The 17th EACSL Annual Conference on Computer Science Logic. The 17th EACSL Annual Conference on Computer Science Logic, CSL 2008, LNCS, vol. 5213 (2008)), 477-491
[15] Parigot, M., \( \lambda \mu \)-calculus: an algorithmic interpretation of classical natural deduction, (Proc. the International Conference on Logic Programming and Automated Reasoning. Proc. the International Conference on Logic Programming and Automated Reasoning, LNCS, vol. 624 (1992)), 190-201 · Zbl 0925.03092
[16] Plotkin, G., Call-by-name, call-by-value, and the \(\lambda \)-calculus, Theoretical Computer Science, 1, 125-159 (1975) · Zbl 0325.68006
[17] Reynolds, J. C., Towards a theory of type structure, (Symposium on Programming. Symposium on Programming, LNCS, vol. 19 (1974)), 408-425
[18] Sabry, A.; Wadler, P., A reflection on call-by-value, ACM Transactions on Programming Languages and Systems, 19, 6, 916-941 (1997)
[19] Sørensen, M. H.; Urzyczyn, P., A syntactic embedding of predicate logic into second-order propositional logic, Notre Dame Journal of Formal Logic, 51, 4, 457-473 (2010) · Zbl 1216.03029
[20] Tatsuta, M.; Fujita, K.; Hasegawa, R.; Nakano, H., Inhabitation of polymorphic and existential types, Annals of Pure and Applied Logic, 161, 1390-1399 (2010) · Zbl 1225.03034
[21] H. Thielecke, Categorical structure of continuation passing style, Ph.D. Thesis, University of Edinburgh, 1997.; H. Thielecke, Categorical structure of continuation passing style, Ph.D. Thesis, University of Edinburgh, 1997.
[22] von Plato, J., Natural deduction with general elimination rules, Archive for Mathematical Logic, 40, 541-567 (2001) · Zbl 1021.03050
[23] Wells, J. B., Typability and type checking in system \(F\) are equivalent and undecidable, Annals of Pure and Applied Logic, 98, 111-156 (1999) · Zbl 0932.03017
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.