|
本課題の主たる目的は、プログラムや証明を一個もしくは複数個の例から合成する手法を、型理論(型付きλ計算)の枠組を用いて研究することにある 本研究では、研究代表者の従来の研究を発展させ、型理論を中心として、プログラムや証明を例から合成する手法を考察し、主として以下のような成果を得た。
★算術制約の入った型理論
算術的な制約を型理論に付加し、制約の推論を暗黙に行うことが可能な体系を用いることにより、従来の体系では一般化が不可能な繰り返し構造を合成することができることを示した。
また、機械学習とは関連がないが、算術制約の技術の応用として、関数型言語のtupling変換に関する研究を行なった。
★機械学習のためのユーザ・インタフェース
-般化機能を、証明テキスト中に挿入され繰り返しを指摘するためのannotationによって呼び出せるようにする方法を考案した。この研究で得たユーザ・インタフェースに関する基本的な考え方に従って、例からプログラムを合成する能力を有するスプレッド・シートを開発した。
★帰納法に関する考察
証明の例からの合成は、帰納法を用いた証明の一方法である 本研究では算術制約の推論機能により繰り返し構造の一般化が容易になることを示したが、さらに、算術制約の推論機能は、例がない場合でも有用であることがわかった。
★自動証明機能を利用した一般化
本研究では、主として、型理論のもとで書かれた証明の一般化について考察したが、その最後の段階で、tacticやresolutionなどの自動証明機能を利用して作られる証明の一般化に関して考察した。
|
