オートマトングラフの比較アルゴリズム

似たことは何度も書いているような気がするが、2011年春夏シーズン向けのアルゴリズム（新作じゃないけど）。

準備

いろいろと記号の約束をする。

• G, Hなどは有向グラフ
• 圏論の記法を借りて、グラフの頂点集合を|G|、辺集合を記号の乱用でGとも書く。
• 辺eに対して src(e)（ソース＝根本）、trg(e)（ターゲット＝行き先）は、圏のdom, codに相当。
• 有向グラフには基点が指定されている。g∈|G|, h∈|H| のように、グラフを表す文字を小文字にして表す（と約束）。
• 有向グラフには頂点ラベル、辺ラベルが付いている、それを、関数 V:|G|→Σ、E:G→Γ で表す。頂点ラベル（色、ノード値とか、呼び名はいろいろ）の集合Σは順序集合、辺ラベルの集合Γ（ガンマ）はなんでもよい。ΣとΓは前もって固定されているとする。記号の乱用で、すべてのグラフに対して同じ記号V, Eを使い回す。
• グラフは決定性のオートマトンを表すので、頂点から出る辺にはすべて異なるラベルが付いている。選択（choice, union）ノードは、辺ラベルというよりは、候補の頂点を調べて遷移を決定するんだが、辺ラベルだと考えてもまーいいだろう。
• 「パラメータ、変数、プレースホルダー、穴（hole）」などと呼ばれる頂点がある。ここでは、グラフGの変数（頂点の一種だよ）の全体をVar(G)と書く。Var(G)が空でもよい。x∈Var(G)ならば、out(x) = 0。outは頂点の出次数（out degree）。

我々が扱う決定性オートマトンを表現するグラフGは：

1. 基点gを持つ。（起点は開始状態）
2. 頂点にラベル（値、属性）が付いている。V:|G|→Σ
3. 辺にラベルが付いている。E:G→Γ
4. 頂点ラベルの集合Σには順序（記号は≦を使う）が入っている。全順序とは限らない。
5. 辺ラベルは決定性である。
6. 変数と呼ばれる頂点がある（かもしれない）。変数頂点は、頂点ラベルによって識別されてもいいし、その他の方法で識別されてもよい。

x∈|G| に対して、頂点xの近傍（正確には、距離1のout近傍だけど）N(x) を次のように定義する。

• N(x) = {y∈|G| | xからyに向かう辺がある}

ほんとは、N_G(x) とか書くべきだろうが、またしても記号の乱用。

アルゴリズム

GとHを与えられた2つのグラフとして、比較の作業はトライアルの繰り返しとなる。トライアルが進むと、Next, Done, Resultという集合が更新される。トライアルが失敗すると全体も失敗し、トライアルが成功すると次のトライアルに進む。次にすべきことがなくなると（Nextが空集合）全体が成功。

• Next⊆(|G|×|H|) 次に調べるべき頂点ペアの集合
• Done⊆(|G|×|H|) 既に調べ終わった頂点ペアの集合
• Result⊆(|G|×|H|) 最汎事前制約。単なる頂点ペアではなくて、どっちかは変数。もう少し正確に書くと、Result⊆(Var(G)×|H| ∪ |G|×Var(H) ∪ Var(G)×Var(H)) ←たいして正確じゃねーな、コレ。

トライアルの手順

1. Nextが空なら全体が終了。そのときのResultが全体の結果。
2. Nextが空でないなら、そこから任意の元（頂点のペア） (x, y) を取り出す。
3. (x, y)に関して頂点の比較（後述）をする。
4. 頂点の比較が失敗すればトライアルは失敗。
5. 頂点の比較が成功すれば、次に辺の比較（後述）を行う。
6. 辺の比較が失敗すればトライアルは失敗。
7. 辺の比較が成功すれば、N(x)とN(y)からペアを作って、N(x, y)を構成する（後述）
8. Nextから (x, y) を取り除きDoneに加える。
9. N(x, y)＼Done をNextに加える。（「＼」は集合の差を表す）

Next, Doneの動きは：

• 失敗の時は何もしない（どうせ全体が失敗する）。
• 成功なら、Next := Next＼{(x, y)}; Done := Done∪{(x, y)}; Next := Next∪(N(x, y)＼Done)

Resultの作り方は後述。

頂点の比較

頂点ペア(x, y)に対して、

1. xが変数のとき（つまり、x∈Var(G)）、(x, y) をResultに入れて成功。Result := Result∪{(x, y)}
2. yが変数のとき（つまり、y∈Var(H)）、(x, y) をResultに入れて成功。Result := Result∪{(x, y)}
3. xもyも変数ではないとき、V(x)≦V(y) なら成功、そうでないなら失敗。

辺の比較

辺の比較も、頂点ペア(x, y)に対して行う。x∈|G|から出る辺を e1, e2, ..., eN とする（Nは頂点xの出次数）。[追記]ウギャ、Nが近傍の記号とかぶった。ここでは非負整数。 [/追記]

1. N = 0 のときは、成功。
2. E(e1) = a1 として、yから出るHの辺でa1をラベルとする辺を探す。なければ失敗。
3. yから出る辺でa1をラベルとする辺（決定性から一意に決まる）があったら、それをf1として、ペア (trg(e1), trg(f1)) を作っておく。
4. e2, ..., eN まで同じことを繰り返す。

以上の過程で出来た集合 {(trg(e1), trg(f1)), (trg(e2), trg(f2)), ..., (trg(eN), trg(fN))} を N(x, y) とする。N(x, y) は、次のトライアルのNextを決めるために使う。

Next := Next＼{(x, y)}; Done := Done∪{(x, y)}; Next := Next∪(N(x, y)＼Done) なので、Next∪N(x, y) 作ってから、{(x, y)}∪Done を取り除いても同じ。

[追記]なるほど、引数なしのN（非負整数）と1 or 2引数のN（近傍 or 近傍の対応）は、アリティでオーバーロードされていて、まったく別な意味で使っているわけね。アドホックつうか無関係なオーバーロードだ。[/追記]

全体のセットアップ

初期状態は：

• Next := {(g, h)} （基点の対）
• Done := {} （空集合）
• Result := {} （空集合）

Doneはトライアルが成功するたびに1個ずつ要素が増える。Nextは増えたり減ったりしながら最終的には空になる（成功の時）。Resultは単調に増えるが、空のままかもしれない。

成功すればResultが得られる。失敗のときは、どこ（どの頂点対）で何が原因で失敗したかを報告する。