--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/pushdown.agda	Sun Aug 26 17:48:26 2018 +0900
@@ -0,0 +1,47 @@
+module pushdown where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Nat
+open import Data.List
+open import Data.Maybe
+open import Data.Bool using ( Bool ; true ; false )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Product
+
+
+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 )
+
+
+
+