2012 Fiscal Year Research-status Report
| Project/Area Number |
23500030
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Keywords | 型理論 / 存在型 |
|---|
| Research Abstract |
双対計算を帰納型と余帰納型により拡張した。双対計算とはWadlerにより提案された型理論であり、古典シーケント計算に基づく型理論である。この型理論においては、古典論理のもつ双対性が、型理論としても表現されている。帰納型とは、リスト、木などの再帰データに対する型の一般化であり、最小不動点により定義される。余帰納型とは、ストリームなど無限データに対する型の一般化であり、最大不動点により定義される。帰納型と余帰納型は双対であると考えられており、カテゴリ理論など様々な側面からその双対性が論じられてきた。しかし、型理論の側面から構文的にその双対性を明らかにした結果はなかった。
まず帰納型と余帰納型をもつ非決定可能双対計算を提案した。この体系は、元の双対計算と同じ双対性をもつ上に、帰納型と余帰納型の双対性をもつ。すなわち、帰納型と余帰納型に対して、項と余項の双対性、および簡約規則の双対性をもつ。この体系の強正規化可能性を、体系を二階双対計算に翻訳することにより証明した。二階双対計算の強正規化可能性は、その体系を二階対称ラムダ計算に翻訳することにより証明した。次に、帰納型および余帰納型をもつ双対計算のうちで値呼び体系と名前呼び体系を提案した。これら体系に対して、値呼びと名前呼びの双対性、チャーチロッサー性、強正規化可能性を証明した。これら体系の強正規化可能性は、これらの体系を帰納型と余帰納型をもつ非決定双対計算に翻訳することにより証明した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
既知の存在型の要素存在性の決定不可能性証明を選言がある場合に拡張する方向性で研究を進めているが、困難があり、Lobなどの他の関連文献により新しいアイデアを求めている状況ではあるが、存在型の基本性質を明らかにする本研究が着実に進んでいるといえる。
また、帰納型、余帰納型、双対性をもつ型理論を提案し、帰納型と余帰納型の双対性、その簡約が強正規化可能であることを証明したことにより、関連する型理論の基本性質を明らかにすることができた。
|
| Strategy for Future Research Activity |
これまでに得られた方向性および新しいアイデアに基づいて、既知の存在型の要素存在性の決定不可能性証明を、選言がある場合に拡張し、存在型の基本性質を明らかにする。
また、次のように研究を進める。存在型の型理論の要素存在性は、否定型、直積型、存在型、多相型からなる型理論では決定可能であるが、矛盾、関数型、直和型、存在型からなる型理論では非決定可能である。本研究では、まず、この２つから出発し、どのような存在型の型理論の要素存在性が決定可能であるか分類する。方法は、既存研究の精密化、拡張である。特に、存在型と関数型だけからなる型理論について要素存在性が決定可能であるか明らかにする。
否定型、直積型、存在型を含むCurry式, type-free式, およびmultiple-quantifier式の型理論の型推論および型検査の非決定可能性は知られているが、しかし、まだ、関数型と存在型の両方を含む型理論について、その型推論および型検査が決定可能であるかどうかは未知である。本研究ではこれを明らかにする。方法は、CPS変換を用いて多相型の性質と比較する方法の拡張、および一階述語論理の二階命題論理への翻訳を用いる方法の拡張、および、Lobの論文など関連文献のアイデアを拡張して適用する方法である。
|
| Expenditure Plans for the Next FY Research Funding |
次年度への繰越は、本研究費による研究討論のための型理論に関する学会出席が予定より少なく、また研究討論のための型理論関連の外国著名研究者への訪問が予定より少なかったため、繰越が生じた。繰越は翌年度の研究費と合わせて次の目的で支出する予定である。
型理論に関連する学会に出席し、発表および研究討論を行うための外国旅費に支出する。また、本研究を推進するため、型理論研究に関連する外国の著名研究者を訪問し研究討論を行うための外国旅費に支出する。また、本研究を推進するための消耗品を購入する。
|
