Mercurial > hg > Members > kono > Proof > automaton1
view 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 source
{-# 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 = {!!}