Mercurial > hg > Members > kono > Proof > automaton

comparison agda/derive.agda @ 36:9558d870e8ae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add cfg and derive
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Nov 2018 21:15:49 +0900
parents
children aa15eff1aeb3
comparison
equal deleted inserted replaced
35:95f2e129cf9e 36:9558d870e8ae
1 module derive where
2
3 open import nfa
4 open import regex1
5 open import Data.Nat
6 open import Data.List
7
8 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
10
11
12 derivatives : {Σ : Set} → Σ → Regex Σ → Regex Σ
13 derivatives x (r *) = {!!}
14 derivatives x (r & r₁) = {!!}
15 derivatives x (r || r₁) = {!!}
16 derivatives x < x₁ > = {!!}
17
18 daccept : {Σ : Set} → ( r : Regex Σ ) → {n : ℕ } (fin : FiniteSet Σ {n}) → ( s : List Σ ) → Bool
19 daccept r fin [] = {!!}
20 daccept r fin (h ∷ t) = regular-language ( derivatives h r ) fin t
21
22 lemma1 : {Σ : Set} → ( r : Regex Σ ) → {n : ℕ } (fin : FiniteSet Σ {n}) → ( s : List Σ )
23 → regular-language r fin s ≡ true → daccept r fin s ≡ true
24 lemma1 = {!!}
25
26 lemma2 : {Σ : Set} → ( r : Regex Σ ) → {n : ℕ } (fin : FiniteSet Σ {n}) → ( s : List Σ )
27 → daccept r fin s ≡ true → regular-language r fin s ≡ true
28 lemma2 = {!!}
29
30
31