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

点击翻译按钮获取中文摘要

時間付きフォーマットなどの操作的規則のメタな統語的記述法を調査した。Kickらによる分配則を使った時間付きプロセスのモデルの理論、Bartelsらによる確率の入ったプロセスのモデルの理論をサーベイし、時間付きプロセスのための分配則については、分配則間の射が時間付きプロセスの双模倣で振舞いを保存する変換を与える見通しを得た。また、確率プロセスのための分配則についても、分配則の射が確率プロセスの双模倣で振舞いを保存する変換を与える見通しを得た。さらに、それぞれについて変換の具体例を探した。操作的規則の分配則間の射の統語的に書き下すことに関して、Klinによるトレース同値の合同関係を与える分配則を統語的に書き下すテクニックを理解し、応用できるかどうかを検討した。分配則から統語的表現へ変換する部分についてはテクニックが使えることがわかった。ただし、分配則の射を統語的表現に直すところは完成していない。操作的意味を保存する言語拡大についてAcetoらのアプローチと分配則の射のインスタンスの相違点について、Acetoらの操作的意味を与えるフォーマットが分配則の与えるフォーマットよりも広いこと、Acetoらの操作的意味を与えるフォーマットを制限すれば変換は一致することがわかった。多ステップの分配則モデルとその間の射を用いて弱双模倣をもたらすプログラム変換の特徴づけする試みはまだ検討中である。