Alloyガール 迷宮編 2

推移閉包

僕: さて、前回は迷路らしきものを作ることはできたけど、入口から出口まで到達できないという問題があった
Ruby: 条件が足りなかったんですね
僕: A から関係 rel を辿って B まで到達できるというのを表現するイディオムならわかるぞ、Alloy*1で何度もやったからね

B in A.^rel

僕: こうだ。"^" は関係の「推移閉包」を得る演算子
Ruby: すいいへいほう?
僕: えーとつまり rel に含まれる任意の 2つのタプル a -> b と b -> c があったときに、それを連結した a -> c も含むような関係のことだ。

all a, b, c: univ | (a -> b in ^rel && b -> c in ^rel) => a -> c in ^rel

僕: ちなみに "." はちゃんと説明しなかったけど、結合演算子
Ruby: メソッド呼び出しみたいですね
Alloy: それとはまったく別物ですけどね。 A.B は A の関係に含まれるタプルの最後の atom と B の関係に含まれる最初の atom が一致する全組み合わせを連結して、1つの関係にする演算子
僕: A が集合(arity が 1 の関係)で、B が2項関係の場合は A の全要素に B を関数として適用するようなイメージも考えられるけどね
Ruby: 関数ですか?
僕: たとえば B が { 1 -> 1, 2 -> 4, 3 -> 9, 4 -> 16 } というタプルを持つ2項関係だとすると、これは関数みたいじゃない?
Ruby: 1.B = 1, 2.B = 4, 3.B = 9 となるんですね
Alloy: 2項関係が「関数的」という時にはタプルの最初の atom が同じようなタプルが 2つ以上含まれていないという条件があるけどね
Ruby: あっ、そうですね B = { 1 -> 1, 1 -> 2 } のような関係だと 1.B が 1 か 2 かどちらかに決まらないです。でもこういう時はどうなるんですか?
Alloy: だから "." は別に関数適用でもメソッド呼び出しでもないから、ルール通り全ての組み合わせで連結されるだけ。 { 1 } . { 1 -> 1, 1 -> 2 } = { 1, 2 }
僕: そうだね、別の言語でのパラダイムはイメージしやすくするために例として上げるぶんにはいいけど、あくまで関係演算子だということは理解しておかないといけないかもね

僕: さて推移閉包に戻るけど、Alloy の文ではないけどこんな表現もできるね

^rel = rel + rel.rel + rel.rel.rel + rel.rel.rel.rel + ...

Ruby: 再帰的なんですね
僕: えっ?
Ruby: なんとなくメソッドの再帰的呼び出しみたいだなぁって思って
僕: うーんまあ繰り返しが任意の回数続くからそうかもなぁ…あれ?
Ruby: どうかしました?
僕: そうか、推移閉包演算子って「任意回数の繰り返し」が含まれている演算子なんだなぁ
Alloy: そう。推移閉包と反射的推移閉包は Alloy の表現力を高める重要な演算子。処理系内部で関係の展開が行なわれる

4項関係の推移閉包?

Alloy: ところで4項関係の paths でどうやって到達可能性を表現するつもり?
僕: えーっと、こんなふうにできるのかな

  // 全ての位置に入口から到達できる
  all col: Col, row: Row | (col -> row) in (^paths)[entrance_x, entrance_y]

Alloy: 以下のようなエラーになるよ

A type error has occurred:
^ can be used only with a binary relation.
Instead, its possible type(s) are:
{this/Col->this/Row->this/Col->this/Row}

僕: あっ、そうか、推移閉包は2項関係にしか使えないんだ。ええと、それじゃあ fun を使って…

fun reachable (col: Col, row: Row) : Col -> Row {
  col -> row + reachable [adjacent[col, row].Row, Col.(adjacent[col, row])]
}
(...snip...)

  // 全ての位置に入口から到達できる
  all col: Col, row: Row | (col -> row) in reachable [entrance_x, entrance_y]

Alloy: それもだめ。 fun は再帰的な定義はできない

A syntax error has occurred:
fun this/reachable cannot call itself recursively!

僕: そうか、高階論理が使えないというのは、そういうことか…
Alloy: そうね、推移閉包と反射的推移閉包が特別扱いと言えるかもね
Ruby: じゃあ、次はどうしましょう?
僕: え、えーっと…あれっ、もしかして 4項関係にしたのはまずかったかな
Alloy: 前回口を挟んだものかどうか迷ってたのだけど、4項関係だと推移閉包が使えないので記述力は落ちることになるね
僕: あー、あの三点リーダー(…)はそういう事だったのか
Ruby: どうしようもないんでしょうか
僕: いや、こうなったらしかたないから、各座標(タイル)に対応する signature を導入してタイル間の行き来ができることを2項関係で表現してみよう
Ruby: はい! あれ、でもそれって…
僕: そうだね、最初にやめた方法だけど、やってみるしかないね。と、今日はこのくらいにしておこう

お茶の時間

Ruby: なんだか今日はのんびりでしたね
僕: うん、正直いきなり Alloy の文法とか演算子の説明とか何もなしだったのでよくなかったかなぁと思って
Alloy: けど演算子の説明にしても結合演算子に `.` と `[]` の2つあることを抜かしてたりして中途半端ね
僕: そのへんどうしたものかなぁ。詳しくは Alloy 本を読むか、英語なら 公式サイトの Documentation を読んで、ということになるし。
Ruby: 抽象によるソフトウェア設計のリンクを貼っておけばいいですね!
僕: 自分なりに、エッセンスっぽいところをかいつまんでいるつもりだけど、あまり細かい説明を続けても話が続かないし
Alloy: どちらかというと、本題のほうがなかなかうまくいかないから細かい説明で時間稼ぎをしているんじゃないの
僕: うっ…