変数の動的束縛機構をもつ新しいソフトウェアの理論的研究

Research Project

Project/Area Number	15017247
Research Category	Grant-in-Aid for Scientific Research on Priority Areas
Allocation Type	Single-year Grants
Review Section	Science and Engineering
Research Institution	Kyoto University
Principal Investigator	佐藤雅彦京都大学, 情報学研究科, 教授 (20027387)
Co-Investigator(Kenkyū-buntansha)	中澤巧爾京都大学, 情報学研究科, 助手 (80362581) 亀山幸義筑波大学, 電子・情報工学系, 助教授 (10195000) 桜井貴文千葉大学, 理学部, 助教授 (60183373)
Project Period (FY)	2003
Project Status	Completed (Fiscal Year 2003)
Budget Amount *help	¥3,100,000 (Direct Cost: ¥3,100,000) Fiscal Year 2003: ¥3,100,000 (Direct Cost: ¥3,100,000)
Keywords	対象言語 / メタ言語 / 文法的対象 / 超変数 / 変数の衝突 / 文脈
Research Abstract	平成13,14年度の特定領域研究で行なった,超変数の概念を持った計算系に関する研究を引き続き行なった.本研究で提案した計算系は,変数にレベルを付与することにより既存の計算体系や論理体系に統一的に超変数の概念を導入し,超変数を形式化した体系を構成するというものである.つまり,対象言語の変数はレベル0,メタ言語の変数はレベル1,メタメタ言語の変数はレベル2,…と設定し,それにより項にもレベルを付与する.そしてβ基がレベルに関するある条件を満たすときには変数の衝突を避けないで代入操作を行なうことにより,レベルの低い項は対象言語の文法的な対象として扱うことができるようにした.そしてその結果としてできる計算体系もsubject reduction、合流性、強正規化性といった好ましい性質を保っていることを示した. 本研究の手法は文脈の概念の形式化をする際にも有効である.つまり,文脈の穴の中に項を挿入するときその項に出現する変数が穴を囲むバインダで束縛されるということが起こるが,それは通常の変数の衝突を避ける代入とは異なる字面上の代入である.この状沢を本研究の方法で形式化するには,穴を高いレベルの変数と見なせばよい.するとその穴への項の代入操作は字面上の代入となる.本年度の成果は,先行研究で考えられていた体系ではできなかった,文脈の合成の表現ができるようになった点である.(この結果については,"Calculi of Meta-variables"という論文で発表した.)