-title: 非決定性オートマトン

決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。

このようなものが必要な理由は、 Regular Language の Concatを考えるためである。

Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y
にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。
しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。

二つのオートマトンが、a0..ae b0..be につながる様子を図にしてみる。

<center><img src="fig/concat.svg"></center>

このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、
一文字毎に増やしてやればよい。増やしたものの一つでも成功すればよい。Bが増えるので、その増えた状態を覚えておく必要がある。

    an (Aのn番目の状態)と、b0...bn の部分集合

状態はAの状態とBの状態の部分集合の組になる。

--(a.*f)(b.*f) を考えよう

abcfbffbcdf は、この正規表現にマッチする。a.*fb.*f と書いても良い。

Perl で書けば

  perl -de 0
  DB<14> if ($x =~ /^(a.*f)(b.*f)$/)  { print "$1 $2\n"; }

  perl -e 'if ($x =~ /^(a.*f)(b.*f)$/)  { print "$1 $2\n"; }'


a.*f は以下の状態遷移で書ける。

State は a0,a1,ae,af で、ae ならば受理。

     δa a0 a = a1
     δa a1 f = ae
     δa a1 _ = a1
     δa a0 _ = af

b.*f もどうように書ける。

     δb b0 b = b1
     δb b1 f = be
     δb b1 _ = b1
     δb b0 _ = bf

これを使って、a.*fb.*f を受理してみる。
<a href="../automaton-in-agda/src/nfa136.agda"> nfa136.agda </a>

<center><img src="fig/af-concat.svg"></center>

受理パターンは二通りある。これを非決定性があるという。

この状況は、f がきた時に a.*f を終了しても良く、終了しなくてよいことから来てる。

なので、それを許すオートマトンを考える。

--非決定性オートマトン

オートマトンの状態遷移は関数だった。

   δ : Q → Σ → Q 

その代わりに、複数の状態を許したい。Aの場合なら、f でaeにもa1にもいって良い。
それには、a1の状態で f がきた時に ae と a1 で true を返すようにすると良い。
行き先の状態を  Q → Bool で、部分集合として指定する。

    record NAutomaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
              Nδ : Q → Σ → Q → Bool
              Nend  :  Q → Bool

これを非決定性オートマトンという。

入力にそって、可能な状態の集合を作ってやれば良い。そうすると
決定性オートマトンにできる。

<center><img src="fig/afbf.svg"></center>


--もう一つの例


この場合では 1 が来た時に q1 に行っても、q2,q3 に行っても良い。q1から始める。

    q1  0 → q1
    q1  1 → q1
    q1  1 → q2
    q1  1 → q3
    q2  0 → q3
    q3  1 → q4
    q4  0 → q4
    q4  1 → q4

最後に q4で accept。

<center><img src="fig/nfa.svg"></center>

この時に、入力に従って状態の部分集合を計算していく方法でNFAのacceptを決定できる。

このNFA(nondeterministic automaton)は .*(101|11).* に対応している。


--Agda での非決定性オートマトン

ここでは、部分集合を写像を使って表す。集合 Q から Bool (true または false) への写像を使う。true になる要素が
部分集合になる。すると、遷移関数は入力Σと状態から Bool への写像となる。終了条件は変わらない。

    record NAutomaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
              Nδ : Q → Σ → Q → Bool
              Nend  :  Q → Bool

これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。

たとえば、以下のように非決定的な状態遷移を定義する

    transition3 : States1  → In2  → States1 → Bool
    transition3 sr i0 sr = true
    transition3 sr i1 ss = true
    transition3 sr i1 sr = true
    transition3 ss i0 sr = true
    transition3 ss i1 st = true
    transition3 st i0 sr = true
    transition3 st i1 st = true
    transition3 _ _ _ = false


<a href="../agda/src/nfa.agda"> nfa.agda </a>

--NAutomatonの受理と遷移

非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
入力を読み終わった後に、終了状態になれば受理されることになる。

このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。

--状態と入力の List を使って深さ優先探索する

    {-# TERMINATING #-}
    NtraceDepth : { Q : Set } { Σ : Set  } 
        → NAutomaton Q  Σ
        → (Nstart : Q → Bool) → List Q  → List  Σ → List (List ( Σ ∧ Q ))
    NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
        ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
        ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
        ndepth1 q i [] is t t1 = t1
        ndepth1 q i (x ∷ qns) is t t1 =  ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
        ndepth [] sb is t t1 =  t1
        ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
        ... | true =  ndepth qs sb [] t ( t  ∷ t1 )
        ... | false =  ndepth qs sb [] t t1
        ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 
        ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
        ... | false = ndepth qs sb (i ∷ is) t t1

確かに動く。しかし、複雑すぎる。

--状態の部分集合を使う

true になるものは複数あるので、やはり部分集合で表される。つまり、

     exists : ( P : Q → Bool ) → Q → Bool

このような関数を実現する必要がある。

もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。


--NAutomatonの受理と遷移

状態の受理と遷移は exists を使って以下のようになる。

    Nmoves : { Q : Set } { Σ : Set  }
        → NAutomaton Q  Σ
        → (exists : ( Q → Bool ) → Bool)
        →  ( Qs : Q → Bool )  → (s : Σ ) → ( Q → Bool )
    Nmoves {Q} { Σ} M exists  Qs  s  = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))

Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、
Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
遷移可能になる。(だいぶ簡単になった)


    Naccept : { Q : Set } { Σ : Set  } 
        → NAutomaton Q  Σ
        → (exists : ( Q → Bool ) → Bool)
        → (Nstart : Q → Bool) → List  Σ → Bool
    Naccept M exists sb []  = exists ( λ q → sb q /\ Nend M q )
    Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q →  exists ( λ qn → (sb qn /\ ( Nδ M qn i q )  ))) t

Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。

--例題

例題1.36 を考えよう。状態遷移関数は以下のようになる。

    transition136 : StatesQ  → A2  → StatesQ → Bool
    transition136 q1 b0 q2 = true
    transition136 q1 a0 q1 = true  -- q1 → ep → q3
    transition136 q2 a0 q2 = true
    transition136 q2 a0 q3 = true
    transition136 q2 b0 q3 = true
    transition136 q3 a0 q1 = true
    transition136 _ _ _ = false

教科書にはε遷移(入力がなくても遷移できる)があるが、ここでは、ε遷移先の矢印を全部手元に持ってきてしまうという
ことしてしまう。

    end136 : StatesQ → Bool
    end136  q1 = true
    end136  _ = false

    start136 : StatesQ → Bool
    start136 q1 = true
    start136 _ = false

    nfa136 :  NAutomaton  StatesQ A2
    nfa136 =  record { Nδ = transition136; Nend = end136 }

<a href=" ../agda/nfa136.agda"> 1.36 の例題  </a>

    example136-1 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ [] )

最初の状態 q1 から a0  ∷ b0  ∷ a0 ∷ [] の入力を受けとる場合を考える。

a0 を受けとると、q1 にしか行けない。q1 で b0 を受けとると、q2 に移動する。q2 で a0 を受けとると、q3 か、または、
q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2
から行けないが、どれかの経路が成功すれば良いので受理となる。

    example136-2 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )