| 研究概要 |
平成13,14年度の特定領域研究で行なった,超変数の概念を持った計算系に関する研究を引き続き行なった.本研究で提案した計算系は,変数にレベルを付与することにより既存の計算体系や論理体系に統一的に超変数の概念を導入し,超変数を形式化した体系を構成するというものである.つまり,対象言語の変数はレベル0,メタ言語の変数はレベル1,メタメタ言語の変数はレベル2,…と設定し,それにより項にもレベルを付与する.そしてβ基がレベルに関するある条件を満たすときには変数の衝突を避けないで代入操作を行なうことにより,レベルの低い項は対象言語の文法的な対象として扱うことができるようにした.そしてその結果としてできる計算体系もsubject reduction、合流性、強正規化性といった好ましい性質を保っていることを示した.
本研究の手法は文脈の概念の形式化をする際にも有効である.つまり,文脈の穴の中に項を挿入するときその項に出現する変数が穴を囲むバインダで束縛されるということが起こるが,それは通常の変数の衝突を避ける代入とは異なる字面上の代入である.この状況を本研究の方法で形式化するには,穴を高いレベルの変数と見なせばよい.するとその穴への項の代入操作は字面上の代入となる.本年度の成果は,先行研究で考えられていた体系ではできなかった,文脈の合成の表現ができるようになった点である.(この結果については,"Calculi of Meta-variables"という論文で発表した.)
|
