決定性オートマトン
Menu数学の本に書いてあることを 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
どれがどこにん対応しているかを確認しよう。
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 の型は何か?)
問題 3.1
教科書のAutomatonの例のいくつかを Agda で定義してみよ。accept される入力と accept されない入力を示し、Agda で true false を確認せよ。
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
Agda での Regular Language
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 で閉じていること
これも問題は上と同じだが...