| Project/Area Number |
09740162
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Tokyo Woman's Christian University |
|---|
Principal Investigator |
永山 操 東京女子大学, 文理学部, 講師 (30237557)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Project Status |
Completed (Fiscal Year 1998)
|
| Budget Amount *help |
¥2,000,000 (Direct Cost: ¥2,000,000)
Fiscal Year 1998: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1997: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | Linear Logic / proof nets / strongly planarity / Correctness theorem / stack condition / non-commutative logic / Lambek Calculus |
|---|
| 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かどうかを判定する方法として、線形時間のものがあることを発表した(証明はまだ公開されていない)。この結果とわれわれの結果にどのような関係があるのか、今後の研究課題としてとても興味深い。
|
