2002 Fiscal Year Annual Research Report
| Project/Area Number |
12680346
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学基礎研究系, 教授 (80216994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
照井 一成 国立情報学研究所, 情報学基礎研究系, 助手 (70353422)
|
|---|
| Keywords | 構成的集合 / 余帰納的定義 / 構成的論理 / 実現可能性解釈 / プログラム合成 / 型理論 |
|---|
| Research Abstract |
本研究の目的は、構成的集合と余帰納的定義をもつ構成的論理を構築し、この論理体系を用いて、余帰納型を用いたプログラムの性質を明らかにし、また、構成的集合と余帰納的定義を用いたプログラム合成システムを試作することであった。特に、(1)余帰納型に内在する計算の本質は何か明らかにする、(2)余帰納的定義の証明論的強さを調べることにより余帰納型により表現できる関数を分類する、(3)構成的集合と余帰納的定義を用いたプログラムの検証、合成を行うための論理体系の構築、(4)構成的集合と余帰納的定義を合わせもつ論理に対する実現可能性解釈の定義、(5)一般的余帰納型による既存プログラミング言語の拡張、(6)構成的集合と余帰納的定義を用いたプログラム検証、合成システムの実現、(7)ストリームプログラム、並行プログラム、セキュリティプロトコールの検証および合成実験、の研究を行うことを目的とした。
本年度では次の研究を行った。
(1)型理論の強正規化可能性および正規化可能性から対応するシーケントによる論理体系のカット除去定理を導く方法が一階述語論理に対して知られていたが、これを二階述語論理に拡張し、同様の結果が成り立つことを証明した。
(2)実現可能性の新しい公理化を検討した。
(3)例外処理計算系の強正規化可能性定理に対してCPS変換およびオグメンテーションを用いた証明方法を検討した。
|
