--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a08/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,60 @@
+-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 --->
+
+              
+