|
昨年度までの、非可換なLinear Logicの証明図にあたるnon-commutative proof netsについての研究をさらに進めた。まず、今まであまり研究されていなかったnon-commutativeなsystemにおけるnetsの概念として、strongly planar marked nets導入し、そのwell-formed structureに対する必要充分条件について考察した。ここで、tree-likeな平面的グラフと、そのグラフによって仕切られるregionsとの条件を考えることにより、平面的グラフに対するオイラーの公式が適用できる。これにより、regionsがあるcondition(region condition)を満たす時、well-formed structureかどうかを調べるのに、旧来のswitching conditionにおいて行われたいた。サブグラフのacyclicityとconnectnessの検証がどちらか一方でよいことがわかった。さらにこのregion conditionのもとでは、switching conditionで考慮されるサブグラフの数も劇的に減らすことができた。旧来のswitching conditionでは、mをpar-linkの個数とすると、2のm乗個のサブグラフの検証が必要となる。しかし新しい必要充分条件では、L-only subgraphとR-only subgraphと呼ばれる2つのサブグラフの検証で充分である。これにより、定理として、marked netがwell-formedとなる必要十分条件は、Gがstrongly planarであり、region conditionを満たし、かつL-only subgraphとR-only subgraphがacyclicかconnectedのどちらか一方であることがわかった。さらに、これからCyclic Linear Logicのmultiplicative fragmentにおけるnon-commutative proof netの新しい特徴づけ定理も得られる。
このように、本年度は研究において大きな前進がみられた。来年度はさらにこれを進め、Non-commutative Linear LogicやLambek Calculusにおける定理の自動証明に適用できるような、具体的なアルゴリズムの研究を行っていきたい。
|
