ポジティブ関係計算とポジティブ存在論理の相互的研究

点击翻译按钮获取中文摘要

本課題では、ポジティブ性をもつ（否定演算を持たない）論理・関係代数の高い決定可能性を起点として、論理と関係代数の双方向的な視点から、新たな決定可能な体系の解明やより精密な計算困難さの解析を与えることを目的として、研究を進めている。2022年度においては以下をおこなった。（１）推移閉包演算を持つ"存在関係計算"の決定可能性／計算困難さに関する研究：３変数存在論理と等価な表現力を持つ関係計算である"存在関係計算"を導入した。この体系は制限された否定演算で拡張されており、ポジティブ関係計算と比べて真に表現力が高い。推移閉包演算で拡張した存在関係計算の体系に対して、辺飽和（edge saturations）を用いたグラフの集合による特徴付けを与え、これを用いて決定可能性／計算困難さを調べた。より具体的には、この体系の等式理論はフルの場合では決定不可能だが、関係積の演算を持たない体系ではcoNEXPで決定可能となることを示し、さらにその２つの部分体系に関してはオートマトンの構築方法を与えることによってPSPACEで決定可能（PSPACE完全）であることを示した。また、推移閉包演算を持たない体系では、coNP完全であることを示した。本結果は、国際会議LICS2023に採択された（to appear）。（２）変数出現を制限した関係計算の決定可能性に関する研究：kをある自然数として、等式の左右の項それぞれに変数が出現する回数を高々k回に制限した場合の等式理論の決定可能性を考えた。具体例として、関係計算のdot-dagger交替階層の各階層における決定可能性を考察し、国内研究集会MLG2022で口頭発表をおこなった。