Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/flcagl.agda @ 406:a60132983557

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, 08 Nov 2023 21:35:54 +0900
parents af8f630b7e60
children 3d0aa205edf9
comparison
equal deleted inserted replaced
405:af8f630b7e60 406:a60132983557
1 {-# OPTIONS --cubical-compatible #-} 1 {-# OPTIONS --cubical-compatible #-}
2
3 {-# OPTIONS --sized-types #-} 2 {-# OPTIONS --sized-types #-}
3
4 --
5 -- induction
6 -- data aaa where
7 -- aend : aaa
8 -- bb : (y : aaa) → aaa
9 -- cc : (y : aaa) → aaa
10 --
11 -- (x : aaa) → bb → cc → aend
12 -- induction : ( P : aaa → Set ) → (x : aaa) → P x
13 -- induction P aend = ?
14 -- induction P (bb y) = ? where
15 -- lemma : P y
16 -- lemma = induction P y
17 -- induction P (cc y) = ?
18 --
19 -- ∙
20 -- / \
21 -- bb cc
22 -- /
23 -- aend
24
25 --
26 -- coinduction
27 -- record AAA : Set where
28 -- field
29 -- bb : (y : AAA)
30 -- cc : (y : AAA)
31
32
4 open import Relation.Nullary 33 open import Relation.Nullary
5 open import Relation.Binary.PropositionalEquality 34 open import Relation.Binary.PropositionalEquality
6 module flcagl 35 module flcagl
7 (A : Set) 36 (A : Set)
8 ( _≟_ : (a b : A) → Dec ( a ≡ b ) ) where 37 ( _≟_ : (a b : A) → Dec ( a ≡ b ) ) where
9 38
10 open import Data.Bool hiding ( _≟_ ) 39 open import Data.Bool hiding ( _≟_ )
11 -- open import Data.Maybe 40 -- open import Data.Maybe
12 open import Level renaming ( zero to Zero ; suc to succ ) 41 open import Level renaming ( zero to Zero ; suc to succ )
13 open import Size 42 open import Size
43 open import Data.Empty
14 44
15 module List where 45 module List where
16 46
17 data List (i : Size) (A : Set) : Set where 47 data List (i : Size) (A : Set) : Set where
18 [] : List i A 48 [] : List i A
48 78
49 trie : ∀{i} (f : List i A → Bool) → Lang i 79 trie : ∀{i} (f : List i A → Bool) → Lang i
50 ν (trie f) = f [] 80 ν (trie f) = f []
51 δ (trie f) a = trie (λ as → f (a ∷ as)) 81 δ (trie f) a = trie (λ as → f (a ∷ as))
52 82
83 -- trie' : ∀{i} (f : List i A → Bool) → Lang i
84 -- trie' {i} f = record {
85 -- ν = f []
86 -- ; δ = λ {j} a → lem {j} a -- we cannot write in this way
87 -- } where
88 -- lem : {j : Size< i} → A → Lang j
89 -- lem {j} a = trie' (λ as → f (a ∷ as))
90
53 ∅ : ∀{i} → Lang i 91 ∅ : ∀{i} → Lang i
54 ν ∅ = false 92 ν ∅ = false
55 δ ∅ x = ∅ 93 δ ∅ x = ∅
56 94
57 ε : ∀{i} → Lang i 95 ε : ∀{i} → Lang i
75 113
76 114
77 _·_ : ∀{i} (k l : Lang i) → Lang i 115 _·_ : ∀{i} (k l : Lang i) → Lang i
78 ν (k · l) = ν k ∧ ν l 116 ν (k · l) = ν k ∧ ν l
79 δ (k · l) x = let k′l = δ k x · l in if ν k then k′l ∪ δ l x else k′l 117 δ (k · l) x = let k′l = δ k x · l in if ν k then k′l ∪ δ l x else k′l
118
119 _+_ : ∀{i} (k l : Lang i) → Lang i
120 ν (k + l) = ν k ∧ ν l
121 δ (k + l) x with ν k
122 ... | false = δ k x + l
123 ... | true = (δ k x + l ) ∪ δ l x
124
125 language : { Σ : Set } → Set
126 language {Σ} = List ∞ Σ → Bool
127
128 split : {Σ : Set} → {i : Size } → (x y : language {Σ} ) → language {Σ}
129 split x y [] = x [] ∨ y []
130 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
131 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
132
133 LtoSplit : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ true → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ true
134 LtoSplit x y [] xy with ν x | ν y
135 ... | true | true = refl
136 LtoSplit x y (h ∷ z) xy = ?
137
138 SplitoL : (x y : Lang ∞ ) → (z : List ∞ A) → ((x + y ) ∋ z) ≡ false → split (λ w → x ∋ w) (λ w → y ∋ w) z ≡ false
139 SplitoL x y [] xy with ν x | ν y
140 ... | false | false = refl
141 ... | false | true = ?
142 ... | true | false = ?
143 SplitoL x y (h ∷ z) xy = ?
144
80 145
81 _*_ : ∀{i} (k l : Lang i ) → Lang i 146 _*_ : ∀{i} (k l : Lang i ) → Lang i
82 ν (k * l) = ν k ∧ ν l 147 ν (k * l) = ν k ∧ ν l
83 δ (_*_ {i} k l) {j} x = 148 δ (_*_ {i} k l) {j} x =
84 let 149 let
474 539
475 nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i 540 nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
476 Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x )) 541 Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x ))
477 Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 542 Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x)
478 543
479 nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i 544 -- nlang1 : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
480 Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa {!!} 545 -- Lang.ν (nlang1 nfa s) = NAutomaton.Nend nfa {!!}
481 Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x) 546 -- Lang.δ (nlang1 nfa s) a = nlang1 nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x)
482 547
483 -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i 548 -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
484 -- Lang.ν (nlang' nfa s) = DA.ν nfa s 549 -- Lang.ν (nlang' nfa s) = DA.ν nfa s
485 -- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a) 550 -- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a)
486 551