Core Concepts
本論文では、正則表現に最小不動点を加えた表記法を用いて、(ω-)文脈自由言語の証明理論を研究する。非良順序証明の健全性と完全性を示し、その結果を用いて、(ω-)文脈自由言語の等式理論の完全な無限アキオマ集合を得る。
Abstract
本論文は以下の内容から成る:
正則表現に最小不動点を加えた表記法を用いて、(ω-)文脈自由言語の証明理論を研究する。
非良順序証明系 µHKA∞の健全性と完全性を示す。これにより、(ω-)文脈自由言語の等式理論の完全な無限アキオマ集合 µCA を得る。
最大不動点を加えた拡張系 µνℓHKA∞の健全性と完全性を示す。これにより、ω-文脈自由言語を特徴付ける。
健全性の証明では、非良順序証明の特性を活用する。完全性の証明では、良順序証明への変換を行う。最大不動点の扱いには、ゲーム理論的手法を用いる。
Stats
文脈自由言語の包含問題はΠ0
1-完全である。
正則表現の等式理論は Kozen と Krob により完全に公理化された。
Grathwohl, Henglein, Kozen は最小不動点付き表現の等式理論の完全な無限アキオマ集合を与えた。
Quotes
"The characterisation of context-free languages (CFLs) as the least solutions of algebraic inequalities, sometimes known as the ALGOL-like theorem, is a folklore result attributed to several luminaries of formal language theory including Ginsburg and Rice [GR62], Schutzenberger [Sch63], and Gruska [Gru71]."
"Inclusion of CFLs is Π0
1-complete, so any recursive (hence also cyclic) axiomatisation must necessarily be incomplete."