ドメイン付きクリーネ代数をAlloyで

久々すぎて、はてなの書き方を忘れてしまいました。

さて（脈絡なし）：

• テスト付きクリーネ代数とその使い方 - 檜山正幸のキマイラ飼育記
• テスト付きクリーネ代数の圏論的な定式化 - 檜山正幸のキマイラ飼育記

上記の記事を今更読んだのですが*1、そういや私め、昔テスト付きクリーネ代数…の拡張のドメイン付きクリーネ代数（Kleene Algebra with Domain, KAD）をAlloyで書いてみたことがありまして。
cf. [cs/0310054] Kleene algebra with domain -- arXiv
GitHubに置いてあるので、とりあえずリンク貼っときます。
このモデルでは、クリーネ代数はシグネチャProp上の2項関係 Prop->Prop で表現していて、ブール値はPropの集合で、乗法はドット結合、論理積は集合積で書いてました。たとえば、

(p∧q)・f = p・(q・f)

は

    (p & q).toKA.f = p.toKA.(q.toKA).f

と書けて（toKAはブールをクリーネ代数に持っていくおまじない）、こんな↓アサーションを書いてやっても反例は出ないようにはなっております。

def_and: check {
  all p, q: set Prop, f: Prop->Prop {
    (p & q).toKA.f = p.toKA.(q.toKA).f
  }
} for 10

以上、ほとんどメモ的な内容で具体的な説明なしで大変不親切なのですが。
最近またKADが自分内でリバイバルし始めてて、本当はがっつり解説書こうかと思ったんですが何かダレた。一部直観的でないところがあったり、今見るとイマイチだなーと思うところもあったりですが、とりあえず。
気分が乗ったら追加でまた書くかも。

*1:ちょうど自分がKATを知った頃に読んだのがこれで、そうかー檜山さん的にはイマイチなのかー、と思った記憶。