1998 Fiscal Year Annual Research Report
| Project/Area Number |
09780244
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
赤間 陽二 東京大学, 大学院・理学系研究科, 助手 (30272454)
|
|---|
| Keywords | linear logic / proof net / linear λ-calculus / tianslation / bisimulation / principal typing / proof expression |
|---|
| Research Abstract |
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ステップの計算に対応することが明らかになった。
|
