半環イロイロ
Esik/Kuichの"Inductive *-Semirings"から定義などを抜き書き。
単項の演算*を持つ半環をスター半環と呼ぶ（それだけの話、他に特別な意味はない）。
帰納的スター半環（inductive *-semiring）は：
- 順序半環（半環演算が単調）
- a・a* + 1 ≦ a* [不動点不等式;the fixed point enequation]
- a・x + b ≦ x ⇒ a*・b≦x [不動点帰納法; the fixed point induction rule]
不動点等式 a・a* + 1 = a* は定理として出る。スターが単調なことも定理。不動点と帰納原理の半環による定式化。
連続半環（contiuous semiring）とは：
- 順序半環
- 0を最小元とするCPO（任意の族がsupを持つ）
- 和と積はCPO構造に関して連続
Σaiは、sup(aiの有限和)で定義できる。
連続スター半環（continuous *-semiring）とは：
- 連続半環である。
- スターはクリーネ級数の総和で与えられる。
連続スター半環は帰納的スター半環になる。クオンテールは連続スター半環になるので、帰納的スター半環である。
スターを持つ順序半環において、次を弱不動点帰納法（weak fixed point induction rule）と呼ぶ。
- a・x + b = x ⇒ a*・b ≦ x （a*はどんな真の不動点よりも小さい）
不動点帰納法は、「a・x + b ≦ x ⇒ a*・b≦x 」と少し強い。
コンウェイ半環（Conway semiring）とは：
- 和スター等式 (a + b)* = (a*・b)*・a*
- 積スター等式 (ab)* = 1 + a・(ba)*・b
弱帰納的スター半環（weak inductive *-semiring）とは：
順序半環が和順序（sum-ordered）とは：
- a≦b ⇔ ∃c. a + c = b
和順序半環が弱帰納的スター半環であるときに、いくつかの定理がある。
スター半環Sに関する次の条件は同値：
- Sはコンウェイ半環
- Sの2×2行列が不動点方程式（等式）を満たす
- 任意のnにおいて、Sのn×n行列（n≧1）が不動点方程式（等式）を満たす
- あるnにおいて、Sのn×n行列が不動点方程式（等式）を満たす
- Sの下三角2×2行列が不動点方程式（等式）を満たす
- Sの上三角2×2行列が不動点方程式（等式）を満たす
これはコンウェイ圏（コンウェイ／ベキック圏；圏的不動点オペレータを持つデカルト圏）における定理にできそうだ。
コンウェイ半環が反復半環（iteration semiring）とは：
- どんな有限群Gに対しても、Gの群等式を満たすこと。
群等式の定義は省略。
次の双対性がある。
帰納的スター半環が対称帰納的スター半環（symmetric - ）であるとは：
連続スター半環は対称帰納的スター半環である。Sが対称なら行列半環も対称になる。
コゥゼン半環（Kozen semiring）とは：
- 加法的ベキ等
- 対称帰納的スター半環
コゥゼン半環はクリーネ代数のことである。クリーネ／コゥゼン半環あたりが妥当な呼び方か？
Sがスター半環、A⊆Sとして、A上のコンウェイ機構（mechanism）とは：
- n≧0
- α∈{0, 1}1×n
- β∈{0, 1}n×1
- M∈(A∪{0, 1})n×n
- (α, M, β)がコンウェイ機構
Dがコンウェイ機構のとき、Dの振る舞い（behaviour）とは：
- 行列の積 αM*β ∈S
Sに関して次が成立するとき、Sはクリーネ型定理（Kleene-style, Kleene-type）を満たすと呼ぶことにする（これは檜山）。
- Aから生成されたSの部分スター半環と、あらゆるコンウェイ機構に関する振る舞いの全体が一致する。
コンウェイ半環はクリーネ型定理を満たす。
