ネロード同値とか
今日はメモ編をやたらにイッパイ書く日だな、ウン。
列言語の理論で、言語Lが正規言語であることは、Lから作ったネロード（マイヒル/ネロード）同値による商集合が有限集合になることと同値となる。このネロード同値関係は、振る舞い同値（behavioural equivalence; 実験・観測で識別不可能）の特殊なケースになっている。
振る舞い同値と商状態空間上の実装
まず、次のようなアメナブルな（アクセッサとミューテータだけからなる）インターフェース（指標）を考える。
- コンストラクターは1つだけ：$()とする。
- アクセッサは1つだけ:ψ(x)とする、値は真偽値。
- ミューテータはいずれも1引数（状態を引数にとる）で、a(-), b(-)など。
状態xに対して、b(a(x))を(x).a.b のようにも書く。a.bのようなパス表記は、ミューテータの連続適用で、{a;b}のような複文ともみなせる。p, qなどはミューテータのパス（あるいは任意の文）を表す。
状態空間がSであるインターフェースの実装（モデル）があったとして、x, ｙ∈Sが振る舞い同値（あるいはネロード同値）だとは、任意パスqとアクセッサψに関して：
- ψ((x).q) = ψ((y).q)
振る舞い同値を≡として、S' = S/≡ を作って、その上に再びインターフェースの（抽象）実装を（理論上は）定義することができる。この（商空間を使った）実装は、“最小”な実装といってよい。
実装と言語の受理
ミューテータと同じ記号集合をアルファベットAとして、Aの列の全体を状態空間とした実装を考える。ミューテータaは、a(x) = x・a （右連接）として定義する。b(a(x)) = (x・a)・b = x・(ab)などに注意。$() = 空列、ψ(x) = [x∈L] とすると、振る舞い同値は、Lによるネロード同値になる。
上の定義は、インターフェースの超越的な、しかし標準的な実装になっている。Lはこの状態空間の部分集合になっている。Lを決めるとψが決まり、それに対して商状態空間も決まる。ミューテータの列により状態空間内を空列（それが始状態）からL内部（それが終状態）まで運動できるかどうかが、言語の受理の問題となる。
別な実装
Ruttenに従えば、もっと巨大な状態空間の標準実装がある。アルファベットAの言語の全体を状態空間とする。ミューテータaをaによる微分として定義する。ψはψ(X) = [ε∈X]で定義する。これも超越的な実装となる。Lは状態空間の点になっている。
振る舞い同値は、
- 任意の列qに対して ε∈q(X) ⇔ ε∈q(Y)
一般に、状態空間Sの実装に対して、Pow(S)の実装を作れるってことだろう。Sが部分力学系（遷移がpartial）でもPow(S)は全域になる点がメリットか？ SでもPow(S)でも振る舞い同値による商は定義できる。
