Agdaによる Automaton の記述
Menu
Automaton を学ぶ理由
人がコンピュータでできることの限界計算量の定義に必要 (NP の意味)
正規表現やハードウェア
仕様記述の基本
Agdaを使った Automaton の学習
今までは一階述語論理が普通 (意味関数と集合論)Agda は高階直観論理 (圏論ベース)
Agda はプログラミング言語でもある (みんな得意なはず
「型と関数」と「命題と証明」が同じ
一度に学べるのでお得
Agdaを使った学習って効果的なの?
自習にはばっちり時間はかかる
学生のやる気に結びつかない
証明は個人的
人によって異なる
List A
型の定義(Sum type)
data List (A : Set ) : Set where
[] : List A
_∷_ : A → List A → List A
これによりappendは以下のように実装される
_++_ : {A : Set } → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
Data.Nat
自然数も型に過ぎない (successor logic)
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
ペアノの公理とは異なる。これによりリストの長さは
length : List A → ℕ length [] = zero length (h :: t) = suc (length t)
等号もデータ型
data _≡_ {A : Set} : A → A → Set where
refl : {x : A} → x ≡ x
例えば List A の長さの分配則の証明
length-lemma : (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-lemma length-lemma [] ys = refl
length-lemma (x :: xs) ys = begin
length ((x :: xs) ++ ys ) ≡⟨ cong suc (length-lemma xs ys) ⟩
length (x :: xs ) + length ys ∎ where open ≡-Reasoning
≡-Reasoning が等式の変形に相当する。
関数型言語 Agda による Automaton の記述
record Automaton ( Q : Set ) ( Σ : Set )
: Set where
field
δ : Q → Σ → Q
aend : Q → Bool
これは Automaton の要件であり、その意味は以下の関数で定義する。
accept : { Q : Set } { Σ : Set }
→ Automaton Q Σ
→ Q
→ List Σ → Bool
accept M q [] = aend M q
accept M q ( H ∷ T ) = accept M ( δ M q H ) T
ここで、Q は有限という条件は付いてない。また、Set ではなく Bool で定義されている。
NFAの記述
非決定性 Automaton (NFA)は以下のように定義する。
record NAutomaton ( Q : Set ) ( Σ : Set )
: Set where
field
Nd : Q → Σ → Q → Bool
Nend : Q → Bool
この意味は、以下のように定義する。
Naccept : { Q : Set } { Σ : Set }
→ NAutomaton Q Σ
→ (exists : ( P : 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 /\ ( Nd M qn i q ) ))) t
NFAの記述と計算量
以下の関数は、Qに関する述語の真偽の判定を返す
exists : ( P : Q → Bool ) → BoolQが有限なら、これは構成できる
NFAが Automaton であることはわかるが計算量は
existsの計算量 関数構築の計算量があるので不明
NFAから Automaton である
subset-construction : { Q : Set } { Σ : Set } →
( ( Q → Bool ) → Bool ) →
(NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )
subset-construction {Q} { Σ} exists NFA = record {
δ = λ f i q → exists ( λ r → f r /\ Nd NFA r i q )
; aend = λ f → exists ( λ q → f q /\ Nend NFA q )
}
と簡単に変換できる
Automaton (Q → Bool) Σ )に着目する
正しい変換であることの証明
subset-construction-lemma→ : { Q : Set } { Σ : Set }
→ (exists : ( Q → Bool ) → Bool )
→ (NFA : NAutomaton Q Σ ) → (astart : Q → Bool )
→ (x : List Σ)
→ Naccept NFA exists astart x ≡ true
→ accept ( subset-construction exists NFA ) astart x ≡ true
subset-construction-lemma→ {Q} {Σ} exists NFA astart x naccept
= lemma1 x astart naccept where
lemma1 : (x : List Σ) → ( states : Q → Bool )
→ Naccept NFA exists states x ≡ true
→ accept ( subset-construction exists NFA ) states x ≡ true
lemma1 [] states naccept = naccept
と簡単に証明できる
高階直観論理での証明が異様に簡単な秘密
状態を数え上げてないので簡単になってる。状態の有限性の仮定(exists)が外部にある
実際に Naccept は決定的に動作する(関数の構築になっている)
状態の表示をする関数も簡単に作れる(演習問題)
Nacceptの計算量は不明だし、そこに立ち入ってない
一階述語論理と高階直観論理向けの記述は異なる
言語は以下のように定義される
language : { Σ : Set } → Set
language {Σ} = List Σ → Bool
ここで Set は型で命題を表す。List Σ → Bool が型であり、命題となっている
data Bool : Set where
true : Bool
false : Bool
一階述語論理では命題は Bool な値を持つしたがって排中律が成立する
Set は、命題であり、真偽を判定するには証明が必要P も ¬ P もどちらも証明がないなら、真偽は不明にある
正規言語の意味
一階述語論理では整数引数で定義を書くのが普通
Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Union {Σ} A B x = A x \/ B x
は簡単だが、
record Split {Σ : Set} (A B : List Σ → Bool )
(x : List Σ ) : Set where
field
sp0 sp1 : List Σ
sp-concat : sp0 ++ sp1 ≡ x
prop0 : A sp0 ≡ true
prop1 : B sp1 ≡ true
Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Concat {Σ} A B x = Split A B
この定義は難しい
高階関数的な Split
split : {Σ : Set} → (x y : language {Σ} ) → language {Σ}
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 [] )
これと Split A B の二つは同値であり、相互変換できる
関数の展開と平行した証明が可能だと思われる (まだ、やってないです)
有限性
NFAで必要なのは、
exits : ( Q → Bool ) → Boolこれは決定性であって有限性ではないのだが、Data.Fin を使って作ることもできる
なのだが、Data.Fin を使うとかなり複雑。
それが一階述語論理での NFA → Automaton の証明を複雑にしている
欲しいのはこれなので、有限性よりも工夫の予知がある(かも、気がする)
Agda の Safe
Q → Bool は関数なので、有限性を示すには、
record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
field
fun← : S → R
fun→ : R → S
fiso← : (x : R) → fun← ( fun→ x ) ≡ x
fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x
を示そうとすると、関数の ≡ を定義する必要がある。
関数外延性
Extensionality : (a b : Level) → Set _
Extensionality a b =
{A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
(∀ x → f x ≡ g x) → f ≡ g
を仮定するのだが、これは safe ではないとされる
これは Agda では真偽を決定できない
関数外延性をさけるには
record FBijection {n m : Level}
(R : Set n) (S : Set m) : Set (n Level.⊔ m) where
field
ffun← : S → R → Bool
ffun→ : (R → Bool) → S
ffiso← : (f : R → Bool ) → (x : R)
→ ffun← ( ffun→ f ) x ≡ f x
とするとよい。これを使って対角線論法が可能。
ffiso→ : (x : S) → ffun→ ( ffun← x ) ≡ x
は使わない
高階直観論理向きの記述
Automatonの教科書だと大体配列で書いてある i₁, i₂ ... 一階述語論理は部分集合が苦手List A と Q → Bool で書いていく
Automaton だと結合が難しくなるので、正規言語を NFA で定義する方が良いかも
ただ、NFAの微分法の記述とかはあんまり直観的にならない
高階直観論理は教育向き?
基本はやさしい複雑なものはやさしくない
学生は証明を追ったりしない
命題の記述や性質の8記述は明確で完結
証明は劇長い
かといって短い証明が良いとは限らない
coindution
帰納法の双対List には普通は長さは入れない
でも、最近は String には length を入れる方向
これが coinduction (データに大きさが入ってる)通常は List を分解していくが、大きさがわかってるので
List を構築する方向に推論できるAutomato に向いてる! 特に結合が自然
Codata
data Colist (i : Size) (A : Set) : Set where
[] : Colist i A
_∷_ : {j : Size< i} (x : A) (xs : Colist j A) → Colist i A
record Lang (i : Size) : Set where
coinductive
field
ν : Bool
δ : ∀{j : Size< i} → A → Lang j
_∋_ : ∀{i} → Lang i → Colist i A → Bool
l ∋ [] = ν l
l ∋ ( a ∷ as ) = δ l a ∋ as
trie : ∀{i} (f : Colist i A → Bool) → Lang i
ν (trie f) = f []
δ (trie f) a = trie (λ as → f (a ∷ as))
_·_ : ∀{i} (k l : Lang i) → Lang i
ν (k · l) = ν k ∧ ν l
δ (k · l) x = let k′l = δ k x · l in if ν k
then k′l ∪ δ l x else k′l
と concat が定義されているが、これは split による concat の定義と一致すれば良い。
算数を高階直観論理でみなおすべき?
累加は高階直観論理的な定義包含除は集合的/商群的な定義
かけ算の順序と関数外延性
高階直観論理では右かけ算と左かけ算がある。(かけ算の順序)
_*_ : ℕ → ℕ → ℕ
zero * y = zero
suc x * y = y + (x * y)
_*ˡ_ : ℕ → ℕ → ℕ
x *ˡ zero = zero
x *ˡ (suc y) = x +ˡ (x *ˡ y)
この二つは関数外延性的には等しい。しかし、関数外延性は否定も証明もできない
関数外延性を仮定すると、両方に等しくなる
これはどっちでも使えるという意味
かけ算原理主義
かけ算原理主義者(かけ算には順序はない)には
二つの定義は存在しない (過激派) 二つの定義をまだ決めてない _*_ ∨ _*ˡ_ (懐疑派) 二つの定義は同じ _*_ ∧ _*ˡ_ (穏健派)の三種類がいるらしい
過激派はかけ算の計算ができない
懐疑派は分配則を使えない
穏健派が無害
こういうのを防ぐためには、高階直観論理が良いかも
高階直観論理は小学生には無理?
段階がある
TM停止問題
高階直観論理では、高階なので決定不能性を直接扱えるrecord TM : Set where
field
tm : List Bool → Maybe Bool
record UTM : Set where
field
utm : TM
encode : TM → List Bool
is-tm : (t : TM) → (x : List Bool)
→ tm utm (encode t ++ x ) ≡ tm t x
record Halt : Set where
field
halt : (t : TM ) → (x : List Bool ) → Bool
is-halt : (t : TM ) → (x : List Bool )
→ (halt t x ≡ true ) ⇔
( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
is-not-halt : (t : TM ) → (x : List Bool )
→ (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )
対角線論法
¬ (S → Bool) <-> S
fdiagonal : { S : Set } → ¬ FBijection S S
fdiagonal {S} b = ¬t=f _ (trans ff4 (sym (ff3 _) ) ) where
ff1 : S
ff1 = ffun→ b (fdiag b)
ff2 : S → Bool
ff2 = ffun← b (ffun→ b (fdiag b) )
ff3 : (x : S) → ffun← b (ffun→ b (fdiag b) ) x ≡ fdiag b x
ff3 x = ffiso← b (fdiag b) x
ff4 : not ( ffun← b (ffun→ b (fdiag b) ) (ffun→ b (fdiag b))) ≡ fdiag b (ffun→ b (fdiag b))
ff4 = refl -- definition of fdiag b
証明
TNLF : (halt : Halt ) → (utm : UTM) → FBijection (List Bool) (List Bool) TNLF = ? TNLF1 : UTM → ¬ Halt TNLF1 utm halt = fdiagonal ( TNLF halt utm )残念ながら証明は複雑
高階直観論理と学習
∧ と ∨ と ¬
基本的な論理演算子として、∧ と ∨ と ¬ を
record _∧_ (A : Set ) ( B : Set ) : Set where
constructor ⟪_,_⟫
field
proj1 : A
proj2 : B
data _∨_ (A : Set ) ( B : Set ) : Set where
case1 : A → A ∨ B
case2 : B → A ∨ B
data ⊥ : Set where
¬_ : Set → Set
¬ A = A → ⊥
と定義できる。record が直積を表し、dataが場合分けを表す。
⊥ は constructor のない型/命題であり、その場合がないこと、あるいは矛盾を表している。
排中律 A ∨ (¬ A) は直観主義論理では「明示的に仮定して使う」
使えないというのはデマです
Bool
命題論理は true / false をつかって表すこともできる。
data Bool : Set where
true : Bool
false : Bool
_/\_ : Bool → Bool → Bool
true /\ true = true
_ /\ _ = false
_\/_ : Bool → Bool → Bool
false \/ false = false
_ \/ _ = true
not : Bool → Bool
not true = false
not false = true
これでだいたい全部
extended automaton
Turing : ( Q : Set ) ( Σ : Set ) → Set
Turing Q Σ = Automaton ( List Q ) Σ
NDTM : ( Q : Set ) ( Σ : Set ) → Set
NDTM Q Σ = Automaton ( List Q → Bool ) Σ
accept は自分で書く必要がある
便利なのかどうかは不明
モデル検査とかきれいに書けるかも
まとめ
Automaton理論に関して、Agda での定義と証明定義は簡潔 証明は複雑で長い
学生とっては証明を読む意味はあまりない
自分で証明を再構成すると理解が進む。
Agdaの safeness は一つのコーディング規則
coindutionがいいかも
高階直観論理を元に小中高の教育をみなおす?!