Mercurial > hg > Members > kono > Proof > automaton

changeset 274:1c8ed1220489

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixes
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Dec 2021 16:27:46 +0900
parents 192263adfc02
children 7828beb7d849
files automaton-in-agda/src/cfg.agda automaton-in-agda/src/cfg1.agda automaton-in-agda/src/derive.agda automaton-in-agda/src/nfa.agda automaton-in-agda/src/non-regular.agda automaton-in-agda/src/regex1.agda automaton-in-agda/src/regular-concat.agda automaton-in-agda/src/regular-star.agda
diffstat 8 files changed, 247 insertions(+), 60 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/cfg.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/cfg.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -11,7 +11,7 @@
 open import Relation.Nullary using (¬_; Dec; yes; no)
 -- open import Data.String
 
-open import nfa
+-- open import nfa
 
 data IsTerm (Token : Set) : Set where
     isTerm :  Token → IsTerm Token
--- a/automaton-in-agda/src/cfg1.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/cfg1.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -182,3 +182,24 @@
 ecfgtest2 = cfg-language E1Grammer (  e[ ∷ e1 ∷ e] ∷ [] )
 ecfgtest3 = cfg-language E1Grammer (  e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] )
 
+open import Function
+
+left : {t : Set } → List E1Token → ( List E1Token → t ) → t
+left ( e[ ∷ t ) next = next t
+left t next = next t 
+
+right : {t : Set } → List E1Token → ( List E1Token → t ) → t
+right ( e] ∷ t ) next = next t
+right t next = next t 
+
+
+{-# TERMINATING #-}
+expr1 : {t : Set } → List E1Token → ( List E1Token → t ) → t
+expr1 ( e1 ∷ t ) next = next t
+expr1 ( expr ∷ t ) next = next t
+expr1 ( term  ∷ t ) next = next t
+expr1 x next = left x $ λ x → expr1 x $ λ x → right x $ next
+
+cfgtest01  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) (λ x → x )
+cfgtest02  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ [] ) (λ x → x )
+cfgtest03  = expr1 ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ e] ∷ [] ) (λ x → x )
--- a/automaton-in-agda/src/derive.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -17,6 +17,8 @@
 open import regex
 open FiniteSet
 
+-- whether a regex accepts empty input
+--
 empty? : Regex  Σ → Bool
 empty?  ε       = true
 empty?  φ       = false
@@ -160,3 +162,16 @@
    regex-derive0 [] t = t
    regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) 
 
+--
+-- if (Derivative r is finite,  regex→automaton is finite
+--
+drive-is-finite : (r : Regex   Σ) → FiniteSet (Derivative r) 
+drive-is-finite ε = {!!}
+drive-is-finite φ = {!!}
+drive-is-finite (r *) = {!!} where
+   d1 :  FiniteSet (Derivative r )
+   d1 = drive-is-finite r
+drive-is-finite (r & r₁) = {!!}
+drive-is-finite (r || r₁) = {!!}
+drive-is-finite < x > = {!!}
+
--- a/automaton-in-agda/src/nfa.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/nfa.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -50,9 +50,8 @@
 Nmoves : { Q : Set } { Σ : Set  }
     → NAutomaton Q  Σ
     → (exists : ( Q → Bool ) → Bool)
-    →  ( Qs : Q → Bool )  → (s : Σ ) → Q → Bool
-Nmoves {Q} { Σ} M exists  Qs  s q  =
-      exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
+    →  ( Qs : Q → Bool )  → (s : Σ ) → ( Q → Bool )
+Nmoves {Q} { Σ} M exists  Qs  s  = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q )  ))
 
 Naccept : { Q : Set } { Σ : Set  } 
     → NAutomaton Q  Σ
--- a/automaton-in-agda/src/non-regular.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -1,20 +1,116 @@
 module non-regular where
 
 open import Data.Nat
+open import Data.Empty
 open import Data.List
+open import Data.Maybe
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import logic
 open import automaton
+open import automaton-ex
 open import finiteSet
 open import Relation.Nullary 
+open import regular-language
 
-inputnn : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ ) → List  Σ → List  Σ 
-inputnn zero {_} _ _ s = s
-inputnn (suc n) x y s = x  ∷ ( inputnn n x y ( y  ∷ s ) )
+open FiniteSet
+
+inputnn :  List  In2 → Maybe (List In2)
+inputnn [] = just []
+inputnn  (i1 ∷ t) = just (i1 ∷ t)
+inputnn  (i0 ∷ t) with inputnn t
+... | nothing = nothing
+... | just [] = nothing
+... | just (i0 ∷ t1) = nothing
+... | just (i1 ∷ t1) = just t1
+
+inputnn1 :  List  In2 → Bool
+inputnn1  s with inputnn  s 
+... | nothing = false
+... | just [] = true
+... | just _ = false
+
+t1 = inputnn1 ( i0 ∷ i1 ∷ [] )
+t2 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
+t3 = inputnn1 ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] )
+
+inputnn0 : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ ) → List  Σ → List  Σ 
+inputnn0 zero {_} _ _ s = s
+inputnn0 (suc n) x y s = x  ∷ ( inputnn0 n x y ( y  ∷ s ) )
+
+t4 : inputnn1 ( inputnn0 5 i0 i1 [] ) ≡ true
+t4 = refl
+
+--
+--  if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
+--  The function is determinted by inputs,
+--
+
+open RegularLanguage
+open Automaton
+
+open _∧_
 
-lemmaNN :  { Q : Set } { Σ : Set  } →  ( x y : Σ ) → ¬ (x ≡ y)
-    → FiniteSet Q
-    → (M : Automaton Q  Σ) (q : Q)
-    → ¬ ( (n : ℕ) →   accept M q ( inputnn n x y [] ) ≡ true )
-lemmaNN = {!!}
+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 = {!!}
 
+
--- a/automaton-in-agda/src/regex1.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/regex1.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -5,11 +5,12 @@
 open import Data.Fin
 open import Data.Nat hiding ( _≟_ )
 open import Data.List hiding ( any ;  [_] )
-import Data.Bool using ( Bool ; true ; false ; _∧_ )
-open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+-- import Data.Bool using ( Bool ; true ; false ; _∧_ )
+-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import regex
+open import logic
 
 -- postulate a b c d : Set
 
@@ -19,6 +20,49 @@
    c : In
    d : In
 
+-- infixr 40 _&_ _||_
+
+r1' =    (< a > & < b >) & < c >                                         --- abc
+r1 =    < a > &  < b > & < c >                                            --- abc
+r0 : ¬ (r1' ≡ r1)
+r0 ()
+any = < a > || < b >  || < c > || < d >                                   --- a|b|c|d
+r2 =    ( any * ) & ( < a > & < b > & < c > )                            -- .*abc
+r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
+r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
+r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
+
+open import nfa
+
+--    former ++ later  ≡ x
+split : {Σ : Set} → ((former : List Σ) → Bool) → ((later :  List Σ) → Bool) → (x : 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
+
+-- tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] )
+-- tt1 P Q = ?
+
+{-# TERMINATING #-}
+repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
+repeat x [] = true
+repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
+
+-- Meaning of regular expression
+
+regular-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y))  →  List Σ → Bool
+regular-language φ cmp _ = false
+regular-language ε cmp [] = true
+regular-language ε cmp (_ ∷ _) = false
+regular-language (x *) cmp = repeat ( regular-language x cmp  )
+regular-language (x & y) cmp  = split ( λ z → regular-language x  cmp z ) (λ z →  regular-language y  cmp z )
+regular-language (x || y) cmp  = λ s → ( regular-language x  cmp s )  \/  ( regular-language y  cmp s)
+regular-language < h > cmp  [] = false
+regular-language < h > cmp  (h1  ∷ [] ) with cmp h h1
+... | yes _ = true
+... | no _  = false
+regular-language < h >  _ (_ ∷ _ ∷ _)  = false
+
 cmpi : (x y : In ) → Dec (x ≡ y)
 cmpi a a = yes refl
 cmpi b b =  yes refl
@@ -37,45 +81,6 @@
 cmpi d b = no (λ ()) 
 cmpi d c = no (λ ()) 
 
--- infixr 40 _&_ _||_
-
-r1' =    (< a > & < b >) & < c >                                         --- abc
-r1 =    < a > & < b > & < c >                                            --- abc
-any = < a > || < b >  || < c >                                           --- a|b|c
-r2 =    ( any * ) & ( < a > & < b > & < c > )                            -- .*abc
-r3 =    ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
-r4 =    ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
-r5 =    ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
-
-open import nfa
-
---    former ++ later  ≡ x
-split : {Σ : Set} → ((former : List Σ) → Bool) → ((later :  List Σ) → Bool) → (x : 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
-
--- tt1 : {Σ : Set} → ( P Q :  List In → Bool ) → split P Q ( a ∷ b ∷ c ∷ [] )
--- tt1 P Q = ?
-
-{-# TERMINATING #-}
-repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
-repeat x [] = true
-repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
-
-regular-language : {Σ : Set} → Regex Σ → ((x y : Σ ) → Dec (x ≡ y))  →  List Σ → Bool
-regular-language φ cmp _ = false
-regular-language ε cmp [] = true
-regular-language ε cmp (_ ∷ _) = false
-regular-language (x *) cmp = repeat ( regular-language x cmp  )
-regular-language (x & y) cmp  = split ( λ z → (regular-language x  cmp) z ) (λ z →  regular-language y  cmp z )
-regular-language (x || y) cmp  = λ s → ( regular-language x  cmp s )  ∨  ( regular-language y  cmp s)
-regular-language < h > cmp  [] = false
-regular-language < h > cmp  (h1  ∷ [] ) with cmp h h1
-... | yes _ = true
-... | no _  = false
-regular-language < h >  _ (_ ∷ _ ∷ _)  = false
-
 test-regex : regular-language r1' cmpi ( a ∷ [] ) ≡ false
 test-regex = refl
 
@@ -84,13 +89,24 @@
 
                                                                                                                     
 test-AB→split : {Σ : Set} → {A B : List In → Bool} → split A B ( a ∷ b ∷ a ∷ [] ) ≡ (
-       ( A [] ∧ B ( a ∷ b ∷ a ∷ [] ) ) ∨
-       ( A ( a ∷ [] ) ∧ B ( b ∷ a ∷ [] ) ) ∨
-       ( A ( a ∷ b ∷ [] ) ∧ B ( a ∷ [] ) ) ∨
-       ( A ( a ∷ b ∷ a ∷ [] ) ∧ B  []  )
+       ( A [] /\ B ( a ∷ b ∷ a ∷ [] ) ) \/
+       ( A ( a ∷ [] ) /\ B ( b ∷ a ∷ [] ) ) \/
+       ( A ( a ∷ b ∷ [] ) /\ B ( a ∷ [] ) ) \/
+       ( A ( a ∷ b ∷ a ∷ [] ) /\ B  []  )
    )
 test-AB→split {_} {A} {B} = refl
 
+list-eq : {Σ : Set} → (cmpi : (s t : Σ)  → Dec (s ≡ t ))  → (s t : List Σ ) → Bool
+list-eq cmpi [] [] = true
+list-eq cmpi [] (x ∷ t) = false
+list-eq cmpi (x ∷ s) [] = false
+list-eq cmpi (x ∷ s) (y ∷ t) with cmpi x y
+... | yes _ = list-eq cmpi s t
+... | no _ = false
+
+-- split-spec-01 :  {s t u : List In } → s ++ t ≡ u → split (list-eq cmpi s) (list-eq cmpi t)  u ≡ true
+-- split-spec-01 = {!!}
+
 -- from example 1.53 1
 
 ex53-1 : Set 
@@ -121,8 +137,42 @@
 -- proof-egex-even (c ∷ []) ()
 -- proof-egex-even (x ∷ x₁ ∷ s) y = proof-egex-even s {!!}
 
-open import derive In cmpi
+open import finiteSet
+
+iFin : FiniteSet In
+iFin = record {
+     finite = finite0
+   ; Q←F = Q←F0
+   ; F←Q = F←Q0
+   ; finiso→ = finiso→0
+   ; finiso← = finiso←0
+ } where
+     finite0 : ℕ
+     finite0 = 4
+     Q←F0 : Fin finite0 → In
+     Q←F0 zero = a
+     Q←F0 (suc zero) = b
+     Q←F0 (suc (suc zero)) = c
+     Q←F0 (suc (suc (suc zero))) = d
+     F←Q0 : In → Fin finite0
+     F←Q0 a = # 0
+     F←Q0 b = # 1
+     F←Q0 c = # 2
+     F←Q0 d = # 3
+     finiso→0 : (q : In) → Q←F0 ( F←Q0 q ) ≡ q
+     finiso→0 a = refl
+     finiso→0 b = refl
+     finiso→0 c =  refl
+     finiso→0 d =  refl
+     finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f
+     finiso←0 zero = refl
+     finiso←0 (suc zero) = refl
+     finiso←0 (suc (suc zero)) = refl
+     finiso←0 (suc (suc (suc zero))) = refl
+
+
+open import derive In iFin
 open import automaton
 
-ra-ex = trace (regex→automaton r2) (record { state = r2 ; is-derived = unit }) ( a ∷ b ∷ c ∷ [])
+ra-ex = trace (regex→automaton cmpi r2) (record { state = r2 ; is-derived = unit }) ( a ∷ b ∷ c ∷ [])
 
--- a/automaton-in-agda/src/regular-concat.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/regular-concat.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -56,6 +56,13 @@
        finf : FiniteSet (states A ∨ states B → Bool ) 
        finf = fin→ fin 
        
+-- 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← = {!!}
+
 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
     field
         sp0 : List Σ
--- a/automaton-in-agda/src/regular-star.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/regular-star.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -34,7 +34,6 @@
        δnfa q i q₁ with aend (automaton A) q
        ... | true = equal? (afin A) ( astart A) q₁ 
        ... | false = equal? (afin A) (δ (automaton A) q i) q₁
-       δnfa _ i _ = false
        nend : states A → Bool
        nend q = aend (automaton A) q