1997 Fiscal Year Annual Research Report
線形論理の意味論的手法による並行計算概念および実行可能計算量概念の論理的分析
| Project/Area Number |
09878062
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Keywords | セマンティクス / タイプ理論 / 並行計算 / 高階論理 / 実現可能計算量 / 計算モデル / 線形論理 / 正規化定理 |
|---|
| Research Abstract |
これまで並行プロセス計算の理論で研究されてきたペトリ・ネットやデータフロー・ネットなどに代表されるような抽象的ネットワークモデルや枠組や、R.Milnerのπ-計算に代表されるような代数的手法の枠組が線形理論の構文論(シンタクス)を用いて論理的な枠組で再構成されることがこれまでに知られてきた。線形論理の構文論の枠組において再構成されたこれらの並行計算モデルに対して、申請者が導入した線形論理のためのダイナミックな意味論を適用することにより、これまでの並行計算理論において得られなかった論理的観点からの並行計算の意味論が与えられた。例えば、π-計算や種々の並行プロセス計算理論で代数的手法により研究されてきた種々のobservable equivalence概念に対して論理的観点からの分析が与えられた。ここで確立した方法論を用いて種々のweak bisimulation equivalence概念に対するphase semanticsによる特徴付けを与えた。又、データフロー・ネットの種々のoptimization problemsへのphase-semanticsの応用を与えた。例えば、bounded buffer-sizaを持つkahnのregular deta flow netに対してdeadlock無しのcommunicationに必要な最小のbuffer-sizeを決定する問題や最大の並行処理を行い最短時間で同等のtaskを行うためのnetworkの仕様を決定する問題などは、論理的枠組を用いずに伝統的な並行アルゴリズムの分析手法だけを用いては体系的な解決が困難な問題であった。一方、これらの問題は、並行プロセスと線形論理の証明との同一視を通せば、証明の正規化概念を用いて線形論理上で正確に問題を定式化できる。申請者が導入したダイナミックなphase semanticsをこの論理的定式化された問題に適応することにより、これらの並行計算ネットワークに関するoptimization(最適化)問題研究への方法論が示された。
|
Research Products
(8 results)
-
[Publications] M.Okada: "Phase Semantics for Higher Order Completeness.Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. (to appear). (1998)
-
[Publications] M.Okada-K.Terui: "The Finite Model Property for Various Fragments of Intuitionistic Linear Logic" J.Symbolic Logic. (to appear). (1998)
-
[Publications] M.Hamano-M.Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear). (1998)
-
[Publications] J-P.Jouannaud,M.Okada: "Abstract Data Type Systems" Theoretical Computer Science. 173. 349-391 (1997)
-
[Publications] M.Hamano-M.Okada: "A Relationship Among Gentzen's Proof Reduction,Kirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)
-
[Publications] M.Kanovitch,M.Okada,A.Scedrov: "Phase Semantics for Light Linear Logic" Electronic Notes of Theoretical Computer Science. 6. 1-14 (1997)
-
[Publications] M.Okada: "Types and Proofs(2 chapters 分担)" Mathematical Society of Japan(近刊), (1998)
-
[Publications] 岡田光弘: "情報科学のための論理学" 産業図書, 250 (1998)
