Mercurial > hg > Members > kono > Proof > automaton

changeset 17:08b589172493

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add pushdown and turing
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 26 Aug 2018 17:48:26 +0900
parents 911899e36b96
children 6ec8e933ab43
files agda/pushdown.agda agda/sbconst1.agda agda/turing.agda
diffstat 3 files changed, 102 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/pushdown.agda	Sun Aug 26 17:48:26 2018 +0900
@@ -0,0 +1,47 @@
+module pushdown where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+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 Level renaming ( suc to succ ; zero to Zero )
+open import Data.Product
+
+
+data PushDown   (  Γ : Set  ) : Set  where
+   pop    : PushDown  Γ
+   push   :  Γ → PushDown  Γ
+
+
+record PushDownAutomaton ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
+       : Set  where
+    field
+        pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
+        pstart : Q
+        pz0 :  Γ
+    pmoves :  Q → List  Σ → ( Q × List  Γ )
+    pmoves q L = move q L [ pz0 ]
+           where
+              move : Q → ( List  Σ ) → ( List  Γ ) → ( Q × List  Γ )
+              move q _ [] = ( q , [] )
+              move q [] S = ( q , S )
+              move q ( H  ∷ T ) ( SH ∷ ST ) with  pδ q H SH 
+              ... | (nq , pop )     = move nq T ST
+              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+    paccept : List  Σ → Bool
+    paccept L = move pstart L [ pz0 ]
+           where
+              move : (q : Q ) ( L : List  Σ ) ( L : List   Γ ) → Bool
+              move q [] [] = true
+              move q _ [] = false
+              move q [] (_ ∷ _ ) = false
+              move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
+              ... | (nq , pop )     = move nq T ST
+              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+
+
+
+
--- a/agda/sbconst1.agda	Fri Aug 24 17:55:22 2018 +0900
+++ b/agda/sbconst1.agda	Sun Aug 26 17:48:26 2018 +0900
@@ -16,26 +16,26 @@
 open Automaton
 open NAutomaton
 
-record FiniteSet ( Q : Set ) ( max1 : ℕ  )
+record FiniteSet ( Q : Set ) ( max : ℕ  )
         : Set  where
      field
-        not-zero : max1 > 0
+        not-zero : max > 0
         ←ℕ : ℕ → Q
         ←Q : Q → ℕ 
-        finite : (q : Q) → ←Q q < max1
+        finite : (q : Q) → ←Q q < max
         finiso→ :(q : Q) → ←ℕ ( ←Q q ) ≡ q
         finiso← :(n : ℕ) → ←Q ( ←ℕ n ) ≡ n
-     max : ℕ
-     max = max1
+     fmax : ℕ
+     fmax = max
 
 open FiniteSet
 
 exists : { Q : Set} {n  : ℕ } → FiniteSet Q n → ( Q → Bool ) → Bool
-exists {Q} {n} N f = exists1 (max N)
+exists {Q} {n} N f = exists1 (fmax N)
   where
      exists1 :  ℕ → Bool
      exists1 zero = false
-     exists1 (suc i) with f (←ℕ N (suc i) ) 
+     exists1 (suc i) with f (←ℕ N i ) 
      ... | true = true
      ... | false = exists1 i
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/turing.agda	Sun Aug 26 17:48:26 2018 +0900
@@ -0,0 +1,48 @@
+module turing where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+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 Level renaming ( suc to succ ; zero to Zero )
+open import Data.Product
+
+
+data PushDown   (  Σ : Set  ) : Set  where
+   pop    : PushDown  Σ
+   push   :  Σ → PushDown  Σ
+
+
+record Turing ( Q : Set ) ( Σ : Set  ) 
+       : Set  where
+    field
+        tδ : Q →  Σ → Q × ( PushDown  Σ ) × ( PushDown  Σ )
+        tstart : Q
+        tend : Q → Bool
+        tz0 :  Σ
+    tmoves :  Q → List  Σ → ( Q × List  Σ × List  Σ )
+    tmoves q L = move q L [ pz0 ]
+           where
+              move : Q → ( List  Σ ) → ( List  Σ ) → ( Q × List  Σ × List  Σ )
+              move q _ [] = ( q , [] )
+              move q [] S = ( q , S )
+              move q ( H  ∷ T ) ( SH ∷ ST ) with  pδ q H SH 
+              ... | (nq , pop )     = move nq T ST
+              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+    taccept : List  Σ → Bool
+    taccept L = move pstart L [ pz0 ]
+           where
+              move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → Bool
+              move q [] [] = true
+              move q _ [] = false
+              move q [] (_ ∷ _ ) = false
+              move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
+              ... | (nq , pop )     = move nq T ST
+              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+
+
+
+