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

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

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

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



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


--push down automaton


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

    record PushDownAutomaton ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
           : Set  where
        field
            pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
            pstart : Q
            pz0 :  Γ
        pmoves :  Q → List  Σ → ( Q × List  Γ )
        pmoves q L = move q L [ pz0 ]
               where
                  move : Q → ( List  Σ ) → ( List  Γ ) → ( Q × List  Γ )
                  move q _ [] = ( q , [] )
                  move q [] S = ( q , S )
                  move q ( H  ∷ T ) ( SH ∷ ST ) with  pδ q H SH 
                  ... | (nq , pop )     = move nq T ST
                  ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
        paccept : List  Σ → Bool
        paccept L = move pstart L [ pz0 ]
               where
                  move : (q : Q ) ( L : List  Σ ) ( L : List   Γ ) → Bool
                  move q [] [] = true
                  move q _ [] = false
                  move q [] (_ ∷ _ ) = false
                  move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
                  ... | (nq , pop )     = move nq T ST
                  ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )


--文脈自由文法



---問題8.1 push down automaton


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