Mercurial > hg > Members > kono > Proof > automaton

changeset 39:3f099f353f1c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 21 Dec 2018 10:56:18 +0900
parents ab265470c2d0
children 6f747411fd6d
files agda/automaton.agda agda/cfg.agda agda/regex1.agda agda/turing.agda
diffstat 4 files changed, 79 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Wed Dec 12 17:50:42 2018 +0900
+++ b/agda/automaton.agda	Fri Dec 21 10:56:18 2018 +0900
@@ -82,8 +82,8 @@
 inputnn {zero} {_} _ _ s = s
 inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )
 
-lemmaNN :  Q : Set } { Σ : Set  } → (M : Automaton Q  Σ) →  ¬ accept M ( inputnn {n} x y [] )
-lemmaNN = ?
+-- lemmaNN :  { Q : Set } { Σ : Set  } → (M : Automaton Q  Σ) →  ¬ accept M ( inputnn {n} x y [] )
+-- lemmaNN = ?
 
 
 
--- a/agda/cfg.agda	Wed Dec 12 17:50:42 2018 +0900
+++ b/agda/cfg.agda	Fri Dec 21 10:56:18 2018 +0900
@@ -1,14 +1,68 @@
 module cfg where
 
 open import Level renaming ( suc to succ ; zero to Zero )
--- open import Data.Fin
+open import Data.Fin
 open import Data.Nat
 open import Data.Product
--- open import Data.List
+open import Data.List
 open import Data.Maybe
 open import Data.Bool using ( Bool ; true ; false )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.String
 
+open import nfa
 
+data Node ( Term NonTerm : Set )  : Set  where
+   term : Term → Node Term NonTerm
+   nonterm : NonTerm → Node Term NonTerm
+
+record CFGGrammer (Node : Set ) : Set where
+   field
+      cfg : Node → List ( Node )
+
+record DFGGrammer ( Node : Set )  : Set where
+   field
+      dfg : List Node → List Node 
+   
+data IFToken : Set where
+   t:EA : IFToken
+   t:EB : IFToken
+   t:EC : IFToken
+   t:IF : IFToken
+   t:THEN : IFToken
+   t:ELSE : IFToken
+   t:SA : IFToken
+   t:SB : IFToken
+   t:SC : IFToken
+
+tokenizer : {Σ : Set} → List Σ  →  IFToken  
+tokenizer = {!!}
+
+data IFNode (T : Set) : Set where
+   Token : T → IFNode T
+   Expr : (Fin 3) → IFNode T
+   Statement : (Fin 5) → IFNode T
+
+IFGrammer : CFGGrammer (IFNode IFToken)
+IFGrammer = record {
+      cfg = cfg
+   } where
+     cfg :  IFNode IFToken → List (IFNode IFToken)
+     cfg (Token t) =  (Token t)  ∷ [] 
+     cfg (Expr zero) =  Token t:EA  ∷ [] 
+     cfg (Expr (suc zero)) =  Token t:EB  ∷ [] 
+     cfg (Expr (suc (suc zero))) =  Token t:EC  ∷ [] 
+     cfg (Expr (suc (suc (suc ()))))
+     cfg (Statement zero) = ( Token t:SA   ∷ [])
+     cfg (Statement (suc (zero))) = ( Token t:SB   ∷ [])
+     cfg (Statement (suc (suc zero))) = ( Token t:SC   ∷ [])
+     cfg (Statement (suc (suc (suc zero)))) = ( Token t:IF ∷ Expr {!!}  ∷ Statement {!!}  ∷ [])
+     cfg (Statement (suc (suc (suc (suc zero))))) = ( Token t:IF ∷ Expr {!!} ∷ Statement {!!}  ∷ Token t:ELSE ∷ Statement {!!}  ∷ [])
+     cfg (Statement (suc (suc (suc (suc (suc ())))))) 
+
+
+cfg-language : {Σ : Set} → CFGGrammer {!!} → {n : ℕ } (fin : FiniteSet Σ {n}) →  List Σ → Bool
+cfg-language = {!!}
+
+
--- a/agda/regex1.agda	Wed Dec 12 17:50:42 2018 +0900
+++ b/agda/regex1.agda	Fri Dec 21 10:56:18 2018 +0900
@@ -36,19 +36,12 @@
 
 open import nfa
 
-_‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
-x ‖ y = λ s → x s ∨ y s
-
-
 split : {Σ : Set} → (List Σ → Bool)
       → ( List Σ → Bool) → 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
 
-_・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
-x ・ y = λ z → split x y z
-
 {-# TERMINATING #-}
 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
 repeat x [] = true
@@ -61,8 +54,8 @@
 
 regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) →  List Σ → Bool
 regular-language (x *) f = repeat ( regular-language x f )
-regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
-regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
+regular-language (x & y) f = split ( regular-language x f ) ( regular-language y f )
+regular-language (x || y) f = λ s → ( regular-language x f s )  ∨  ( regular-language y f s)
 regular-language < h > f [] = false
 regular-language < h > f (h1  ∷ [] ) with cmpi f h h1
 ... | yes _ = true
--- a/agda/turing.agda	Wed Dec 12 17:50:42 2018 +0900
+++ b/agda/turing.agda	Fri Dec 21 10:56:18 2018 +0900
@@ -29,6 +29,24 @@
 -- left         push SR , pop      
 -- right        pop     , push SL      
 
+{-# TERMINATING #-}
+move : {Q Σ : Set } → { tone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move } → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q  L  ( tnone  ∷ [] ) 
+move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q  ( tnone  ∷ [] )  R 
+move {Q} {Σ} {tnone} {tδ} q ( LH  ∷ LT ) ( RH ∷ RT ) with  tδ q LH  
+... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ LT ) , RT )
+... | nq , write x , right = ( nq , LT , ( x  ∷ RH  ∷ RT ) )
+... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  RH ∷ RT ) )
+... | nq , wnone , left    = ( nq , ( RH  ∷ LH  ∷ LT ) , RT  )
+... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
+... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
+{-# TERMINATING #-}
+move-loop : {Q Σ : Set } → {tend :  Q → Bool}   → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+move-loop {Q} {Σ} {tend}  q L R with tend q
+... | true = ( q , L , R )
+... | flase = move-loop {Q} {Σ} {tend} ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
+        where
+        next = move  q  L  R 
 
 record Turing ( Q : Set ) ( Σ : Set  ) 
        : Set  where
@@ -38,24 +56,6 @@
         tend : Q → Bool
         tnone :  Σ
     {-# TERMINATING #-}
-    move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-    move q L [] = move q  L  ( tnone  ∷ [] ) 
-    move q [] R = move q  ( tnone  ∷ [] )  R 
-    move q ( LH  ∷ LT ) ( RH ∷ RT ) with  tδ q LH  
-    ... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ LT ) , RT )
-    ... | nq , write x , right = ( nq , LT , ( x  ∷ RH  ∷ RT ) )
-    ... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  RH ∷ RT ) )
-    ... | nq , wnone , left    = ( nq , ( RH  ∷ LH  ∷ LT ) , RT  )
-    ... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
-    ... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
-    {-# TERMINATING #-}
-    move-loop : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
-    move-loop  q L R with tend q
-    ... | true = ( q , L , R )
-    ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
-      where
-        next = move  q  L  R 
-    {-# TERMINATING #-}
     move0 : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
     move0  q L R with tend q
     ... | true = ( q , L , R )
@@ -68,7 +68,6 @@
     ... | nq , wnone , left    = move0 nq ( RH  ∷ LH  ∷ LT ) RT  
     ... | nq , wnone , right   = move0 nq  LT ( LH  ∷ RH  ∷ RT ) 
     ... | nq , wnone , mnone   = move0 nq ( LH  ∷ LT ) (  RH ∷ RT )  
-    {-# TERMINATING #-}
     taccept : List  Σ → ( Q × List  Σ × List  Σ )
     taccept L = move0 tstart L []
 
@@ -116,7 +115,7 @@
         loop zero q L R = ( q , L , R )
         loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) )  ( proj₂  ( proj₂ t1 ) )
           where
-              t1 = Turing.move copyMachine q L R
+              t1 = move {CopyStates} {ℕ} {0} {Copyδ} q L R
 
 
 ---