文章基本信息

标题：Decidable structures between Church-style and Curry-style
本地全文：下载
作者：Ken-etsu Fujita ; Aleksy Schubert
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2013
卷号：21
页码：190-205
DOI：10.4230/LIPIcs.RTA.2013.190
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：It is well-known that the type-checking and type-inference problems are undecidable for second order lambda-calculus in Curry-style, although those for Church-style are decidable. What causes the differences in decidability and undecidability on the problems? We examine crucial conditions on terms for the (un)decidability property from the viewpoint of partially typed terms, and what kinds of type annotations are essential for (un)decidability of type-related problems. It is revealed that there exists an intermediate structure of second order lambda-terms, called a style of hole-application, between Church-style and Curry-style, such that the type-related problems are decidable under the structure. We also extend this idea to the omega-order polymorphic calculus F-omega, and show that the type-checking and type-inference problems then become undecidable.
关键词：2nd-order lambda-calculus; type-checking; type-inference; Church-style and Curry-style