弱模倣＝非決定性コンパイル

無音{記号,遷移,アクション}またはブランク{記号,遷移,アクション}をアンダースコアで表す。入力記号Xと出力記号Yに対して、X_ = X + {_}、Y_ = Y + {_} とする。入出力記号は、X_×Y_ = X×Y + X×{_} + {_}×Y + {_}×{_} とする。

アルファベットΣを、Σ=X_×Y_ としたオートマトンがIOオートマトン。x, yはブランクになることもあるとして、(x, y)∈Σ とする。

F = (|F|, i_F, X, Y, f:Σ×|F|→*|F|) とする。|F|は状態空間、→* は非決定性写像を表す。記号の乱用で、fのグラフもFと書くことにする。F ⊆ Σ×|F|×|F|。

n≧1 として、s_i（i = 0, 1, ..., n）を|F|の点列、a₁, ..., a_nをラベル列とする。(s₀, a₁, s₁, ..., a_n, s_n) を遷移経路と呼ぶ。(s₀, a, s₁)を遷移ステップと呼ぶ。

Σ×|F|×|F||F|×Σ×|F| だから、F⊆|F|×Σ×|F| とみなして、遷移ステップとFの要素を同一視する。

遷移経路pに対して、入力アルファベットの列をIn(p), 出力アルファベットの列をOut(p)とする。In(p)∈(X_)⁺、In(p)∈(Y_)⁺ となる。

FとGが2つのIOオートマトンとして、R⊆|F|×|G| で (s, t)∈R を s〜t と書くことにする。

以上の準備のもとで、RがGによるFの弱模倣（weak bisimulation）であるとは、

1. s〜t、 (s, (x, y), s')∈F に対して、tからt'に至る遷移経路pがあって、In(p) =~ _*x_*、Out(p) =~ _*y_* が成立する。
2. i_F〜i_G

ここで、=~ は正規表現マッチを意味する。強模倣は、In（p）= x、Out(p) = y で、pも遷移ステップになる。強模倣は強すぎて使い途がないので、もっぱら弱模倣を考える。

弱模倣に方向を考えて、F⇒G のように書く。模倣されるオートマトン⇒模倣するオートマトン の順。弱模倣の条件から、α:F→*G という非決定性写像が決まる。この非決定性写像は、全域になる。どの遷移ステップ p∈F に対してもα(p)≠空。R:|F|→*|G| と α:F→*G の組を再びαと書く。

α::F⇒G は、弱模倣の非決定性写像（関係）による表現だが、p∈F に対するコンパイル結果がα(p)∈Pow(Path(G)) だと考えることができる。Fの遷移パスに対して、Gの遷移パスで同等な（弱同値な）入出力記号列を作るものを探すことができる。

非決定性コンパイル α::F⇒G が存在するとき、「FはG上で実現できる」「FはG上のアプリケーションである」「GはFのプラットフォームである」などと言う。弱模倣可能性＝コンパイル可能性＝振る舞い（意味）を変えずに翻訳可能＝GプラットフォームでFアプリケーションを実現可能、となる。

弱模倣可能性は、非決定性コンパイルの存在のことなので、非決定性コンパイルを具体的に構成すれば、弱模倣可能性を示したことになる。