包摂格子

包含格子は、自動定理証明やその他の記号計算アプリケーションの理論的背景で使用される数学的構造です。

置換σが存在し、σ をt _{1に適用すると}t ₂になる場合、項t _1は項 t ₂を包含すると言われます。この場合、t _1はt ₂よりも一般的とも呼ばれ、t _{2 は}t ₁またはt ₁のインスタンスよりも具体的とも呼ばれます。

与えられた署名上のすべての（一次）項の集合は、次のように 部分順序関係「... は ... よりも具体的である」上の格子にすることができます。

• 変数名のみが異なる2つの項は等しいとみなす。^[1]
• 他のどの項よりも具体的であると考えられる人工的な極小要素 Ω (過剰指定された項) を追加します。

この格子は包摂格子と呼ばれます。2 つの項の交わりが Ω と異なる場合、それらの項は統一可能であると言われます。

この格子における結合と会合の操作は、それぞれ反統一と統一と呼ばれます。変数xと人工要素 Ω は、それぞれ格子の最上位要素と最下位要素です。各基底項、つまり変数のない各項は、格子の原子です。格子には、x、g ( x )、g ( g ( x ))、g ( g ( g ( x )))、... などの無限の下降チェーンがありますが、無限の上昇チェーンはありません。

fが2項関数記号、gが1項関数記号、xとy が変数を表す場合、項f ( x , y )、f ( g ( x )、y )、f ( g ( x )、g ( y ))、f ( x、x )、f ( g ( x )、g ( x )) は、最小の非モジュラー格子 N ₅を形成します(図 1 を参照)。この格子の出現により、包摂格子はモジュラーになることができず、したがって分配的になることもできません。

与えられた項と統一化可能な項の集合はmeet に関して閉じている必要はありません。図 2 は反例を示しています。

項tのすべての基底インスタンスの集合をGnd( t )と表記すると、次の性質が成り立つ: ^[2]

• tはGnd( t )のすべてのメンバーの結合に等しく、名前の変更を法とする。
• t _{1 が}t ₂のインスタンスとなるのは、Gnd( t ₁ ) ⊆ Gnd( t ₂ ) の場合のみである。
• 同じ基底インスタンスの集合を持つ項は、名前の変更を除いて等しい。
• t がt ₁とt ₂の交点である場合、Gnd( t ) = Gnd( t ₁ ) ∩ Gnd( t ₂ )、
• t がt ₁とt ₂の結合である場合、Gnd( t ) ⊇ Gnd( t ₁ ) ∪ Gnd( t ₂ ) です。

線形項、つまり変数が複数回出現しない項の集合は、包摂格子の部分ポセットであり、それ自体が格子です。この格子も、N ₅と最小の非分配格子 M _{3 を}部分格子として含み (図 3 と図 4 を参照)、したがってモジュラーではなく、分配的ではありません。

meet演算は、すべての項の格子でも線形項の格子でも常に同じ結果を生成します。すべての項の格子でのjoin演算は、常に線形項の格子での join のインスタンスを生成します。たとえば、(基底)項f ( a , a ) とf ( b , b ) は、すべての項の格子と線形項の格子でそれぞれ結合f ( x , x ) とf ( x , y )を持ちます。join 演算は一般に一致しないため、線形項の格子は厳密に言えばすべての項の格子のサブ格子ではありません。

^{2つの適切な[3]}線型項の結合と会合、すなわちそれらの反統一と統一は、それぞれそれらの経路集合の交差と和に対応する。したがって、Ωを含まない線型項の格子のすべての部分格子は集合格子と同型であり、したがって分配的である（図5を参照）。

どうやら、包摂格子は1970年にゴードン・D・プロトキンによって初めて研究されたようです。 ^[4]