1998 Fiscal Year Annual Research Report
| Project/Area Number |
09740162
|
|---|
| Research Institution | Tokyo Woman's Christian University |
|---|
Principal Investigator |
永山 操 東京女子大学, 文理学部, 講師 (30237557)
|
|---|
| Keywords | Linear Logic / proof nets / strongly planarity / Correctness theorem / stack condition / non-commutative logic |
|---|
| Research Abstract |
昨年度までの、非可換なLinear Logicの証明図にあたるnon-commutative proof netsについての研究をさらに進めた。non-commutativeなsystemにおけるnetsの概念であるmarked netsのwell-formed structureに対する必要十分条件を考える。今年度は、昨年得ていた定理である、marked net Gがwell-formedとなる必要十分条件は、Gがstrongly planarであり、region conditionを満たし、かつL-only subgraphとR-only subgraphがacyclicかconnectedのどちらか一方である、をさらに分析し、平面的グラフの概念を用いないstack conditionによって同値の条件が表現できることが分かった。新しい定理は、marked net Gがwell-formedとなる必要十分条件は、Gがstack conditionを満し、R-only subgraphがacyclicかconnectcdのどちらか一方である、というものである。このstack conditionは、基本的なアルゴリズムを用いて記述でき、その計算量は線形時間であることがすぐにわがる。従って、marked netがnon-commutative proof netかどうかの判定は線形時間である、という新しい結果が得られた。これは、今までnetが(commutative)proof netかどうかを判定するのにquadratic timeががることが知られていたので、non-commutativityが判定アルゴリズムを単純化することに相当する。
一方最近になって、Stefano Guerriniは、ある種のproof structureが(commutative)Proof netかどうかを判定する方法として、線形時間のものがあることを発表した(証明はまだ公開されていない)。この結果とわれわれの結果にどのような関係があるのか、今後の研究課題としてとても興味深い。
|
-
[Publications] Misao NAGAYAMA Mitsuhiro OKADA: "A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic" Theoretical Computer Science. Special issue(to appear). (1999)
-
[Publications] 田中一之(編,監訳): "数学の基礎をめぐる論争" シュプリンガーフェアラーク東京, 213 (1999)
