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

数学の本に書いてあることを Agda で定義してみる。なるべく、数学の本に近くする。

Agda は関数型言語なので、数字の添字を使うものは合わない。そのあたりは修正する。

Agda は直観主義論理なので、排他律が成立しない。存在を示すには構成的、つまり関数で構成する必要がある。

数学の本でも、構成的な証明かどうかは(選択公理を使っているかどうかなどで)区別されていることが多い。

-- Automaton オートマトンの定義 ( Q, Σ, σ, q0, F )

教科書では以下のようになっている。

    1. Q is a finte set calles states
    2. Σ is a finte set calles alphabet
    3. δ : Q x Σ is the transition function
    4. q0 ∈ Q is the start state
    5. F ⊆ Q is the set of accept states

これを Agda で表すには record を使う。

    record Automaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
            δ : Q → Σ → Q
            aend : Q → Bool

どれがどこにん対応しているかを確認しよう。

<a href="../agda/automaton.agda"> automaton.agda </a>
<br>
<a href="../agda/logic.agda"> logic.agda </a>
<br>

record は名前のついた数学的構造で、二つの集合 Q と Σの関係定義する関数からなる。

record は直積で複数の集合の組だが、ここでは関係を表す論理式/関数の型の組になっている。

      δ : Q → Σ → Q

は関数で、引数を二つ持っている。ここでは論理式ではない。入力となるaplhabet(文字) とstate (状態)から次の状態を指定する関数である。
transition function (状態遷移関数)と呼ばれる。

       aend : Q → Bool

これはQの部分集合を指定している。Bool は

     data Bool : Set where
        true   : Bool
        false  : Bool

で、true false の二つの要素を持つ集合である。(これでどうして部分集合になるのか? F ⊆ Q を Agda ではどう定義するべきか? Set を使わないのはなぜか)

start state はrecordで定義しない方が便利だと言うことがこの後わかる。

--オートマトンの入力

オートマトンの入力は文字列である。文字列を表すには List を用いる。

    data  List  (A : Set ) : Set  where
       [] : List A
       _∷_ : A → List A → List A

    l2 = a ∷ b ∷ a ∷ c ∷  []

だったことを思い出そう。(Agda のbuiltinのListは ∷ を使う)


--状態遷移

状態遷移関数をListに適用する。

    moves : { Q : Set } { Σ : Set  }
        → Automaton Q  Σ
        → Q → List  Σ → Q
    moves {Q} { Σ} M q L = move q L
       where
          move : (q : Q ) ( L : List  Σ ) → Q
          move q [] = q
          move q ( H  ∷ T ) = move (  (δ M) q H ) T

List に沿って、状態が変わる。

    accept : { Q : Set } { Σ : Set  }
        → Automaton Q  Σ
        → (astart : Q)
        → List  Σ → Bool
    accept {Q} { Σ} M astart L = move astart L
       where
          move : (q : Q ) ( L : List  Σ ) → Bool
          move q [] = aend M q
          move q ( H  ∷ T ) = move (  (δ M) q H ) T


最後の状態が aend ならば accept される。これらを、record Automaton 内で定義しても良い。

---具体的なオートマトン

reccord Automaton は抽象的なオートマトンで実装がない。(Java/C++ の abstract classと同じ)
実装を与えるには、record のfield の型を持つ関数を与えれば良い。

まず、状態と文字を定義する。

    data  States1   : Set  where
       sr : States1
       ss : States1
       st : States1

    data  In2   : Set  where
       i0 : In2
       i1 : In2

状態遷移関数と accept state を作ろう。

    transition1 : States1  → In2  → States1
    transition1 sr i0  = sr
    transition1 sr i1  = ss
    transition1 ss i0  = sr
    transition1 ss i1  = st
    transition1 st i0  = sr
    transition1 st i1  = st

    fin1 :  States1  → Bool
    fin1 st = true
    fin1 _ = false

st になればok。record は以下のように作る。

    am1  :  Automaton  States1 In2
    am1  =  record {  δ = transition1 ; aend = fin1   }

これを動かすには、

    example1-1 = accept am1 ( i0  ∷ i1  ∷ i0  ∷ [] )
    example1-2 = accept am1 ( i1  ∷ i1  ∷ i1  ∷ [] )

とする。( example1-1 の型は何か?)

<a href="../agda/automaton-ex.agda"> Agda による Automaton の例題 </a>

--問題 3.1

教科書のAutomatonの例のいくつかを Agda で定義してみよ。

accept される入力と accept されない入力を示し、Agda で true false を確認せよ。

<a href=""> </a>  <!---  Exercise 3.1 --->


--Regular Language

Automaton は List Σ に対して true / false を返す。つまり、文字列の部分集合を決定する。

文字列の部分集合を (Automaton の専門用語として) Language という。でたらめの発声の部分集合が日本語なので言語といえなくもない。

    language : { Σ : Set } → Set
    language {Σ} = List Σ → Bool

なんらかのAutomaton が受け付ける文字列の部分集合を Regular Language という。この範囲に収まらない Language も後で調べる。


--Agda によるRegular Languageの集合演算

何かのAutomaton で判定される言語は ∃ automaton だが、これを record で書く。

    record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
       field
          states : Set 
          astart : states 
          automaton : Automaton states Σ
       contain : List Σ → Bool
       contain x = accept automaton astart x

contain が language の定義の形になっていることを確認しよう。

--Regular Languageの演算

Regular Languageは以下の演算に付いて閉じていることが知られている。閉じているとは以下の集合演算をしても、それはやはり
Regular Language つまり、Automaton で、その集合に入っているかどうかを判定できる。

    二つの文字列集合から、その結合を集める Concatenation

    文字列の集合の和集合 Union

    結合の繰り返し Star

<a href="../agda/regular-language.agda"> Agda での Regular Language </a>

Union は Bool 演算を使って簡単に表される。

    Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
    Union {Σ} A B x = (A x ) \/ (B x)

Concat はそんなに簡単ではない。ある文字列が、前半はAの要素で、後半がBの要素であれば良いのだが、

    Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
    Concat {Σ} A B x = ?

前半と後半の分け方には非決定性がある。

--Split による List の分割

i0 ∷ i1 ∷ i0 ∷ [] の分け方は and と or で以下のようになる。

       ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
       ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
       ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
       ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 

Agda は高階論理なので、これを任意長の List に対して定義できる。

    split : {Σ : Set} → (List Σ → Bool)
          → ( List Σ → Bool) → List Σ → Bool
    split x y  [] = x [] /\ y []
    split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
      split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

これが、実際に文字列の分解になっていることを確認する。

    test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
           ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
           ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
           ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
           ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 
       )
    test-AB→split {_} {A} {B} = refl

これを使って Concat と Star を書ける。

    Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
    Concat {Σ} A B = split A B

    {-# TERMINATING #-}
    Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
    Star {Σ} A [] = true
    Star {Σ} A (h ∷ t) = split A ( Star {Σ} A ) (h ∷ t)

{-# TERMINATING #-}は Agda が停止性を判定できないというエラーを抑止するのだった。

--Union が RegularLanguage で閉じていること

RegularLanguage かどうかは以下の命題を作れるかどうかでわかる。

    isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
    isRegular A x r = A x ≡ contain r x 

たとえば Union に付いて閉じているかどうかは

     closed-in-union :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )

とかける。この時に 

     M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ

で、これは Automaton を具体的に作る必要がある。

この証明は M-Union の定義とUnionが同じことなので簡単に証明できる。


--Concat が RegularLanguage で閉じていること

これは割と難しい。Automaton の状態が有限であることが必要になる。

A x ≡ contain r x は両辺が true の場合と false の場合がある。これを示すことになる。

    ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B

をつかって

    closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
    closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
    closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
    closed-in-concat→ = ?
    closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
    closed-in-concat← = ?

とする。

問題は  M-Concat A B つまり、Concat を受け付ける automaton をどうやって定義するかになる。

これは次の lecture で行う。

--Star が RegularLanguage で閉じていること

これも問題は上と同じだが...