ドメイン付きクリーネ代数と制限圏

Aがテスト付き半環で、test(A)がそのテスト元の集合だとする。δ:A→test(A) がプレドメイン作用素だとは、

• ∀a∈A.∀p∈test(A).( δ(a) ≦ p ⇔ a ≦ pa )

のこと。次でも同値。

• ∀a∈A.∀p∈test(A).(1. a ≦ δ(a)a, 2. δ(pa) ≦ p)

プレドメイン作用素は次を満たす。

1. (i) δ is fully strict. δ(a) ≤ 0 ⇔ a ≤ 0.
2. (ii) δ is additive. δ(a + b) = δ(a) + δ(b).
3. (iii) δ is monotonic. a ≤ b ⇒ δ(a) ≤ δ(b).
4. (iv) δ is an identity on tests. δ(p) = p.
5. (v) δ is idempotent. δ(δ(a)) = δ(a).
6. (vi) δ yields a left invariant. a = δ(a)a.
7. (vii) δ satisfies an import/export law. δ(pa) = pδ(a).
8. (viii) δ satisfies a decomposition law. δ(ab) ≤ δ(aδ(b)).
9. (ix) δ commutes with the complement operation on tests. δ(p)' = δ(p').

次を満たすプレドメイン作用素がドメイン作用素。

• δ(aδ(b)) ≤ δ(ab)

一方で、制限圏の公理は次：

• (R1) δ(f);f = f for all f : A → B;
• (R2) δ(f);δ(g)= δ(g);δ(f) for all f : A → B and g : A → C;
• (R3) δ(δ(f);g) = δ(f);δ(g) for all f : A → B and g : A → C;
• (R4) f;δ(g) = δ(f;g);f for all f : A → B and g : B → C.