LIPIcs.RTA.2010.103.pdf
- Filesize: 184 kB
- 16 pages
Document
The Undecidability of Type Related Problems in Type-free Style System F
Authors
-
Part of:
Volume:
Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2010-07-06
Cite As Get BibTex
Ken-Etsu Fujita and Aleksy Schubert. The Undecidability of Type Related Problems in Type-free Style System F. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 103-118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/LIPIcs.RTA.2010.103
Abstract
We consider here a number of variations on the System F, that are predicative second-order systems whose terms are intermediate between the Curry style and Church style. The terms here contain the information on where the universal quantifier elimination and introduction in the type inference process must take place, which is similar to Church forms. However, they omit the information on which types are involved in the rules, which is similar to Curry forms. In this paper we prove the undecidability of the type-checking, type inference and typability problems for the system. Moreover, the proof works for the predicative version of the system with finitely stratified polymorphic types. The result includes the bounds on the Leivant’s level numbers for types used in the instances leading to the undecidability.
Subject Classification
Keywords
- Lambda calculus and related systems
- type checking
- typability
- partial type inference
- 2nd order unification
- undecidability
- Curry style type system
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads