アクション代数

代数論理学において、作用代数は、剰余半束とクリーネ代数の両方である代数構造である。これは、後者のスターまたは反射推移閉包演算を前者に追加し、前者の左および右の剰余または含意演算を後者に追加します。プログラムと命題が 2 つの異なる種類を形成する動的論理やその他のプログラムの様相論理とは異なり、作用代数はこの 2 つを 1 つの種類に組み合わせます。これは、スターと、単位元が最上位要素である必要がない非可換連言を持つ直観主義論理の変形と考えることができます。クリーネ代数とは異なり、作用代数は多様体を形成し、さらに有限に公理化可能であり、重要な公理はa •( a → a )* ≤ aです。クリーネ代数の方程式理論のモデル（正規表現方程式）とは異なり、作用代数のスター演算は方程式のあらゆるモデルにおいて反射的推移閉包である。作用代数は、ヨーロッパワークショップ JELIA'90 でVaughan Prattによって導入された。^[1]

作用代数( A , ∨, 0, •, 1, ←, →, *) は、( A , ∨, •, 1, ←, →)がWard と Dilworth の意味で残余半格子を形成するような代数構造である^[2]。一方、( A , ∨, 0, •, 1, *) はDexter Kozenの意味でクリーネ代数を形成する。^[3] つまり、両方のクラスの代数の結合理論の任意のモデルである。 さて、クリーネ代数は準方程式、つまり 2 つ以上の方程式間の含意によって公理化されるため、このように直接公理化された場合、作用代数も同様に公理化される。 しかし、作用代数には、純粋に方程式である同等の公理化もあるという利点がある。作用代数の言語は、meet演算を組み込むことによって、自然に作用格子の言語に拡張される。^[4]

以下では、不等式a ≤ b を等式a ∨ b = bの省略形として書きます。これにより、不等式を使用して理論を公理化できるだけでなく、不等式を等式に展開したときに純粋に等式による公理化が可能になります。

作用代数を公理化する方程式は、残余半格子に対する方程式であり、星に対する次の方程式もこれに含まれます。

1 ∨ a *• a * ∨ a   ≤   a *

a * ≤ ( a ∨ b )*

( a → a )*   ≤a → a

最初の等式は、1 ≤ a *、a *• a * ≤ a *、a ≤ a * の 3 つの等式に分解できます。2項関係からの抽象化により、 1 ≤ aの場合にaが反射的、 a • a ≤ aの場合に推移的であると定義すると、最初の 2 つの等式はa * が反射的かつ推移的であることを強制し、3 つ目の等式はa * がa以上であることを強制します。次の公理は、 star が単調であることを主張します。最後の公理は、a •( a → a )* ≤ aと同等に記述でき、この形式により、帰納法としての役割がより明らかになります。これらの 2 つの公理は、残余半格子の公理と組み合わせることで、a * がa以上である要素の半格子の最も反射性の低い推移的要素であることを強制します。これをaの反射的推移閉包の定義とすると、任意の作用代数のすべての要素aに対して、 a * はaの反射的推移閉包であることがわかります。

作用代数の含意のないフラグメントの等式理論、つまり → または ← を含まない等式は、正規表現等式としても知られるクリーネ代数の等式理論と一致することが示され得る。その意味で、上記の公理は正規表現の有限公理化を構成する。レドコは 1967 年に正規表現等式には有限公理化がないことを示し、ジョン・ホートン・コンウェイは1971 年にこれに対してより短い証明を与えた。^{[5] [6]} アルト・サロマはこの理論を公理化する等式スキーマを与え、その後デクスター・コーゼンはこれを準等式、つまり等式間の含意を使った有限公理化として再定式化した。重要な準等式は帰納法の準等式である。すなわち、x • a ≤ xならばx • a * ≤ xであり、a • x ≤ xならばa *• x ≤ xである。コーゼンは、クリーネ代数をこの有限公理化の任意のモデルとして定義しました。

Conway は、正規表現の等式理論では、a * がaの反射推移閉包ではないモデルが許容されることを、 a • a = aとなる0 ≤ 1 ≤ a ≤ a * の4 要素モデルを与えることで示しました。Conway のモデルでは、a は反射的かつ推移的であるため、その反射推移閉包はaになるはずです。しかし、正規表現ではこれを強制せず、a * がaよりも厳密に大きいことを許可しています。このような異常な動作は、 a * が最も推移的でない反射要素であることを 強制するアクション代数では不可能です。

任意のHeyting 代数(したがって任意のブール代数) は、• を ∧ およびa * = 1とすることで作用代数になります。Heyting代数の最上位の要素 1 は、その唯一の反射要素であり、推移的であり、代数のすべての要素より大きいか等しいため、これは star にとって必要かつ十分です。

アルファベット Σ 上のすべての形式言語(有限文字列の集合) の集合 2 ^{Σ*は、0 を空集合、1 = {ε}、∨ を和集合、• を連結、} L ← M をxM ⊆ L (およびM → Lについても双対的に)となるすべての文字列xの集合、L * をL内のすべての文字列の文字列の集合(クリーネ閉包) とする作用代数を形成します。

集合X上のすべての二項関係の集合 2 ^{X ²}は、 0 を空関係、 1 を恒等関係または等式、 ∨ を和集合、 • を関係合成、R ← S を、Xのすべてのzに対してySz はxRz を意味する( S → Rに対しても双対的に) ようなすべてのペア ( x,y ) からなる関係、R* を、整数n ≥ 0 に対してすべての関係R ⁿの和集合として定義されるRの反射推移閉包とする作用代数を形成します。

前の 2 つの例は冪集合であり、これは通常の集合論的演算である和集合、積集合、補集合の下でのブール代数です。これは、これらをブール アクション代数と呼ぶのにふさわしいものです。関係の例は、反射的推移閉包の演算を備えた関係代数を構成します。すべてのブール代数は Heyting 代数であり、したがって最初の例のインスタンスであるためアクション代数であることに注意してください。

• 動的論理（様相論理）
• クリーネスター
• 正規表現