diff agda/utm.agda @ 139:3be1afb87f82

add utm
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Mar 2020 17:34:54 +0900
parents
children 4c3fbfde1bc2
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/utm.agda	Sat Mar 14 17:34:54 2020 +0900
@@ -0,0 +1,234 @@
+module utm where
+
+open import turing
+open import Data.Product
+open import Data.Bool
+open import Data.List
+open import Data.Nat
+
+data utmStates : Set where
+     read0 : utmStates
+     read1 : utmStates
+     read2 : utmStates
+     read3 : utmStates
+     read4 : utmStates
+     read5 : utmStates
+     read6 : utmStates
+     
+     loc0 : utmStates
+     loc1 : utmStates
+     loc2 : utmStates
+     loc3 : utmStates
+     loc4 : utmStates
+     loc5 : utmStates
+     loc6 : utmStates
+     
+     fetch0 : utmStates
+     fetch1 : utmStates
+     fetch2 : utmStates
+     fetch3 : utmStates
+     fetch4 : utmStates
+     fetch5 : utmStates
+     fetch6 : utmStates
+     fetch7 : utmStates
+     
+     print0 : utmStates
+     print1 : utmStates
+     print2 : utmStates
+     print3 : utmStates
+     print4 : utmStates
+     print5 : utmStates
+     print6 : utmStates
+     print7 : utmStates
+     
+     mov0 : utmStates
+     mov1 : utmStates
+     mov2 : utmStates
+     mov3 : utmStates
+     mov4 : utmStates
+     mov5 : utmStates
+     mov6 : utmStates
+     
+     tidy0 : utmStates
+     tidy1 : utmStates
+     halt : utmStates
+
+data utmΣ : Set where
+    0 : utmΣ
+    1 : utmΣ
+    B : utmΣ
+    * : utmΣ
+    $ : utmΣ
+    ^ : utmΣ
+    X : utmΣ
+    Y : utmΣ
+    Z : utmΣ
+    @ : utmΣ
+    b : utmΣ
+
+utmδ :  utmStates →  utmΣ  → utmStates × (Write utmΣ) × Move
+utmδ read0  * = read1 , write * , left
+utmδ read0  x = read0 , write x , right
+utmδ read1  x = read2 , write @ , right
+utmδ read2  ^ = read3 , write ^ , right
+utmδ read2  x = read2 , write x , right
+utmδ read3  0 = read4 , write 0 , left
+utmδ read3  1 = read5 , write 1 , left
+utmδ read3  b = read6 , write b , left
+utmδ read4  @ = loc0 , write 0 , right
+utmδ read4  x = read4 , write x , left
+utmδ read5  @ = loc0 , write 1 , right
+utmδ read5  x = read5 , write x , left
+utmδ read6  @ = loc0 , write B , right
+utmδ read6  x = read6 , write x , left
+utmδ loc0  0 = loc0 , write X , left
+utmδ loc0  1 = loc0 , write Y , left
+utmδ loc0  B = loc0 , write Z , left
+utmδ loc0  $ = loc1 , write $ , right
+utmδ loc0  x = loc0 , write x , left
+utmδ loc1  X = loc2 , write 0 , right
+utmδ loc1  Y = loc3 , write 1 , right
+utmδ loc1  Z = loc4 , write B , right
+utmδ loc1  * = fetch0 , write * , right
+utmδ loc1  x = loc1 , write x , right
+utmδ loc2  0 = loc5 , write X , right
+utmδ loc2  1 = loc6 , write Y , right
+utmδ loc2  B = loc6 , write Z , right
+utmδ loc2  x = loc2 , write x , right
+utmδ loc3  1 = loc5 , write Y , right
+utmδ loc3  0 = loc6 , write X , right
+utmδ loc3  B = loc6 , write Z , right
+utmδ loc3  x = loc3 , write x , right
+utmδ loc4  B = loc5 , write Z , right
+utmδ loc4  0 = loc6 , write X , right
+utmδ loc4  1 = loc6 , write Y , right
+utmδ loc4  x = loc4 , write x , right
+utmδ loc5  $ = loc1 , write $ , right
+utmδ loc5  x = loc5 , write x , left
+utmδ loc6  $ = halt , write $ , right
+utmδ loc6  * = loc0 , write * , left
+utmδ loc6  x = loc6 , write x , right
+utmδ fetch0  0 = fetch1 , write X , left
+utmδ fetch0  1 = fetch2 , write Y , left
+utmδ fetch0  B = fetch3 , write Z , left
+utmδ fetch0  x = fetch0 , write x , right
+utmδ fetch1  $ = fetch4 , write $ , right
+utmδ fetch1  x = fetch1 , write x , left
+utmδ fetch2  $ = fetch5 , write $ , right
+utmδ fetch2  x = fetch2 , write x , left
+utmδ fetch3  $ = fetch6 , write $ , right
+utmδ fetch3  x = fetch3 , write x , left
+utmδ fetch4  0 = fetch7 , write X , right
+utmδ fetch4  1 = fetch7 , write X , right
+utmδ fetch4  B = fetch7 , write X , right
+utmδ fetch4  * = print0 , write * , left
+utmδ fetch4  x = fetch4 , write x , right
+utmδ fetch5  0 = fetch7 , write Y , right
+utmδ fetch5  1 = fetch7 , write Y , right
+utmδ fetch5  B = fetch7 , write Y , right
+utmδ fetch5  * = print0 , write * , left
+utmδ fetch5  x = fetch5 , write x , right
+utmδ fetch6  0 = fetch7 , write Z , right
+utmδ fetch6  1 = fetch7 , write Z , right
+utmδ fetch6  B = fetch7 , write Z , right
+utmδ fetch6  * = print0 , write * , left
+utmδ fetch6  x = fetch6 , write x , right
+utmδ fetch7  * = fetch0 , write * , right
+utmδ fetch7  x = fetch7 , write x , right
+utmδ print0  X = print1 , write X , right
+utmδ print0  Y = print2 , write Y , right
+utmδ print0  Z = print3 , write Z , right
+utmδ print1  ^ = print4 , write ^ , right
+utmδ print1  x = print1 , write x , right
+utmδ print2  ^ = print5 , write ^ , right
+utmδ print2  x = print2 , write x , right
+utmδ print3  ^ = print6 , write ^ , right
+utmδ print3  x = print3 , write x , right
+utmδ print4  x = print7 , write 0 , left
+utmδ print5  x = print7 , write 1 , left
+utmδ print6  x = print7 , write B , left
+utmδ print7  X = mov0 , write X , right
+utmδ print7  Y = mov1 , write Y , right
+utmδ print7  x = print7 , write x , left
+utmδ mov0  ^ = mov2 , write ^ , left
+utmδ mov0  x = mov0 , write x , right
+utmδ mov1  ^ = mov3 , write ^ , right
+utmδ mov1  x = mov1 , write x , right
+utmδ mov2  0 = mov4 , write ^ , right
+utmδ mov2  1 = mov5 , write ^ , right
+utmδ mov2  B = mov6 , write ^ , right
+utmδ mov3  0 = mov4 , write ^ , left
+utmδ mov3  1 = mov5 , write ^ , left
+utmδ mov3  B = mov6 , write ^ , left
+utmδ mov4  ^ = tidy0 , write 0 , left
+utmδ mov5  ^ = tidy0 , write 1 , left
+utmδ mov6  ^ = tidy0 , write B , left
+utmδ tidy0  $ = tidy1 , write $ , left
+utmδ tidy0  x = tidy0 , write x , left
+utmδ tidy1  X = tidy1 , write 0 , left
+utmδ tidy1  Y = tidy1 , write 1 , left
+utmδ tidy1  Z = tidy1 , write B , left
+utmδ tidy1  $ = read0 , write $ , right
+utmδ tidy1  x = tidy1 , write x , left
+utmδ _  x = halt , write x , mnone
+
+U-TM : Turing utmStates utmΣ
+U-TM = record {
+        tδ = utmδ
+     ;  tstart = read0
+     ;  tend = tend
+     ;  tnone =  b
+  } where
+      tend : utmStates →  Bool
+      tend halt = true
+      tend _ = false
+
+-- Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move
+-- Copyδ s1 0  = H    , wnone       , mnone
+-- Copyδ s1 1  = s2   , write 0 , right
+-- Copyδ s2 0  = s3   , write 0 , right
+-- Copyδ s2 1  = s2   , write 1 , right
+-- Copyδ s3 0  = s4   , write 1 , left
+-- Copyδ s3 1  = s3   , write 1 , right
+-- Copyδ s4 0  = s5   , write 0 , left
+-- Copyδ s4 1  = s4   , write 1 , left
+-- Copyδ s5 0  = s1   , write 1 , right
+-- Copyδ s5 1  = s5   , write 1 , left
+-- Copyδ H  _  = H    , wnone   , mnone
+-- Copyδ _  (suc (suc _))      = H    , wnone       , mnone
+
+Copyδ-encode : List utmΣ
+Copyδ-encode = 
+       0  ∷ 0  ∷ 1  ∷ 0  ∷  1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ 0 ∷   -- s1 0  = H    , wnone       , mnone
+  *  ∷ 0  ∷ 0  ∷ 1  ∷ 1  ∷  0 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ 1 ∷   -- s1 1  = s2   , write 0 , right
+  *  ∷ 0  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ 1 ∷ 1 ∷ 0 ∷ 0 ∷ 1 ∷   -- s2 0  = s3   , write 0 , right
+  *  ∷ 0  ∷ 1  ∷ 0  ∷ 1  ∷  0 ∷ 1 ∷ 0 ∷ 1 ∷ 0 ∷ 1 ∷   -- s2 1  = s2   , write 1 , right
+  *  ∷ 0  ∷ 1  ∷ 1  ∷ 0  ∷  1 ∷ 0 ∷ 0 ∷ 1 ∷ 0 ∷ 0 ∷   -- s3 0  = s4   , write 1 , left
+  *  ∷ 0  ∷ 1  ∷ 1  ∷ 1  ∷  0 ∷ 1 ∷ 1 ∷ 1 ∷ 0 ∷ 1 ∷   -- s3 1  = s3   , write 1 , right
+  *  ∷ 1  ∷ 0  ∷ 0  ∷ 0  ∷  1 ∷ 0 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷   -- s4 0  = s5   , write 0 , left
+  *  ∷ 1  ∷ 0  ∷ 0  ∷ 1  ∷  1 ∷ 0 ∷ 0 ∷ 1 ∷ 0 ∷ 0 ∷   -- s4 1  = s4   , write 1 , left
+  *  ∷ 1  ∷ 0  ∷ 1  ∷ 0  ∷  0 ∷ 0 ∷ 1 ∷ 1 ∷ 0 ∷ 1 ∷   -- s5 0  = s1   , write 1 , right
+  *  ∷ 1  ∷ 0  ∷ 1  ∷ 1  ∷  1 ∷ 0 ∷ 1 ∷ 1 ∷ 0 ∷ 0 ∷   -- s5 1  = s5   , write 1 , left
+  []  
+      
+
+input-encode : List utmΣ
+input-encode =  1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  
+
+input+Copyδ : List utmΣ
+input+Copyδ = ( $  ∷ 0  ∷ 0  ∷  0 ∷  0 ∷  * ∷  [] ) -- start state
+        ++   Copyδ-encode
+        ++ ( $ ∷ ^ ∷ input-encode )
+
+utm-test1 : utmStates × ( List  utmΣ ) × ( List  utmΣ )
+utm-test1 = Turing.taccept U-TM  input+Copyδ
+
+utm-test2 : ℕ  → utmStates × ( List  utmΣ ) × ( List  utmΣ )
+utm-test2 n  = loop n (Turing.tstart U-TM) input+Copyδ []
+  where
+        loop :  ℕ → utmStates → ( List  utmΣ ) → ( List  utmΣ ) → utmStates × ( List  utmΣ ) × ( List  utmΣ )
+        loop zero q L R = ( q , L , R )
+        loop (suc n) q L R with  move {utmStates} {utmΣ} {0} {utmδ} q L R
+        ... | nq , nL , nR = loop n nq nL nR
+
+t1 = utm-test2 10