数学基礎論のプログラミング言語理論への応用

昨年度までの、非可換な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かどうかを判定する方法として、線形時間のものがあることを発表した(証明はまだ公開されていない)。この結果とわれわれの結果にどのような関係があるのか、今後の研究課題としてとても興味深い。

昨年度までの、非可換な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かどうかを判定する方法として、線形時間のものがあることを発表した(証明はまだ公開されていない)。この結果とわれわれの結果にどのような関係があるのか、今後の研究課題としてとても興味深い。