Mercurial > hg > Members > kono > Proof > automaton

changeset 164:bee86ee07fff

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 Fri, 12 Mar 2021 21:45:53 +0900
parents 26407ce19d66
children 6cb442050825
files a10/lecture.ind a13/lecture.ind agda/gcd.agda agda/halt.agda agda/omega-automaton.agda agda/root2.agda agda/turing.agda
diffstat 7 files changed, 215 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
--- a/a10/lecture.ind	Wed Jan 13 10:52:01 2021 +0900
+++ b/a10/lecture.ind	Fri Mar 12 21:45:53 2021 +0900
@@ -6,13 +6,20 @@
 
 計算を Turing machine で行ない、その Turing machine が計算終了までに費すステップと使用したテープの長さを使う。
 
-計算量は、n の式で表す。係数は問わない。
+nの式で表す。係数は問わない。
+
+--table: いろんな計算量
+
 
-　　o(n)             入力に比例した計算時間
-　　o(n^2)           入力の長さの二乗の計算時間
-　　o(n * log n)         
-　　o(exp n)         入力の長さの指数的な計算時間
-　　o(exp (exp n))   入力の長さの指数的な計算時間
+　　	o(n)             	入力に比例した計算時間
+　　	o(n^2)           	入力の長さの二乗の計算時間
+　　	o(n * log n)         
+　　	o(exp n)         	入力の長さの指数的な計算時間
+　　	o(exp (exp n))   	入力の長さの指数的な計算時間
+
+
+--table-end:
+
 
 Turing machine ではなく、もっと高級なモデル(例えばメモリを持つもの)を考えても、計算量は同じ。
 
--- a/a13/lecture.ind	Wed Jan 13 10:52:01 2021 +0900
+++ b/a13/lecture.ind	Fri Mar 12 21:45:53 2021 +0900
@@ -4,6 +4,46 @@
 
 --SAT
 
+Boolean Formula の satisfiabity を調べるツール
+
+時間は入ってない
+
+<a href="https://github.com/msoos/cryptominisat"> cryptominisat </a>
+
+--Spin
+
+<a href="https://github.com/nimble-code/Spin"> Spin </a>
+
+Promela という言語で仕様を記述するモデル検査
+
+比較的大きな仕様まで検証できる
+
+--JavaPathfinder
+
+Javaのモデル検査器。Thread を見てくれる。
+
+--CPAcheker
+
+Cで書いたプログラムを検証してくれる
+
+<a href="https://cpachecker.sosy-lab.org/doc.php"> CPachecker</a>
+
+--mCRL2
+
+独自言語
+
+<a href="https://www.mcrl2.org/web/user_manual/index.html"> mCRL2 </a>
+
+--PRISM
+
+確率付きオートマトン
+
+<a href="http://www.prismmodelchecker.org/people.php"> PRISM </a>
+
+--TLA+
+
+<a href="http://lamport.azurewebsites.net/tla/toolbox.html"> TLA+ </a>
+
 --nuXmv
 
 <a href="https://nuxmv.fbk.eu">nuXmv  </a> <br>
--- a/agda/gcd.agda	Wed Jan 13 10:52:01 2021 +0900
+++ b/agda/gcd.agda	Fri Mar 12 21:45:53 2021 +0900
@@ -27,6 +27,49 @@
 gcd : ( i j : ℕ ) → ℕ
 gcd i j = gcd1 i i j j 
 
+record Factor (n m : ℕ ) : Set where
+   field 
+      -- n<m : n ≤ m
+      factor : ℕ
+      remain : ℕ
+      is-factor : factor * n + remain ≡ m
+
+open Factor
+
+open ≡-Reasoning
+
+decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
+decf {n} {k} x with remain x
+... | zero = record { factor = factor x ; remain = k ; is-factor = {!!} }
+... | suc r = record { factor = factor x ; remain = r ; is-factor = {!!} }
+
+ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
+ifk0 i0 k i0f i0=0 = begin
+   factor i0f * k + 0  ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0)  ⟩
+   factor i0f * k + remain i0f  ≡⟨ is-factor i0f ⟩
+   i0 ∎ 
+
+ifzero : {k : ℕ } → (jf :  Factor k zero ) →  remain jf ≡ 0
+ifzero = {!!}
+
+gcd-gt : ( i i0 j j0 k : ℕ ) → (if : Factor k i) (i0f : Factor k i0 ) (jf : Factor k i ) (j0f : Factor k j0)
+   → remain i0f ≡ 0 → remain j0f ≡  0
+   → (remain if + i ) ≡ i0  → (remain jf + j ) ≡ j0
+   → Factor k ( gcd1 i i0 j j0 ) 
+gcd-gt zero i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 with <-cmp i0 j0
+... | tri< a ¬b ¬c = record { factor = factor i0f ; remain = 0 ; is-factor = ifk0 i0 k i0f i0=0 } 
+... | tri≈ ¬a refl ¬c = record { factor = factor i0f ; remain = 0 ; is-factor = ifk0 i0 k i0f i0=0 } 
+... | tri> ¬a ¬b c = record { factor = factor j0f ; remain = 0 ; is-factor = ifk0 j0 k j0f j0=0 } 
+gcd-gt zero i0 (suc zero) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
+gcd-gt zero zero (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = record { factor = factor j0f ; remain = 0 ; is-factor = ifk0 j0 k j0f j0=0 } 
+gcd-gt zero (suc i0) (suc (suc j)) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 =  
+    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k (decf i0f)  i0f (decf i0f)
+       record { factor = factor jf ; remain = remain jf ; is-factor = {!!} } i0=0 {!!} {!!} {!!}  
+gcd-gt (suc zero) i0 zero j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- can't happen
+gcd-gt (suc (suc i)) i0 zero zero k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!}
+gcd-gt (suc (suc i)) i0 zero (suc j0) k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!}
+gcd-gt (suc i) i0 (suc j) j0 k if i0f jf j0f i0=0 j0=0 ir=i0 jr=j0 = {!!} -- gcd-gt i i0 j j0 k (decf if) i0f (decf jf) j0f ? ? ? ?
+
 -- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
 -- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n
 
--- a/agda/halt.agda	Wed Jan 13 10:52:01 2021 +0900
+++ b/agda/halt.agda	Fri Mar 12 21:45:53 2021 +0900
@@ -21,25 +21,76 @@
        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
        fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x 
 
+injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
+injection R S f = (x y : R) → f x ≡ f y → x ≡ y
+
 open Bijection 
 
+b→injection0 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection R S (fun→ b)
+b→injection0 R S b x y eq = begin
+          x
+        ≡⟨ sym ( fiso← b x ) ⟩
+          fun← b ( fun→ b x )
+        ≡⟨ cong (λ k → fun← b k ) eq ⟩
+          fun← b ( fun→ b y )
+        ≡⟨  fiso← b y  ⟩
+          y  
+        ∎  where open ≡-Reasoning
+
+b→injection1 : {n m : Level} (R : Set n) (S : Set m)  → (b : Bijection R S) → injection S R (fun← b)
+b→injection1 R S b x y eq = trans (  sym ( fiso→ b x ) ) (trans (  cong (λ k → fun→ b k ) eq ) ( fiso→ b y  ))
+
+--  ¬ A = A → ⊥ 
+
+diag :  (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ → Bool
+diag b n = not (fun← b n n)
+
 diagonal : ¬ Bijection  ( ℕ → Bool ) ℕ
-diagonal b = diagn1 (fun→ b diag) refl where
-    diag :  ℕ → Bool
-    diag n = not (fun← b n n)
-    diagn1 : (n : ℕ ) → ¬ (fun→ b diag ≡ n ) 
-    diagn1 n dn = ¬t=f (diag n ) ( begin
-           not diag n 
+diagonal b = diagn1 (fun→ b (diag b) ) refl where
+    diagn1 : (n : ℕ ) → ¬ (fun→ b (diag b) ≡ n ) 
+    diagn1 n dn = ¬t=f (diag b n ) ( begin
+           not (diag b n)
         ≡⟨⟩
            not (not fun← b n n)
         ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
-           not (fun← b (fun→ b diag)  n)
+           not (fun← b (fun→ b (diag b))  n)
         ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
            not (fun← b n n)
         ≡⟨⟩
-           diag n 
+           diag b n 
         ∎ ) where open ≡-Reasoning
 
+b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ 
+b1 b = fun→ b (diag b)
+
+b-iso : (b : Bijection  ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
+b-iso b = fiso← b _
+
+postulate
+   utm         : List Bool → List Bool → Maybe Bool
+
+record TM : Set where
+   field
+      tm : List Bool → Maybe Bool
+      encode : List Bool
+      is-tm : utm encode ≡ tm
+
+open TM
+
+Halt1 : TM → List Bool  → Bool -- ℕ → ( ℕ → Bool )
+Halt1 = {!!}
+
+record Halt1-is-tm : Set where
+   field
+       htm : TM
+       htm-is-Halt1 : (t : TM ) → (x : List Bool) → (Halt1 t x ≡ true) ⇔ ((tm htm (encode t ++ x)) ≡ just true)
+
+Halt2 : (tm : TM ) →  List Bool -- ( ℕ → Bool ) → ℕ  
+Halt2 tm = encode tm
+
+not-halt : {!!}
+not-halt = {!!}
+
 to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
 to1 {n} {R} b = record {
        fun←  = to11
@@ -69,21 +120,11 @@
 LBℕ : Bijection  ( List Bool ) ℕ
 LBℕ = {!!}
 
-postulate
-   utm         : List Bool → List Bool → Maybe Bool
 
 open import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) 
 
-record TM : Set where
-   field
-      tm : List Bool → Maybe Bool
-      encode : List Bool
-      is-tm : utm encode ≡ tm
-
-open TM
-
 record Halt : Set where
    field
       htm : TM
@@ -107,6 +148,12 @@
          tmb1 x with is-tm x | inspect is-tm x
          ... | refl | record { eq = refl } = tm-cong (is-tm x) refl refl
 
+TNℕ : Bijection  TM ℕ
+TNℕ = {!!}
+
+--  Halt1 (Halt2 x) ≡ x
+--  Halt2 (Halt2 y) ≡ y
+
 halting : ¬ Halt
 halting h with tm (htm h) (encode (nhtm h) ++ encode (nhtm h))
 ... | just true = ¬t=f {!!} {!!}
--- a/agda/omega-automaton.agda	Wed Jan 13 10:52:01 2021 +0900
+++ b/agda/omega-automaton.agda	Fri Mar 12 21:45:53 2021 +0900
@@ -14,23 +14,39 @@
 
 open Automaton 
 
-ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q )  →  ℕ → ( ℕ → Σ )  → Q
+ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q ) →  ℕ → ( ℕ → Σ )  → Q
 ω-run Ω x zero s = x
-ω-run Ω x (suc n) s = δ Ω (ω-run Ω ? n s) ( s n )
+ω-run Ω x (suc n) s = δ Ω (ω-run Ω x n s) ( s n )
 
+--
+-- accept as Buchi automaton
+--
 record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         from : ℕ
-        stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω ? n S ) ≡ true
+        stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x n S ) ≡ true
 
 open Buchi
-       
+
+--  after sometimes, always p
+--
+--                       not p
+--                   ------------>
+--        <> [] p *                 <> [] p 
+--                   <-----------
+--                       p
+
     
+--
+-- accept as Muller automaton
+--
 record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
     field
         next     : (n : ℕ ) → ℕ 
-        infinite : (n : ℕ ) →  aend Ω ( ω-run Ω ? (n + (next n)) S ) ≡ true 
+        infinite : (x : Q) → (n : ℕ ) →  aend Ω ( ω-run Ω x (n + (next n)) S ) ≡ true 
 
+--  always sometimes p
+--
 --                       not p
 --                   ------------>
 --        [] <> p *                 [] <> p 
@@ -67,16 +83,25 @@
 flip-seq zero = false
 flip-seq (suc n) = not ( flip-seq n )
 
+lemma0 : Muller ωa1 flip-seq 
+lemma0 = record {
+        next = λ n → suc (suc n)
+      ; infinite = lemma01
+   } where
+        lemma01 :  (x : States3) (n : ℕ) →
+           aend ωa1 (ω-run ωa1 x (n + suc (suc n)) flip-seq) ≡ true
+        lemma01 = {!!}
+
 lemma1 : Buchi ωa1 true-seq 
 lemma1 = record {
         from = zero
-      ; stay = lem1
+      ; stay = {!!}
    } where
-      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 ? n true-seq ) ≡ true
+      lem1 : ( n :  ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} n true-seq ) ≡ true
       lem1 zero ()
-      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 ? n true-seq 
-      lem1 (suc n) (s≤s z≤n) | ts* = ?
-      lem1 (suc n) (s≤s z≤n) | ts = ?
+      lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} n true-seq 
+      lem1 (suc n) (s≤s z≤n) | ts* = {!!}
+      lem1 (suc n) (s≤s z≤n) | ts = {!!}
 
 ωa2 : Automaton States3 Bool
 ωa2 = record {
@@ -97,27 +122,23 @@
        ∎
 
 flip-dec2 : (n : ℕ ) → not flip-seq (suc n)  ≡  flip-seq n 
-flip-dec2 n = ?
+flip-dec2 n = {!!}
 
 
 record flipProperty : Set where
     field
-       flipP : (n : ℕ) →  ω-run ωa2 ?  flip-seq  ≡ ω-run ωa2 n flip-seq
+       flipP : (n : ℕ) →  ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!}
 
 lemma2 : Muller ωa2 flip-seq 
 lemma2 = record {
           next = next
-       ;  infinite = infinite
+       ;  infinite = {!!}
    }  where
      next : ℕ → ℕ
-     next n with ω-run ωa2 n flip-seq | flip-seq n
-     next n | ts | true = 2
-     next n | ts | false = 1
-     next n | ts* | true = 2
-     next n | ts* | false = 1
-     infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 (ω-run ωa2 (m + (next m)) flip-seq) ≡ true → aend ωa2 (ω-run ωa2 (n + (next n)) flip-seq) ≡ true
+     next = {!!}
+     infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true
      infinite' = {!!}
-     infinite : (n : ℕ) → aend ωa2 (ω-run ωa2 (n + (next n)) flip-seq) ≡ true
+     infinite : (n : ℕ) → aend ωa2 {!!} ≡ true
      infinite = {!!}
 
 lemma3 : Buchi ωa1 false-seq  →  ⊥
--- a/agda/root2.agda	Wed Jan 13 10:52:01 2021 +0900
+++ b/agda/root2.agda	Fri Mar 12 21:45:53 2021 +0900
@@ -52,6 +52,11 @@
 
 -- gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
 
+gcd-even : { n m : ℕ} → Even n → Even m → Even ( gcd n m )
+gcd-even {n} {m} en em = record { j = {!!} ; is-twice = {!!} } where
+   gcd-even1 : ( n m : ℕ) → Even n → Even m → Even ( gcd n m )
+   gcd-even1 n m gn gm = {!!}
+
 root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
 root2-irrational n m n>1 m>1 2nm = gcd24 {n} {m} n>1 m>1 (s≤s (s≤s z≤n)) (even→gcd=2 rot7 (rot5 n>1)) (even→gcd=2 ( even^2 {m} ( rot1)) (rot5 m>1))where
     rot5 : {n : ℕ} → n > 1 → n > 0
--- a/agda/turing.agda	Wed Jan 13 10:52:01 2021 +0900
+++ b/agda/turing.agda	Fri Mar 12 21:45:53 2021 +0900
@@ -4,12 +4,12 @@
 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.Maybe hiding ( map )
 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
+open import Data.Product hiding ( map )
 
 
 data Write   (  Σ : Set  ) : Set  where
@@ -121,3 +121,9 @@
           where
               t1 = move {CopyStates} {ℕ} {0} {Copyδ} q L R
 
+-- testn = map (\ n -> test2 n) ( 0 ∷  1 ∷  2 ∷  3 ∷  4 ∷  5 ∷  6 ∷  [] )
+
+testn : ℕ →  List ( CopyStates × ( List  ℕ ) × ( List  ℕ ) )
+testn 0 = test2 0 ∷ []
+testn (suc n)  = test2 n ∷ testn n
+