自己反映的プログラミングのための計算・論理体系

点击翻译按钮获取中文摘要

本研究では、これまで行ってきた計算体系における自己反映性の研究を基にして、自己反映性を持つ論理・計算体系の確立を目標とした。具体的には高階型理論の一種である多相型付きラムダ計算を、ファーストクラス環境の機能を付加することにより拡張した論理・計算体系を構築した。本年度においては次のような計画のもとに研究は遂行された。【ファーストクラス環境を持つ多相型理論の基本的性質の解明】従来の多相型つきラムダ計算においては、さまざまな数学的性質が知られていた。それらの性質がファーストクラスな環境をもつ多相型理論において、どのように成り立つのかということの解明に取り組んだ。特に、ファーストクラス環境をもつ多相型つきラムダ計算の型推論アルゴリズムの提案と、そのアルゴリズムの健全性・停止性・完全性について研究した。【ファーストクラス環境を持つ多相型理論の意味論】ファーストクラス環境を持つ多相型付きラムダ計算の意味論について研究した。意味論は、レコードを含むような多相型付きラムダ計算への変換により与えられた。【プロトタイプシステムの実装】ファーストクラス環境をもつ多相型つきラムダ計算の型推論アルゴリズムのプロトタイプシステムを実装し、その有効性について検討した。