| 研究実績の概要 |
コンパクト集合の T^omega 表現についての研究をより精密化した。コンパクト集合の T^omega 表現の hereditary, faithful, matching representation などの性質を整理し，Proper Dyadic subbase との関係性を明確にした。最終的に，computably compact computable metric space のコンパクト集合全体は，faithful な T^omega 表現を持つという形の主定理が得られた。それ以外にも，証明や論文の手直しを行い，論文誌への投稿を行なった。
IFP について研究を進めた。IFP は，一階述語論理に最小不動点，最大不動点として述語を定義する機能を付け加えた論理体系であり，抽象的な数学の証明からプログラムを抽出することができる。IFP は，これまでのプログラム抽出のための論理体系とは異なり，計算的な対象とはならない数学的対象の上で量化子を行なうことができる。このことを用いて，部分関数を意味するプログラムを抽出することが可能となり，その応用としてグレイコードを出力するプログラムを数学的証明から抽出することができる。IFP において抽出されたプログラムが正しく動くことの証明は，Adequacy theorem を経由して証明される。IFP の無限的部分計算の機能に合致した adequacy theorem を，induction, coinduction という IFP の枠組みに沿った形で行なった。また，この意味論を CFP のプログラムの実行の正しさとつなげるための研究も行なった。
|
