操作的意味を保存するプログラム変換の研究

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14780251
• Research Institution: National Institute of Advanced Industrial Science and Technology
• Principal Investigator: 渡邊 宏 独立行政法人 産業技術総合研究所, 情報処理研究部門, 研究員 (80344183)
• Keywords: 操作的意味 / 余代数 / 分配則 / モナド / プログラム変換 / 遷移系

Research Abstract

操作的規則の分配則モデル間のマップが,言語の振舞いを記述した遷移系の間の双模倣を導き,操作的意味を保存する変換を与えることを示した.そのような変換を実際のプログラミング言語やプロセス代数の具体例の中で見つけるための道具として,分配則のマップの存在を示すのに使える補題を4つ作った.この補題を使って次の三つの分配則のマップのインスタンスを示した.
一つ目は言語の意味保存拡大の例である.与えられた言語に対して,言語のシグネチャをと操作的規則を増やして言語を拡張することが,分配則のマップのインスタンスとして捉えられることを示した.分配則のマップがあることで,拡張前後のプログラムの振舞いを記述した遷移系の間の双模倣が存在し,拡張前の言語のプログラムの振舞いが拡張後も変化しないことが保証される.
二つめはインターリービングによるパラレルオペレーターを持つプログラミング言語をレフトマージオペレーターと非決定的和を持つプログラム言語へ変換する事例である.
三つ目はプログラム変換と少し異なり,一つの言語についての二つの操作的規則どうしが矛盾しないことを示す例である.プロセス代数に対して,通常の遷移系を生成する操作的規則と,トレースを生成する操作的規則が互いに矛盾しないことを,それらの操作的規則のモデルの分配則間にマップがあること示して説明した.

Research Products

• [Publications] Hiroshi Watanabe: "Well-behaved Translations between Structural Operational Semantics"Electronic Notes in Theoretical Computer Science. 65・1. (2002)
• [Publications] John Power, Hiroshi Watanabe: "Combining a monad and a comonad"Theoretical Computer Science. 280. 137-162 (2002)