Polymorphic Combinatory Categorial Grammar for Incremental Parsing

今年度の研究では、前年度の成果を基に、形式化と検証を重視し、計算機科学的・証明論的性質の調査を行った。具体的には、以下の3つの対象について研究を進めた。まず、QコンビネータおよびDコンビネータを用いた組合せ範疇文法における左分岐木を木構造の書き換え系として分析し、漸進的構文解析と漸進的構文解析の関係性を明らかにした。次に、型の繰り上げ規則を加えた範疇文法の構文解析アルゴリズムが決定可能であることを証明論的手法によって示した。これは、範疇文法に基づく構文解析において、効率的かつ正確な解析が可能であることを示すものである。最後に、継続渡し形式変換規則のランベック計算における証明不能性について研究した。これはランベック計算のカット除去定理に基づく成果であり、与えられた規則の導出可能性が有限時間の証明探索で検証可能であることを示した。さらに、従来の継続渡し形式変換規則に制約を加えることで導出可能な規則を構成できることを証明論によって示した。これらの研究成果については、LENLS、TPS、KSE、ESSLLIなどの国内外の学会や研究会で発表した。また、研究成果を定理証明支援系で形式化し、フレームワーク上に構文解析器を実装したことで、組合せ範疇文法において左再帰構文木の存在が理論的に証明され、その動作が定理証明支援系によって検証された。研究成果は、言語学と情報科学の学際領域における新たな知見を提供するものであり、今後もさらなる研究につながる成果であると考えている。

今年度の研究では、前年度の成果を基に、形式化と検証を重視し、計算機科学的・証明論的性質の調査を行った。具体的には、以下の3つの対象について研究を進めた。まず、QコンビネータおよびDコンビネータを用いた組合せ範疇文法における左分岐木を木構造の書き換え系として分析し、漸進的構文解析と漸進的構文解析の関係性を明らかにした。次に、型の繰り上げ規則を加えた範疇文法の構文解析アルゴリズムが決定可能であることを証明論的手法によって示した。これは、範疇文法に基づく構文解析において、効率的かつ正確な解析が可能であることを示すものである。最後に、継続渡し形式変換規則のランベック計算における証明不能性について研究した。これはランベック計算のカット除去定理に基づく成果であり、与えられた規則の導出可能性が有限時間の証明探索で検証可能であることを示した。さらに、従来の継続渡し形式変換規則に制約を加えることで導出可能な規則を構成できることを証明論によって示した。これらの研究成果については、LENLS、TPS、KSE、ESSLLIなどの国内外の学会や研究会で発表した。また、研究成果を定理証明支援系で形式化し、フレームワーク上に構文解析器を実装したことで、組合せ範疇文法において左再帰構文木の存在が理論的に証明され、その動作が定理証明支援系によって検証された。研究成果は、言語学と情報科学の学際領域における新たな知見を提供するものであり、今後もさらなる研究につながる成果であると考えている。