変数の動的束縛機構をもつ新しいソフトウェアの理論的研究
| Project/Area Number |
14019047
|
|---|
| 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) |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
|
|---|
| Project Period (FY) |
2002
|
| Project Status |
Completed (Fiscal Year 2002)
|
| Budget Amount *help |
¥3,000,000 (Direct Cost: ¥3,000,000)
Fiscal Year 2002: ¥3,000,000 (Direct Cost: ¥3,000,000)
|
|---|
| Keywords | 対象言語 / メタ言語 / 文法的対象 / 超変数 / 変数の衝突 / 合流性 / 強正規化性 |
|---|
| Research Abstract |
超変数の概念を持った計算系に関する研究を行なった。この計算系は、対象言語、メタ言語、メタメタ言語、…という無限個の階層から成り、ある階層の言語はそれより下の階層の言語のメタ言語となっている。メタ言語で対象言語を扱う仕組を形式化するときは符号化の手法を用いることが多いが、本研究ではより自然にかつ直接的に対象言語を扱えるような機構を提案した。まず、対象言語の変数はレベル0、メタ言語の変数はレベル1、メタメタ言語の変数はレベル2、…と設定し、それにより項にもレベルを付与する。そしてβ基がレベルに関するある条件を満たすときには変数の衝突を避けないで代入操作を行なうことにより、レベルの低い項は対象言語の文法的な対象として扱うことができる。
この仕組は対象言語に依存しないものであり、論理学や計算機科学でよく現れる現象を形式化できる。たとえば論理式を定義するときには限量子で変数を束縛することにより新しい論理式が作られるステップがあるが、それは「対象言語の変数(論理式を構成する変数)に具体化される超変数を含む表現が新しい論理式を定義するが、そのときその変数は限量子で束縛される」というように記述される。このような現象はいわゆる文脈を扱うときにも見られる。すなわち、穴の中に項を挿入するときその項に出現する変数が穴を囲むバインダで束縛されるということが起こるが、それは通常の変数の衝突を避ける代入とは異なる。
なお、この計算系では、subject reduction、合流性、強正規化性といった種々の良い性質が成立することも証明した。
|
Report
(1 results)
Research Products
(4 results)
