Mercurial > hg > Members > kono > Proof > automaton1

changeset 19:b16f7e6fd52b

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 Wed, 02 Dec 2020 23:03:39 +0900
parents e168140d15b0
children bdca72fe271e
files halt.agda logic.agda nfa.agda nfa1.agda
diffstat 4 files changed, 199 insertions(+), 75 deletions(-) [+]
line wrap: on
line diff
--- a/halt.agda	Sun Nov 22 19:18:15 2020 +0900
+++ b/halt.agda	Wed Dec 02 23:03:39 2020 +0900
@@ -6,96 +6,83 @@
 open import Data.Nat.Properties
 open import Relation.Nullary
 open import Data.Empty
+open import Data.Unit
 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
+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 
+       fiso← : (x : R)  → fun← ( fun→ x )  ≡ x 
+       fiso→ : (x : ℕ ) → fun→ ( fun← x )  ≡ x 
 
-open Bijection
+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 ]
+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 
+        ≡⟨⟩
+           not (not fun← b n n)
+        ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
+           not (fun← b (fun→ b diag)  n)
+        ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
+           not (fun← b n n)
+        ≡⟨⟩
+           diag n 
+        ∎ ) where open ≡-Reasoning
+
+to1 : {n : Level} {R : Set n} → Bijectionℕ R → Bijectionℕ (⊤ ∨ R )
+to1 = {!!}
+
+ton : {n : Level} {R : Set n} → Bijectionℕ R → Bijectionℕ (ℕ ∨ R )
+ton = {!!}
+
+to∨ : {n : Level} {R S : Set n} → Bijectionℕ R → Bijectionℕ S → Bijectionℕ (S ∨ R )
+to∨ = {!!}
 
-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
+to⊤ : Bijectionℕ ( List ⊤ )
+to⊤ = {!!}
 
-
-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 ]
+{-# TERMINATING #-}
+to2 : Bijectionℕ ( List Bool )
+to2 = record {
+       fun← = λ n → l→ (n← n)
+     ; fun→  = λ x → b→ (b← x)
+     ; fiso← = {!!} 
+     ; fiso→ = {!!} 
+  } where
+     b← : List Bool → ⊤ ∨ List Bool ∨ List Bool 
+     b← [] = case1 tt
+     b← (true  ∷ x ) = case2 (case1 x)
+     b← (false ∷ x ) = case2 (case1 x)
+     b→ : ⊤ ∨ List Bool ∨ List Bool  → ℕ
+     b→ (case1 tt) = fun→ (to1 (to∨ to2 to2)) (case1 tt)
+     b→ (case2 (case1 x)) = fun→ (to1 (to∨ to2 to2))(case2 (  case1 x ))
+     b→ (case2 (case2 x)) = fun→ (to1 (to∨ to2 to2))(case2 (  case2 x ))
+     n← : ℕ → ⊤ ∨ List Bool ∨ List Bool 
+     n← n = fun← (to1 (to∨ to2 to2)) n
+     l→ : ⊤ ∨ List Bool ∨ List Bool → List Bool 
+     l→ (case1 tt) = []
+     l→ (case2 (case1 x)) = true ∷ x
+     l→ (case2 (case2 x)) = false ∷ x
+     iso1 :  (x : List Bool) → l→ (n← (b→ (b← x))) ≡ x
+     iso1 x = begin
+           l→ (n← (b→ (b← x)))
+        ≡⟨ {!!}  ⟩
+           l→ (b← x)
+        ≡⟨ {!!}  ⟩
+           x
+        ∎  where open ≡-Reasoning
 
 
-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	Sun Nov 22 19:18:15 2020 +0900
+++ b/logic.agda	Wed Dec 02 23:03:39 2020 +0900
@@ -93,5 +93,9 @@
 false <=> false = true
 _ <=> _ = false
 
+¬t=f : (t : Bool ) → ¬ ( not t ≡ t) 
+¬t=f true ()
+¬t=f false ()
+
 infixr  130 _\/_
 infixr  140 _/\_
--- a/nfa.agda	Sun Nov 22 19:18:15 2020 +0900
+++ b/nfa.agda	Wed Dec 02 23:03:39 2020 +0900
@@ -68,6 +68,8 @@
 
 example136-2 = naccept exists-in-Q3 nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
 
+example136-3 = ntrace exists-in-Q3 nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
+
 subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
     (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
 subset-construction {n} {Q} { Σ} Nexists  nfa = record {
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nfa1.agda	Wed Dec 02 23:03:39 2020 +0900
@@ -0,0 +1,131 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
+module nfa1 where
+open import Level renaming ( suc to Suc ; zero to Zero )
+
+open import Relation.Binary.PropositionalEquality 
+open import Data.List hiding ([_])
+open import Relation.Nullary
+open import logic
+
+record NAutomaton {n m : Level} ( Q : Set n ) ( Σ : Set  )
+       : Set  (n ⊔ Suc m) where
+    field
+          Nδ : Q → Σ → Q → Set m
+          NF : Q → Set m
+
+open NAutomaton
+
+record Automaton {n m : Level} (Q : Set n) (Σ : Set ) : Set (n ⊔ Suc m) where
+    field
+          δ : Q → Σ → Q
+          F : Q → Set m
+
+open Automaton
+
+accept : {n m : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set m
+accept {n} {Q} {Σ} atm q [] = F atm q
+accept {n} {Q} {Σ} atm q (x ∷ input) = 
+    accept atm (δ atm q x ) input
+
+trace : {n m : Level} {Q : Set n} {Σ : Set } → (A : Automaton {n} {m} 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 )
+
+subset-construction : {n m : Level} { Q : Set n } { Σ : Set  }   →
+    (NAutomaton {n} {m} Q  Σ ) → Automaton {Suc n ⊔ (Suc (Suc m))} (Q → Set (n ⊔ Suc m)) Σ
+subset-construction {n} {m} {Q} { Σ} nfa = record {
+        δ = λ qs x q' → ((q : Q) → qs q ∧ Nδ nfa q x q' )
+     ;  F = λ qs → ( (q : Q) → qs q ∧ NF nfa q )
+   }
+
+naccept : {n m : Level} {Q : Set n} {Σ : Set } → NAutomaton {n} {m} Q Σ → (Q → Set (Suc n ⊔ m)) → List Σ → Set (Suc n ⊔ m)
+naccept {n} {m} {Q} {Σ} nfa qs [] = (q : Q) → qs q ∧ NF nfa q
+naccept {n} {m} {Q} {Σ} nfa qs (x ∷ input) = 
+    naccept nfa (λ q → (( q' : Q) → qs q ∧ Nδ nfa q x q' )) input
+
+qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec (P q))  → List Q → List Q
+qlist P dec [] = []
+qlist P dec (q ∷ qs) with dec q
+... | yes _ = q ∷ qlist P dec qs
+... | no _ = qlist P dec qs
+
+naccept? : {n m : Level} {Q : Set n} {Σ : Set } → (nfa : NAutomaton {n} {m} Q Σ ) → Set (Suc (Suc n) ⊔ Suc m) 
+naccept? {n} {m} {Q} {Σ} nfa = (qs : Dec (Q → Set (Suc n ⊔ m))) → (i : List Σ ) → Dec ((qs : Q → Set (Suc n ⊔ m)) → naccept nfa qs i)
+
+ntrace : {n m : Level} {Q : Set n} {Σ : Set } → (nfa : NAutomaton {n} {m} Q Σ) → (qs : Dec (Q → Set (Suc n ⊔ m))) → (input : List Σ )
+     → (a : naccept? {n} {m}{Q} {Σ} nfa  )
+     → List (List Q)
+ntrace {n} {m} {Q} {Σ} nfa qs [] a with a qs []
+... | yes t = {!!}
+... | no t = {!!}
+ntrace {n} {m} {Q} {Σ} nfa qs (x ∷ t) a =
+      {!!} ∷ ntrace nfa {!!} t a
+
+record FindQ {n : Level} (Q : Set n) (Nexists : (Q → Set)  → Set) : Set (Suc n) where
+    field
+       create : {P : Q → Set} (q : Q ) → P q  → Nexists (λ q → P q) 
+       found  : {P : Q → Set} → Nexists (λ q → P q) → Q
+       exists : {P : Q → Set} → (n : Nexists (λ q → P q)) → P (found n)
+
+data Q3 : Set where
+  q₁ : Q3
+  q₂ : Q3
+  q₃ : Q3
+
+data Σ2 : Set where
+  s0 : Σ2
+  s1 : Σ2
+
+data transition136 : Q3  → Σ2  → Q3 → Set  where
+    d0 : transition136 q₁ s1 q₂ 
+    d1 : transition136 q₁ s0 q₁ 
+    d2 : transition136 q₂ s0 q₂ 
+    d3 : transition136 q₂ s0 q₃ 
+    d4 : transition136 q₂ s1 q₃ 
+    d5 : transition136 q₃ s0 q₁ 
+
+start136 : Q3 → Set (Suc Zero)
+start136 q = Lift (Suc Zero) (q ≡ q₁)
+
+nfa136 :  NAutomaton Q3 Σ2 
+nfa136 =  record { Nδ = transition136 ; NF = λ q → q ≡ q₁ }
+
+accept-136 : naccept? {_} {_} {Q3} nfa136
+accept-136 qs1 [] = {!!}
+accept-136 qs1 (x ∷ i) = {!!}
+
+example136-1 = naccept nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
+e1 : naccept nfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] )
+e1 = {!!}
+
+example136-0 = naccept nfa136 start136 ( s0 ∷ [] )
+
+example136-2 = naccept nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
+
+dfa136 : Automaton (Q3 → Set (Suc Zero)) Σ2
+dfa136 = subset-construction nfa136
+
+t136 : accept dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ []) → List (Q3 → Set (Suc Zero))
+t136 = trace  dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) 
+
+open _∧_
+-- 
+-- subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
+--     (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
+--     → (x : List Σ)
+--     → naccept NFA ( λ q1 → astart q1) x 
+--     → accept (  subset-construction NFA ) ( λ q1 → astart q1) x 
+-- subset-construction-lemma→ {Q} {Σ} Nexists nfa qs [] na = na
+-- subset-construction-lemma→ {Q} {Σ} Nexists nfa qs (x ∷ t) na = 
+--    subset-construction-lemma→ Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t na 
+-- 
+-- subset-construction-lemma← : { Q : Set } { Σ : Set  }   → 
+--     (Nexists : (Q → Set)  → Set) →
+--     (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
+--     → (x : List Σ)
+--     → accept (  subset-construction Nexists NFA ) ( λ q1 → astart q1) x 
+--     → naccept Nexists NFA ( λ q1 →  astart q1) x 
+-- subset-construction-lemma← {Q} {Σ} Nexists nfa qs [] a = a 
+-- subset-construction-lemma← {Q} {Σ} Nexists nfa qs (x ∷ t) a = 
+--    subset-construction-lemma← Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a 
+--