|
超変数の概念を持った計算系に関する研究を行なった。この計算系は、対象言語、メタ言語、メタメタ言語、…という無限個の階層から成り、ある階層の言語はそれより下の階層の言語のメタ言語となっている。メタ言語で対象言語を扱う仕組を形式化するときは符号化の手法を用いることが多いが、本研究ではより自然にかつ直接的に対象言語を扱えるような機構を提案した。まず、対象言語の変数はレベル0、メタ言語の変数はレベル1、メタメタ言語の変数はレベル2、…と設定し、それにより項にもレベルを付与する。そしてβ基がレベルに関するある条件を満たすときには変数の衝突を避けないで代入操作を行なうことにより、レベルの低い項は対象言語の文法的な対象として扱うことができる。
この仕組は対象言語に依存しないものであり、論理学や計算機科学でよく現れる現象を形式化できる。たとえば論理式を定義するときには限量子で変数を束縛することにより新しい論理式が作られるステップがあるが、それは「対象言語の変数(論理式を構成する変数)に具体化される超変数を含む表現が新しい論理式を定義するが、そのときその変数は限量子で束縛される」というように記述される。このような現象はいわゆる文脈を扱うときにも見られる。すなわち、穴の中に項を挿入するときその項に出現する変数が穴を囲むバインダで束縛されるということが起こるが、それは通常の変数の衝突を避ける代入とは異なる。
なお、この計算系では、subject reduction、合流性、強正規化性といった種々の良い性質が成立することも証明した。
|
