Mercurial > hg > Members > kono > Proof > automaton
diff a04/lecture.ind @ 69:f124fceba460
subset construction
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 06 Nov 2019 17:18:58 +0900 (2019-11-06) |
parents | a7f09c9a2c7a |
children | fba1cd54581d |
line wrap: on
line diff
--- a/a04/lecture.ind Thu Oct 31 21:41:54 2019 +0900 +++ b/a04/lecture.ind Wed Nov 06 17:18:58 2019 +0900 @@ -9,65 +9,14 @@ record NAutomaton ( Q : Set ) ( Σ : Set ) : Set where field - nδ : Q → Σ → List Q - sid : Q → ℕ - nstart : Q - nend : Q → Bool + Nδ : Q → Σ → Q → Bool + Nend : Q → Bool これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。 -次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。 - -少し複雑がだが、insert と merge を定義して、 - -<a href="../agda/nfa-list.agda"> nfa-list.agda </a> - - insert : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → Q → List Q - insert M [] q = q ∷ [] - insert M ( q ∷ T ) q' with (sid M q ) ≟ (sid M q') - ... | yes _ = insert M T q' - ... | no _ = q ∷ (insert M T q' ) - - merge : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → List Q → List Q - merge M L1 [] = L1 - merge M L1 ( H ∷ L ) = insert M (merge M L1 L ) H - - Nmoves : { Q : Set } { Σ : Set } - → NAutomaton Q Σ - → List Q → List Σ → List Q - Nmoves {Q} { Σ} M q L = Nmoves1 q L [] - where - Nmoves1 : (q : List Q ) ( L : List Σ ) → List Q → List Q - Nmoves1 q [] _ = q - Nmoves1 [] (_ ∷ L) LQ = Nmoves1 LQ L [] - Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge M ( nδ M q H ) LQ ) +<a href="../agda/nfa.agda"> nfa.agda </a> - Naccept : { Q : Set } { Σ : Set } - → NAutomaton Q Σ - → List Σ → Bool - Naccept {Q} { Σ} M L = - checkAccept ( Nmoves M ((nstart M) ∷ [] ) L ) - where - checkAccept : (q : List Q ) → Bool - checkAccept [] = false - checkAccept ( H ∷ L ) with (nend M) H - ... | true = true - ... | false = checkAccept L - -とする。 - ---部分集合を使うと簡単になる - -<a href="../agda/nfa-list.agda"> nfa-list.agda </a> - - - record NAutomaton ( Q : Set ) ( Σ : Set ) - : Set where - field - Nδ : Q → Σ → Q → Bool - Nstart : Q → Bool - Nend : Q → Bool - +状態の受理と遷移は以下のようになる。 Nmoves : { Q : Set } { Σ : Set } → NAutomaton Q Σ @@ -76,16 +25,18 @@ Nmoves {Q} { Σ} M fin Qs s q = exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q ) )) - - Naccept : { Q : Set } { Σ : Set } + Naccept : { Q : Set } { Σ : Set } → NAutomaton Q Σ → {n : ℕ } → FiniteSet Q {n} - → List Σ → Bool - Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input - where - Naccept1 : NAutomaton Q Σ → ( Q → Bool ) → List Σ → Bool - Naccept1 M sb [] = exists fin ( λ q → sb q ∧ Nend M q ) - Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M fin sb i ) t + → (Nstart : Q → Bool) → List Σ → Bool + Naccept M fin sb [] = exists fin ( λ q → sb q ∧ Nend M q ) + Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t + +次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。 +しかし、List で定義すると少し複雑になる。 + +部分集合を使うと簡単になる。Q の部分集合は Q → Bool で true になるものであるとする。 + --例題 @@ -109,9 +60,21 @@ start1 _ = false am2 : NAutomaton States1 In2 - am2 = record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1} + am2 = record { Nδ = transition3 ; Nend = fin1} + + example2-1 = Naccept am2 finState1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) + example2-2 = Naccept am2 finState1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) - example2-1 = Naccept am2 finState1 ( i0 ∷ i1 ∷ i0 ∷ [] ) - example2-2 = Naccept am2 finState1 ( i1 ∷ i1 ∷ i1 ∷ [] ) + fin0 : States1 → Bool + fin0 st = false + fin0 ss = false + fin0 sr = false + test0 : Bool + test0 = exists finState1 fin0 + test1 : Bool + test1 = exists finState1 fin1 + + test2 = Nmoves am2 finState1 start1 +