Mercurial > hg > Members > kono > Proof > automaton1
diff regular-language.agda @ 0:9615a94b18ca
new automaton in agda
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 12 Nov 2020 11:45:34 +0900 |
parents | |
children | 7399aae907fc |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/regular-language.agda Thu Nov 12 11:45:34 2020 +0900 @@ -0,0 +1,97 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module regular-language where + +open import Level renaming ( suc to Suc ; zero to Zero ) +open import Data.List +-- open import Data.Nat hiding ( _≟_ ) +-- open import Data.Bool +-- open import Data.Fin hiding ( _+_ ) +open import Data.Empty +open import Data.Unit +open import Data.Product +open import Data.Maybe +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Binary.Definitions +open import logic +open import nat +open import automaton +-- open import finiteSet + +language : { Σ : Set } → Set (Suc Zero) +language {Σ} = List Σ → Set + +open Automaton + +record RegularLanguage {n : Level} ( Σ : Set ) : Set (Level.suc n ) where + field + states : Set n + astart : states + automaton : Automaton states Σ + contain : List Σ → Set + contain x = accept automaton astart x + +split : {Σ : Set} → (List Σ → Set) + → ( List Σ → Set) → List Σ → Set +split x y [] = x [] ∧ y [] +split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ + split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t + +Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} +Union {Σ} A B x = (A x ) ∨ (B x) + +Concat : {n : Level} {Σ : Set } → ( A B : language {Σ} ) → language {Σ} +Concat {Σ} A B = split A B + +{-# TERMINATING #-} +Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ} +Star {Σ} A = split A ( Star {Σ} A ) + +data In2 : Set where + i0 : In2 + i1 : In2 + +test-AB→split : {Σ : Set} → {A B : List In2 → Set} → 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} = refl + +open RegularLanguage +isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set (Suc Zero) +isRegular A x r = A x ≡ contain r x + +-- +-- (states A × states B → Set) → ( states A → Set ) → ( states B → Set ) → Set +-- +exists-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → (states A × states B → Set) → Set +exists-Union A B Pab = exists (automaton A) (λ qa → exists (automaton B) (λ qb → Pab (qa , qb)) ) + +M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ +M-Union {n} {Σ} A B = record { + states = states A × states B + ; astart = ( astart A , astart B ) + ; automaton = record { + δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x ) + ; F = λ q → ( F (automaton A) (proj₁ q) ∨ F (automaton B) (proj₂ q) ) + ; exists = exists-Union A B + } + } + +closed-in-union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B ) +closed-in-union A B [] = lemma where + lemma : F (automaton A) (astart A) ∨ F (automaton B) (astart B) ≡ + F (automaton A) (astart A) ∨ F (automaton B) (astart B) + lemma = refl +closed-in-union {n} {Σ} A B ( h ∷ t ) = lemma4 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where + lemma4 : (t : List Σ) → (qa : states A ) → (qb : states B ) → + accept (automaton A) qa t ∨ accept (automaton B) qb t + ≡ accept (automaton (M-Union A B)) (qa , qb) t + lemma4 [] qa qb = refl + lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h)) + +-- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!} +-- closed-in-concat = {!!} +