| 研究課題/領域番号 |
21K13828
|
|---|
| 研究種目 |
若手研究
|
| 配分区分 | 基金 |
|---|
| 審査区分 |
小区分12030:数学基礎関連
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
中村 誠希 東京工業大学, 情報理工学院, 助教 (00866311)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2022年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2025年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2024年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2023年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2022年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2021年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | 関係代数 / 有限モデル理論 / 数理論理学 / 計算困難さ / グラフ / オートマトン / 関係計算 / 計算複雑さ |
|---|
| 研究開始時の研究の概要 |
論理の決定可能性および計算複雑さの解析の問題は、Church-Turingによる一階述語論理の決定不能性の結果にはじまる。
申請者の近年の研究では、Tarski-Givantによる３変数一階述語論理と関係計算の表現力の等価性の結果を一般化し、３変数ポジティブ存在論理とポジティブ関係計算の表現力の等価性を明らかにした。
本研究では、ポジティブ性をもつ（否定演算を持たない）論理・関係代数の高い決定可能性を起点として、論理と関係代数の双方向的な視点から、新たな決定可能な体系の解明やより精密な計算複雑さの解析を与えることを目的とする。
|
| 研究実績の概要 |
本課題では、ポジティブ性をもつ（否定演算を持たない）論理・関係代数の高い決定可能性を起点として、論理と関係代数の双方向的な視点から、新たな決定可能な体系の解明やより精密な計算困難さの解析を与えることを目的として、研究を進めている。2022年度においては以下をおこなった。
（１）推移閉包演算を持つ"存在関係計算"の決定可能性／計算困難さに関する研究：３変数存在論理と等価な表現力を持つ関係計算である"存在関係計算"を導入した。この体系は制限された否定演算で拡張されており、ポジティブ関係計算と比べて真に表現力が高い。推移閉包演算で拡張した存在関係計算の体系に対して、辺飽和（edge saturations）を用いたグラフの集合による特徴付けを与え、これを用いて決定可能性／計算困難さを調べた。より具体的には、この体系の等式理論はフルの場合では決定不可能だが、関係積の演算を持たない体系ではcoNEXPで決定可能となることを示し、さらにその２つの部分体系に関してはオートマトンの構築方法を与えることによってPSPACEで決定可能（PSPACE完全）であることを示した。また、推移閉包演算を持たない体系では、coNP完全であることを示した。本結果は、国際会議LICS2023に採択された（to appear）。
（２）変数出現を制限した関係計算の決定可能性に関する研究：kをある自然数として、等式の左右の項それぞれに変数が出現する回数を高々k回に制限した場合の等式理論の決定可能性を考えた。具体例として、関係計算のdot-dagger交替階層の各階層における決定可能性を考察し、国内研究集会MLG2022で口頭発表をおこなった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究計画に挙げていた項目に対して、研究実績に挙げた通りの一定の進展を得たため。
一方で、採択に至っていない内容や研究計画に残されている課題もあるため、これらについて引き続き取り組む必要がある。
|
| 今後の研究の推進方策 |
引き続き研究計画をもとに進める。進行中の課題の遂行を主とするが、上記の研究結果と関連して新たに公理化に関する問題が現れたため、関係代数、数理論理学、形式言語理論などの既存結果を踏まえつつ並行して考察を行いたい。
|
