日々の流転

λ. 単純オートマトンの型について (HIMA' の補足)

先日のHIMA'で、

data Auto i o = A{ unA :: i → (o, Auto i o) }

という型*1が何故オートマトンの型なのかという話が少しあったので、簡単に補足しておく。 まず、入出力を扱う基本的なオートマトンとして、ミーリ・マシン（Mealy Machine）とムーア・マシン（Moore Machine）というものがある。

ミーリ・マシンは以下の組で定義される。

• 入力アルファベット集合 I
• 出力アルファベット集合 O
• 状態空間 S
• 初期状態 s0
• 遷移関数 δ: S×I→S×O

同様にムーア・マシンは以下の組で定義される。

• 入力アルファベット集合 I
• 出力アルファベット集合 O
• 状態空間 S
• 初期状態 s0
• 遷移関数 δ: S×I→S
• 出力関数 v: S→O

普通は入出力のアルファベットは固定したうえで、様々なオートマトンを考えると思うので、ここでは入出力のアルファベットはi,oに固定されているとする。すると、これらのオートマトンの初期状態を除いた構造は、

type T1 i o s = i → (o, s)
type T2 i o s = (o, i → s)

という型を定義して、ミーリ・マシンでは型S と 関数 S → T1 i o S の組によって、ムーア・マシンでは型Sと関数 S → T2 i o S の組によって表現できる。

T1 i o と T2 i o はともに関手になっていて、このような関手Tが与えれたときに、集合Xと関数 X → T X の組はT余代数(T-coalgebra)とも呼ばれる。そして、オートマトンの状態というのはこういう構造(=演算)を持った集合Sの要素であると考えることができる。

ただ、個々のオートマトン毎に型Sは異なっているので、いろんなオートマトンをシミュレーションしようと思うと、Haskellの型システム的には面倒くさい。それに、あるオートマトン(S1,δ1)の状態s1∈S1と、(S2,δ2)の状態s2∈S2は振る舞いが全く同じでも、値としては違う値であるかもしれなくて、これもよろしくない場合がある。

そこでS1やS2に相当する状態をすべて含んだ上で、かつ同じ振る舞いをする状態は同じ値になるような、そういう特別なオートマトンを考える。ミーリ・マシンの場合には (Auto i o, unA) がそれである。そして、以下のような関数 unfold phi によって、任意の (s, phi :: s → T1 i o s) の状態から、対応する (Auto i o, unA) の状態へと変換することができる。

unfold :: (s → T1 i o s) → s → Auto i o
unfold phi s = Auto $ \i →
  case phi s i of
    (o, s) → (o, unfold phi s)

余代数の言葉でいえば (Auto i o, unA) は T1 i o の終余代数(final (T1 i o)-coalgebra) で、unfold phi は (s, phi :: s → T1 i o s) から (Auto i o, unA) への一意な準同型射である。

このように、(Auto i o, unA) はある意味であらゆるオートマトンを表現できるような特別なオートマトンなので、これをオートマトンの型として扱っていると。