Σコゥゼン σ-順序代数
デクスター・コゥゼンの "A Complete Gentzen-style Axiomatization for Set Constraints" とか読んで思ったこと。
「Σコゥゼン σ-順序代数」という概念を考えた。Σ-kozen σ-ordered algebra, あるいは、Σ-kozen ordered σ-algebra かな。コゥゼンの termset algebra の一般化なんだけど、単に一般化しました、ってわけじゃなくて必要性があった。まずは、σ-順序代数から説明する。
等式的論理に、定数記号 0, 1 と 演算記号∩、∪、関係記号⊆（記号は何でもいい、'≦'とかでもいい）を入れて、束と順序の公理を付け加えた等式的理論（equational theory）を考える。0, 1 は最小元と最大元。∪は無限個の項を取ってもいいとする。この理論（公理系）のモデルは束；もちろん、等号'='は実際の「等しい」として解釈する。σは、演算記号の集合だとする。σは空であってもかまわない。σは指標、コゥゼンは ranked alphabet と呼んでいる。
演算子記号（関数記号と本質的に同じ）としてσを加えて、σの演算に関する法則を等式、または不等式（'⊆'を使った論理式）で与えた理論を考える。このようにして定義される理論のモデルを総称してσ-順序代数と呼ぶ。⊆（場合によっては=さえも）他の演算や関係の組み合わせで定義されてもかまわない。演算が先か順序が先かは問わない。
σ-順序代数の例には、束、ブール束、分配則、加法的ベキ等な可換半環、クリーネ代数などがある。これらの例は、演算が先にあれば順序を事後的に定義できる。その他、順序が事前または事後的に定義できるならなんでもいい。σには、補集合、集合差、クリーネスターなどが入る。
Σは、σとは別に与えられた指標（ranked alphabet）。こっちは、コンストラクタ記号の集まりだと考える。σ-順序代数の理論に対して、Σの記号も入れて項の定義を拡張する。さらに、次の公理を付け加える。x, yなどは任意の項だが、理論（の言語）内に変数があり、自由変数の置換ができるなら、x, yなどは変数だとしてもよい。f, gなどはΣに含まれる関数記号。
- [ジョイン演算の保存]f(..., x∪y, ...) = f(..., x, ...)∪f(..., y, ...)
- [全射性（生成性）] ∪f(1, ...,1) = 1、ただしすべてのf∈Σに関して合併をとる。fには定数記号も含まれる。
- [分離性（排他性）] f≠g ならば、f(1, ..., 1)∩g(1, ..., 1) = 0。f, gには定数記号も含まれる。
- [非退化性] 有限個のxiに関して ∧(xi ≠ 0) ならば、f(x, ..., x) ≠ 0
σ-順序代数を、Σにより拡張して、上記の公理系を付け加えた理論を、もとの理論のΣコゥゼン拡張と呼ぶ。Σコゥゼン拡張のモデルをΣコゥゼン σ-順序代数と呼ぶことにする。σに含まれる演算に関する法則を追加することがある。コゥゼンのもとの例では、任意のfが集合差を保存することを公理に入れている。
Catyの文脈では、JSONインスタンス領域上の型（部分集合）の代数がΣコゥゼン順序代数になる（σが空のときは、「σ-」を省略する）。Σは以下の集合の合併である。
