2006-09-06

余代数は、相変わらずよく分からない。(決定性有限)オートマトンは、一種の等式系と見なせる。そして、それは余代数の例になってるらしい

簡単な例。入力記号集合が{s,t}で、状態集合を{q0,q1,q2,q3}とする。遷移関係は



delta(s,q0)=q2 , delta(t,q0)=q1

delta(s,q1)=q3 , delta(t,q1)=q0

delta(s,q2)=q0 , delta(t,q2)=q3

delta(s,q3)=q1 , delta(t,q3)=q2

で与えられて、開始状態と受理状態は、q0とする。

で、上の遷移関係を形式的に



q0->s*q2 + t*q1

q1->s*q3 + t*q0

q2->s*q0 + t*q3

q3->s*q1 + t*q2

と書く。更に、遷移関係を等式に置き換えてしまう



q0 = s*q2 + t*q1 + e

q1 = s*q3 + t*q0 + 0

q2 = s*q0 + t*q3 + 0

q3 = s*q1 + t*q2 + 0

いくつかお約束。*,+演算は共に、結合的で、かつ+演算は可換であるとする。あと、通常の分配則も認める。また、eと0は、



0+x = x+0 = x

0*x = x*0 = 0

x*e = e*x = x

という関係を満たすとする。eというのは、空列に対応する記号で、q0が開始状態なので付けてるお呪い。0は、別になくてもいいけど、気分の問題。どっちにしろ、x+0=xなので、無視できる

で、上の等式を全く形式的に解く。q0が受理状態なので、q0=(何か)という形にしたい



q0 = s*(s*q0+t*q3+0) + t*(s*q3+t*q0+0) + e = (s*s+t*t)*q0 + (s*t+t*s)*q3 + e = a*q0+b*q3+e

q3 = s*(s*q3+t*q0+0) + t*(s*q0+t*q3+0) + 0 = (s*s+t*t)*q3 + (s*t+t*s)*q3 = b*q0+a*q3

a = s*s+t*t

b = s*t+t*s

となる。更に、形式的な計算を繰り返して



q0 = a*(a*q0+b*q3+e) + b*(b*q0+a*q3) + e

   = e + a + a*a*q0 + b*b*q0 + a*b*q3 + b*a*q3

   = e + a + a*a + b*b + b*b*a + a*a*a + etc....

となる。最後のは、形式的な無限級数。で、a=s*s+t*tなのだけど、これは、記号列ssとttがこの有限オートマトンで受理されることを意味する。また、eは空列に対応して、この有限オートマトンでは、空列も受理されることが分かる(開始状態=受理状態なので当然)。以下面倒なので、*記号を省略すると、aa=ssss+sstt+ttss+ttttなので、この4種の記号列{ssss,sstt,ttss,tttt}も受理されることが分かる。つまり、先の等式を形式的に解くと、q0は、この有限オートマトンで受理される全ての記号列の形式和と等しい。同様にq1について解くと、q1は、q1を受理状態としたときに受理される全ての記号列の形式和で表される。

もっとシンプルな場合は、



q = a*q + e

という等式で、形式的に解けば



q = a*(a*q+e)+e

  = e + a + a*a*q

  = e + a + a*a + etc...

で、qはaのKleene閉包となる。てなわけで、オートマトンの受理集合は、ある種の等式系の形式解と同一視できるということが分かる。

これのどこが余代数なのか。一見普通の等式系と一緒に見える。けど、じっと見てると、最初の矢印の向きが、普通の項書換え系と逆。つまり、普通の項代数なんかだと、x=F(x)という等式があったら、よりsimpleな方にF(x)->xという項書換え規則に変換する。例えば、x=x+0のようなのが、典型的な例。一方で、q=a*q+eを、a*q+e->qという書換えにしてしまうと、重要な情報が全部失われてしまう。こうすると、計算は停止しなくなるけど、現実のシステムの中には、停止するより、半永久的に動作することを想定されているものも多い(例えば、OSとか)。というわけで、そういうシステムの定式化には、余代数が合っているということなのかもしれない。

で、まあだからどうした？って話。オートマトンがある種の等式系と等価なんてのは、物事には色んな見方があるってだけの話で、そういう見方を知るのも悪くはないけど、敢えてそういう視点を取ることで、どういうメリットがあるのか。余代数として見ると、何かできるようになることがあるのか、そのへんが不透明

意味論の使い道

オートマトンと等式系