2013 Fiscal Year Research-status Report
| Project/Area Number |
23500030
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Keywords | 型理論 / 存在型 / 国際情報交換 / イタリア |
|---|
| Research Abstract |
含意をもつ様々な部分古典論理に基づく算術に対するゲーム意味論を与えた。この意味論はシグマ0-1論理式に限定した排中律をもつ直観主義算術に対応する無限シーケント計算に意味論を与えその論理体系を明らかにした。逐次バックトラック付きゲームを提案し、そのゲーム意味論が、その論理体系および関連する他の様々な部分古典論理に対して、健全かつ完全な意味論を与えることを示した。それを示すために、その論理体系の片側版の論理体系で、ゲーム意味論の必勝戦略に木同型な証明図をもつ論理体系を定義した。
逐次バックトラックは、従来の古典論理のゲーム意味論において用いられたバックトラックと、直観主義論理のゲーム意味論に用いられたバックトラックを発展させることにより定義した。これを用いて、直観主義論理、シグマ0-1論理式に関する排中律をもつ論理、古典論理に対する統一的な意味論を与えた。シグマ0-1論理式に関する排中律をもつ論理体系と同等な論理体系として、交換規則のない無限算術と、その片側版の論理体系を定義し、それぞれの体系における証明可能性とゲーム意味論において真であることが同等であることを証明した。交換規則のない無限算術とその片側版の論理体系はそれらの証明可能性は同等である。また、片側版の論理体系の証明図は、ゲーム意味論の必勝戦略と木同型であり、それらの証明可能性と真であることは同等である。また、交換規則のない無限算術とシグマ0-1論理式に関する排中律をもつ論理体系は同等である。以上の同等性により健全性と完全性を証明した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
既知である存在型の要素存在性の決定不可能性証明を選言がある場合に拡張する方向性で研究を進めてきている。困難な点もあるが、Urzyczynなどの他の関連文献により新しいアイデアを求めている状況において、存在型の基本性質を明らかにする本研究が着実に進んでいるといえる。
また、含意をもつ様々な部分古典論理に基づく算術に対するゲーム意味論を与え、そのゲーム意味論が、前述の論理体系および関連する他の様々な部分古典論理に対して、健全かつ完全な意味論を与えることを示した。これにより、関連する論理体系の基本性質を明らかにすることができた。
|
| Strategy for Future Research Activity |
これまでに得られた方向性および新しいアイデアに基づいて、既知の存在型の要素存在性の決定不可能性証明を、選言がある場合に拡張し、存在型の基本性質を明らかにする。
否定型、直積型、存在型を含む型理論を、レコード型に拡張した体系を考え、要素存在性の証明をこの体系に拡張する。この拡張した体系は、抽象データ型を含むので、要素存在性アルゴリズムをコンピュータ上に実装することにより、抽象データ型の無矛盾性を検査するソフトウェアを作成する。
否定型、直積型、存在型を含むCurry式, type-free式, およびmultiple-quantifier式の型理論の型推論および型検査の非決定可能性は知られているが、まだ、関数型と存在型の両方を含む型理論について、その型推論および型検査が決定可能であるかどうかは未知である。本研究ではこれを明らかにする。一階述語論理の二階命題論理への翻訳を用いる方法の拡張、および、Urzyczynの文献など関連文献のアイデアを拡張して適用する方法である。
|
| Expenditure Plans for the Next FY Research Funding |
次年度への繰越は、本研究費による研究討論のための型理論に関する学会出席が予定より少なく、また研究討論のための型理論関連の外国著名研究者への訪問が予定より少なかったため、繰越が生じた。
型理論に関連する学会に出席し、発表および研究討論を行うための外国旅費に支出する。また、本研究を推進するため、型理論研究に関連する外国の著名研究者を訪問し研究討論を行うための外国旅費に支出する。その他、本研究の理論的成果をコンピュータ上に実装するため、研究員を雇用し謝金を支払い、本研究を推進するための消耗品を購入する。
|
