Mercurial > hg > Members > kono > Proof > automaton
changeset 139:3be1afb87f82
add utm
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 14 Mar 2020 17:34:54 +0900 |
| parents | 7a0634a7c25a |
| children | 4c3fbfde1bc2 |
| files | a02/agda/data1.agda a02/agda/equality.agda a02/agda/lambda.agda a02/agda/practice-logic.agda a02/lecture.ind a13/smv/test10.smv agda/omega-automaton.agda agda/turing.agda agda/utm.agda |
| diffstat | 9 files changed, 324 insertions(+), 62 deletions(-) [+] |
line wrap: on
line diff
--- a/a02/agda/data1.agda Wed Dec 18 17:34:15 2019 +0900 +++ b/a02/agda/data1.agda Sat Mar 14 17:34:54 2020 +0900 @@ -5,16 +5,16 @@ p2 : B → A ∨ B ex1 : {A B : Set} → A → ( A ∨ B ) -ex1 = ? +ex1 = {!!} ex2 : {A B : Set} → B → ( A ∨ B ) -ex2 = ? +ex2 = {!!} ex3 : {A B : Set} → ( A ∨ A ) → A -ex3 = ? +ex3 = {!!} ex4 : {A B C : Set} → A ∨ ( B ∨ C ) → ( A ∨ B ) ∨ C -ex4 = ? +ex4 = {!!} record _∧_ A B : Set where field @@ -58,5 +58,21 @@ ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) +data ⊥ : Set where + +⊥-elim : {A : Set } -> ⊥ -> A +⊥-elim () + +¬_ : Set → Set +¬ A = A → ⊥ +data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where + direct : E x y -> connected E x y + indirect : { z : V } -> E x z -> connected {V} E z y -> connected E x y + +dag : { V : Set } ( E : V -> V -> Set ) -> Set +dag {V} E = ∀ (n : V) → ¬ ( connected E n n ) + +lemma : ¬ (dag 3Ring ) +lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 )))
--- a/a02/agda/equality.agda Wed Dec 18 17:34:15 2019 +0900 +++ b/a02/agda/equality.agda Sat Mar 14 17:34:54 2020 +0900 @@ -16,5 +16,11 @@ ex4 : {A B : Set} {x y : A } { f : A → B } → x == y → f x == f y ex4 = {!!} +subst : {A : Set } → { x y : A } → ( f : A → Set ) → x == y → f x → f y +subst {A} {x} {y} f refl fx = fx + +ex5 : {A : Set} {x y z : A } → x == y → y == z → x == z +ex5 {A} {x} {y} {z} x==y y==z = subst {!!} {!!} {!!} +
--- a/a02/agda/lambda.agda Wed Dec 18 17:34:15 2019 +0900 +++ b/a02/agda/lambda.agda Sat Mar 14 17:34:54 2020 +0900 @@ -7,6 +7,11 @@ lemma2 : (A : Set ) → A → A lemma2 A a = {!!} +→intro : {A B : Set } → A → B → ( A → B ) +→intro _ b = λ x → b + +→elim : {A B : Set } → A → ( A → B ) → B +→elim a f = f a ex1 : {A B : Set} → Set ex1 {A} {B} = ( A → B ) → A → B
--- a/a02/agda/practice-logic.agda Wed Dec 18 17:34:15 2019 +0900 +++ b/a02/agda/practice-logic.agda Sat Mar 14 17:34:54 2020 +0900 @@ -7,7 +7,7 @@ postulate b : B lemma0 : A -> B -lemma0 = {!!} +lemma0 a = b id : { A : Set } → ( A → A ) id = {!!} @@ -23,7 +23,7 @@ Lemma1 = A -> ( A -> B ) -> B lemma1 : Lemma1 -lemma1 a b = {!!} +lemma1 a f = f a -- lemma1 a a-b = a-b a
--- a/a02/lecture.ind Wed Dec 18 17:34:15 2019 +0900 +++ b/a02/lecture.ind Sat Mar 14 17:34:54 2020 +0900 @@ -1,7 +1,7 @@ -title: 証明と関数型言語、Agda 問題は、メールでSubjectを (a01 の 問題2.5ならば) - Subject: Report on Automan Lecture 2.5 + Subject: Report on Automaton Lecture 2.5 として、問題毎に提出すること。 kono@ie.u-ryukyu.ac.jp まで送ること。
--- a/a13/smv/test10.smv Wed Dec 18 17:34:15 2019 +0900 +++ b/a13/smv/test10.smv Sat Mar 14 17:34:54 2020 +0900 @@ -8,4 +8,4 @@ y=7: next(y)=0; TRUE : next(y) = ((y + 1) mod 16); esac -LTLSPEC G ( y=4 -> X y=6 ) +LTLSPEC G ( y=4 -> X y=5 )
--- a/agda/omega-automaton.agda Wed Dec 18 17:34:15 2019 +0900 +++ b/agda/omega-automaton.agda Sat Mar 14 17:34:54 2020 +0900 @@ -4,23 +4,24 @@ open import Data.Nat open import Data.List open import Data.Maybe -open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate ) +-- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) renaming ( not to negate ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Nullary using (not_; Dec; yes; no) open import Data.Empty +open import logic open import automaton open Automaton -ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → ℕ → ( ℕ → Σ ) → Q -ω-run Ω zero s = astart Ω -ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n ) +ω-run : { Q Σ : Set } → (Ω : Automaton Q Σ ) → (astart : Q ) → ℕ → ( ℕ → Σ ) → Q +ω-run Ω x zero s = x +ω-run Ω x (suc n) s = δ Ω (ω-run Ω ? n s) ( s n ) record Buchi { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where field from : ℕ - stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true + stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω ? n S ) ≡ true open Buchi @@ -28,9 +29,9 @@ record Muller { Q Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where field next : (n : ℕ ) → ℕ - infinite : (n : ℕ ) → aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true + infinite : (n : ℕ ) → aend Ω ( ω-run Ω ? (n + (next n)) S ) ≡ true --- ¬ p +-- not p -- ------------> -- [] <> p * [] <> p -- <----------- @@ -53,7 +54,6 @@ ωa1 : Automaton States3 Bool ωa1 = record { δ = transition3 - ; astart = ts* ; aend = mark1 } @@ -65,24 +65,23 @@ flip-seq : ℕ → Bool flip-seq zero = false -flip-seq (suc n) = negate ( flip-seq n ) +flip-seq (suc n) = not ( flip-seq n ) lemma1 : Buchi ωa1 true-seq lemma1 = record { from = zero ; stay = lem1 } where - lem1 : ( n : ℕ ) → n > zero → aend ωa1 (ω-run ωa1 n true-seq ) ≡ true + lem1 : ( n : ℕ ) → n > zero → aend ωa1 (ω-run ωa1 ? n true-seq ) ≡ true lem1 zero () - lem1 (suc n) (s≤s z≤n) with ω-run ωa1 n true-seq - lem1 (suc n) (s≤s z≤n) | ts* = refl - lem1 (suc n) (s≤s z≤n) | ts = refl + lem1 (suc n) (s≤s z≤n) with ω-run ωa1 ? n true-seq + lem1 (suc n) (s≤s z≤n) | ts* = ? + lem1 (suc n) (s≤s z≤n) | ts = ? ωa2 : Automaton States3 Bool ωa2 = record { δ = transition3 - ; astart = ts* - ; aend = λ x → negate ( mark1 x ) + ; aend = λ x → not ( mark1 x ) } flip-dec : (n : ℕ ) → Dec ( flip-seq n ≡ true ) @@ -90,17 +89,15 @@ flip-dec n | false = no λ () flip-dec n | true = yes refl -flip-dec1 : (n : ℕ ) → flip-seq (suc n) ≡ negate ( flip-seq n ) +flip-dec1 : (n : ℕ ) → flip-seq (suc n) ≡ ( not ( flip-seq n ) ) flip-dec1 n = let open ≡-Reasoning in flip-seq (suc n ) ≡⟨⟩ - negate ( flip-seq n ) + ( not ( flip-seq n ) ) ∎ -flip-dec2 : (n : ℕ ) → ¬ flip-seq (suc n) ≡ flip-seq n -flip-dec2 n neq with flip-seq n -flip-dec2 n () | false -flip-dec2 n () | true +flip-dec2 : (n : ℕ ) → not flip-seq (suc n) ≡ flip-seq n +flip-dec2 n = ? record flipProperty : Set where
--- a/agda/turing.agda Wed Dec 18 17:34:15 2019 +0900 +++ b/agda/turing.agda Sat Mar 14 17:34:54 2020 +0900 @@ -1,7 +1,8 @@ +{-# OPTIONS --allow-unsolved-metas #-} module turing where open import Level renaming ( suc to succ ; zero to Zero ) -open import Data.Nat hiding ( erase ) +open import Data.Nat -- hiding ( erase ) open import Data.List open import Data.Maybe open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate ) @@ -30,7 +31,7 @@ -- right pop , push SL {-# TERMINATING #-} -move : {Q Σ : Set } → { tone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) +move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] ) move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH @@ -41,12 +42,28 @@ ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) ) ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) ) {-# TERMINATING #-} -move-loop : {Q Σ : Set } → {tend : Q → Bool} → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) -move-loop {Q} {Σ} {tend} q L R with tend q +move-loop : {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } + → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) +move-loop {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q ... | true = ( q , L , R ) -... | flase = move-loop {Q} {Σ} {tend} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) +... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) where - next = move {Q} {Σ} {{!!}} {{!!}} q L R + next = move {Q} {Σ} {tnone} {tδ} q L R + +{-# TERMINATING #-} +move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q → Σ → Q × ( Write Σ ) × Move) + (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) +move0 tend tnone tδ q L R with tend q +... | true = ( q , L , R ) +move0 tend tnone tδ q L [] | false = move0 tend tnone tδ q L ( tnone ∷ [] ) +move0 tend tnone tδ q [] R | false = move0 tend tnone tδ q ( tnone ∷ [] ) R +move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH +... | nq , write x , left = move0 tend tnone tδ nq ( RH ∷ x ∷ LT ) RT +... | nq , write x , right = move0 tend tnone tδ nq LT ( x ∷ RH ∷ RT ) +... | nq , write x , mnone = move0 tend tnone tδ nq ( x ∷ LT ) ( RH ∷ RT ) +... | nq , wnone , left = move0 tend tnone tδ nq ( RH ∷ LH ∷ LT ) RT +... | nq , wnone , right = move0 tend tnone tδ nq LT ( LH ∷ RH ∷ RT ) +... | nq , wnone , mnone = move0 tend tnone tδ nq ( LH ∷ LT ) ( RH ∷ RT ) record Turing ( Q : Set ) ( Σ : Set ) : Set where @@ -55,21 +72,8 @@ tstart : Q tend : Q → Bool tnone : Σ - {-# TERMINATING #-} - move0 : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) - move0 q L R with tend q - ... | true = ( q , L , R ) - move0 q L [] | false = move0 q L ( tnone ∷ [] ) - move0 q [] R | false = move0 q ( tnone ∷ [] ) R - move0 q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH - ... | nq , write x , left = move0 nq ( RH ∷ x ∷ LT ) RT - ... | nq , write x , right = move0 nq LT ( x ∷ RH ∷ RT ) - ... | nq , write x , mnone = move0 nq ( x ∷ LT ) ( RH ∷ RT ) - ... | nq , wnone , left = move0 nq ( RH ∷ LH ∷ LT ) RT - ... | nq , wnone , right = move0 nq LT ( LH ∷ RH ∷ RT ) - ... | nq , wnone , mnone = move0 nq ( LH ∷ LT ) ( RH ∷ RT ) taccept : List Σ → ( Q × List Σ × List Σ ) - taccept L = move0 tstart L [] + taccept L = move0 tend tnone tδ tstart L [] data CopyStates : Set where s1 : CopyStates @@ -81,18 +85,18 @@ 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δ 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 copyMachine : Turing CopyStates ℕ copyMachine = record {
--- /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 + ０ : utmΣ + １ : 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 ０ = read4 , write ０ , left +utmδ read3 １ = read5 , write １ , left +utmδ read3 b = read6 , write b , left +utmδ read4 ＠ = loc0 , write ０ , right +utmδ read4 x = read4 , write x , left +utmδ read5 ＠ = loc0 , write １ , right +utmδ read5 x = read5 , write x , left +utmδ read6 ＠ = loc0 , write B , right +utmδ read6 x = read6 , write x , left +utmδ loc0 ０ = loc0 , write X , left +utmδ loc0 １ = 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 ０ , right +utmδ loc1 Y = loc3 , write １ , right +utmδ loc1 Z = loc4 , write B , right +utmδ loc1 * = fetch0 , write * , right +utmδ loc1 x = loc1 , write x , right +utmδ loc2 ０ = loc5 , write X , right +utmδ loc2 １ = loc6 , write Y , right +utmδ loc2 B = loc6 , write Z , right +utmδ loc2 x = loc2 , write x , right +utmδ loc3 １ = loc5 , write Y , right +utmδ loc3 ０ = 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 ０ = loc6 , write X , right +utmδ loc4 １ = 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 ０ = fetch1 , write X , left +utmδ fetch0 １ = 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 ０ = fetch7 , write X , right +utmδ fetch4 １ = 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 ０ = fetch7 , write Y , right +utmδ fetch5 １ = 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 ０ = fetch7 , write Z , right +utmδ fetch6 １ = 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 ０ , left +utmδ print5 x = print7 , write １ , 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 ０ = mov4 , write ^ , right +utmδ mov2 １ = mov5 , write ^ , right +utmδ mov2 B = mov6 , write ^ , right +utmδ mov3 ０ = mov4 , write ^ , left +utmδ mov3 １ = mov5 , write ^ , left +utmδ mov3 B = mov6 , write ^ , left +utmδ mov4 ^ = tidy0 , write ０ , left +utmδ mov5 ^ = tidy0 , write １ , left +utmδ mov6 ^ = tidy0 , write B , left +utmδ tidy0 $ = tidy1 , write $ , left +utmδ tidy0 x = tidy0 , write x , left +utmδ tidy1 X = tidy1 , write ０ , left +utmδ tidy1 Y = tidy1 , write １ , 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 = + ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷ -- s1 0 = H , wnone , mnone + * ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ -- s1 1 = s2 , write 0 , right + * ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ -- s2 0 = s3 , write 0 , right + * ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ -- s2 1 = s2 , write 1 , right + * ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ -- s3 0 = s4 , write 1 , left + * ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ -- s3 1 = s3 , write 1 , right + * ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ -- s4 0 = s5 , write 0 , left + * ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ -- s4 1 = s4 , write 1 , left + * ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ -- s5 0 = s1 , write 1 , right + * ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ -- s5 1 = s5 , write 1 , left + [] + + +input-encode : List utmΣ +input-encode = １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ [] + +input+Copyδ : List utmΣ +input+Copyδ = ( $ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷ * ∷ [] ) -- 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Σ} {０} {utmδ} q L R + ... | nq , nL , nR = loop n nq nL nR + +t1 = utm-test2 10