Mercurial > hg > Members > kono > Proof > automaton
changeset 277:42563cc6afdf
non-regular
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 25 Dec 2021 19:16:59 +0900 |
| parents | a14999c44cf9 |
| children | e89957b99662 |
| files | automaton-in-agda/src/cfg.agda automaton-in-agda/src/cfg1.agda automaton-in-agda/src/non-regular.agda |
| diffstat | 3 files changed, 51 insertions(+), 68 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/src/cfg.agda Mon Dec 20 07:54:09 2021 +0900 +++ b/automaton-in-agda/src/cfg.agda Sat Dec 25 19:16:59 2021 +0900 @@ -11,8 +11,6 @@ open import Relation.Nullary using (¬_; Dec; yes; no) -- open import Data.String -left : {t : Set } → List - data IsTerm (Token : Set) : Set where isTerm : Token → IsTerm Token noTerm : IsTerm Token
--- a/automaton-in-agda/src/cfg1.agda Mon Dec 20 07:54:09 2021 +0900 +++ b/automaton-in-agda/src/cfg1.agda Sat Dec 25 19:16:59 2021 +0900 @@ -201,6 +201,7 @@ expr1 ( expr ∷ t ) fail next = next t expr1 ( term ∷ t ) fail next = next t expr1 x fail next = left x fail $ λ x → expr1 x fail $ λ x → right x fail $ next +-- expr1 x fail next = left x fail ( λ x → expr1 x fail ( λ x → right x fail ( next ))) cfgtest01 = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x → ⟪ true , x ⟫ ) cfgtest02 = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) (λ x → ⟪ false , x ⟫ ) (λ x → ⟪ true , x ⟫ )
--- a/automaton-in-agda/src/non-regular.agda Mon Dec 20 07:54:09 2021 +0900 +++ b/automaton-in-agda/src/non-regular.agda Sat Dec 25 19:16:59 2021 +0900 @@ -20,8 +20,8 @@ inputnn (i0 ∷ t) with inputnn t ... | nothing = nothing ... | just [] = nothing -... | just (i0 ∷ t1) = nothing -... | just (i1 ∷ t1) = just t1 +... | just (i0 ∷ t1) = nothing -- can't happen +... | just (i1 ∷ t1) = just t1 -- remove i1 from later part inputnn1 : List In2 → Bool inputnn1 s with inputnn s @@ -31,7 +31,7 @@ t1 = inputnn1 ( i0 ∷ i1 ∷ [] ) t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) -t3 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) +t3 = inputnn1 ( i0 ∷ i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) inputnn0 : ( n : ℕ ) → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ inputnn0 zero {_} _ _ s = s @@ -50,67 +50,51 @@ open _∧_ +data Trace { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) : (is : List Σ) → ( List Q) → Set where + tend : {q : Q} → aend fa q ≡ true → Trace fa [] (q ∷ []) + tnext : {q : Q} → {i : Σ} { is : List Σ} {qs : List Q} + → Trace fa is (δ fa q i ∷ qs) → Trace fa (i ∷ is) ( q ∷ δ fa q i ∷ qs ) + +tr-accept→ : { Q : Set } { Σ : Set } + → (fa : Automaton Q Σ ) + → (is : List Σ) → (q : Q) → (qs : List Q) → Trace fa is (q ∷ qs) → accept fa q is ≡ true +tr-accept→ {Q} {Σ} fa [] q [] (tend x) = x +tr-accept→ {Q} {Σ} fa (i ∷ is) q (x ∷ qs) (tnext tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) qs tr + +tr-accept← : { Q : Set } { Σ : Set } + → (fa : Automaton Q Σ ) + → (is : List Σ) → (q : Q) → accept fa q is ≡ true → Trace fa is (trace fa q is) +tr-accept← {Q} {Σ} fa [] q ac = tend ac +tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext (tend ac ) +tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext (tr-accept← fa (x1 ∷ is) (δ fa q x) ac) + +memberQ : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool +memberQ {Q} finq q [] = false +memberQ {Q} finq q (q0 ∷ qs) with equal? finq q q0 +... | true = true +... | false = memberQ finq q qs + +tr-append-is : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q ) + → memberQ finq q qs ≡ true + → Trace fa is (q ∷ qs) → List Σ ∧ List Q +tr-append-is {Q} {Σ} fa finq q [] [] () (tend x) +tr-append-is {Q} {Σ} fa finq q (x ∷ is) [] () tr +tr-append-is {Q} {Σ} fa finq q (x ∷ is) (q0 ∷ qs) mb tr with equal? finq q q0 +... | true = ⟪ x ∷ [] , q0 ∷ [] ⟫ +tr-append-is {Q} {Σ} fa finq q (x ∷ is) (.(δ fa q x) ∷ qs) mb (tnext tr) | false = tr3 (δ fa q x ∷ qs) tr2 is tr where + tr2 : memberQ finq q (δ fa q x ∷ qs) ≡ true + tr2 = {!!} + tr3 : (qs : List Q) → memberQ finq q qs ≡ true → (is : List Σ) → Trace fa is qs → List Σ ∧ List Q + tr3 (x ∷ []) mb [] (tend x₁) = {!!} + tr3 (q0 ∷ qs) mb (x₁ ∷ is) (tnext tr) with equal? finq q q0 + ... | true = ⟪ x ∷ [] , {!!} ⟫ + ... | false = ⟪ x ∷ proj1 (tr3 qs mb is tr) , {!!} ⟫ + +tr-append : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q ) + → (mb : memberQ finq q qs ≡ true ) + → (tr : Trace fa is ( q ∷ qs )) + → Trace fa (proj1 (tr-append-is fa finq q is qs mb tr) ++ is) (proj2 (tr-append-is fa finq q is qs mb tr) ++ (q ∷ qs)) +tr-append = {!!} + lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) -lemmaNN r Rg = lem1 {!!} (Rg {!!}) {!!} {!!} where - lem1 : (s : List In2) → isRegular inputnn1 s r → inputnn1 s ≡ false → accept (automaton r) (astart r) s ≡ true → ⊥ - lem1 s rg a b with inputnn1 s | accept (automaton r) (astart r) s - lem1 s () a b | false | true - lem1 s refl refl () | false | false - lemn : isRegular inputnn1 (inputnn0 (finite (afin r) ) i0 i1 [] ) r - lemn = Rg (inputnn0 (finite (afin r) ) i0 i1 [] ) - member : ( h : states r ) → ( x : List (states r) ) → Bool - member h [] = false - member h (x ∷ t) with equal? (afin r) h x - ... | true = true - ... | false = member h t - member-n : ( h : states r ) → ( x : List (states r) ) → ℕ → Maybe ℕ - member-n h [] _ = nothing - member-n h (x ∷ t) n with equal? (afin r) h x - ... | true = just n - ... | false = member-n h t (suc n) - data Trace : (List ( states r )) → Set where - init : Trace ( astart r ∷ [] ) - former : { x : List (states r) } → { h : states r} → Trace (h ∷ x ) → Trace ( δ (automaton r) h i0 ∷ h ∷ x ) - later : { x : List (states r) } → { h : states r} → Trace (h ∷ x ) → Trace ( δ (automaton r) h i1 ∷ h ∷ x ) - input-trace1 : List In2 → states r → List ( states r ) → List ( states r ) - input-trace1 [] q x = q ∷ x - input-trace1 (x ∷ x₁) q s = input-trace1 x₁ ( δ (automaton r) q x ) ( q ∷ s ) - input-trace : (s : List In2 ) → Trace ( input-trace1 s (astart r) [] ) - input-trace s = input-trace3 s (astart r) init where - input-trace3 : (s : List In2 ) → (q : states r) → { x : List (states r) } → Trace (q ∷ x ) → Trace ( input-trace1 s q x ) - input-trace3 [] q {x} dt = dt - input-trace3 (i0 ∷ s) q {x} dt = input-trace3 s ( δ (automaton r) q i0 ) ( former dt ) - input-trace3 (i1 ∷ s) q {x} dt = input-trace3 s ( δ (automaton r) q i1 ) ( later dt ) - trace-input : (x : List ( states r )) ( dt : Trace x) → List In2 - trace-input (x ∷ []) dt = [] - trace-input (.(δ (automaton r) _ i0) ∷ x) (former dt) = i0 ∷ trace-input x dt - trace-input (.(δ (automaton r) _ i1) ∷ x) (later dt) = i1 ∷ trace-input x dt - trace-accepted : {x : List ( states r )} {e : states r} → ( aend (automaton r) e ≡ true) → ( dt : Trace (e ∷ x) ) - → accept (automaton r) (astart r) (trace-input (e ∷ x) dt ) ≡ true - trace-accepted {x} {e} end dt = {!!} where - trace-accepted2 : (x : List ( states r )) → List ( states r ) ∧ states r - trace-accepted2 [] = ⟪ [] , astart r ⟫ - trace-accepted2 (x ∷ []) = ⟪ [] , astart r ⟫ - trace-accepted2 (x ∷ x₁ ∷ x₂) = ⟪ x ∷ proj1 (trace-accepted2 (x₁ ∷ x₂)) , proj2 (trace-accepted2 (x₁ ∷ x₂)) ⟫ - trace-accepted1 : (n : ℕ) → (x : List ( states r )) → ( n ≡ length x) → (q : states r) → ( dt : Trace (e ∷ x) ) - → accept (automaton r) q (trace-input (e ∷ x) dt ) ≡ true - trace-accepted1 n x eq q dt = {!!} - the-state : {x : List ( states r )} ( dt : Trace x) → length x > finite (afin r) → states r - the-state = {!!} - the-dtrace : {x : List ( states r )} ( dt : Trace x) → length x > finite (afin r) → List ( states r ) - the-dtrace = {!!} - the-loop : {x : List ( states r )} ( dt : Trace x) → (lt : length x > finite (afin r)) → - ( member ( the-state dt lt) ( the-dtrace dt lt) ≡ true ) ∧ Trace ( the-state dt lt ∷ the-dtrace dt lt ) - the-loop = {!!} - new-state-list : {x : List ( states r )} ( dt : Trace x) → length x > finite (afin r) → List ( states r ) - new-state-list = {!!} - new-trace : {x : List ( states r )} ( dt : Trace x) → (lt : length x > finite (afin r)) → Trace (new-state-list dt lt ) - new-trace dt lt = {!!} - new-input-list-is-accepted : {x : List ( states r )} ( dt : Trace x) → (lt : length x > finite (afin r)) - → accept (automaton r) {!!} ( trace-input (new-state-list dt lt) (new-trace dt lt) ) ≡ true - new-input-list-is-accepted = {!!} - new-input-list-is-not-nn : {x : List ( states r )} ( dt : Trace x) → (lt : length x > finite (afin r)) - → inputnn1 (trace-input (new-state-list dt lt) (new-trace dt lt) ) ≡ false - new-input-list-is-not-nn = {!!} - - +lemmaNN r Rg = {!!}