Alloy: A Lightweight Object Modelling Notation

http://sdg.csail.mit.edu/pubs/2002/alloy-journal.pdf

Alloy が難しく見えるのはオブジェクト指向っぽい文法とその意味に隔たりがあるからかも知れません。Alloy のアイデアが書かれてあるこの論文を読んで思いました。この論文のおすすめ読み方。

1. 導入を読む
記号が苦手じゃなければ 3.1, 3.2, 3.3 カーネル言語について読む
4. 5. 6. 他の言語との比較を読む
2. Example と残りを読む。

頭から順に読むとかなり意味不明でした。特に 3 章のはじめのカーネル言語の話が面白いので書きます。

Alloy の設計は二段構えになっています。単純で機能の少ないカーネル言語をオブジェクト指向風の文法で包む形になっています。文法は一見 Java のクラス定義っぽくて親しみやすいですが、細かい所で全然違うのでカーネル言語の性質が分からないとドツボにはまります。Alloy の基本的なアイデアは「関係」と言って、項目が二つの表で表現出来ます。SQL の正規形や、アリティ2しか無い prolog と思えば良いです。

一方で、オブジェクト指向のプロパティは「関数」です。関数というのはある引き数が値一つを指し示す仕組みです。関数も二項目の表で表現出来ますが、その場合キーになる側の項目が必ずユニークになります。Alloy の関係にはこのような制限がありません。

この二つの方式では、集合を扱う時と、逆演算を考える時に違いが出てきます。関係モデルでは、表の検索結果はゼロ個も含む集合になりますが、関数で集合を返すには時は特別にリストデータ構造が必要だったり、値が未定義の場合の扱い(null やエラー)を考える必要があります。また、関係モデルでは表の右をキーにして検索するか左をキーにして検索するかだけの違いなので、いつでも逆演算を定義出来る一方で、関数では特別(全単射)な場合だけ逆演算が可能です。

Alloy の面白い所は、扱うデータが全てこの「関係」だという事です。一番低レベルな部分では、単なる集合も要素も無くて、それらは関係の特別な場合だという決まりになっています。例えば、バナナと魚を含む集合 Food があるとします。すると集合 Food = {バナナ, 魚} は

Food = {(unit, バナナ), (unit, 魚)}

という風に特別なアトム unit との関係だという風に考えます。しかも、実はその集合の中身であるバナナ自体も要素が一つしか無い集合で、結局は

バナナ = {(unit, バナナ)}

という事になるのです。じゃ、その中身は何なんだ！という事は考えないみたいです。要素を集合として考える利点は、要素のための特別な演算を用意しなくて良い事です。例えば、バナナが食べ物に含まれるという文も、果物が食べ物に含まれるという文も同じように表現出来ます。私が思う欠点は、たまに要素が一つの時を特別扱いする必要がある事です。まあ、これはどっちもどっちなので仕方が無いです。

Alloy では、この関係を元に色々面白い演算子が定義されています。特に面白いのが ~ (転置) と . (結合)です。特に . は一つの演算子でプロパティアクセスと表結合と直積を全部表現出来るすごいアイデアです。

まず転置から。~ は関係の右と左を入れ替えます。例えば

like = { (ドラえもん, ドラ焼き), (しずか, 焼き芋) }
の時
~like = { (ドラ焼き, ドラえもん), (焼き芋, しずか) }

のようになります。これで逆関数を表現出来ます。

次に . は二つの表を結合します。結合する時に、前の表の二番目の項目と後の表の一番目の項目が同じ物だけを抜き出して、前の表の一番目の項目と後の表の二番目の項目を返します。と書くとややこしいですが、Haskell 風に式で書くと

a . b = [(x, z) | (x, y) <- a, (y', z) <- b, y == y']

で、例を挙げると

like = { (ドラえもん, ドラ焼き), (しずか, 焼き芋), (コロ助, コロッケ) }
taste = { (ドラ焼き, 甘い), (焼き芋, 甘い), (コロッケ, 塩味) }
の時
like . taste = { (ドラえもん, 甘い), (しずか, 甘い), (コロ助, 塩味) }

面白いのが、これがプロパティアクセス風に使える事です。なぜなら

ドラえもん = { (unit, ドラえもん) }
like = { (ドラえもん, ドラ焼き), (しずか, 焼き芋), (コロ助, コロッケ) }
なので、
ドラえもん . like = { (unit, ドラえもん) } . { (ドラえもん, ドラ焼き), (しずか, 焼き芋), (コロ助, コロッケ) }
                 = { (unit, ドラ焼き) }
                 = ドラ焼き

さらに、~ と . を組み合わせると直積を作れます。a と b の直積を求めるには ~a.b とします(論文には a.~b と書いてあるけど、多分間違い？)。

Person = { ドラえもん, しずか, コロ助 }
Kind = { 人間, ロボット }
の直積は、

~Person . Kind = ~{ (unit, ドラえもん), (unit, しずか), (unit, コロ助) } . { (unit, 人間), (unit, ロボット) }
               =  { (ドラえもん, unit), (しずか, unit), (コロ助, unit) } . { (unit, 人間), (unit, ロボット) }
	       =  { (ドラえもん, 人間), (ドラえもん, ロボット), (しずか, 人間), (しずか, ロボット), (コロ助, 人間), (コロ助, ロボット) }

残念ながら、Alloy にカーネル言語を直接使う仕組みが無いので、上の例を実際試すのはちょっとややこしいです。しかしとりあえず Alloy というモデル検査プログラムの基礎が二項関係という単純な仕組みだけで出来ていて凄いという事を書きました。

言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Alloy: A Lightweight Object Modelling Notation