Mercurial > hg > Members > kono > Proof > automaton
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