bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

ドメイン付きクリーネ代数を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を知った頃に読んだのがこれで、そうかー檜山さん的にはイマイチなのかー、と思った記憶。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。