| 研究課題/領域番号 |
09740162
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
数学一般(含確率論・統計数学)
|
|---|
| 研究機関 | 東京女子大学 |
|---|
研究代表者 |
永山 操 東京女子大学, 文理学部, 講師 (30237557)
|
|---|
| 研究期間 (年度) |
1998 – 1999
|
| 研究課題ステータス |
完了 (1998年度)
|
| 配分額 *注記 |
2,000千円 (直接経費: 2,000千円)
1998年度: 1,100千円 (直接経費: 1,100千円)
1997年度: 900千円 (直接経費: 900千円)
|
|---|
| キーワード | Linear Logic / proof nets / strongly planarity / Correctness theorem / stack condition / non-commutative logic / Lambek Calculus |
|---|
| 研究概要 |
昨年度までの、非可換な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かどうかを判定する方法として、線形時間のものがあることを発表した(証明はまだ公開されていない)。この結果とわれわれの結果にどのような関係があるのか、今後の研究課題としてとても興味深い。
|
