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

2001 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

今年度は,まず,Mayrによるプロセス書換え系と抽象高階書換え系との対応関係について検討し,ついでMilnerにより提案されたπ-計算系の抽象高階書換え系による定式化の検討を行った.この過程でいくつかの問題点が浮かび上がった.その中でもっとも大きな問題点は,局所化に関する違いの問題である.抽象高階書換え系は,関数の数学的理論であるλ計算に基礎を置いている.このため,局所化はλ抽象により導入される束縛変数により局所化を実現している.一方,π-計算系が提供している局所化の枠組みはλ抽象に類似しているが,それよりも柔軟性が高い.このため,抽象高階書換え系により定式化しようとすると,局所化の部分で微妙にずれが生じてしまうことがわかった.この問題に関して,いくつかの解決策を検討したが,決定的なものはまだ得られていない.平成14年度には,この点についての検討をひきつづき行い,π-計算系の抽象高階書換え系への定式化方法の確立をめざす.
また,プロセス計算を抽象高階書換え系で定式化できれば,高階項書換え系上での高階ナローイングの研究と組み合わせることで,並行関数論理型プログラミング言語に関する自然な計算モデルが得られることが期待される.この方向へ研究をすすめるために、Prehoferにより提案された高階ナローイング計算系を出発点として,新たな高階ナローイング計算系をいくつか提案し,それらの完全性を示した.高階ナローイング計算系では,その探索空間の広さが実装上の大きな問題点となるが,提案された計算系は,Prehoferのものより探索空間をより小さくできる.

Research Products

• [Publications] A.Middeldorp, T.Suzuki, M.Hamada: "Complete Selection Functions for a Lazy Conditional Narrowing Calculus"Journal of Functional Logic Programming. (To Appear). (2002)
• [Publications] M.Marin, T.Suzuki, T.Ida: "Higher-Order Lazy Narrowing for Left-Linear Fully-Extended Pattern Rewrite Systems"筑波大学電子・情報工学系テクニカルレポート. ISE-TR-01-180. (2001)