注目すべき等式やら命題やら

もう少しチャントまとまったら書こうと思っていたが、とりあえず叩き台。

●不動点等式／不等式／帰納法

• a・a* + 1 = a* [不動点等式; the fixed point equation]
• a・a* + 1 ≦ a* [不動点不等式; the fixed point enequation]
• a・x + b ≦ x ⇒ a*・b≦x [不動点帰納法; the fixed point induction rule]
• x・a + b ≦ x ⇒ b・a* ≦ x [双対不動点帰納法； dual- ]
• a・x + b = x ⇒ a*・b ≦ x [弱不動点帰納法; weak fixed point induction rule]

弱不動点帰納法では、仮定が不等式から等式へと強くなる。よって、推論原理としては弱くなる。

●クリーネ代数／クリーネ圏

コゥゼン（Kozen）の定義：

1. 1 + a・a* ≦ a*
2. 1 + a*・a ≦ a*
3. b + a・x ≦ x ⇒ a*・b ≦ x
4. b + x・a ≦ x ⇒ b・a* ≦ x

カール（Kahl）の定義：
r:A→A, q:B→A、s:A→Cに対して：

1. r* = 1 + r + r*;r*
2. q;r⊆q ⇒ q;r* ⊆q
3. r;s⊆s ⇒ r*;s ⊆s

木下の定義：
q:A→A, r, x:X→A、s, y:A→Yに対して：

1. 1 + q*;q = q*
2. 1 + q;q* = q*
3. r + x;q ⊆x ⇒ r;q*⊆x
4. s + q;y ⊆y ⇒ q*;s⊆y

ホプキンス（Hopkins）の定義：
u: A→B, v: A→A, w: B→B, x: A→B に対して：

1. 1_A + ff* ≦ f*
2. u + xv + wx ≦ x ⇒ w* u v* ≦ x

●一様性原理／帰納原理

• [HU] f;(B+ψ) = (A+ψ);g ⇒ f↑ = g↑
• [PU] f;ψ = (A+ψ);g ⇒ f^†;ψ = g^†
• [KU] f;ψ = ψ;g ⇒ f^*;ψ = ψ;g^*
• [KI-1] f;ψ ≦ ψ ⇒ f^*;ψ ≦ ψ
• [KI-2] ψ;g ≦ ψ⇒ ψ;g^* ≦ ψ

●スター／ダガー公式群

コンウェイ（Conway）等式 コンウェイ（Conway）半環の定義
和ダガー等式／積ダガー等式

• (a + b)^† = (a^†b)^†a^†
• (ab)^† = 1 + a(ba)^†b

和スター等式／積スター等式

• (a + b)* = (a*・b)*・a*
• (ab)* = 1 + a・(ba)*・b

行列スター公式：
M = [a, b; c, d], M* = [α, β; γ, δ] として：

1. α = (a + bd*c)*
2. β = αbd*
3. γ = δca*
4. δ = (d + ca*b)*

●Conway不動点

コンウェイ（Conway）オペレータ公理：

• [対角自然性] f:A×U→V, g:U→V に対して、(f;g)^† = (A×g;f)^†;g
• [対角性(diagonal prop.)] f:A×U×U→Uとして、((A×Δ);f)^† = (f^†)^†

f:A,X→X, g:A,Y→Y が2つの系だとして、制御パラメータ領域Aは共通。このとき、並列結合 A,X×Y→X×Y が定義できる。この並列結合をと書くことにする。の不動点^†をfの不動点とgの不動点によって書き下す公式がBekicの公式。（Bekicの公式を今は書き下さない。）

●相互関係

トレース付きモノイド圏（対称性は当然に仮定）がデカルトのとき、f:A×X→Xの不動点f^†は次のように定義できる。

• f^† = Tr^X_A,X(f;Δ_X)

さらに双デカルトなら、f:X→X の繰り返し（repetition）f*は：

• f* = Tr^X_X,X(∇_X;f;Δ_X)

これらから、双デカルト・モノイド圏では：

• f* = (∇;f)^†

逆に、スターでダガーを定義できる。f:A×X→Xのとき

• f^† = ((Δ_A+X);(A+f))*

ダガーによるトレースの定義は：

• Tr^X_A,B(f) = (π¹_2A,B;f)^†;π²_2B,X

ここで、π¹₂、π²₂は、それぞれ第一、第二射影（直積因子は２つ）。

※以下、f∨g = Δ;(f + g);∇ とする。

f^* = 1 ∨ f⁺ を絵算で示すときに、どうも次の公式が必須なようだ。

• ∇;Δ = (Δ+Δ);(1+σ+1);(∇+∇)

□≡(Δ+Δ);(1+σ+1);(∇+∇) と置けば、

• ∇;Δ = □

それで：

• f^* = Tr[(1+Δ);(σ + f);(1 + ∇)]
• f^* = Tr[(1+f);□] = Tr[□;(1+f)]
• f^* = 1 ∨ Tr(∇;f;Δ) = 1 ∨ f⁺