2003 Fiscal Year Annual Research Report
| Project/Area Number |
12680346
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
龍田 真 国立情報学研究所, 情報学基礎研究系, 教授 (80216994)
|
|---|
| Keywords | 構成的集合 / 余帰納的定義 / 構成的論理 / 実現可能性解釈 / プログラム合成 / 型理論 |
|---|
| Research Abstract |
本研究の目的は、構成的集合と余帰納的定義をもつ構成的論理を構築し、この論理体系を用いて、余帰納型を用いたプログラムの性質を明らかにし、また、構成的集合と余帰納的定義を用いたプログラム合成システムを試作することであった。特に、(1)余帰納型に内在する計算の本質は何か明らかにする、(2)余帰納的定義の証明論的強さを調べることにより余帰納型により表現できる関数を分類する、(3)構成的集合と余帰納的定義を用いたプログラムの検証、合成を行うための論理体系の構築、(4)構成的集合と余帰納的定義を合わせもつ論理に対する実現可能性解釈の定義、(5)一般的余帰納型による既存プログラミング言語の拡張、(6)構成的集合と余帰納的定義を用いたプログラム検証、合成システムの実現、(7)ストリームプログラム、並行プログラム、セキュリティプロトコールの検証および合成実験、の研究を行うことを目的とした。
本年度では次の研究を行った。
(1)置換簡約を含む構成的二階述語自然演繹の強正規化可能性定理を証明した。この体系は、選言、一階限量子、二階限量子およびそれに対する置換簡約を含む。原子選言の体系の強正規化可能性を先ずReducibilityと飽和集合を用いて証明し、次に二階述語自然演繹をこの体系に翻訳することにより,前者の強正規化可能性を後者のそれに帰着することにより証明を完成させた。
(2)例外処理計算系の強正規化可能性定理に対してCPS変換およびオグメンテーションを用いた証明方法を検討した。
|
Research Products
(1 results)
