2014 Fiscal Year Annual Research Report
| Project/Area Number |
23500030
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Project Period (FY) |
2011-04-28 – 2015-03-31
|
| Keywords | 型理論 / 存在型 / 国際情報交換 / シンガポール |
|---|
| Outline of Annual Research Achievements |
メンドラー式の帰納的定義および余帰納的定義のg-実現可能性解釈とr-実現可能性解釈を定義した。これらの解釈は、簡潔で本質的な実現子を、非単調である場合も含む帰納的および余帰納的定義の一般的枠組みに対して与える。これらの解釈の健全性定理を証明した。g-実現可能性解釈の健全性により、項存在性、論理和性、プログラム抽出定理を証明した。また、r-実現可能性解釈の健全性により、負論理式に対する選択公理とマルコフ原理との無矛盾性を証明した。
分離論理を二階論理に拡張し、その体系を考察した。アサーションを、二階変数による原子論理式と、二階変数の全称限量子に拡張した。高階分離論理が活発に研究されているが、この体系は高階分離論理を二階の範囲で含む。ポインタプログラムの性質を証明するために、この体系をホーア論理に拡張した。この拡張されたホーア論理体系に対して、(1) 最弱事前条件を記述する論理式が存在すること (表現性)、(2) 真であるアサーションを仮定すれば、真である判定が証明可能であること (相対完全性)、の２つの定理を証明した。
二階存在型の要素存在性の判定手続きを実装した。OCamlの抽象データ型を、二階存在型に翻訳する手続きを実装した。この２つの手続きを用いることにより、OCamlのライブラリ関数の依存関係を解析した。
|
