Mercurial > hg > Members > kono > Proof > automaton1

changeset 18:e168140d15b0

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 Sun, 22 Nov 2020 19:18:15 +0900
parents 5f97e5606e7e
children b16f7e6fd52b
files automaton.agda halt.agda logic.agda regex.agda regular-language.agda turing.agda
diffstat 6 files changed, 332 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/automaton.agda	Mon Nov 16 18:51:57 2020 +0900
+++ b/automaton.agda	Sun Nov 22 19:18:15 2020 +0900
@@ -19,10 +19,30 @@
 accept {n} {Q} {Σ} atm q (x ∷ input) = 
     accept atm (δ atm q x ) input
 
+-- data Dec' {n : Level} (P : Set n) : Set n where -- Law of Exclude Middle / LEM
+--   yes' : (p :   P ) → Dec' P
+--   no'  : (p : ¬ P ) → Dec' P
+
+record Automaton-Language {n : Level} (Q : Set n) (Σ : Set ) : Set ((Level.suc n) ) where
+  field
+     ATM : Automaton Q Σ
+  field
+     startq : Q
+     decF : (q : Q) → Dec (F ATM q )
+     accept-by : (x : List Σ ) → (q : Q) → Dec ( accept ATM q x)
+     -- Accept : (x : List Σ ) → accept-by x startq where
+  -- accept-by : (x : List Σ ) → (q : Q) → Dec ( accept ATM q x)
+  -- accept-by [] q = decF q
+  -- accept-by (x ∷ t) q = accept-by t (δ ATM q x)
+
 trace : {n  : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
 trace {n} {Q} {Σ} A q [] a = q ∷ []
 trace {n} {Q} {Σ} A q (x ∷ t) a = q ∷ ( trace A (δ A q x) t a )
 
+trace' : {n  : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → List Q
+trace' {n} {Q} {Σ} A q [] = q ∷ []
+trace' {n} {Q} {Σ} A q (x ∷ t) = q ∷ ( trace' A (δ A q x) t )
+
 data Q3 : Set where
   q₁ : Q3
   q₂ : Q3
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/halt.agda	Sun Nov 22 19:18:15 2020 +0900
@@ -0,0 +1,101 @@
+module halt where
+
+open import Level renaming ( zero to Zero ; suc to Suc )
+open import Data.Nat
+open import Data.List hiding ([_])
+open import Data.Nat.Properties
+open import Relation.Nullary
+open import Data.Empty
+open import  Relation.Binary.Core
+open import  Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+
+open import logic
+
+record Bijection {n : Level} (R : Set n)  : Set (Suc n) where
+   field
+       fun←  :  ℕ → R
+       fun→  :  R → ℕ
+       fiso← : (x : R) → fun← ( fun→ x )  ≡ x 
+       fiso→ : (x : ℕ ) →  fun→ ( fun← x )  ≡ x 
+
+open Bijection
+
+add1BL : List Bool → List Bool ∧ Bool
+add1BL [] =  [ [] , true ]
+add1BL (false ∷ x) with add1BL x 
+... | [ x1 , true  ] = [ true  ∷ x1 , false ]
+... | [ x1 , false ] = [ false ∷ x1 , false ]
+add1BL (true ∷ x)   with add1BL x 
+... | [ x1 , true  ] = [ false ∷ x1 , true  ]
+... | [ x1 , false ] = [ true  ∷ x1 , false ]
+
+open _∧_
+--               10              11                    100                 101
+-- 0 = [], 1 = false ∷ [], 2 = true ∷ [], 3 = false ∷ false ∷ [], 4 = false ∷ true ∷ [] ...
+toBL : ℕ → List Bool
+toBL 0 = []
+toBL (suc n) with add1BL (toBL n)
+... | [ x , true ] = false ∷ x 
+... | [ x , false ] = x
+
+
+sub1BL : List Bool → List Bool ∧ Bool
+sub1BL [] = [ [] , false ]
+sub1BL (false ∷ x) with sub1BL x 
+... | [ x1 , true  ] = [ true  ∷ x1 , false ]
+... | [ x1 , false ] = [ false ∷ x1 , false ]
+sub1BL (true ∷ x)   with sub1BL x 
+... | [ x1 , true  ] = [ false ∷ x1 , true  ]
+... | [ x1 , false ] = [ true  ∷ x1 , false ]
+
+
+fromBL1 : List Bool →  ℕ ∧ ℕ
+fromBL1 [] = [ 0 , 1 ]
+fromBL1 (true ∷ t)  = [ proj1 (fromBL1 t) + proj2 (fromBL1 t) , proj2 (fromBL1 t) + proj2 (fromBL1 t) ]
+fromBL1 (false ∷ t) = [ proj1 (fromBL1 t) , proj2 (fromBL1 t) + proj2 (fromBL1 t) ]
+
+minus1 : ℕ → ℕ
+minus1 zero = zero
+minus1 (suc x) = x
+
+fromBL : List Bool → ℕ
+fromBL [] = 0
+fromBL (false ∷ x) = minus1 ( proj1 (fromBL1 (true ∷ false ∷ x )) )
+fromBL (true ∷  x) = minus1 ( proj1 (fromBL1 (true ∷ true ∷ x )))
+
+test0 = toBL 0 ∷ toBL 1 ∷ toBL 2 ∷ toBL 3 ∷ toBL 4 ∷ toBL 5 ∷ []
+test1 = fromBL (  toBL 0 ) ∷ fromBL ( toBL 1) ∷ fromBL ( toBL 2) ∷ fromBL ( toBL 3) ∷ fromBL ( toBL 4) ∷ fromBL (toBL 5) ∷ []
+
+L-Bijection : Bijection (List Bool) 
+L-Bijection = record {
+       fun←  = toBL
+    ;  fun→  = fromBL
+    ;  fiso← = LB1
+    ;  fiso→ = LB2 } where
+    addBLeq : (x : List Bool) → suc (fromBL x) ≡ fromBL (proj1 (add1BL x))
+    addBLeq = {!!}
+    addB2Leq : (n : ℕ) → proj1 (add1BL (toBL n)) ≡ toBL (suc n)
+    addB2Leq = {!!}
+    LB1 : (x : List Bool) → toBL (fromBL x) ≡ x
+    LB1 [] = refl
+    LB1 (true ∷ t)  = {!!}
+    LB1 (false ∷ t) = {!!}
+    LB2 : (x : ℕ) → fromBL (toBL x) ≡ x
+    LB2 = {!!}
+
+
+import Axiom.Extensionality.Propositional
+postulate 
+   f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
+
+diagonal : Bijection (ℕ → Bool) → ℕ → Bool
+diagonal bi n = not (fun← bi n n)
+
+neq : {s t : Bool} → s ≡ t → ¬ (s ≡ not t )
+neq {true} {true} refl ()
+neq {false} {false} refl ()
+
+diagonal-lemma : ¬ ( Bijection  (ℕ → Bool) )
+diagonal-lemma bi = {!!}
+
--- a/logic.agda	Mon Nov 16 18:51:57 2020 +0900
+++ b/logic.agda	Sun Nov 22 19:18:15 2020 +0900
@@ -29,6 +29,9 @@
 id : {n : Level} {A : Set n} → A → A
 id x = x
 
+-- lemma : {n  : Level } → { A : Set n } → A ⇔ A
+-- lemma {n} {A} = [ id , id ]
+
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
 
--- a/regex.agda	Mon Nov 16 18:51:57 2020 +0900
+++ b/regex.agda	Sun Nov 22 19:18:15 2020 +0900
@@ -53,6 +53,79 @@
 test-regex1 = concat (atom a) (concat (atom b) (atom c)) 
 
 open import regular-language
+open import Data.Empty 
+open import  Relation.Nullary
+
+regex-language : {Σ : Set} → (r : Regex Σ) →  ((i j : Σ) → Dec ( i ≡ j)) →  (t : List Σ ) → Set
+regex-language φ dec  _ = ⊥
+regex-language ε dec [] = ⊤
+regex-language ε dec (_ ∷ _) = ⊥
+regex-language (x *) dec f = Star ( regex-language x dec )  f
+regex-language (x & y) dec f = split ( regex-language x dec ) ( regex-language y dec ) f
+regex-language (x || y) dec f = ( regex-language x dec f )  ∨  ( regex-language y dec f )
+regex-language < h > dec [] = ⊥
+regex-language < h > dec (h1  ∷ [] ) with dec h h1
+... | yes _ = ⊤
+... | no _  = ⊥
+regex-language < h > f _  = ⊥
+
+char-dec : (i j : char) → Dec (i ≡ j)
+char-dec a a = yes refl
+char-dec b b = yes refl
+char-dec c c = yes refl
+char-dec d d = yes refl
+char-dec a b = no (λ ())
+char-dec a c = no (λ ())
+char-dec a d = no (λ ())
+char-dec b a = no (λ ())
+char-dec b c = no (λ ())
+char-dec b d = no (λ ())
+char-dec c a = no (λ ())
+char-dec c b = no (λ ())
+char-dec c d = no (λ ())
+char-dec d a = no (λ ())
+char-dec d b = no (λ ())
+char-dec d c = no (λ ())
+
+char-list : List char
+char-list = a ∷ b ∷ c ∷ d ∷ []
+
+test-regex2 : ¬ (regex-language r1 char-dec ( a ∷ [] ) )
+test-regex2 (case1 ())
+test-regex2 (case2 ())
+
+test-regex3 : regex-language r1 char-dec  ( a ∷ b ∷ c ∷ [] ) 
+test-regex3 = case2 (case1 [ tt , case2 (case1 [ tt , tt ]) ] )
+
+splitb : {Σ : Set} → (List Σ → Bool)
+      → ( List Σ → Bool) → List Σ → Bool
+splitb x y  [] = x [] /\ y []
+splitb x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
+  splitb (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
+
+{-# TERMINATING #-}
+repeatb : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
+repeatb x [] = true
+repeatb {Σ} x ( h  ∷ t ) = splitb x (repeatb {Σ} x) ( h  ∷ t )
+
+regular-language : {Σ : Set} → Regex Σ → ((i j : Σ) → Dec ( i ≡ j)) →  List Σ → Bool
+regular-language ε dec _ = false
+regular-language φ dec [] = true
+regular-language φ dec (_ ∷ _ ) = false
+regular-language (x *) dec = repeatb ( regular-language x dec )
+regular-language (x & y) dec = splitb ( regular-language x dec ) ( regular-language y dec )
+regular-language (x || y) dec = λ s → ( regular-language x dec s )  \/ ( regular-language y dec s)
+regular-language < h > dec [] = false
+regular-language < h > dec (h1  ∷ [] ) with dec h h1
+... | yes _ = true
+... | no _  = false
+regular-language < h > dec _ = false
+
+test-regex4 : Bool
+test-regex4 = regular-language  r1 char-dec ( a ∷ [] ) 
+
+test-regex5 : Bool
+test-regex5 = regular-language  r1 char-dec  ( a ∷ b ∷ c ∷ [] )
 
 -- open import Data.Nat.DivMod
 
@@ -118,27 +191,6 @@
       F finish = ⊤
       F _ = ⊥
 
-char-dec : (i j : char) → Dec (i ≡ j)
-char-dec a a = yes refl
-char-dec b b = yes refl
-char-dec c c = yes refl
-char-dec d d = yes refl
-char-dec a b = no (λ ())
-char-dec a c = no (λ ())
-char-dec a d = no (λ ())
-char-dec b a = no (λ ())
-char-dec b c = no (λ ())
-char-dec b d = no (λ ())
-char-dec c a = no (λ ())
-char-dec c b = no (λ ())
-char-dec c d = no (λ ())
-char-dec d a = no (λ ())
-char-dec d b = no (λ ())
-char-dec d c = no (λ ())
-
-char-list : List char
-char-list = a ∷ b ∷ c ∷ d ∷ []
-
 open Automaton 
 
 a2 : accept (regex→automaton r2 char-dec ) (continue r2) ( a ∷ a ∷ b ∷ c ∷ [] )
--- a/regular-language.agda	Mon Nov 16 18:51:57 2020 +0900
+++ b/regular-language.agda	Sun Nov 22 19:18:15 2020 +0900
@@ -17,7 +17,7 @@
 open import automaton
 -- open import finiteSet
 
-language :  { Σ : Set } → Set (Suc Zero)
+language :  { Σ : Set } → Set₁ -- Set (Suc Zero)
 language {Σ} = List Σ → Set
 
 open Automaton
@@ -37,7 +37,7 @@
   split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t
 
 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
-Union {Σ} A B x = (A x ) ∨ (B x)
+Union {Σ} A B x = A x ∨ B x
 
 Concat : {n : Level}  {Σ : Set } → ( A B : language {Σ} ) → language {Σ}
 Concat {Σ} A B = split A B
@@ -87,6 +87,6 @@
    lemma4 [] qa qb = [ id , id ]
    lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
 
--- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!}
+-- closed-in-concat :  {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular {n} (Concat {n} (contain A (astart A)) (contain B (astart B))) x {!!}
 -- closed-in-concat = {!!}
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/turing.agda	Sun Nov 22 19:18:15 2020 +0900
@@ -0,0 +1,132 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module turing where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat -- hiding ( erase )
+open import Data.List
+open import Data.Maybe
+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
+
+
+data Write   (  Σ : Set  ) : Set  where
+   write   : Σ → Write  Σ
+   wnone   : Write  Σ
+   --   erase write tnone
+
+data Move : Set  where
+   left   : Move  
+   right  : Move  
+   mnone  : Move  
+
+-- at tδ both stack is poped
+
+-- write S      push S  , push SR
+-- erase        push SL , push tone 
+-- none         push SL , push SR 
+-- left         push SR , pop      
+-- right        pop     , push SL      
+
+{-# TERMINATING #-}
+move : {Q Σ : Set } → { tnone : Σ} → {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}  → { tnone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move }
+    → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+move-loop {Q} {Σ} {tend} {tnone} {tδ}  q L R with tend q
+... | true = ( q , L , R )
+... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
+        where
+        next = move {Q} {Σ} {tnone} {tδ} q  L  R 
+
+{-# TERMINATING #-}
+move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move)
+   (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+move0 tend tnone tδ  q L R with tend q
+... | true = ( q , L , R )
+move0 tend tnone tδ  q L [] | false = move0 tend tnone tδ  q  L  ( tnone  ∷ [] ) 
+move0 tend tnone tδ  q [] R | false = move0 tend tnone tδ  q  ( tnone  ∷ [] )  R 
+move0 tend tnone tδ  q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH  
+... | nq , write x , left  = move0 tend tnone tδ  nq ( RH ∷ x  ∷ LT ) RT 
+... | nq , write x , right = move0 tend tnone tδ  nq LT ( x  ∷ RH  ∷ RT ) 
+... | nq , write x , mnone = move0 tend tnone tδ  nq ( x  ∷ LT ) (  RH ∷ RT ) 
+... | nq , wnone , left    = move0 tend tnone tδ  nq ( RH  ∷ LH  ∷ LT ) RT  
+... | nq , wnone , right   = move0 tend tnone tδ  nq  LT ( LH  ∷ RH  ∷ RT ) 
+... | nq , wnone , mnone   = move0 tend tnone tδ  nq ( LH  ∷ LT ) (  RH ∷ RT )  
+
+record Turing ( Q : Set ) ( Σ : Set  ) 
+       : Set  where
+    field
+        tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move 
+        tstart : Q
+        tend : Q → Bool
+        tnone :  Σ
+    taccept : List  Σ → ( Q × List  Σ × List  Σ )
+    taccept L = move0 tend tnone tδ tstart L []
+
+data CopyStates : Set where
+   s1 : CopyStates
+   s2 : CopyStates
+   s3 : CopyStates
+   s4 : CopyStates
+   s5 : CopyStates
+   H  : CopyStates
+
+
+Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move 
+Copyδ s1 0  = H    , wnone       , mnone 
+Copyδ s1 1  = s2   , write 0 , right 
+Copyδ s2 0  = s3   , write 0 , right 
+Copyδ s2 1  = s2   , write 1 , right 
+Copyδ s3 0  = s4   , write 1 , left 
+Copyδ s3 1  = s3   , write 1 , right 
+Copyδ s4 0  = s5   , write 0 , left 
+Copyδ s4 1  = s4   , write 1 , left 
+Copyδ s5 0  = s1   , write 1 , right 
+Copyδ s5 1  = s5   , write 1 , left 
+Copyδ H  _  = H    , wnone   , mnone 
+Copyδ _  (suc (suc _))      = H    , wnone       , mnone 
+
+copyMachine : Turing CopyStates ℕ
+copyMachine = record {
+        tδ = Copyδ
+     ;  tstart = s1
+     ;  tend = tend
+     ;  tnone =  0
+  } where
+      tend : CopyStates →  Bool
+      tend H = true
+      tend _ = false
+
+test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
+test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )
+
+test2 : ℕ  → CopyStates × ( List  ℕ ) × ( List  ℕ )
+test2 n  = loop n (Turing.tstart copyMachine) ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  ) []
+  where
+        loop :  ℕ → CopyStates → ( List  ℕ ) → ( List  ℕ ) → CopyStates × ( List  ℕ ) × ( List  ℕ )
+        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 = move {CopyStates} {ℕ} {0} {Copyδ} q L R
+
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function.Bijection 
+
+-- turing-stepiwize-eq : {Q1 Q2 : Set} → {S1 S2 : Set} → (t1 : Turing Q1 S1) → (t2 : Turing Q2 S2) → Bijection S1 (List S2) → 
+-- turing-stepiwize-eq = {!!}
+
+-- turing→01 : Turing  {!!} {!!} → Turing {!!} Bool
+-- turing→01 = {!!}
+