抽象高階書換え系によるプロセス計算系の定式化に関する研究

2002 Fiscal Year Annual Research Report

• Project/Area Number: 13680388
• Research Institution: The University of Aizu
• Principal Investigator: 鈴木 大郎 会津大学, コンピュータ理工学部, 講師 (90272179)
• Co-Investigator(Kenkyū-buntansha): 奥居 哲 中部大学, 工学部, 助教授 (00283515)
• Keywords: π-計算系 / 抽象高階項書換え系 / 等式付き項書換え系 / 書換え論理 / 高階ナローイング / パターン項書換え系

Research Abstract

今年度は,(1)π計算系の等式付き抽象高階項書換え系による定式化 (2)抽象高階項書換え系による一階および高階のナローイングの一般化の二つの作業を行った.
(1)に関しては,まず,昨年度の問題点であった変数の局所化に関するπ計算系と抽象高階書換え系の違いをどう埋めるかについて,考察を行った.その結果,λ抽象をうまく用いることで,二つの体系の間の差を埋めることに成功した.また,抽象高階項書換え系に等式の集合を追加することで,π計算系の構造合同性が自然に定式化できることを見出した.このため,等式付き抽象高階項書換え系の定義を行い,それを用いてπ計算系の定式化を得た.さらに,プロセス定義式を直接定式化することで,二つのプロセス式間の構造合同性の決定可能性に関する十分条件を書換え系の枠組みで検討することへの道筋を開いた.今後,この方向へ研究を続けることで,書換え的手法を用いたプロセス計算系の理論的性質の解明を行っていきたい.
今後研究を進めたいのは,今回の定式化の結果で用いた体系とMesegureの書換え論理との関係である.書換え論理は,等式付き項書換え系がみたす論理体系を記述したものとみなせるが,等式付き項書換え系そのものではなく,その論理としたことで抽象的な枠組みを獲得している.一方,等式付き抽象高階項書換え系は,高階性を導入したことで,抽象的な枠組みを獲得している.後者の方が,λ項という構文的により豊かな枠組みをもっているために,対象の理論的性質を構文論的な手法で議論するには適すると予想しているが,両者の厳密な比較はこれからの課題である.
(2)は抽象高階項書換え系と一階および高階ナローイングとの関係についての研究である.プロセス計算系は並列論理型言語の意味論を与えることは知られているが,ナローイングは関数型と論理型を包含した関数論理型言語の意味論を与える.このことから,抽象高階項書換え系におけるナローイングの研究とプロセス計算系の定式化の研究を並行して行った.ナローイングを抽象高階項書換え系を用いて二通りの方法で定式化できることと,見かけ上まったく異なるそれらの定式化がパターン項書換え系と呼ばれる標準的なクラスでは一致することを示した.また,この定式化にしたがうナローイングが求解完全性をもつことを示した.

Research Products

• [Publications] T.Ida, M.Marin, T.Suzuki: "Reducing Search Space in Solving Higher-Order Equations"Lecture Notes in Artificial Intelligence 2281. 19-30 (2002)
• [Publications] 奥居哲, 鈴木太朗: "抽象高階書換え系におけるナローイング"会津大学テクニカルレポート. (予定). (2003)
• [Publications] 鈴木太朗, 奥居哲: "π計算系の抽象高階項書換え系による定式化"会津大学テクニカルレポート. (予定). (2003)