2011 Fiscal Year Research-status Report
| Project/Area Number |
23500030
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Project Period (FY) |
2011-04-28 – 2015-03-31
|
| Keywords | 型理論 / 存在型 |
|---|
| Research Abstract |
二相再帰の型理論を提案しその型推論が決定可能であることを証明した。二相再帰とは、多相再帰を制限した再帰に対する型付けであり、関数定義の中ですべての関数呼び出しは同じ型をもつ必要がある。多相再帰の型推論は決定不可能であることが知られており、二相再帰型理論は、型付けが決定可能であるように多相再帰を制限する方法を与えた。 ウルツィクチンらによる存在型の要素存在性の決定不可能性証明を、選言がある場合に拡張することを試み、その方向性を得た。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
既知の存在型の要素存在性の決定不可能性証明を、選言がある場合に拡張する方向性を得たことにより、存在型の基本性質を明らかにする本研究が進んでいる。 また、二相再帰の型理論を提案しその型推論が決定可能であることを証明したことにより、関連する型理論の基本性質を明らかにすることができた。
|
| Strategy for Future Research Activity |
これまでに得られた方向性に基づいて、既知の存在型の要素存在性の決定不可能性証明を、選言がある場合に拡張し、存在型の基本性質を明らかにする。 また、次のように研究を進める。存在型の型理論の要素存在性は、否定型、直積型、存在型、多相型からなる型理論では決定可能であるが、矛盾、関数型、直和型、存在型からなる型理論では非決定可能である。本研究では、まず、この２つから出発し、どのような存在型の型理論の要素存在性が決定可能であるか分類する。方法は、既存研究の精密化、拡張である。特に、存在型と関数型だけからなる型理論について要素存在性が決定可能であるか明らかにする。 否定型、直積型、存在型を含むCurry式, type-free式, およびmultiple-quantifier式の型理論の型推論および型検査の非決定可能性は知られているが、しかし、まだ、関数型と存在型の両方を含む型理論について、その型推論および型検査が決定可能であるかどうかは未知である。本研究ではこれを明らかにする。方法は、CPS変換を用いて多相型の性質と比較する方法の拡張、および一階述語論理の二階命題論理への翻訳を用いる方法の拡張である。
|
| Expenditure Plans for the Next FY Research Funding |
型理論に関連する学会に出席し、発表および研究討論を行うための外国旅費に支出する。 また、本研究を推進するため、型理論研究に関連する外国の著名研究者を訪問し研究討論を行うための外国旅費に支出する。
|
