Alloyを勉強する日記(0)

Java-ja温泉にてid:warufuzaketaichiに教えてもらったAlloyについて、勉強過程のログを記録しておく。

教科書は買ったけどまだ届いていない。

Alloyでググっていたら圏の勉強の時にだいぶ参考にさせていただいた檜山さんのブログで言及されているのを発見したので、ざっと眺める。「関係圏Relでは、指数演算の実体が直積になっている」とか眼から鱗な感じ。ref. Alloyの矢印記法と、モノイド閉圏としての関係圏 - 檜山正幸のキマイラ飼育記

まあ、どう眼から鱗だったのか噛み砕いて説明できないのでわかった気になっているだけかもしれませんが ;p

Alloy: A Lightweight Object Modelling Notation - 言語ゲームの説明はとてもわかりやすかった。若干もやっとするので、きっと僕の脳内のモデルとこの文章を書いた人のモデルにどこか食い違いがあるんだと思うけど、どこが食い違っているか明確に言語化できていない。

オブジェクト指向のプロパティは関数」というあたりが食い違いかな?

追記: 理解した。ここで言う「関数」って言葉の意味は「定義域のオブジェクト一つに対して値域のオブジェクトがただ一つ対応する」っていう制約のことを言ってるんですね。納得。たしかに一般的な言語でfoo.barってやったばあい1つの値が返ってきて、なのでそれに慣れていると暗黙に「値域のオブジェクトは1個」と思い込んでしまいがち。だけど関係一般について考えると、これは0個かもしれないし5個かもしれない。そういうことを言いたかったのだと理解しました。

論文のとりあえず3章を眺める http://sdg.csail.mit.edu/pubs/2002/alloy-journal.pdf

Alloyの文脈では、まず基本ブロックとして使われる「関係」が二項関係なので「より多項の関係を扱いたくなった時にどうするの?」「それ関数でできるよ!カリー化!カリー化!」って言わんがために「関数」があるという印象。

スコーレム化:「全ての x について、ある y が存在し、R(x,y) が成り立つ」とは「ある関数 f が全ての x を y にマッピングし、全ての x について R(x,f(x)) が成り立つ」ref. スコーレム標準形 - Wikipedia

シングルトンであるという制約をsome x: T | x = vで表現しているのが理解出来ない。このコードを「あるSet Tの要素xについてx = v」と理解しているのだけど、それだとシングルトンだという制約には不足じゃないだろうか。all x: T | x = v なら「Tの任意の要素xについてx = v、つまりTの要素はv1個だけ」になりそうだ。

著者らいわく目新しいところはthe treatment of scalars as singleton sets, the encoding of sets as degenerate relations, and the dot operator used to form ‘navigation expressions'とのことで。1つ目のはまあ「要素(スカラー)と集合の演算」と「集合と集合の演算」の両方を考えるのはめんどいから要素はそれ1個が含まれている集合だとみなしましょう、ってこと。ちょうど最近のスクリプト言語が文字と文字列を区別するのがめんどくさくて、文字を長さ1の文字列とみなしているようなもの。

2つ目のは「集合に入っているものがスカラーなのか関係なのか」とか考えるのは面倒だから関係じゃないものXが入ってた場合(Unit, X)っていう関係が入っているものとみなそう、って話。

3つ目の‘navigation expressions'ってのが何を指しているのかはいまいちよくわかってない。double dutyって言葉で表現されているけどもs.tのドットは単に関係の合成をする演算子だけども、sが集合でtが関係の時にはpythonで表現すると[x.t for x in s]みたいな感じになる。s.~tではなく~s.tが直積じゃないか、という点に関してはid:propellaさんに同意。

AlloyはSat4jを使っているんだっけ?適当にいじって遊べるようなSATソルバってないかなぁ。あ、 http://alloy.mit.edu/alloy4/quickguide/gui.html をみると色々切り替えられるようだな。じゃあこの中からいじりやすい物を探すか。

んん、sat4jとかのレイヤーの上にKodkodってのが乗ってるのか http://alloy.mit.edu/kodkod/download.html Alloyで制約問題を解いているのは実際にはこいつなのかな。Kodkodを使っているアプリの一覧が興味深い http://alloy.mit.edu/kodkod/apps.html