|
本研究の目的は、構成的集合と余帰納的定義をもつ構成的論理を構築し、この論理体系を用いて、余帰納型を用いたプログラムの性質を明らかにし、また、構成的集合と余帰納的定義を用いたプログラム合成システムを試作することであった。次のような3つの研究成果を得た。(1)論理式Aが長D-正規証明をもつならば、Aの長正規証明が唯一であることを証明した。(2)古典二階自然演繹の強正規化可能性の証明に関して、CPS変換を用いた従来の証明が本質的誤っていることを主補題に対する反例をあげて示し、この原因が継続消滅の現象によることを指摘し、オグメンテーションの概念を用いてこの証明を完成させた。例外処理ラムダ計算や値呼びラムダミュー計算など他の類似の体系のCPS変換を用いた強正規化可能性の従来の証明が、継続証明により同様にして本質的に誤っていることを指摘した。(3)構成的二階自然演繹に置換簡約を追加した論理体系の強正規化可能性の簡明な証明を与えた。従来知られている証明は、Prawitzによる証明だけであり、これは記述が不完全であり、また複雑な帰納法を必要とした。原子選言論理のアイデアを用い、構成的二階自然演繹に置換簡約を追加した論理体系が原子選言論理に簡約を保存して翻訳できること、原子選言論理は飽和集合が定義でき飽和集合を用いた強正規化可能性の証明方法が使えることの2つから、新しい簡明な証明を得た。
|
