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

-- 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>
<a href="../agda/finiteSet.agda"> finiteSet.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 ではどう定義するべきか?)

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 の型は何か?)

--問題 3.1

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

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

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


--Regular Language

Language とは?

Regular Language とは?

--Regular Languageの演算

Concatenation

Union

Star

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