| 配分額 *注記 |
7,300千円 (直接経費: 7,300千円)
2003年度: 1,700千円 (直接経費: 1,700千円)
2002年度: 2,600千円 (直接経費: 2,600千円)
2001年度: 3,000千円 (直接経費: 3,000千円)
|
|---|
| 研究概要 |
本研究の目的は,環境と文脈の概念を第一義的な要素としてもつ計算体系を構築し,この計算体系を論理の立場より分析することによって,環境と文脈を持つ計算体系の特性を明らかにすることである.本研究の主要な成果は以下の通りである.
1.明示的環境や明示的文脈を持った計算体系
環境や文脈を第一義的な要素として扱うことができる計算体系を提案した.この体系では,通常メタレベルで扱われる環境や文脈を,体系内で形式化している.この体系は型理論に基づいて構築し,型の保存性,合流性,強正規化可能性,従来の体系に対する保守的拡大性などを証明した.
2.超変数を持った計算体系
文脈の穴は,その穴にプログラムを挿入するときに変数束縛が発生するなど,超変数の役割を持っている.本研究では,超変数を持つ計算体系を提案し,その性質を調べた.この体系は,対象言語の変数をレベル0,メタ言語の変数をレベル1,メタメタ言語の変数をレベル2,などと設定し,それにより項にもレベルを付与することにより,超変数への代入の際に発生する変数束縛を表現できるようにした.これにより,レベルの低い項は対象言語の文法的な対象として扱うことができる.この体系は,変数衝突を避けない代入を表現できるため,文脈の概念を形式化する際にも有効である.実際に,上で提案した計算体系では実現できなかった文脈の合成が,この体系では表現できることを明らかにした.さらに,この計算体系が型の保存性,合流性,強正規化可能性などの好ましい性質をもつことを証明した.
|
