構成的集合と余帰納的定義を用いたプログラム合成

2001 Fiscal Year Annual Research Report

• Project/Area Number: 12680346
• Research Institution: National Institute of Informatics
• Principal Investigator: 龍田 真 国立情報学研究所, 情報学基礎研究系, 教授 (80216994)
• Co-Investigator(Kenkyū-buntansha): 照井 一成 国立情報学研究所, 情報学基礎研究系, 助手
• Keywords: プログラム合成 / 構成的集合 / 余帰納的定義 / 構成的論理 / 実現可能性解釈

Research Abstract

本研究の目的は、構成的集合と余帰納的定義をもつ構成的論理を構築し、この論理体系を用いて、余帰納型を用いたプログラムの性質を明らかにし、また、構成的集合と余帰納的定義を用いたプログラム合成システムを試作することであった。特に、(1)余帰納型に内在する計算の本質は何か明らかにする、(2)余帰納的定義の証明論的強さを調べることにより余帰納型により表現できる関数を分類する、(3)構成的集合と余帰納的定義を用いたプログラムの検証、合成を行うための論理体系の構築、(4)構成的集合と余帰納的定義を合わせもつ論理に対する実現可能性解釈の定義、(5)一般的余帰納型による既存プログラミング言語の拡張、(6)構成的集合と余帰納的定義を用いたプログラム検証、合成システムの実現、(7)ストリームプログラム、並行プログラム、セキュリティプロトコールの検証および合成実験、の研究を行うことを目的とした。
1.二階古典自然演繹の強正規化性に関してCPS変換をもちいたParigotの証明の誤りを指摘し、その原因であるCPS変換の継続消滅について論じ、オグメンテーションの概念を用いて証明を完成させた。
2.12年度の研究により得られた論理体系を用いて、証明論的強さを調べることにより一般的余帰納型により表現できる関数の分類を明らかにした。
3.ストリームプログラム、並行プログラム、セキュリティプロトコールの検証、合成の可能性を明らかにした。