push donwオートマトンと文法クラス
Menu任意の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 を停止することが分かっているアルゴリズムで決めれば良い。