並行計算のための簡約意味論

概要

論文の詳細を見る
本稿では,観測,あるいは,停止性の概念に基づかない,並行プロセスのための等価理論の定式化を提示する.この定式化では,簡約関係と等式推論のみを基礎に据えた新しい意味論構築方法に基づき,強相互模倣性に対応する強い等式理論と,弱相互模倣性に対応する弱い等式理論が導出される.様々な形式系にこの等式理論を適用すると,相互模倣性に基づいた動作等価性と一致するか,あるいは,それをより一般化した等価概念を導く.われわれは,まず名前通信に基づく簡潔な形式系であるν-計算を例として,等式理論の基本的な諸定義を与え,並行計算の等価性の基礎として,簡約閉包性の概念を導入する.さらに,λ-計算の不定式に対応した不作用項とよばれる項集合の同一視という条件を簡約閉包性に加えることで,形式系特有の観測可能性が導かれることを示す.この結果を用いて,簡約閉包であり,かつ,不作用項の同一視を行なう等価理論の属の中で,その等価性において最大のものが導出される.この規範的な等価理論,および,そこから簡約回数を数えることで導びかれる強い等価理論の性質を,従来の相互模倣性の等価性との比較を中心に考察する.また,他の形式系にこの簡約を基礎とした意味論構築を適用した結果についても,簡単に議論する.
1994-09-16

並行計算のための簡約意味論

スポンサーリンク

概要

著者

関連論文

スポンサーリンク