Core Concepts
Kleene代数の拡張に対する完全性を証明するための一般的な手法を提供する。様々な具体例を通して、この手法の有効性を示す。
Abstract
本論文では、Kleene代数の拡張に対する完全性を証明するための一般的な手法を提供する。
まず、Kleene代数の基本的な概念と、仮定を含むKleene代数の閉包言語モデルについて説明する。次に、ある仮定集合Hから別の仮定集合H'への「還元」という概念を導入し、これを用いて完全性を証明する手法を示す。
具体的には以下の手順を踏む:
還元の定義と、還元が存在すれば完全性が得られることを示す(定理2.11)。
還元を構築するための基本的なツールを提供する。特に、準同型写像を用いた還元の簡単な条件(命題3.2)や、有限オートマトンを使った還元の構築方法(命題3.7)を示す。
様々な仮定集合に対する基本的な還元を示す(補題3.8)。
還元を組み合わせるための高度な手法を提供する(第5節)。
KAT、KAO、NetKATなどの具体例に対して、この手法を適用して完全性を証明する(各節)。
この手法は、Kleene代数の拡張に対する完全性を一般的かつ体系的に証明するための強力なツールを提供する。