Mercurial > hg > Members > kono > Proof > automaton

changeset 318:91781b7c65a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Jan 2022 07:27:52 +0900
parents 16e47a3c4eda
children cd91a9f313dd
files automaton-in-agda/src/automaton.agda automaton-in-agda/src/cfg.agda automaton-in-agda/src/cfg1.agda automaton-in-agda/src/finiteSet.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/pushdown.agda automaton-in-agda/src/turing.agda
diffstat 7 files changed, 134 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/automaton.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/automaton.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -15,16 +15,16 @@
 
 accept : { Q : Set } { Σ : Set  }
     → Automaton Q  Σ
-    → (astart : Q)
+    → Q
     → List  Σ → Bool
-accept {Q} { Σ} M q [] = aend M q
-accept {Q} { Σ} M q ( H  ∷ T ) = accept M ( (δ M) q H ) T
+accept M q [] = aend M q
+accept M q ( H  ∷ T ) = accept M ( δ M q H ) T
 
 moves : { Q : Set } { Σ : Set  }
     → Automaton Q  Σ
     → Q → List  Σ → Q
-moves {Q} { Σ} M q [] = q
-moves {Q} { Σ} M q ( H  ∷ T ) = moves M ( δ M q H)  T
+moves M q [] = q
+moves M q ( H  ∷ T ) = moves M ( δ M q H)  T
 
 trace : { Q : Set } { Σ : Set  }
     → Automaton Q  Σ
--- a/automaton-in-agda/src/cfg.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/cfg.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -11,7 +11,7 @@
 open import Relation.Nullary using (¬_; Dec; yes; no)
 -- open import Data.String
 
-data IsTerm (Token : Set) : Set where
+data IsTerm (Token : Set) : Set (succ Zero) where
     isTerm :  Token → IsTerm Token
     noTerm  : IsTerm Token
 
--- a/automaton-in-agda/src/cfg1.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/cfg1.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -257,5 +257,48 @@
       ; pnc-p = λ q st → PushDownAutomaton.paccept pnc q x st ; success = λ _ p → p ; failure = λ _ p → p }
       (λ x p → {!!} ) (λ x p → {!!} )
 
+----
+--
+--  CFG to PDA
+--
 
+cfg→pda-state :  {Symbol  : Set} → CFGGrammer Symbol → Set 
+cfg→pda-state cfg = {!!}
 
+cfg→pda-start :  {Symbol  : Set} → (cfg : CFGGrammer Symbol) → cfg→pda-state cfg
+cfg→pda-start cfg = {!!}
+
+cfg→pda :  {Symbol  : Set} → (cfg : CFGGrammer Symbol) → PDA (cfg→pda-state cfg) Symbol (cfg→pda-state cfg)
+cfg→pda cfg = {!!}
+
+cfg->pda : {Symbol  : Set} → (input : List Symbol)
+    → (cfg : CFGGrammer Symbol)
+    → PDA.paccept (cfg→pda cfg ) (cfg→pda-start cfg) input [] ≡  cfg-language cfg input
+cfg->pda = {!!}
+
+----
+--
+--  PDA to CFG 
+--
+open import pushdown
+
+pda→cfg :  {Symbol  : Set} { Q : Set} → (pda : PDA Q Symbol Q) → CFGGrammer Symbol
+pda→cfg pda = record {
+      cfg = {!!}
+    ; top = {!!}
+    ; eq? = {!!}
+    ; typeof = {!!}
+   } 
+
+pda->cfg : {Symbol  : Set} { Q : Set} → (start : Q) →  (input : List Symbol)
+    → (pda : PDA  Q Symbol Q)
+    → PDA.paccept pda start input [] ≡  cfg-language (pda→cfg pda) input
+pda->cfg = {!!}
+
+record CDGGrammer  (Symbol  : Set) : Set where
+   field
+      cdg : Seq Symbol  → Body Symbol 
+      top : Symbol
+      eq? : Symbol → Symbol → Bool
+      typeof : Symbol →  Node Symbol
+
--- a/automaton-in-agda/src/finiteSet.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/finiteSet.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -3,7 +3,7 @@
 
 open import Data.Nat hiding ( _≟_ )
 open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
--- open import Data.Fin.Properties
+-- open import Data.Fin.Properties  hiding ( ≤-refl )
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary.Definitions
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -44,6 +44,10 @@
         ≡⟨  finiso→   q1 ⟩
             q1
         ∎  where open ≡-Reasoning
+     eqP : (x y : Q) → Dec ( x ≡ y )
+     eqP x y with F←Q x ≟ F←Q y
+     ... | yes eq = yes (subst₂ (λ j k → j ≡ k ) (finiso→ x) (finiso→ y) (cong Q←F eq) )
+     ... | no n = no (λ eq → n (cong F←Q eq))
      End : (m : ℕ ) → (p : Q → Bool ) → Set
      End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i )  ≡ false 
      first-end :  ( p : Q → Bool ) → End finite p
--- a/automaton-in-agda/src/pushdown.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/pushdown.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -10,6 +10,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 -- open import Data.Product
 open import logic
+open import automaton
 
 
 data PushDown   (  Γ : Set  ) : Set  where
@@ -46,6 +47,23 @@
     ... | ⟪ nq , none ⟫    = paccept nq T (SH ∷ ST)
     ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns  ∷  SH ∷ ST )
 
+record PDA ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
+       : Set  where
+    field
+        automaton : Automaton Q Σ
+        pδ : Q →  PushDown  Γ 
+    open Automaton
+    paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
+    paccept q [] [] = aend automaton q 
+    paccept q (H  ∷ T) [] with pδ  (δ automaton q H) 
+    paccept q (H ∷ T) [] | pop     = paccept (δ automaton q H) T []
+    paccept q (H ∷ T) [] | none    = paccept (δ automaton q H) T []
+    paccept q (H ∷ T) [] | push x  = paccept (δ automaton q H) T (x  ∷ [] )
+    paccept q [] (_ ∷ _ ) = false
+    paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ (δ automaton q H) 
+    ... | pop      = paccept (δ automaton q H) T ST
+    ... | none     = paccept (δ automaton q H) T (SH ∷ ST)
+    ... | push ns  = paccept (δ automaton q H) T ( ns  ∷  SH ∷ ST )
 
 data  States0   : Set  where
    sr : States0
@@ -64,10 +82,32 @@
         pδ sr i0 _ = ⟪ sr , push sr ⟫
         pδ sr i1 _ = ⟪ sr , pop  ⟫ 
 
+data  States2   : Set  where
+   ph1 : States2
+   ph2 : States2
+   phf : States2
+
+pnnp : PDA States2 In2 States2
+pnnp = record {
+         automaton = record { aend = aend ; δ = δ }
+       ; pδ  = pδ
+   } where
+        δ : States2 → In2 → States2
+        δ ph1 i0 = ph1
+        δ ph1 i1 = ph2
+        δ ph2 i1 = ph2
+        δ _ _ = phf
+        aend : States2 → Bool
+        aend ph2 = true
+        aend _ = false
+        pδ  : States2 → PushDown States2
+        pδ ph1 = push ph1 
+        pδ ph2 = pop   
+        pδ phf = none   
+
 data  States1   : Set  where
    ss : States1
    st : States1
-
 pn1 : PushDownAutomaton States1 In2 States1
 pn1 = record {
          pδ  = pδ
--- a/automaton-in-agda/src/turing.agda	Mon Jan 03 18:50:01 2022 +0900
+++ b/automaton-in-agda/src/turing.agda	Thu Jan 06 07:27:52 2022 +0900
@@ -5,11 +5,12 @@
 open import Data.Nat -- hiding ( erase )
 open import Data.List
 open import Data.Maybe hiding ( map )
-open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate )
+-- open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Product hiding ( map )
+open import logic 
 
 
 data Write   (  Σ : Set  ) : Set  where
@@ -75,6 +76,33 @@
     taccept : List  Σ → ( Q × List  Σ × List  Σ )
     taccept L = move0 tend tnone tδ tstart L []
 
+open import automaton
+open Automaton
+
+{-# TERMINATING #-}
+move1 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (δ : Q →  Σ → Q ) (tδ : Q → Σ →  Write  Σ  ×  Move)
+   (q : Q ) ( L : List  Σ ) ( R : List   Σ ) →  Q × List  Σ × List  Σ 
+move1 tend tnone δ tδ  q L R with tend q
+... | true = ( q , L , R )
+move1 tend tnone δ tδ  q L [] | false = move1 tend tnone δ tδ  q  L  ( tnone  ∷ [] ) 
+move1 tend tnone δ tδ  q [] R | false = move1 tend tnone δ tδ  q  ( tnone  ∷ [] )  R 
+move1 tend tnone δ tδ  q ( LH  ∷ LT ) ( RH ∷ RT ) | false with tδ (δ q LH) LH
+... |  write x , left  = move1 tend tnone δ tδ  (δ q LH) ( RH ∷ x  ∷ LT ) RT 
+... |  write x , right = move1 tend tnone δ tδ  (δ q LH) LT ( x  ∷ RH  ∷ RT ) 
+... |  write x , mnone = move1 tend tnone δ tδ  (δ q LH) ( x  ∷ LT ) (  RH ∷ RT ) 
+... |  wnone , left    = move1 tend tnone δ tδ  (δ q LH) ( RH  ∷ LH  ∷ LT ) RT  
+... |  wnone , right   = move1 tend tnone δ tδ  (δ q LH)  LT ( LH  ∷ RH  ∷ RT ) 
+... |  wnone , mnone   = move1 tend tnone δ tδ  (δ q LH) ( LH  ∷ LT ) (  RH ∷ RT )  
+
+record TM ( Q : Set ) ( Σ : Set  ) 
+       : Set  where
+    field
+        automaton : Automaton  Q Σ
+        tδ : Q → Σ → Write  Σ  ×  Move 
+        tnone :  Σ
+    taccept : Q → List  Σ → ( Q × List  Σ × List  Σ )
+    taccept q L = move1 (aend automaton) tnone (δ automaton) tδ q L []
+
 data CopyStates : Set where
    s1 : CopyStates
    s2 : CopyStates
@@ -109,6 +137,16 @@
       tend H = true
       tend _ = false
 
+copyTM : TM CopyStates ℕ
+copyTM = record {
+        automaton = record { δ = λ q i → proj₁ (Copyδ q i) ; aend = tend }
+     ;  tδ = λ q i → proj₂ (Copyδ q i )
+     ;  tnone =  0
+  } where
+      tend : CopyStates →  Bool
+      tend H = true
+      tend _ = false
+
 test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
 test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )