決定性オートマトン
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 ) TList に沿って、状態が変わる。
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 _ = falsest になれば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 xcontain が language の定義の形になっていることを確認しよう。
Regular Languageの演算
Regular Languageは以下の演算に付いて閉じていることが知られている。閉じているとは以下の集合演算をしても、それはやはりRegular Language つまり、Automaton で、その集合に入っているかどうかを判定できる。
二つの文字列集合から、その結合を集める Concatenation 文字列の集合の和集合 Union 結合の繰り返し StarAgda での 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 で閉じていること
これも問題は上と同じだが...