Maudeによる否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築

摘要

本稿では，プロセス計算の操作意味を定義するときに一般的に用いられる構造操作意味定義(SOS)によって定義されるラベル付き遷移系を実現するインタプリタを書換え論理の処理系であるMaudeによって実装する．SOS規則の前件に否定を含む場合の充足性検査として，Maudeのメタレベルの探索機能を用いることで，一般的なSOSを解釈するインタプリタを構築する．さらに，SOSから導出されるラベル付き遷移系上での項に対する強双模倣等価性検証器をMaudeによって実装し，SOSによって定義される動作仕様上での等価性判定を行うツールを構築し，否定を含むSOSによって定義されるプロセス計算の例として，HennessyのTPLにおける等価性判定を示す．