|
本研究の目的は、構成的集合と余帰納的定義をもつ構成的論理を構築し、この論理体系を用いて、余帰納型を用いたプログラムの性質を明らかにし、また、構成的集合と余帰納的定義を用いたプログラム合成システムを試作することである。特に、(1)余帰納型に内在する計算の本質は何か明らかにする、(2)余帰納的定義の証明論的強さを調べることにより余帰納型により表現できる関数を分類する、(3)構成的集合と余帰納的定義を用いたプログラムの検証、合成を行うための論理体系の構築、(4)構成的集合と余帰納的定義を合わせもつ論理に対する実現可能性解釈の定義、(5)一般的余帰納型による既存プログラミング言語の拡張、(6)構成的集合と余帰納的定義を用いたプログラム検証、合成システムの実現、(7)ストリームプログラム、並行プログラム、セキュリティプロトコールの検証および合成実験、の研究を行う。
本年度では次の研究を行った。(1)余帰納型の形式化の方式および余帰納型に内在する計算の本質の捉え方の比較検討を行い、余帰納型のもつ計算の本質を明らかにした。(2)これにより得られた知見に基づいて、構成的集合と余帰納的定義を用いて余帰納型を用いたプログラムの検証、合成を行うための論理を構築した。(3)により得られた知見を用いて、既存の関数型プログラミング言語の拡張を試みた。
|
