Mercurial > hg > Members > kono > Proof > automaton
diff a04/lecture.ind @ 326:a3fb231feeb9
omega
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 21 Jan 2022 10:45:42 +0900 (2022-01-21) |
parents | b3f05cd08d24 |
children | 9324852d3a17 |
line wrap: on
line diff
--- a/a04/lecture.ind Sat Jan 15 01:12:43 2022 +0900 +++ b/a04/lecture.ind Fri Jan 21 10:45:42 2022 +0900 @@ -66,6 +66,29 @@ このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。 +--状態と入力の List を使って深さ優先探索する + + {-# TERMINATING #-} + NtraceDepth : { Q : Set } { Σ : Set } + → NAutomaton Q Σ + → (Nstart : Q → Bool) → List Q → List Σ → List (List ( Σ ∧ Q )) + NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where + ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) ) + ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q )) + ndepth1 q i [] is t t1 = t1 + ndepth1 q i (x ∷ qns) is t t1 = ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 ) + ndepth [] sb is t t1 = t1 + ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q + ... | true = ndepth qs sb [] t ( t ∷ t1 ) + ... | false = ndepth qs sb [] t t1 + ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q + ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) + ... | false = ndepth qs sb (i ∷ is) t t1 + +確かに動く。しかし、複雑すぎる。 + +--状態の部分集合を使う + true になるものは複数あるので、やはり部分集合で表される。つまり、 exists : ( P : Q → Bool ) → Q → Bool @@ -76,6 +99,8 @@ --finiteSet +有限な集合を表すのに、個々の data を使えばよいが、統一的に扱いたい。Agda には Data.Fin が用意されている。 + Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。 record FiniteSet ( Q : Set ) { n : ℕ } : Set where @@ -116,7 +141,7 @@ Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば -遷移可能になる。 +遷移可能になる。(だいぶ簡単になった) Naccept : { Q : Set } { Σ : Set } → NAutomaton Q Σ @@ -168,10 +193,6 @@ example136-2 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) ---問題 - -... 作成中... - --非決定性オートマトンと決定性オートマトン @@ -216,7 +237,7 @@ 終了条件は f q /\ Nend NFA q ) -' + で良い。 これが true になるものを exists を使って探し出す。 Q が FiniteSet Q {n} であれば @@ -236,6 +257,8 @@ であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。 +これで実際に、NFAから DFA を作成することができた。ここで、状態の有限性を使っていることを確認しよう。 + <a href=" ../agda/sbconst2.agda"> subset construction </a> --subset constructionの状態数 @@ -260,3 +283,19 @@ 実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。 +--NFAの実行 + +subset construction した automaton はすべての状態を生成する前でも実行することができる。 +ただし、毎回、nest した exists を実行することになる。 + + + + + + + + + + + +