-title: push donwオートマトンと文法クラス

任意のnについて 0{n}1{n} に対応する有限オートマトンはない。

    inputnn0 : ( n :  ℕ )  →  { Σ : Set  } → ( x y : Σ ) → List  Σ → List  Σ 
    inputnn0 zero {_} _ _ s = s
    inputnn0 (suc n) x y s = x  ∷ ( inputnn0 n x y ( y  ∷ s ) )

inputnn だけ受け付けて、それ以外を受け付けないということができない。

かっこの対応が取れないことに相当する。

    inputnn :  List  In2 → Maybe (List In2)
    inputnn [] = just []
    inputnn  (i1 ∷ t) = just (i1 ∷ t)
    inputnn  (i0 ∷ t) with inputnn t
    ... | nothing = nothing
    ... | just [] = nothing
    ... | just (i0 ∷ t1) = nothing   -- can't happen
    ... | just (i1 ∷ t1) = just t1   -- remove i1 from later part

    inputnn1 :  List  In2 → Bool
    inputnn1  s with inputnn  s 
    ... | nothing = false
    ... | just [] = true
    ... | just _ = false

こちらは  0{n}1{n} を受け付けるかどうか調べるプログラムである。

inputnn1 が inpuynn0 を受けつけるかどうかを証明する必要がある。

    nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
    nn01  = ?

これはやさしくない。一般的にプログラムが正しく動くことを証明することに相当する。

--pumping lemma

まず Trace を定義する。

    data Trace { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) : (is : List Σ) → Q → Set where
        tend  : {q : Q} → aend fa q ≡ true → Trace fa [] q
        tnext : (q : Q) → {i : Σ} { is : List Σ} 
            → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q 

これは Automaton が受け付ける文字列を生成する data である。実際、

    tr-accept→ : { Q : Set } { Σ : Set  }
        → (fa : Automaton Q  Σ )
        → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
    tr-accept→ {Q} {Σ} fa [] q (tend x)  = x
    tr-accept→ {Q} {Σ} fa (i ∷ is) q  (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr

    tr-accept← : { Q : Set } { Σ : Set  }
        → (fa : Automaton Q  Σ )
        → (is : List Σ) → (q : Q)  → accept fa q is ≡ true → Trace fa is q
    tr-accept← {Q} {Σ} fa [] q ac = tend ac
    tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac )
    tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 

もし、ある文字列を受け付ける Automaton の状態に重複があれば


    record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
        field
           x y z : List Σ
           xyz=is : x ++ y ++ z ≡ is 
           trace-xyz  : Trace fa (x ++ y ++ z)  q
           trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
           non-nil-y : ¬ (y ≡ [])

    pumping-lemma : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
         → (tr : Trace fa is q )
         → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
         → TA fa q is

を示すことができる。(Agda ではあんまりやさしくないが、割と自明)

状態数よりも長い文字列を使えば、必ずこの方法で延長できる。 inputnn0 は、この性質を持たないので(なぜか?)
inputnn0 が正規言語でないことがわかる。

--push down automaton

Automatonを拡張して、これを受け付けるようにすることができる。

    data PushDown   (  Γ : Set  ) : Set  where
       pop    : PushDown  Γ
       push   :  Γ → PushDown  Γ
       none   :  PushDown  Γ

    record PDA ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
           : Set  where
        field
            automaton : Automaton Q Σ
            pδ : Q →  PushDown  Γ 
        open Automaton
        paccept : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
        paccept q [] [] = aend automaton q 
        paccept q (H  ∷ T) [] with pδ  (δ automaton q H) 
        paccept q (H ∷ T) [] | pop     = paccept (δ automaton q H) T []
        paccept q (H ∷ T) [] | none    = paccept (δ automaton q H) T []
        paccept q (H ∷ T) [] | push x  = paccept (δ automaton q H) T (x  ∷ [] )
        paccept q [] (_ ∷ _ ) = false
        paccept q ( H  ∷ T ) ( SH  ∷ ST ) with pδ (δ automaton q H) 
        ... | pop      = paccept (δ automaton q H) T ST
        ... | none     = paccept (δ automaton q H) T (SH ∷ ST)
        ... | push ns  = paccept (δ automaton q H) T ( ns  ∷  SH ∷ ST )

例えば

    pnnp : PDA States2 In2 States2
    pnnp = record {
             automaton = record { aend = aend ; δ = δ }
           ; pδ  = pδ
       } where
            δ : States2 → In2 → States2
            δ ph1 i0 = ph1
            δ ph1 i1 = ph2
            δ ph2 i1 = ph2
            δ _ _ = phf
            aend : States2 → Bool
            aend ph2 = true
            aend _ = false
            pδ  : States2 → PushDown States2
            pδ ph1 = push ph1 
            pδ ph2 = pop   
            pδ phf = none   

これと inputnn1 が同じ動作をすることを示せれば良い。

--文脈自由文法

PDA で受け付ける言語を文脈自由文法(context free grammer)という。

実際のプログラミング言語は、型宣言とかの文脈に依存するので、CFGではない。

しかし、文法自体は CFG で定義されることが多い。

文法定義には BNF (Buckas Noar Form)を使う。

     expr :  EA  |  EB   |   EC  ; 
     statement : 
           SA  |   SB   |   SC 
         |  IF   expr  THEN  statement 
         |  IF   expr  THEN  statement    ELSE    statement 
         ; 

これらを実際に parse するのには再帰下降法が便利なことが知られている。

現在のコンパイラは。だいたいそれで実装されている。

文法規則がプログラムで直接記述されるという利点もある。

--文脈依存文法

     expr :  EA  |  EB   |   EC  ; 

の部分を

     delcare exprt :  EA  |  EB   |   EC  ; 

のように : の左側に複数の要素を許す
と、文脈依存文法になる。これを判定して停止するプログラムは、stack を二つ持つ Automaton になるが、
Turing Machine と呼ばれる。 その停止性を判定することはできない。それを次の講義で示す。

実用的には文法規則の適当な subset を停止することが分かっているアルゴリズムで決めれば良い。

---問題8.1 push down automaton


<a href="../exercise/004.html"> 例題  </a> <!---  Exercise 8.1 --->