# HG changeset patch # User Shinji KONO # Date 1712291900 -32400 # Node ID b85402051cdb1f8b6dc79dcfc4c80744b5be68fa # Parent 207e6c4e155c354f03896f4f85ace778a67e5d54 add mul diff -r 207e6c4e155c -r b85402051cdb a11/lecture.ind --- a/a11/lecture.ind Wed Nov 29 17:40:55 2023 +0900 +++ b/a11/lecture.ind Fri Apr 05 13:38:20 2024 +0900 @@ -6,43 +6,6 @@ 例えば、信号機は停まらずにずーっと動くことが期待されていて、正しい信号機の動作とそうでない動作がある。そして信号機はオートマトン的に動作している。 ---ωオートマトンの定義 - -オートマトンの定義は同じものを用いる。ただし、入力は無限にある。 - - record Automaton ( Q : Set ) ( Σ : Set ) - : Set where - field - δ : Q → Σ → Q - astart : Q - aend : Q → Bool - -automaton の定義にはもともと入力の実装が何かは記述されていない。 - -Agda では無限の長さのリストを扱うことはできない。その代わり、自然数 n から入力Σを生成する関数( ℕ → Σ )を用いる。 -これを用いて、 - - - ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → ℕ → ( ℕ → Σ ) → Q - ω-run Ω zero s = astart Ω - ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n ) - -と言う形でオートマトンが無限に実行される。 - -この無限長の入力をどう受け付けるかを定義する必要がある。これには二通りの方法がある。 - - record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where - field - from : ℕ - stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true - - record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where - field - next : (n : ℕ ) → ℕ - infinite : (n : ℕ ) → aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true - -Buchi ではある時刻から先では、aend で定義される状態の集合にずーっと留まる。Muller ではaendで定義されるある状態の集合を無限回通る。 - --ωオートマトンと様相論理 これらは時間の様相を表す論理に関係している。 @@ -92,12 +55,55 @@ ; aend = mark1 } -ここで、[] <> p * ( 上では ts* ) を無限回通れば、 [] <> p が成立していることになる。(Muller automaton ) +ここで、[] <> p * ( 上では ts* ) を無限回通れば、 [] <> p が成立していることになる。(Buchi automaton ) + +これの否定は、<> [] ( ¬ p ) ということになる。これは、ある時点からずーっと ¬ p が続く。(Muller automaton ) + +--ωオートマトンの定義 + +オートマトンの定義は同じものを用いる。ただし、入力は無限にある。 -これの否定は、<> [] ( ¬ p ) ということになる。これは、ある時点からずーっと ¬ p が続く。(Buchi automaton ) + record Automaton ( Q : Set ) ( Σ : Set ) + : Set where + field + δ : Q → Σ → Q + astart : Q + aend : Q → Bool + +automaton の定義にはもともと入力の実装が何かは記述されていない。 + +Agda では無限の長さのリストを扱うことはできない。その代わり、自然数 n から入力Σを生成する関数( ℕ → Σ )を用いる。 +これを用いて、 + ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → ℕ → ( ℕ → Σ ) → Q + ω-run Ω zero s = astart Ω + ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n ) + +と言う形でオートマトンが無限に実行される。 + +この無限長の入力をどう受け付けるかを定義する必要がある。これには二通りの方法がある。 + + record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where + field + from : ℕ + stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x S n ) ≡ true + + record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where + field + next : (n : ℕ ) → ℕ + infinite : (x : Q) → (n : ℕ ) → aend Ω ( ω-run Ω x S (n + (suc (next n)))) ≡ true +Muller ではある時刻から先では、aend で定義される状態の集合にずーっと留まる。Buchi ではaendで定義されるある状態の集合を無限回通る。 +--Muller automaton と Buchi automaton の関係 + B→M : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q + → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) + + M→B : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q + → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) + +これが証明できる + diff -r 207e6c4e155c -r b85402051cdb a13/lecture.ind --- a/a13/lecture.ind Wed Nov 29 17:40:55 2023 +0900 +++ b/a13/lecture.ind Fri Apr 05 13:38:20 2024 +0900 @@ -22,6 +22,8 @@ Javaのモデル検査器。Thread を見てくれる。 + JavaPathFinder + --CPAcheker Cで書いたプログラムを検証してくれる diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/cfg1.agda --- a/automaton-in-agda/src/cfg1.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/cfg1.agda Fri Apr 05 13:38:20 2024 +0900 @@ -60,6 +60,10 @@ split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t +-- +-- we can rewrite cfg-language without Termination check violation +-- + cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool {-# TERMINATING #-} diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/derive.agda --- a/automaton-in-agda/src/derive.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/derive.agda Fri Apr 05 13:38:20 2024 +0900 @@ -66,7 +66,8 @@ derive-step r d0 s = derive (is-derived d0) s refl regex→automaton : (r : Regex Σ) → Automaton (Derivative r) Σ -regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl } +regex→automaton r = record { δ = λ d s → + record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl } ; aend = λ d → empty? (state d) } regex-match : (r : Regex Σ) → (List Σ) → Bool @@ -183,6 +184,21 @@ s : Regex Σ is-sub : SB r s +SubtermS : (x : Regex Σ ) → Set +SubtermS x = (y : Regex Σ) → SB x y → Bool + +nderivative : (x : Regex Σ) → SubtermS x → Σ → SubtermS x +nderivative = ? + +open import nfa + +regex→nautomaton : (r : Regex Σ) → NAutomaton ? Σ +regex→nautomaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl } + ; aend = λ d → empty? (state d) } + +regex-nmatch : (r : Regex Σ) → (List Σ) → Bool +regex-nmatch ex is = ? -- accept ( regex→nautomaton ex ) record { state = ex ; is-derived = unit refl } is + open import bijection using ( InjectiveF ; Is ) finISB : (r : Regex Σ) → FiniteSet (ISB r) @@ -396,4 +412,23 @@ +--- +-- empty? ((< a > * || < b > * ) & < c > ) = falsee +-- +-- derive ((< a > * || < b > * ) & < c > ) a = < a > * & < c > +-- derive ((< a > * || < b > * ) & < c > ) b = < b > * & < c > +-- derive ((< a > * || < b > * ) & < c > ) c = ε +-- derive ((< a > * || < b > * ) & < c > ) d = φ +-- +-- empty? ((< a > * ) & < c > ) = falsee +-- derive (< a > * & < c > ) a = < a > * & < c > +-- derive (< a > * & < c > ) b = φ +-- derive (< a > * & < c > ) c = ε +-- derive (< a > * & < c > ) d = φ +-- +-- empty? ((< b > * ) & < c > ) = falsee +-- derive (< b > * & < c > ) a = φ +-- derive (< b > * & < c > ) b = < b > * & < c > +-- derive (< b > * & < c > ) c = ε +-- derive (< b > * & < c > ) d = φ diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/deriveUtil.agda --- a/automaton-in-agda/src/deriveUtil.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/deriveUtil.agda Fri Apr 05 13:38:20 2024 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical-compatible --safe #-} +-- {-# OPTIONS --cubical-compatible safe #-} module deriveUtil where diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/finiteSet.agda --- a/automaton-in-agda/src/finiteSet.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/finiteSet.agda Fri Apr 05 13:38:20 2024 +0900 @@ -40,3 +40,12 @@ equal? q0 q1 with F←Q q0 ≟ F←Q q1 ... | yes p = true ... | no ¬p = false + +record FiniteSetF ( Q : Set ) : Set where + field + finite : ℕ + Q←F : Fin finite → Q → Bool + F←Q : (Q → Bool) → Fin finite + finiso→ : (f : Q → Bool ) → (q : Q) → Q←F ( F←Q f ) q ≡ f q + finiso← : (f : Fin finite ) → F←Q ( Q←F f ) ≡ f + diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/flcagl.agda --- a/automaton-in-agda/src/flcagl.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/flcagl.agda Fri Apr 05 13:38:20 2024 +0900 @@ -8,7 +8,7 @@ -- bb : (y : aaa) → aaa -- cc : (y : aaa) → aaa -- --- Lang : {Σ : Set } → List Σ → Bool +-- Lang : {Σ : Set } → Colist Σ → Bool -- Lang [] = ? -- Lang (h ∷ t) = ? -- @@ -46,28 +46,29 @@ open import Level renaming ( zero to Zero ; suc to succ ) open import Size open import Data.Empty +open import Data.List hiding (map ; foldr ; any) -module List where +module Colist where - data List (i : Size) (A : Set) : Set where - [] : List i A - _∷_ : {j : Size< i} (x : A) (xs : List j A) → List i A + data Colist (i : Size) (A : Set) : Set where + [] : Colist i A + _∷_ : {j : Size< i} (x : A) (xs : Colist j A) → Colist i A - map : ∀{i A B} → (A → B) → List i A → List i B + map : ∀{i A B} → (A → B) → Colist i A → Colist 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 : ∀{i} {A B : Set} → (A → B → B) → B → Colist 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 : ∀{i A} → (A → Bool) → Colist i A → Bool any p xs = foldr _∨_ false (map p xs) module Lang where - open List + open Colist -- Lnag ≅ Bool × (Σ → Lang) -- @@ -79,15 +80,19 @@ open Lang - _∋_ : ∀{i} → Lang i → List i A → Bool + _∋_ : ∀{i} → Lang i → Colist i A → Bool l ∋ [] = ν l l ∋ ( a ∷ as ) = δ l a ∋ as - trie : ∀{i} (f : List i A → Bool) → Lang i + trie : ∀{i} (f : Colist i A → Bool) → Lang i ν (trie f) = f [] δ (trie f) a = trie (λ as → f (a ∷ as)) - -- trie' : ∀{i} (f : List i A → Bool) → Lang i + -- _∋'_ : ∀{i} → Lang i → List A → Bool + -- l ∋' [] = ν l + -- l ∋' ( a ∷ as ) = δ l a ∋' as + + -- trie' : ∀{i} (f : Colist i A → Bool) → Lang i -- trie' {i} f = record { -- ν = f [] -- ; δ = λ {j} a → lem {j} a -- we cannot write in this way @@ -124,31 +129,41 @@ δ (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 - δ (k + l) x with ν k | ν l - ... | false | true = δ k x + l - ... | false | false = δ k x + l - ... | true | true = (δ k x + l ) ∪ δ l x - ... | true | false = (δ k x + l ) ∪ δ l x + ν (k + l) = ν l + δ (k + l) x with ν k + ... | false = δ k x + l + ... | true = (δ k x + l ) ∪ δ l x language : { Σ : Set } → Set - language {Σ} = List ∞ Σ → Bool + language {Σ} = Colist ∞ Σ → Bool split : {Σ : Set} → {i : Size } → (x y : language {Σ} ) → language {Σ} - split x y [] = x [] ∨ y [] + split x y [] = x [] ∧ y [] split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t - LtoSplit : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ true → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true - LtoSplit x y [] xy with ν x | ν y - ... | true | true = refl + data In2 : Set where + i0 : In2 + i1 : In2 + + test-AB→split : {Σ : Set} → {A B : Colist ∞ In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ ( + ( A [] ∧ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) ∨ + ( A ( i0 ∷ [] ) ∧ B ( i1 ∷ i0 ∷ [] ) ) ∨ + ( A ( i0 ∷ i1 ∷ [] ) ∧ B ( i0 ∷ [] ) ) ∨ + ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) ∧ B [] ) + ) + test-AB→split {_} {A} {B} = ? + + LtoSplit : (x y : Lang ∞ ) → (z : Colist ∞ A) → ((x · y ) ∋ z) ≡ true → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true + LtoSplit x y [] xy with ν x + ... | true = xy LtoSplit x y (h ∷ z) xy = ? - SplitoL : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ false → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false + SplitoL : (x y : Lang ∞ ) → (z : Colist ∞ A) → ((x · y ) ∋ z) ≡ false → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false SplitoL x y [] xy with ν x | ν y ... | false | false = refl - ... | false | true = ? - ... | true | false = ? + ... | false | true = refl + ... | true | false = refl SplitoL x y (h ∷ z) xy = ? @@ -225,10 +240,10 @@ ≅ν (union-cong p q) = cong₂ _∨_ (≅ν p) (≅ν q) ≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q 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 + -- 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) @@ -406,15 +421,15 @@ ∎ where open EqR (Bis _) -open List +open Colist 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 + νs : ∀{i} (ss : Colist.Colist i S) → Bool + νs ss = Colist.any ν ss + δs : ∀{i} (ss : Colist.Colist i S) (a : A) → Colist.Colist i S + δs ss a = Colist.map (λ s → δ s a) ss open Lang @@ -459,7 +474,7 @@ ν (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 : ∀{S} (da : DA S) → DA (Colist ∞ S) ν (powA da) ss = νs da ss δ (powA da) ss a = δs da ss a @@ -469,12 +484,12 @@ ≅ν (powA-nil da) = refl ≅δ (powA-nil da) a = powA-nil da -powA-cons : ∀{i S} (da : DA S) {s : S} {ss : List ∞ S} → +powA-cons : ∀{i S} (da : DA S) {s : S} {ss : Colist ∞ 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 : ∀{S1 S2} (da1 : DA S1)(s2 : S2)(da2 : DA S2) → DA (S1 × Colist ∞ S2) ν (composeA da1 s2 da2) (s1 , ss2) = (ν da1 s1 ∧ ν da2 s2) ∨ νs da2 ss2 δ (composeA da1 s2 da2) (s1 , ss2) a = δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a @@ -482,7 +497,7 @@ -- import Relation.Binary.EqReasoning as EqR import Relation.Binary.Reasoning.Setoid as EqR -composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) → +composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : Colist ∞ 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) = refl ≅δ (composeA-gen da1 da2 s1 s2 ss) a with ν da1 s1 @@ -513,14 +528,14 @@ -finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (List ∞ (Maybe S)) +finalToInitial : ∀{S} (da : DA (Maybe S)) → DA (Colist ∞ (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 : ∀{S}(s0 : S)(da : DA S) → DA (Colist ∞(Maybe S)) starA s0 da = finalToInitial (acceptingInitial s0 da) @@ -529,12 +544,22 @@ lang (acceptingInitial s0 da) (just s) ≅⟨ i ⟩≅ lang da s acceptingInitial-nothing : ∀{i S} (s0 : S) (da : DA S) → lang (acceptingInitial s0 da) nothing ≅⟨ i ⟩≅ ε ∪ lang da s0 - starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : List ∞ (Maybe S))→ + starA-lemma : ∀{i S}(da : DA S)(s0 : S)(ss : Colist ∞ (Maybe S))→ lang (starA s0 da) ss ≅⟨ i ⟩≅ lang (powA (acceptingInitial s0 da)) ss · (lang da s0) * starA-correct : ∀{i S} (da : DA S) (s0 : S) → lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) * +record Automaton ( Q : Set ) ( Σ : Set ) + : Set where + field + δ : Q → Σ → Q + aend : Q → Bool + +accept : ∀{i} {S} (da : Automaton S A) (s : S) → Lang i +Lang.ν (accept da s) = Automaton.aend da s +Lang.δ (accept da s) a = accept da (Automaton.δ da s a) + record NAutomaton ( Q : Set ) ( Σ : Set ) : Set where field diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/halt.agda --- a/automaton-in-agda/src/halt.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/halt.agda Fri Apr 05 13:38:20 2024 +0900 @@ -25,7 +25,7 @@ ffun→ : (R → Bool) → S ffiso← : (f : R → Bool ) → (x : R) → ffun← ( ffun→ f ) x ≡ f x - -- ffun← ( ffun→ f ) ≡ f , if we have functional extensionality but it is unsafe +-- ffiso→ : (x : S) → ffun→ ( ffun← x ) ≡ x -- , if we have functional extensionality but it is unsafe open FBijection @@ -86,6 +86,9 @@ open Halt +-- +-- List boot <-> ( List Bool → Bool ) +-- TNLF : (halt : Halt ) → (utm : UTM) → FBijection (List Bool) (List Bool) TNLF halt utm = record { ffun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x) diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/mul.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/automaton-in-agda/src/mul.agda Fri Apr 05 13:38:20 2024 +0900 @@ -0,0 +1,122 @@ +module mul where + +open import Relation.Binary.PropositionalEquality + +data ℕ : Set where + zero : ℕ + suc : ℕ → ℕ + +lemmm00 : ℕ +lemmm00 = suc (suc zero) + +_+_ : ℕ → ℕ → ℕ +zero + y = y +suc x + y = suc (x + y) + +_*_ : ℕ → ℕ → ℕ +zero * y = zero +suc x * y = y + (x * y) + +lemmm01 : ℕ +lemmm01 = suc (suc zero) + suc (suc zero) + ++-comm : ∀ x y → (x + y) ≡ (y + x) ++-comm zero zero = refl ++-comm zero (suc y) = cong suc (+-comm zero y) ++-comm (suc x) zero = cong suc (+-comm x zero) ++-comm (suc x) (suc y) = begin + suc (x + suc y) ≡⟨ (cong suc (+-comm x (suc y))) ⟩ + suc (suc (y + x)) ≡⟨ cong suc (cong suc (+-comm y x)) ⟩ + suc (suc (x + y)) ≡⟨ cong suc ( +-comm (suc x) y) ⟩ + suc (y + suc x) ∎ where open ≡-Reasoning + ++-assoc : ∀ x y z → (x + (y + z)) ≡ ((x + y) + z) ++-assoc zero y z = refl ++-assoc (suc x) y z = cong suc (+-assoc x y z) + +*-distr-r : {y x z : ℕ } → (y * z) + (x * z) ≡ ((y + x) * z) +*-distr-r {zero} {x} {z} = refl +*-distr-r {suc y} {x} {z} = trans (sym (+-assoc z _ _)) (cong (λ k → z + k)(*-distr-r {y} {x} {z})) + +*-distr-l : {y x z : ℕ } → (y * z) + (y * x) ≡ y * (z + x ) +*-distr-l {zero} {x} = refl +*-distr-l {suc y} {x} {z} = begin + (z + (y * z)) + (x + (y * x)) ≡⟨ +-assoc (z + (y * z)) x _ ⟩ + ((z + (y * z)) + x) + (y * x) ≡⟨ cong (λ k → k + (y * x)) (sym (+-assoc z _ _)) ⟩ + (z + ((y * z) + x)) + (y * x) ≡⟨ cong (λ k → (z + k) + (y * x) ) (+-comm _ x) ⟩ + (z + (x + (y * z))) + (y * x) ≡⟨ cong (λ k → k + (y * x)) (+-assoc z _ _) ⟩ + ((z + x) + (y * z)) + (y * x) ≡⟨ sym (+-assoc (z + x) _ _) ⟩ + (z + x) + ((y * z) + (y * x)) ≡⟨ cong (λ k → (z + x) + k) (*-distr-l {y} {x} {z}) ⟩ + (z + x) + (y * (z + x)) ∎ where open ≡-Reasoning + +*-comm : ∀ x y → (x * y) ≡ (y * x) +*-comm zero zero = refl +*-comm zero (suc y) = *-comm zero y +*-comm (suc x) y = lemma2 where + lemma3 : {y : ℕ}　→ y ≡ (y * suc zero) + lemma3 {zero} = refl + lemma3 {suc y} = cong suc (lemma3 {y}) + lemma2 : (y + (x * y)) ≡ (y * suc x) + lemma2 = begin + (y + (x * y)) ≡⟨ cong₂ (λ j k → j + k ) lemma3 (*-comm x y) ⟩ + (y * suc zero) + (y * x) ≡⟨ *-distr-l {y} ⟩ + y * suc x ∎ where open ≡-Reasoning + +*-assoc : ∀ x y z → (x * y) * z ≡ x * (y * z) +*-assoc zero y z = refl +*-assoc (suc x) y z = begin + ((y + (x * y)) * z) ≡⟨ sym (*-distr-r {y} ) ⟩ + (y * z) + ((x * y) * z) ≡⟨ cong (λ k → (y * z) + k) (*-assoc x y z) ⟩ + (y * z) + (x * (y * z)) ∎ where open ≡-Reasoning + +_+ˡ_ : ℕ → ℕ → ℕ +x +ˡ zero = x +x +ˡ suc y = suc (x +ˡ y) + +theorem00 : ∀ x y → (x +ˡ y) ≡ (y + x) +theorem00 x zero = refl +theorem00 x (suc y) = cong suc (theorem00 x y) + +_*ˡ_ : ℕ → ℕ → ℕ +x *ˡ zero = zero +x *ˡ (suc y) = x +ˡ (x *ˡ y) + + +open import Data.Empty +open import Data.Unit +open import Relation.Nullary + +-- theorem000 : ¬ ( _*_ ≡ _*ˡ_ ) +-- theorem000 () + +theorem01 : ∀ x y → (x *ˡ y) ≡ (y * x) +theorem01 x zero = refl +theorem01 x (suc y) = begin + (x *ˡ suc y) ≡⟨ refl ⟩ + x +ˡ (x *ˡ y) ≡⟨ cong (λ k → x +ˡ k) (theorem01 x y) ⟩ + x +ˡ (y * x) ≡⟨ theorem00 x _ ⟩ + (y * x) + x ≡⟨ +-comm _ x ⟩ + x + (y * x) ∎ where open ≡-Reasoning + ++ˡ-assoc : ∀ x y z → (x +ˡ (y +ˡ z)) ≡ ((x +ˡ y) +ˡ z) ++ˡ-assoc x y zero = refl ++ˡ-assoc x y (suc z) = cong suc (+ˡ-assoc x y z) + +-- *ˡ-distr-l : {y x z : ℕ } → (y *ˡ z) +ˡ (y *ˡ x) ≡ y *ˡ (z +ˡ x ) +-- *ˡ-distr-l {y} {zero} {z} = refl +-- *ˡ-distr-l {y} {suc x} {z} = trans ? (cong (λ k → y +ˡ k)(*ˡ-distr-l {y} {x} {z})) + + +theorem02 : ∀ x y → (x *ˡ y) ≡ (x * y) +theorem02 x y = trans (theorem01 x y) (*-comm y x) + +-- record Monad (M : Set → Set) : Set₁ where +-- field +-- return : {A : Set} → A → M A +-- _>>=_ : {A B : Set} → M A → (A → M B) → M B + +--*-Monad : { M : Set → Set } → Monad M → ℕ → ℕ → ℕ +--*-Monad {M} m n n = ? + + + diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/non-regular.agda --- a/automaton-in-agda/src/non-regular.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/non-regular.agda Fri Apr 05 13:38:20 2024 +0900 @@ -40,6 +40,9 @@ inputnn0 : ( n : ℕ ) → List In2 inputnn0 n = input-addi0 n (input-addi1 n) +-- +-- using count of i0 and i1 makes the proof easier +-- inputnn1-i1 : (i : ℕ) → List In2 → Bool inputnn1-i1 zero [] = true inputnn1-i1 (suc _) [] = false diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/omega-automaton.agda --- a/automaton-in-agda/src/omega-automaton.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/omega-automaton.agda Fri Apr 05 13:38:20 2024 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible --safe #-} module omega-automaton where open import Level renaming ( suc to succ ; zero to Zero ) @@ -19,14 +20,14 @@ ω-run Ω x s (suc n) = δ Ω (ω-run Ω x s n) ( s n ) -- --- accept as Buchi automaton +-- accept as Muller automaton -- -record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where +record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where field from : ℕ stay : (x : Q) → (n : ℕ ) → n > from → aend Ω ( ω-run Ω x S n ) ≡ true -open Buchi +open Muller -- after sometimes, always p -- @@ -37,14 +38,14 @@ -- p -- --- accept as Muller automaton +-- accept as Buchi automaton -- -record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where +record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where field next : (n : ℕ ) → ℕ infinite : (x : Q) → (n : ℕ ) → aend Ω ( ω-run Ω x S (n + (suc (next n)))) ≡ true -open Muller +open Buchi -- always sometimes p -- -- not p @@ -56,12 +57,6 @@ open import nat open import Data.Nat.Properties --- LEMB : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S ∨ (¬ ( Buchi Ω S )) --- LEMB Ω S Q = {!!} -- S need not to be constructive, so we have no constructive LEM - --- LEMM : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S ∨ (¬ ( Muller Ω S )) --- LEMM = {!!} - ω-run-eq : { Q Σ : Set } → (Ω Ω' : Automaton Q Σ ) → (q : Q) → ( S : ℕ → Σ ) → (x : ℕ) → δ Ω ≡ δ Ω' → ω-run Ω q S x ≡ ω-run Ω' q S x @@ -77,7 +72,7 @@ -- -B→M : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) +B→M : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) B→M {Q} {Σ} Ω S q b m = ¬-bool bm04 bm02 where q1 : Q q1 = ω-run Ω q S (from b + suc (next m (from b))) @@ -99,7 +94,7 @@ -- [] <> p → ¬ <> [] ¬ p -- -M→B : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Muller Ω S → ¬ ( Buchi record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) +M→B : { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) → Q → Buchi Ω S → ¬ ( Muller record { δ = δ Ω ; aend = λ q → not (aend Ω q)} S ) M→B {Q} {Σ} Ω S q m b = ¬-bool bm04 bm02 where q1 : Q q1 = ω-run Ω q S (from b + suc (next m (from b))) @@ -117,6 +112,23 @@ not (aend Ω' (ω-run Ω' q S (from b + (suc (next m (from b)))))) ≡⟨ cong (λ k → not k ) bm03 ⟩ false ∎ where open ≡-Reasoning +open import finiteSet + +-- q₀ → q₁ → ... q +-- q₀ → q₁ → q₅ .... q₅ ... q + +open FiniteSet + +descendSubset : { Q : Set } → (fin : FiniteSet Q) → ( I : Q → Bool) → ( P : Q → Bool ) + → exists fin (λ q → I q /\ P q) ≡ true → Q → Bool +descendSubset = ? + +is-Muller-valid : { Q Σ : Set } (Ω : Automaton Q Σ ) → FiniteSet Q → Q → Dec ((S : ℕ → Σ) → Muller Ω S) +is-Muller-valid = ? + +-- descendSubset monotonically descend +-- derivation tree of Q will be constructed +-- check contruction of Muller Ω S data States3 : Set where @@ -127,6 +139,7 @@ transition3 ts* true = ts* transition3 ts* false = ts transition3 ts true = ts* + transition3 ts false = ts mark1 : States3 → Bool @@ -149,21 +162,21 @@ flip-seq zero = false flip-seq (suc n) = not ( flip-seq n ) --- flip-seq is acceepted by Muller automaton ωa1 +-- flip-seq is acceepted by Buchi automaton ωa1 -lemma1 : Buchi ωa1 true-seq -lemma1 = record { - from = zero - ; stay = {!!} - } where - lem1 : ( n : ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} true-seq n ) ≡ true - lem1 zero () - lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} true-seq n - lem1 (suc n) (s≤s z≤n) | ts* = {!!} - lem1 (suc n) (s≤s z≤n) | ts = {!!} +-- lemma1 : Muller ωa1 true-seq +-- lemma1 = record { +-- from = zero +-- ; stay = {!!} +-- } where +-- lem1 : ( n : ℕ ) → n > zero → aend ωa1 (ω-run ωa1 {!!} true-seq n ) ≡ true +-- lem1 zero () +-- lem1 (suc n) (s≤s z≤n) with ω-run ωa1 {!!} true-seq n +-- lem1 (suc n) (s≤s z≤n) | ts* = {!!} +-- lem1 (suc n) (s≤s z≤n) | ts = {!!} -lemma0 : Muller ωa1 flip-seq -lemma0 = {!!} +-- lemma0 : Buchi ωa1 flip-seq +-- lemma0 = {!!} ωa2 : Automaton States3 Bool ωa2 = record { @@ -183,30 +196,30 @@ ( not ( flip-seq n ) ) ∎ -flip-dec2 : (n : ℕ ) → ? -- not flip-seq (suc n) ≡ flip-seq n -flip-dec2 n = {!!} +-- flip-dec2 : (n : ℕ ) → ? -- not flip-seq (suc n) ≡ flip-seq n +-- flip-dec2 n = {!!} -record flipProperty : Set where - field - flipP : (n : ℕ) → ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!} +-- record flipProperty : Set where +-- field +-- flipP : (n : ℕ) → ω-run ωa2 {!!} {!!} ≡ ω-run ωa2 {!!} {!!} -lemma2 : Muller ωa2 flip-seq -lemma2 = record { - next = next1 - ; infinite = {!!} - } where - next1 : ℕ → ℕ - next1 = {!!} - infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true - infinite' = {!!} - infinite2 : (n : ℕ) → aend ωa2 {!!} ≡ true - infinite2 = {!!} - -lemma3 : Buchi ωa1 false-seq → ⊥ -lemma3 = {!!} - -lemma4 : Muller ωa1 flip-seq → ⊥ -lemma4 = {!!} - - +-- lemma2 : Buchi ωa2 flip-seq +-- lemma2 = record { +-- next = next1 +-- ; infinite = {!!} +-- } where +-- next1 : ℕ → ℕ +-- next1 = {!!} +-- infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 {!!} ≡ true → aend ωa2 {!!} ≡ true +-- infinite' = {!!} +-- infinite2 : (n : ℕ) → aend ωa2 {!!} ≡ true +-- infinite2 = {!!} +-- +-- lemma3 : Muller ωa1 false-seq → ⊥ +-- lemma3 = {!!} +-- +-- lemma4 : Buchi ωa1 flip-seq → ⊥ +-- lemma4 = {!!} +-- +-- diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/regular-concat.agda --- a/automaton-in-agda/src/regular-concat.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/regular-concat.agda Fri Apr 05 13:38:20 2024 +0900 @@ -82,6 +82,7 @@ exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q) h) ) nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) + acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) → Naccept NFA (CNFA-exist A B) nq z ≡ true acceptB [] q nq nqt fb = lemma8 where diff -r 207e6c4e155c -r b85402051cdb automaton-in-agda/src/regular-language.agda --- a/automaton-in-agda/src/regular-language.agda Wed Nov 29 17:40:55 2023 +0900 +++ b/automaton-in-agda/src/regular-language.agda Fri Apr 05 13:38:20 2024 +0900 @@ -33,25 +33,6 @@ Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} Concat {Σ} A B = split A B --- {-# TERMINATING #-} --- Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ} --- Star1 {Σ} A [] = true --- Star0 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t) - --- Terminating version of Star1 --- - --- regular-langue (P *) ( a ∷ b ∷ c ∷ [] ) = --- (P []) \/ --- (P (a ∷ []) /\ repeat P (b ∷ c ∷ []) ) \/ --- (P (a ∷ b ∷ []) /\ repeat P (c ∷ []) ) \/ --- (P (a ∷ b ∷ c ∷ []) --- --- repeat : {Σ : Set} → (x : language {Σ} ) → language {Σ} --- repeat x [] = true --- repeat x (h ∷ t) = (x [] /\ ? (h ∷ t)) \/ --- repeat (λ t1 → x ( h ∷ t1 )) t - repeat : {Σ : Set} → (P : List Σ → Bool) → (pre y : List Σ ) → Bool repeat P [] [] = true repeat P (h ∷ t) [] = P (h ∷ t) @@ -78,6 +59,11 @@ open import automaton-ex +-- test-AB→star : {Σ : Set} → {A B : List In2 → Bool} → Star1 A ( i1 ∷ i1 ∷ i1 ∷ [] ) ≡ ? +-- test-AB→star = ? + +test-aaa = Star (accept am1 sr) ( i1 ∷ i1 ∷ i1 ∷ [] ) + test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ ( ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ @@ -243,26 +229,26 @@ open import Data.List.Properties -Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x -Star→StarProp {Σ} A x ax = ss00 [] x ax where - ss00 : (pre x : List Σ) → repeat A pre x ≡ true → StarProp A (pre ++ x ) - ss00 [] [] eq = record { spn = [] ; spn-concat = refl ; propn = eq } - ss00 (h ∷ t) [] eq = record { spn = (h ∷ t) ∷ [] ; spn-concat = refl ; propn = bool-and-tt eq refl } - ss00 pre (h ∷ []) eq = record { spn = (pre ++ (h ∷ [])) ∷ [] ; spn-concat = ++-assoc pre _ _ - ; propn = bool-and-tt (trans (sym (ss01 pre (h ∷ []) refl )) eq) refl } where - ss01 : (pre x : List Σ) → x ≡ h ∷ [] → repeat A pre x ≡ A (pre ++ (h ∷ [])) - ss01 [] (h ∷ []) refl = refl - ss01 (x ∷ pre) (h ∷ []) refl = refl - ss00 pre (h ∷ y@(i ∷ t)) eq = ? where - ss01 : (pre x : List Σ) → x ≡ y → ( ((A (pre ++ (h ∷ []))) /\ repeat A [] y ) \/ repeat A (pre ++ (h ∷ [])) y ) ≡ repeat A pre (h ∷ y ) - ss01 = ? - ss02 : StarProp A (pre ++ h ∷ y ) - ss02 with (A (pre ++ (h ∷ []))) /\ repeat A [] y in eq1 - ... | true = ? - ... | false = ? where - ss03 : repeat A (pre ++ (h ∷ [])) y ≡ true - ss03 = ? - +-- Star→StarProp : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → Star A x ≡ true → StarProp A x +-- Star→StarProp {Σ} A x ax = ss00 [] x ax where +-- ss00 : (pre x : List Σ) → repeat A pre x ≡ true → StarProp A (pre ++ x ) +-- ss00 [] [] eq = record { spn = [] ; spn-concat = refl ; propn = eq } +-- ss00 (h ∷ t) [] eq = record { spn = (h ∷ t) ∷ [] ; spn-concat = refl ; propn = bool-and-tt eq refl } +-- ss00 pre (h ∷ []) eq = record { spn = (pre ++ (h ∷ [])) ∷ [] ; spn-concat = ++-assoc pre _ _ +-- ; propn = bool-and-tt (trans (sym (ss01 pre (h ∷ []) refl )) eq) refl } where +-- ss01 : (pre x : List Σ) → x ≡ h ∷ [] → repeat A pre x ≡ A (pre ++ (h ∷ [])) +-- ss01 [] (h ∷ []) refl = refl +-- ss01 (x ∷ pre) (h ∷ []) refl = refl +-- ss00 pre (h ∷ y@(i ∷ t)) eq = ? where +-- ss01 : (pre x : List Σ) → x ≡ y → ( ((A (pre ++ (h ∷ []))) /\ repeat A [] y ) \/ repeat A (pre ++ (h ∷ [])) y ) ≡ repeat A pre (h ∷ y ) +-- ss01 = ? +-- ss02 : StarProp A (pre ++ h ∷ y ) +-- ss02 with (A (pre ++ (h ∷ []))) /\ repeat A [] y in eq1 +-- ... | true = ? +-- ... | false = ? where +-- ss03 : repeat A (pre ++ (h ∷ [])) y ≡ true +-- ss03 = ? +-- -- -- StarProp→Star : {Σ : Set} → ( A : language {Σ} ) → (x : List Σ) → StarProp A x → Star A x ≡ true -- StarProp→Star {Σ} A x sp = subst (λ k → Star A k ≡ true ) (spsx (spn sp) refl) ( sps1 (spn sp) refl ) where