| 研究課題/領域番号 |
14780251
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 独立行政法人産業技術総合研究所 |
|---|
研究代表者 |
渡邊 宏 独立行政法人産業技術総合研究所, システム検証研究センター, 研究員 (80344183)
|
|---|
| 研究期間 (年度) |
2002 – 2004
|
| 研究課題ステータス |
完了 (2004年度)
|
| 配分額 *注記 |
3,300千円 (直接経費: 3,300千円)
2004年度: 1,100千円 (直接経費: 1,100千円)
2003年度: 1,100千円 (直接経費: 1,100千円)
2002年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | 操作的意味 / 余代数 / 分配則 / モナド / プログラム変換 / 遷移系 |
|---|
| 研究概要 |
時間付きフォーマットなどの操作的規則のメタな統語的記述法を調査した。Kickらによる分配則を使った時間付きプロセスのモデルの理論、Bartelsらによる確率の入ったプロセスのモデルの理論をサーベイし、時間付きプロセスのための分配則については、分配則間の射が時間付きプロセスの双模倣で振舞いを保存する変換を与える見通しを得た。また、確率プロセスのための分配則についても、分配則の射が確率プロセスの双模倣で振舞いを保存する変換を与える見通しを得た。さらに、それぞれについて変換の具体例を探した。
操作的規則の分配則間の射の統語的に書き下すことに関して、Klinによるトレース同値の合同関係を与える分配則を統語的に書き下すテクニックを理解し、応用できるかどうかを検討した。分配則から統語的表現へ変換する部分についてはテクニックが使えることがわかった。ただし、分配則の射を統語的表現に直すところは完成していない。
操作的意味を保存する言語拡大についてAcetoらのアプローチと分配則の射のインスタンスの相違点について、Acetoらの操作的意味を与えるフォーマットが分配則の与えるフォーマットよりも広いこと、Acetoらの操作的意味を与えるフォーマットを制限すれば変換は一致することがわかった。
多ステップの分配則モデルとその間の射を用いて弱双模倣をもたらすプログラム変換の特徴づけする試みはまだ検討中である。
|
