| 研究課題/領域番号 |
09780244
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
赤間 陽二 東京大学, 大学院・理学系研究科, 助手 (30272454)
|
|---|
| 研究期間 (年度) |
1997 – 1998
|
| 研究課題ステータス |
完了 (1998年度)
|
| 配分額 *注記 |
2,300千円 (直接経費: 2,300千円)
1998年度: 1,100千円 (直接経費: 1,100千円)
1997年度: 1,200千円 (直接経費: 1,200千円)
|
|---|
| キーワード | linear logic / proof net / linear λ-calculus / tianslation / bisimulation / principal typing / proof expression / 組合せ論理 / 強正規 / 翻訳 / 環境計算 / 外延性 / 交型理論 / 部分組合せ代数 / 終代数 |
|---|
| 研究概要 |
BerryとBoudolが導入したCHAMは並行計算を記述するための項の書き換え系で、並行計算を化学反応になぞらえて得られた論点は以下の2点である。
1. 計算論的な抽象的な資源の移り変わり。
項(“分子")を資源として扱うために項の多重集合(“溶液")もまた項とされ、多重集合のなかの各項に書き換え(“化学反応")が独立に起きる。
2. カプセル化された計算。
書き換えの及ぶ範囲が定められているため、や、ネットワークの動的な変化が記述できる。Girardの線形論理は、推論過程における論理的な資源の移り変わりを記述できるのだが、線形論理により、CHAMの上記1点目のことが記述できる考える。また、線形論理の証明図の表現の一つであるGirardのproof netは、boxと呼ばれる入れ子構造を持つのだが、対応してCHAMでは複数の計算主体が単一のものとみなされることがある。
私は、CHAMの一種でAbramskyが導入したlinear chemical abstract machine(LCHAM)をまず取り扱い、そこにおける計算資源の移り変わりが機械的に推論するできること(主型定理)を証明した。また、関数型プログラミング言語の中間言語の一つである線形λ計算からLCHAMへの翻訳を導入した。線形λ計算の項のその翻訳による結果は、入出力ポートが原始的であるような計算単位となる。また、この翻訳により、線形λ計算における1ステップの計算はLCHAMにおける1ステップの計算に対応することが明らかになった。
|
