| Project/Area Number |
25400192
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Foundations of mathematics/Applied mathematics
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
古森 雄一 千葉大学, 大学院理学研究科, 名誉教授 (10022302)
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| Research Collaborator |
Schubert Aleksy University of Warsaw, Institute of Informatics, Professor
KASHIMA RYO 東京工業大学, 情報理工学院, 准教授
NAKAZAWA KOJI 名古屋大学, 情報科学研究科, 准教授
MATSUDA NAOSUKE 神奈川大学, 理学部, 助手
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
Fiscal Year 2015: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | ラムダ計算 / 型検査問題 / 型推論問題 / 決定可能性 / チャーチ流 / カリー流 / チャーチ・ロッサーの定理 / 型検査 / 型推論 / 合流性 |
|---|
| Outline of Final Research Achievements |
We study decidability and undecidability of type-related problems of lambda-calculi from the viewpoint of styles of terms between Church and Curry. First, intermediate lambda-terms are introduced with a style between decidable Church-style and undecidable Curry-style. Then an order is naturally associated to the style, which is preserved under CPS-translations from polymorphic lambda-terms into existential lambda-terms. In this way, we obtain a general framework such that undecidable problems of polymorphic lambda-calculus can be embedded into those of existential lambda-calculus. This study reveals what causes the differences in decidability and undecidability on the type-related problems in terms of styles of terms.
|
