ガード条件の連接と論理AND

「テスト付きクリーネ代数の圏論的な定式化」の簡単な例題の話。

罫線付きノートをスキャンするとこうなるなヤッパリ。無地ノートが意外と売ってない。

p, qがブール値のクエリー射 p, q:A→B×A （ブール代数を左側にした）として、ブーリアンANDを演算とするモノイドの作用μ（絵では小さい黒三角）を使って、p~ := p;μ、q~ := q;μ のように定義する。p~, q~ は、ガードあるいはテストを意味する。p・f := p~;f とすれば、クエリーが通常の射に（スカラー積として）作用しているように思える。

それで、示したいのは、p~;q~ = (p∧q)~ という等式；上の絵の上段で、双代数法則と作用の結合法則で変形している。残りは下段の変形だが、これは普通にブール代数の計算。絵算でやればより面白いが、単なる等式計算でも簡単。

p~;q~ = (p∧q)~ を示すのに、関連するほとんどすべての法則を使う所が面白い。論理OR ∨ のほうの法則は、そもそもどうやってテスト付きクリーネ代数の法則を再現するかも難しい（だいたいは分かるが）。分配性って、up-to-iso で成立してはいなくて、lax（またはoplax）でしか意味ないのかも知れない -- よくワカランけど。