| 研究概要 |
本研究は,書換え系の枠組みで移動体(mobile)プロセスの諸計算系の定式化を行うことを目的とした.この定式化を行うことで,書換え系の視点からプロセスの等価性や型判定などの自動検証に寄与できる
抽象高階書換え系はvan Oostromにより提案された高階項書換え系である力舳の高階項書換え系と大きく異なるのは,代入計算と呼ばれる仕組みを導入することで,書換えを代入のフェーズと置換のフェーズに明確に分離している点である.正確には,抽象高階項書換え系はメタな枠組みであり,具体的に代入計算を与えることで様々な書換え系を表現することができる.我々は,この特徴に着目し,抽象高階項書換え系を用いてπ計算系をはじめとする種々の移動体プロセス計算系の定式化を試みた.その結果として,抽象高階項書換え系に等式の集合を追加することで,π計算系を定式化できることを見いだした.
今回,プロセス計算系と書き換え系とを対応づけたことによって,プロセス計算系の理論的性質を書き換え的なアプローチから解明することが可能となった.今後,この方向にさらなる研究を続けていきたい.
もう一つの我々の研究成果は,抽象高階項書換え系と一階および高階ナローイングとの関係についての研究,および高階ナローイングの理論的性質に関する研究である.プロセス計算系は並列論理型言語の意味論を与えることは知られているが,ナローイングは関数型と論理型を包含した関数論理型言語の意味論を与える.このことから,抽象高階項書換え系におけるナローイングの研究とプロセス計算系の定式化の研究を並行して行った.まず、我々はPrehoferにより提案された高階ナローイング計算系を出発点として,新たな高階ナローイング計算系をいくつか提案し,それらの完全性を示した.高階ナローイング計算系では,その探索空間の広さが実装上の大きな問題点となるが,提案された計算系は,Prehoferのものよりも探索空間をより小さくできることを示した.さらに,一階および高階のナローイングを抽象高階項書換え系を用いて二通りの方法で定式化できることと,見かけ上まったく異なるそれらの定式化がパターン項書換え系と呼ばれる標準的なクラスでは一致することを示した.また,この定式化にしたがうナローイングが求解完全性をもつことを示した.
|
