環境と文脈を持つ計算体系とその論理

2002 Fiscal Year Annual Research Report

• Project/Area Number: 13480082
• Research Institution: Kyoto University
• Principal Investigator: 佐藤 雅彦 京都大学, 情報学研究科, 教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 五十嵐 淳 京都大学, 情報学研究科, 講師 (40323456) ; 竹内 泉 東邦大学, 理学部, 講師 (20264583) ; 亀山 幸義 筑波大学, 電子・情報工学系, 助教授 (10195000)
• Keywords: 文脈 / 環境 / 対象言語 / メタ言語 / 超変数 / 合流性 / 強正規化性 / 変数の衝突

Research Abstract

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

Research Products

• [Publications] Masahiko Sato: "CAL : A Computer Assisted Learning system for Computation and Logic"EUROCAST 2001, LNCS 2178. 509-524 (2002)
• [Publications] Masahiko Sato: "A Simply Typed Context Calculus with First-Class Environments"The Journal of Functional and Logic Programming. 2002・4. 1-41 (2002)
• [Publications] Azza, A.Taha: "A Second Order Context Calculus"Journal of Information Processing Society of Japan. 19・3. 158-175 (2002)
• [Publications] Yukiyoshi Kameyama: "Strong Normalizability of the Non-deterministic Catch/Throw Calculi"Theoretical Computer Science. 272・1-2. 223-245 (2002)
• [Publications] 山本 和樹: "擬似引用を持つ型付計算体系λq"日本ソフトウェア科学会第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集. 87-102 (2003)