--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/turing.agda	Sun Aug 26 17:48:26 2018 +0900
@@ -0,0 +1,48 @@
+module turing 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 Turing ( Q : Set ) ( Σ : Set  ) 
+       : Set  where
+    field
+        tδ : Q →  Σ → Q × ( PushDown  Σ ) × ( PushDown  Σ )
+        tstart : Q
+        tend : Q → Bool
+        tz0 :  Σ
+    tmoves :  Q → List  Σ → ( Q × List  Σ × List  Σ )
+    tmoves q L = move q L [ pz0 ]
+           where
+              move : Q → ( List  Σ ) → ( List  Σ ) → ( Q × List  Σ × 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 )
+    taccept : List  Σ → Bool
+    taccept 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 )
+
+
+
+