このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

ドメイン作用素付きブール／クリーネ加群（BKMD）

プログラム意味論 その他代数

A, Bがブール代数、Mが(A, B)両側半加群（加法的にベキ等；順序付き）、δ:M→A、ρ:M→B があって次を満たすとき、(A, B, M, δ, ρ)をドメイン作用素付きブール／クリーネ加群（BKMD; Boole/Kleene Module with Domain）と呼ぶ。

  1. x≦δ(x)・x
  2. x≦x・ρ(x)
  3. δ(p・x)≦p
  4. ρ(x・q)≦q
  5. δ(x・δ(y))≦δ(x;y)
  6. ρ(ρ(x)・y)≦ρ(x;y)

δ(0) = 0、δ(x + y) = δ(x) + δ(y) は定理として示せる（ρも同様）。
Mが(A, A)-半加群なら、p∈A、x∈Mに対して、x←(p) を δ(x・p)、x→(p) を ρ(p・t) で定義できそうだ。

  • x←(0) = δ(x・0) = δ(0) = 0
  • x←(p + q) = δ(x・(p + q)) = δ(x・p + x・q) = δ(x・p) + δ(x・q) = x←(p) + x←(q)
  • Mが(A, A)-半加群なら、1A∈Mがあるので、A×M→MによりAはMに作用する。これでテスト付きクリーネ代数（KAT）が実現できる。