仮説を有するクレーネ代数の完全性に関するツールについて

クレーネ代数に関する文献では、テストを用いたクレーネ代数（KAT）や最近の観察を用いたクレーネ代数（KAO）など、理論によって指定された追加の構造を課すいくつかの変種が提案されています。また、NetKATのように特定の定数についての仮定を行うものもあります。これらの変種の多くは、与えられた仮説の集合から構成された標準的な言語モデルを伴う、仮説を有するクレーネ代数によって提供される統一的な観点に適合します。KATの場合、このモデルは表現を保護された文字列の言語として解釈する一般的な解釈に対応します。したがって、関連する質問は、与えられた仮説の集合とともにクレーネ代数がその標準的な言語モデルに関して完全であるかどうかです。本論文では、この質問に関する既存の結果を再考し、組み合わせ、拡張して完全性をモジュール方式で証明するためのツールを得ます。これらのツールを用いて、KAT、KAO、NetKATの完全性に関する新しいモジュール的な証明を示し、完全性が証明されたいくつかの新しいKATの変種についても紹介します。これには完全関係のための定数を付加したKAT、逆演算を付加したKAT、テストの集合が分配格子のみを形成するKATのバージョンが含まれます。