| 研究概要 |
関数型プログラム言語における非局所脱出機構を取り上げ,構成的論理との対応を調べた.まず,Common Lispなどにおける非局所脱出機構であるCatch/Throw機構を取り上げ,CatchとThrowのそれぞれに対応する推論規則を持つ型理論的体系について検討した.型理論の体系では最も興味深い性質の1つである停止性(強正規化可能性)が,従来提案されていた体系に対して成立することを,強いreducibilityという概念を新たに用いることにより証明した.
次に,従来提案されていた体系では,プログラムの記述力が弱く,高階関数プログラミングを自然に展開することができないことを指摘し,停止性が成立する範囲内でどこまで体系の表現力を上げることができるか検討した.その結果,新たに,「データの型(関数型構成子を使わないで構成できる型)に対するCatch/Throwは無制限に使ってよい,という緩い制限のもとでも,型理論的体系が構成でき,停止性も成立することを示した.現実のプログラムの中で発生するCatch/Throwは,基礎データの受け渡しに使われることが大部分であるため,この制限は非常に合理的である.新しく提案したCatch/Throw機構を持つ体系において,多くのプログラム例を記述し,提案した体系が構成的プログラミングの観点から有用なものであることを示した.
本研究では主としてCatch/Throw機構を扱ったが,関数型言語MLにおける非局所脱出機構であるException機構も,同様に,本研究での体系で記述することができる.そこで,Exception機構を用いた例も作成した.
|
