Alapfogalmak
正規表現の言語間の最短識別語距離を完全に公理化した。
Kivonat
この論文では、正規表現の言語間の最短識別語距離を完全に公理化した。
まず、決定性有限オートマトンの概念と正規表現の意味論を復習した。正規表現の言語間の距離は、最短識別語距離と呼ばれる概念で定義できる。この距離は、状態間の距離を状態の観測可能な振る舞いの距離に持ち上げることで定義される。
次に、この距離を公理的に扱うための量的等式論理の枠組みを紹介した。この枠組みでは、項e が項fから距離εの範囲内にあることを表す e ≡ε f という判断が扱える。
著者らは、正規表現の最短識別語距離を公理化した量的等式論理REGを提示した。REGは、非決定的選択、順序合成、ループなどの正規表現の演算子の性質を捉えた公理から成る。特に注目すべきは、固定点導入規則を必要としないことである。これは、量的等式論理の無限規則と λ-前置公理により、サロマーの固定点規則が導出可能であることを示したことによる。
最後に、REGが正規表現の最短識別語距離に関して完全であることを示した。この証明の核心は、正規表現の言語間距離が有限状態オートマトンの状態間距離として簡単に計算できることを示すことにある。
Statisztikák
正規表現e, fについて、dL(JeK, JfK) ≤ ε ⇔ ⊢ e ≡ε f
Idézetek
"正規表現の言語間の最短識別語距離を完全に公理化した。"
"量的等式論理の無限規則と λ-前置公理により、サロマーの固定点規則が導出可能である。"
"正規表現の言語間距離が有限状態オートマトンの状態間距離として簡単に計算できる。"