| Research Abstract |
本研究の目的は,分散環境のみならず,より一般的な枠組において,ソフトウェアの動的な移動の機能を実現し,さらにそれを解析できるようにするための理論的な裏付けを与えることであった.そのために,本研究では,変数の動的な束縛機構をもつ新しい計算体系を提案しその理論的な性質を解明することを目標とした.
本研究では,明示的環境や明示的文脈を持った計算系を提案した.この体系では,通常メタレベルで扱われる環境や文脈を体系内で形式化している.しかし,文脈の扱いについては,依然として,メタレベルで可能なすべての操作ができるような体系にはなっていないので柔軟性を欠く点があり,さらに研究を進めている必要がある.
この体系の計算では,文脈の穴が超変数の役割を持っていて,穴へプログラムを挿入するときに変数への束縛が起こるとみなすことが出来る.この点に注目すれば,文脈に関するメタレベルでの操作をすべて形式化することが出来るであろう.更に,超変数の概念を形式化するにはメタレベルでのどのような概念を形式化すればよいのかがはっきりしてくるはずである.
この計算系は型理論に基くものである.本研究ではこの計算系に対する理論的考察を行った.ここでいう理論的考察とは,型の保存性,合流性,強正規化可能性,従来の体系に対する保守的拡大性などのことである.この計算系はこれらの性質を充すことが確かめられた.
この体系は計算機上に部分的にではあるが実装された.
|
