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

动态变量绑定机制的新软件理论研究

基本信息

批准号：
15017247
负责人：
佐藤雅彦
金额：
$ 1.98万
依托单位：
Kyoto University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas
财政年份：
2003
资助国家：
日本
起止时间：
2003 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15017247/
关键词：
対象言語メタ言語文法的対象超変数変数の衝突文脈

项目摘要

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

我们继续以超变量的概念对计算系统进行研究，这是我们在2001年和2001年在特定领域研究中进行的。本研究提出的计算系统通过为变量分配级别来改进现有的计算系统，其想法是统一引入该概念。将超变量划分为逻辑系统和逻辑系统，构建一个将超变量形式化的系统。换句话说，目标语言中的变量处于0级，元语言中的变量是数字被设置在级别1，元元语言变量被设置在级别2等，术语也相应地被赋予级别。当β群满足关于级别的特定条件时，在不避免变量冲突的情况下执行赋值操作。这样，我们就可以将低级术语视为目标语言的语法对象。由此产生的计算系统也可以视为目标语言的语法对象。我们表明它保持了理想的属性，例如减少、融合和强标准化。当插入术语时，该研究的方法在形式化上下文概念时也很有效，该术语中出现的变量受到周围的绑定器的约束。漏洞，但这与避免变量冲突的正常赋值不同。为了使用本研究的方法形式化这个条件，将空洞视为一个高级变量就足够了。然后，为空洞分配一个术语的操作是一个文本分配。今年的结果是：我们已经能够表达上下文的组成，这对于以前的研究中考虑的系统来说是不可能的。（发表在题为“元变量”的论文中。）