| 研究概要 |
最初に,代入文,繰り返し文をもつ関数型プログラム言語Λの設計,理論的性質の解析を行った.Λは,手続き型言語の特長である代入文糖を持ちながら,関数型言語としての特徴である参照透明性やChurch-Rosser性が成立する,という極めてユニークなプログラム言語である.今年度の研究では,従来のΛを更に洗練,改良する研究として,文脈を利用したΛの定義,および,それに基づく各種の性質の証明の改良を行った.これにより,Λの定義が簡潔になり,見通しのよい証明が得られた.
次に,プログラムの制御構文に対する検討の一環として,Catch/Throw機構に対応する構成的理論体系について検討した.Catch/Throw機構を用いることにより,プログラムを簡潔に記述できることが多く,また,実行効率の良さも期待できることが多い.構成的プログラミングの原理であるCurry-Howardの同型対応では,型付きラムダ計算と純粋な直観主義理論の対応のみが与えられており,Catch/Throwなど,プログラムの制御を与える構文に対しては対応は与えられていなかった.そこで,本年度の研究では,Catch/Throw機構に対応する理論体系を構築することを目標とし,NJ_<ct>とNK_<ct>を提案した.後者は,制限なくCatch/Throw機構を使えるとしたものであり,古典理論に対応し,前者は,ラムダ抽象の導入において一定の制御を加えることにより,直観主義的体系としたものである.NJ_<ct>は構成的プログラミングを行うことがでるので,プログラム作成に利用できることが示された.
|
