Shinji KONO

github.io

Automaton in Agda

Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus

Automaton and NFA

record Automaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
        δ : Q → Σ → Q
        aend : Q → Bool

record NAutomaton ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
          Nδ : Q → Σ → Q → Bool
          Nend  :  Q → Bool

Automaton in Agda

automaton automaton definition

nfa non deterministic

sbconst2 subset construction

regular-language Regular Language

regex Regular Expression

finiteSet Finite Set

derive generating FA from Regex

pumping Pumping Lemma

pumping Application of Pumping Lemma

turing Turing Machine

halt Halting Problem

automaton-ex

bijection

cfg

deriveUtil

even

fin

finiteSetUtil

induction-ex

libbijection

pushdown /

puzzle /

regex1-ex /

regex2 /

regular-concat /

regular-star /

utm /

FiniteSet

record FiniteSet ( Q : Set ) : Set  where
     field
        finite : ℕ
        Q←F : Fin finite → Q
        F←Q : Q → Fin finite
        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
        finiso← : (f : Fin finite ) → F←Q ( Q←F f ) ≡ f

fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) 

Regular Language

What we need is a bounded OD, the containment is limited by an ordinal.

record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
   field
      states : Set
      astart : states
      afin : FiniteSet states
      automaton : Automaton states Σ
   contain : List Σ → Bool
   contain x = accept automaton astart x

Semantics of Regular Language

``
Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} Union {Σ} A B x = A x \/ B x

split : {Σ : Set} → (x y : language {Σ} ) → language {Σ}
split x y  [] = x [] /\ y []
split x y (h  ∷ t) = (x [] /\ y (h  ∷ t)) \/
  split (λ t1 → x (  h ∷ t1 ))  (λ t2 → y t2 ) t

Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
Concat {Σ} A B = split A B

-- Terminating version of Star1
--
repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool
repeat2 x pre [] = false
repeat2 x pre (h ∷ y) = 
   (x (pre ++ (h ∷ [])) /\ repeat x y )
   \/ repeat2 x (pre ++ (h ∷ [])) y 

repeat {Σ} x [] = true
repeat {Σ} x (h ∷ y) = repeat2 x [] (h ∷ y) 

Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
Star {Σ} x y = repeat x y ```

Turing Machine

    record TM ( Q : Set ) ( Σ : Set  ) 
           : Set  where
        field
            automaton : Automaton  Q Σ
            tδ : Q → Σ → Write  Σ  ×  Move 
            tnone :  Σ

Halting Problem

    record UTM : Set where
       field
          utm : TM
          encode : TM → List Bool
          is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x

    record Halt : Set where
       field
          halt :  (t : TM ) → (x : List Bool ) → Bool
          is-halt :     (t : TM ) → (x : List Bool ) → (halt t x ≡ true )  ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
          is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )

    TNL1 : UTM → ¬ Halt