Mercurial > hg > Members > kono > Proof > automaton
changeset 46:964e4bd0272a
add coinduction
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Apr 2019 16:13:44 +0900 |
| parents | e9edc777dc03 |
| children | dfc2f65b07ea |
| files | a06/lecture.ind agda/cfg.agda agda/cfg1.agda agda/finiteSet.agda agda/flcagl.agda agda/turing.agda |
| diffstat | 6 files changed, 554 insertions(+), 14 deletions(-) [+] |
line wrap: on
line diff
--- a/a06/lecture.ind Sat Dec 22 15:48:05 2018 +0900 +++ b/a06/lecture.ind Fri Apr 05 16:13:44 2019 +0900 @@ -59,10 +59,7 @@ --複数文字列に対する Boyer-Moore Search - - - +---問題6.1 正規表現の決定性オートマトンへの変換 - +<a href="../exercise/005.html"> 例題 </a> <!--- Exercise 6.1 ---> -
--- a/agda/cfg.agda Sat Dec 22 15:48:05 2018 +0900 +++ b/agda/cfg.agda Fri Apr 05 16:13:44 2019 +0900 @@ -118,17 +118,17 @@ ( Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ [] ) ∷ [] -cgftest1 = cfg-language IFGrammer ( t:SA ∷ [] ) +cfgtest1 = cfg-language IFGrammer ( t:SA ∷ [] ) -cgftest2 = cfg-language2 IFGrammer (Token t:SA) ( t:SA ∷ [] ) +cfgtest2 = cfg-language2 IFGrammer (Token t:SA) ( t:SA ∷ [] ) -cgftest3 = cfg-language1 IFGrammer (Token t:SA ∷ [] ) ( t:SA ∷ [] ) +cfgtest3 = cfg-language1 IFGrammer (Token t:SA ∷ [] ) ( t:SA ∷ [] ) -cgftest4 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:SA ∷ [] ) +cfgtest4 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:SA ∷ [] ) -cgftest5 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:EA ∷ [] ) -cgftest6 = cfg-language2 IFGrammer statement (t:IF ∷ t:EA ∷ t:SA ∷ [] ) -cgftest7 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) +cfgtest5 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:EA ∷ [] ) +cfgtest6 = cfg-language2 IFGrammer statement (t:IF ∷ t:EA ∷ t:SA ∷ [] ) +cfgtest7 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) -cgftest8 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) +cfgtest8 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/cfg1.agda Fri Apr 05 16:13:44 2019 +0900 @@ -0,0 +1,138 @@ +module cfg1 where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat hiding ( _≟_ ) +open import Data.Fin +open import Data.Product +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) + +data Node (Symbol : Set) : Set where + T : Symbol → Node Symbol + N : Symbol → Node Symbol + +data Seq (Symbol : Set) : Set where + _，_ : Symbol → Seq Symbol → Seq Symbol + _． : Symbol → Seq Symbol + Error : Seq Symbol + +data Body (Symbol : Set) : Set where + _｜_ : Seq Symbol → Body Symbol → Body Symbol + _； : Seq Symbol → Body Symbol + +record CFGGrammer (Symbol : Set) : Set where + field + cfg : Symbol → Body Symbol + top : Symbol + eq? : Symbol → Symbol → Bool + typeof : Symbol → Node Symbol + +infixr 80 _｜_ +infixr 90 _； +infixr 100 _，_ +infixr 110 _． + +open CFGGrammer + +----------------- +-- +-- CGF language +-- +----------------- + +split : {Σ : Set} → (List Σ → Bool) + → ( List Σ → Bool) → List Σ → Bool +split x y [] = x [] ∧ y [] +split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ + split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t + + +cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool + +{-# TERMINATING #-} +cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool +cfg-language1 cg Error x = false +cfg-language1 cg (S ， seq) x with typeof cg S +cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eq? cg x x' ∧ cfg-language1 cg seq t +cfg-language1 cg (_ ， seq) [] | T x = false +cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x +cfg-language1 cg (S ．) x with typeof cg S +cfg-language1 cg (_ ．) (x' ∷ []) | T x = eq? cg x x' +cfg-language1 cg (_ ．) _ | T x = false +cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x + +cfg-language0 cg _ [] = false +cfg-language0 cg (rule ｜ b) x = + cfg-language1 cg rule x ∨ cfg-language0 cg b x +cfg-language0 cg (rule ；) x = cfg-language1 cg rule x + +cfg-language : {Symbol : Set} → CFGGrammer Symbol → List Symbol → Bool +cfg-language cg = cfg-language0 cg (cfg cg (top cg )) + + +data IFToken : Set where + EA : IFToken + EB : IFToken + EC : IFToken + IF : IFToken + THEN : IFToken + ELSE : IFToken + SA : IFToken + SB : IFToken + SC : IFToken + expr : IFToken + statement : IFToken + +token-eq? : IFToken → IFToken → Bool +token-eq? EA EA = true +token-eq? EB EB = true +token-eq? EC EC = true +token-eq? IF IF = true +token-eq? THEN THEN = true +token-eq? ELSE ELSE = true +token-eq? SA SA = true +token-eq? SB SB = true +token-eq? SC SC = true +token-eq? expr expr = true +token-eq? statement statement = true +token-eq? _ _ = false + +typeof-IFG : IFToken → Node IFToken +typeof-IFG expr = N expr +typeof-IFG statement = N statement +typeof-IFG x = T x + +IFGrammer : CFGGrammer IFToken +IFGrammer = record { + cfg = cfg' + ; top = statement + ; eq? = token-eq? + ; typeof = typeof-IFG + } where + cfg' : IFToken → Body IFToken + cfg' expr = EA ． ｜ EB ． ｜ EC ． ； + cfg' statement = + SA ． ｜ SB ． ｜ SC ． + ｜ IF ， expr ， THEN ， statement ． + ｜ IF ， expr ， THEN ， statement ， ELSE ， statement ． + ； + cfg' x = Error ； + +cfgtest1 = cfg-language IFGrammer ( SA ∷ [] ) + +cfgtest2 = cfg-language1 IFGrammer ( SA ．) ( SA ∷ [] ) + +cfgtest3 = cfg-language1 IFGrammer ( SA ． ) ( SA ∷ [] ) + +cfgtest4 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ SA ∷ [] ) + +cfgtest5 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ． ) (IF ∷ EA ∷ THEN ∷ SA ∷ [] ) +cfgtest6 = cfg-language1 IFGrammer ( statement ．)(IF ∷ EA ∷ SA ∷ [] ) +cfgtest7 = cfg-language1 IFGrammer ( IF ， expr ， THEN ， statement ， ELSE ， statement ． ) + (IF ∷ EA ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] ) +cfgtest8 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] ) +cfgtest9 = cfg-language IFGrammer (IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] ) +
--- a/agda/finiteSet.agda Sat Dec 22 15:48:05 2018 +0900 +++ b/agda/finiteSet.agda Fri Apr 05 16:13:44 2019 +0900 @@ -4,6 +4,7 @@ open import Data.Bool open import Data.Fin renaming ( _<_ to _<<_ ) open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality record FiniteSet ( Q : Set ) { n : ℕ } : Set where
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/flcagl.agda Fri Apr 05 16:13:44 2019 +0900 @@ -0,0 +1,404 @@ +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality +module flcagl + (A : Set) + ( _≟_ : (a b : A) → Dec ( a ≡ b ) ) where + +open import Data.Bool hiding ( _≟_ ) +-- open import Data.Maybe +open import Level renaming ( zero to Zero ; suc to succ ) +open import Size + +module List where + + data List (i : Size) (A : Set) : Set where + [] : List i A + _∷_ : {j : Size< i} (x : A) (xs : List j A) → List i A + + + map : ∀{i A B} → (A → B) → List i A → List i B + map f [] = [] + map f ( x ∷ xs)= f x ∷ map f xs + + foldr : ∀{i} {A B : Set} → (A → B → B) → B → List i A → B + foldr c n [] = n + foldr c n (x ∷ xs) = c x (foldr c n xs) + + any : ∀{i A} → (A → Bool) → List i A → Bool + any p xs = foldr _∨_ false (map p xs) + +module Lang where + + open List + + record Lang (i : Size) : Set where + coinductive + field + ν : Bool + δ : ∀{j : Size< i} → A → Lang j + + open Lang + + _∋_ : ∀{i} → Lang i → List i A → Bool + l ∋ [] = ν l + l ∋ ( a ∷ as ) = δ l a ∋ as + + trie : ∀{i} (f : List i A → Bool) → Lang i + ν (trie f) = f [] + δ (trie f) a = trie (λ as → f (a ∷ as)) + + ∅ : ∀{i} → Lang i + ν ∅ = false + δ ∅ x = ∅ + + ε : ∀{i} → Lang i + ν ε = true + δ ε x = ∅ + + open import Relation.Nullary.Decidable + + char : ∀{i} (a : A) → Lang i + ν (char a) = false + δ (char a) x = if ⌊ a ≟ x ⌋ then ε else ∅ + + compl : ∀{i} (l : Lang i) → Lang i + ν (compl l) = not (ν l) + δ (compl l) x = compl (δ l x) + + + _∪_ : ∀{i} (k l : Lang i) → Lang i + ν (k ∪ l) = ν k ∨ ν l + δ (k ∪ l) x = δ k x ∪ δ l x + + + _·'_ : ∀{i} (k l : Lang i) → Lang i + ν (k ·' l) = ν k ∧ ν l + δ (k ·' l) x = let k′l = δ k x ·' l in if ν k then k′l ∪ δ l x else k′l + + _·_ : ∀{i} (k l : Lang i ) → Lang i + ν (k · l) = ν k ∧ ν l + δ (_·_ {i} k l) {j} x = + let + k′l : Lang j + k′l = _·_ {j} (δ k {j} x) l + in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l + + _* : ∀{i} (l : Lang i) → Lang i + ν (l *) = true + δ (l *) x = δ l x · (l *) + + record _≅⟨_⟩≅_ (l : Lang ∞ ) i (k : Lang ∞) : Set where + coinductive + field ≅ν : ν l ≡ ν k + ≅δ : ∀ {j : Size< i } (a : A ) → δ l a ≅⟨ j ⟩≅ δ k a + + open _≅⟨_⟩≅_ + + ≅refl : ∀{i} {l : Lang ∞} → l ≅⟨ i ⟩≅ l + ≅ν ≅refl = refl + ≅δ ≅refl a = ≅refl + + + ≅sym : ∀{i} {k l : Lang ∞} (p : l ≅⟨ i ⟩≅ k) → k ≅⟨ i ⟩≅ l + ≅ν (≅sym p) = sym (≅ν p) + ≅δ (≅sym p) a = ≅sym (≅δ p a) + + ≅trans : ∀{i} {k l m : Lang ∞} + ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m + ≅ν (≅trans p q) = trans (≅ν p) (≅ν q) + ≅δ (≅trans p q) a = ≅trans (≅δ p a) (≅δ q a) + + open import Relation.Binary + + ≅isEquivalence : ∀(i : Size) → IsEquivalence _≅⟨ i ⟩≅_ + ≅isEquivalence i = record { refl = ≅refl; sym = ≅sym; trans = ≅trans } + + Bis : ∀(i : Size) → Setoid _ _ + Setoid.Carrier (Bis i) = Lang ∞ + Setoid._≈_ (Bis i) = _≅⟨ i ⟩≅_ + Setoid.isEquivalence (Bis i) = ≅isEquivalence i + + import Relation.Binary.EqReasoning as EqR + + ≅trans′ : ∀ i (k l m : Lang ∞) + ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m + ≅trans′ i k l m p q = begin + k ≈⟨ p ⟩ + l ≈⟨ q ⟩ + m ∎ where open EqR (Bis i) + + open import Data.Bool.Properties + + union-assoc : ∀{i} (k {l m} : Lang ∞) → ((k ∪ l) ∪ m ) ≅⟨ i ⟩≅ ( k ∪ (l ∪ m) ) + ≅ν (union-assoc k) = ∨-assoc (ν k) _ _ + ≅δ (union-assoc k) a = union-assoc (δ k a) + union-comm : ∀{i} (l k : Lang ∞) → (l ∪ k ) ≅⟨ i ⟩≅ ( k ∪ l ) + ≅ν (union-comm l k) = ∨-comm (ν l) _ + ≅δ (union-comm l k) a = union-comm (δ l a) (δ k a) + union-idem : ∀{i} (l : Lang ∞) → (l ∪ l ) ≅⟨ i ⟩≅ l + ≅ν (union-idem l) = ∨-idem _ + ≅δ (union-idem l) a = union-idem (δ l a) + union-emptyl : ∀{i}{l : Lang ∞} → (∅ ∪ l ) ≅⟨ i ⟩≅ l + ≅ν union-emptyl = refl + ≅δ union-emptyl a = union-emptyl + + union-cong : ∀{i}{k k′ l l′ : Lang ∞} + (p : k ≅⟨ i ⟩≅ k′)(q : l ≅⟨ i ⟩≅ l′ ) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l′ ) + ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q) + ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a) + + -- union-union-distr : ∀{i} (k {l m} : Lang ∞) → ( ( k ∪ l ) ∪ m ) ≅⟨ i ⟩≅ ( ( k ∪ m ) ∪ ( l ∪ m ) ) + -- ≅ν (union-union-distr k) = {!!} + -- ≅δ (union-union-distr k) a = {!!} + + + withExample : (P : Bool → Set) (p : P true) (q : P false) → + {A : Set} (g : A → Bool) (x : A) → P (g x) + withExample P p q g x with g x + ... | true = p + ... | false = q + + rewriteExample : {A : Set} {P : A → Set} {x : A} (p : P x) + {g : A → A} (e : g x ≡ x) → P (g x) + rewriteExample p e rewrite e = p + + infixr 7 _∪_ + infixr 7 _·_ + infix 5 _≅⟨_⟩≅_ + concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m ) + concat-union-distribl = {!!} + + union-swap24 : {!!} + union-swap24 = {!!} + + concat-union-distribr : ∀{i} (k {l m} : Lang ∞) → k · ( l ∪ m ) ≅⟨ i ⟩≅ ( k · l ) ∪ ( k · m ) + ≅ν (concat-union-distribr k) = {!!} -- ∧-distribʳ-∨ (ν k) _ _ + ≅δ (concat-union-distribr k) a with ν k + ≅δ (concat-union-distribr k {l} {m}) a | true = begin + {!!} -- δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a) + -- ≈⟨ ? union-cong (concat-union-distribr (δ k a)) ⟩ + -- ≈⟨ ? ⟩ + -- (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a) + ≈⟨ {!!} ⟩ + {!!} -- (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a) + ∎ + where open EqR (Bis _) + ≅δ (concat-union-distribr k) a | false = concat-union-distribr (δ k a) + + concat-congl : ∀{i} {m l k : Lang ∞} + → l ≅⟨ i ⟩≅ k + → l · m ≅⟨ i ⟩≅ k · m + concat-congl = {!!} + concat-congr : ∀{i} {m l k : Lang ∞} + → l ≅⟨ i ⟩≅ k + → m · l ≅⟨ i ⟩≅ m · k + concat-congr = {!!} + + + concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m) + concat-assoc = {!!} + + concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅ + concat-emptyl = {!!} + concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅ + concat-emptyr = {!!} + concat-unitl : ∀{i} l → ε · l ≅⟨ i ⟩≅ l + concat-unitl = {!!} + concat-unitr : ∀{i} l → l · ε ≅⟨ i ⟩≅ l + concat-unitr = {!!} + + + star-empty : ∀{i} → ∅ * ≅⟨ i ⟩≅ ε + star-empty = {!!} + + star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l * + ≅ν (star-concat-idem l) = refl + ≅δ (star-concat-idem l) a = begin + {!!} + ≈⟨ {!!} ⟩ + {!!} + -- δ l a · l * · l * ∪ δ l a · l * + -- ≈⟨ union-cong (concat-assoc _) ⟩ + --≈⟨ ? ⟩ + -- δ l a · (l * · l *) ∪ δ l a · l * + --≈⟨ ? ⟩ + ---- ≈⟨ union-cong (concat-congr (star-concat-idem _)) ⟩ + -- δ l a · l * ∪ δ l a · l * + --≈⟨ ? ⟩ + ---- ≈⟨ union-idem _ ⟩ + -- δ l a · l * + ∎ where open EqR (Bis _) + + star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l * + ≅ν (star-idem l) = refl + ≅δ (star-idem l) a = begin + {!!} + ≈⟨ {!!} ⟩ + {!!} + -- δ l a · l * · (l *) * ≈⟨ ? ⟩ + -- δ l a · l * · l * ≈⟨ ? ⟩ + -- δ l a · (l * · l *) ≈⟨ concat-congr (star-concat-idem l) ⟩ + -- δ l a · l * + ∎ where open EqR (Bis _) + + star-rec : ∀{i} (l : Lang ∞) → l * ≅⟨ i ⟩≅ ε ∪ (l · l *) + star-rec = {!!} + + star-from-rec : ∀{i} (k {l m} : Lang ∞) + → ν k ≡ false + → l ≅⟨ i ⟩≅ k · l ∪ m + → l ≅⟨ i ⟩≅ k * · m + ≅ν (star-from-rec k n p) with ≅ν p + ... | b rewrite n = {!!} + ≅δ (star-from-rec k {l} {m} n p) a with ≅δ p a + ... | q rewrite n = begin + (δ l a) + --≈⟨ q ⟩ + -- δ k a · l ∪ δ m a + --≈⟨ union-cong (concat-congr (star-from-rec k {l} {m} n p)) ⟩ + -- (δ k a · (k * · m) ∪ δ m a) + --≈⟨ union-cong (≅sym (concat-assoc (δ k a))) ⟩ + -- (δ k a · k * · m ∪ δ m a) + ≈⟨ {!!} ⟩ + {!!} + ∎ where open EqR (Bis _) + + +open List + +record DA (S : Set) : Set where + field ν : (s : S) → Bool + δ : (s : S)(a : A) → S + νs : ∀{i} (ss : List.List i S) → Bool + νs ss = List.any ν ss + δs : ∀{i} (ss : List.List i S) (a : A) → List.List i S + δs ss a = List.map (λ s → δ s a) ss + +open Lang + +lang : ∀{i} {S} (da : DA S) (s : S) → Lang i +Lang.ν (lang da s) = DA.ν da s +Lang.δ (lang da s) a = lang da (DA.δ da s a) + +open import Data.Unit hiding ( _≟_ ) + +open DA + +∅A : DA ⊤ +ν ∅A s = false +δ ∅A s a = s + +εA : DA Bool +ν εA b = b +δ εA b a = false + +open import Relation.Nullary.Decidable + +data 3States : Set where + init acc err : 3States + +charA : (a : A) → DA 3States +ν (charA a) init = false +ν (charA a) acc = true +ν (charA a) err = false +δ (charA a) init x = + if ⌊ a ≟ x ⌋ then acc else err +δ (charA a) acc x = err +δ (charA a) err x = err + + +complA : ∀{S} (da : DA S) → DA S +ν (complA da) s = not (ν da s) +δ (complA da) s a = δ da s a + +open import Data.Product + +_⊕_ : ∀{S1 S2} (da1 : DA S1) (da2 : DA S2) → DA (S1 × S2) +ν (da1 ⊕ da2) (s1 , s2) = ν da1 s1 ∨ ν da2 s2 +δ (da1 ⊕ da2) (s1 , s2) a = δ da1 s1 a , δ da2 s2 a + +powA : ∀{S} (da : DA S) → DA (List ∞ S) +ν (powA da) ss = νs da ss +δ (powA da) ss a = δs da ss a + +open _≅⟨_⟩≅_ + +powA-nil : ∀{i S} (da : DA S) → lang (powA da) [] ≅⟨ i ⟩≅ ∅ +≅ν (powA-nil da) = refl +≅δ (powA-nil da) a = powA-nil da + +powA-cons : ∀{i S} (da : DA S) {s : S} {ss : List ∞ S} → + lang (powA da) (s ∷ ss) ≅⟨ i ⟩≅ lang da s ∪ lang (powA da) ss +≅ν (powA-cons da) = refl +≅δ (powA-cons da) a = powA-cons da + +composeA : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × List ∞ S2) +ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ ν da2 {!!} +δ (composeA da1 s2 da2) (s1 , ss2) a = + δ da1 s1 a , {!!} -- δ da2 ? a -- (if ν da1 s1 then s2 ∷ ss2 else ss2) a + +import Relation.Binary.EqReasoning as EqR + +composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) → + lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss +≅ν (composeA-gen da1 da2 s1 s2 ss) = {!!} +≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1 +... | false = {!!} -- composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 ss a) +... | true = begin + {!!} +-- lang (composeA da1 s2 da2) (δ da1 s1 a , δ da2 s2 a ∷ δs da2 ss a) +-- ≈⟨ composeA-gen da1 da2 (δ da1 s1 a) s2 (δs da2 (s2 ∷ ss) a) ⟩ +-- lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang (powA da2) (δs da2 (s2 ∷ ss) a) +-- ≈⟨ ? ⟩ lang da1 (δ da1 s1 a) · lang da2 s2 ∪ +-- (lang da2 (δ da2 s2 a) ∪ lang (powA da2) (δs da2 ss a)) +-- ≈⟨ ≅sym ? ⟩ +-- (lang da1 (δ da1 s1 a) · lang da2 s2 ∪ lang da2 (δ da2 s2 a)) ∪ lang (powA da2) (δs da2 ss a) + ≈⟨ {!!} ⟩ + {!!} + ∎ where open EqR (Bis _) + +composeA-correct : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) s1 s2 → + lang (composeA da1 s2 da2) (s1 , []) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 +composeA-correct = {!!} + + +open import Data.Maybe + +acceptingInitial : ∀{S} (s0 : S) (da : DA S) → DA (Maybe S) +ν (acceptingInitial s0 da) (just s) = ν da s +δ (acceptingInitial s0 da) (just s) a = just (δ da s a) +ν (acceptingInitial s0 da) nothing = true +δ (acceptingInitial s0 da) nothing a = just (δ da s0 a) + + + +finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (List ∞ (Maybe S)) +ν (finalToInitial da) ss = νs da ss +δ (finalToInitial da) ss a = + let ss′ = δs da ss a + in if νs da ss then δ da nothing a ∷ ss′ else ss′ + + +starA : ∀{S}(s0 : S)(da : DA S) → DA (List ∞(Maybe S)) +starA s0 da = finalToInitial (acceptingInitial s0 da) + + +acceptingInitial-just : ∀{i S} (s0 : S) (da : DA S) {s : S} → + lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s +acceptingInitial-just = {!!} + +acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) → + lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0 +acceptingInitial-nothing = {!!} + + +starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→ + lang (starA s0 da) ss ≅⟨ i ⟩≅ + lang (powA (acceptingInitial s0 da)) ss · (lang da s0) * +starA-lemma = {!!} + + +starA-correct : ∀{i S} (da : DA S) (s0 : S) → + lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) * +starA-correct = {!!} +
--- a/agda/turing.agda Sat Dec 22 15:48:05 2018 +0900 +++ b/agda/turing.agda Fri Apr 05 16:13:44 2019 +0900 @@ -46,7 +46,7 @@ ... | true = ( q , L , R ) ... | flase = move-loop {Q} {Σ} {tend} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) where - next = move q L R + next = move {Q} {Σ} {{!!}} {{!!}} q L R record Turing ( Q : Set ) ( Σ : Set ) : Set where