Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/turing.agda @ 407:c7ad8d2dc157

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe halt.agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 09 Nov 2023 18:04:55 +0900
parents 6f3636fbc481
children
comparison
equal deleted inserted replaced
406:a60132983557 407:c7ad8d2dc157
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2 -- {-# OPTIONS --allow-unsolved-metas #-}
2 module turing where 3 module turing where
3 4
4 open import Level renaming ( suc to succ ; zero to Zero ) 5 open import Level renaming ( suc to succ ; zero to Zero )
5 open import Data.Nat -- hiding ( erase ) 6 open import Data.Nat -- hiding ( erase )
6 open import Data.List 7 open import Data.List
29 -- erase push SL , push tone 30 -- erase push SL , push tone
30 -- none push SL , push SR 31 -- none push SL , push SR
31 -- left push SR , pop 32 -- left push SR , pop
32 -- right pop , push SL 33 -- right pop , push SL
33 34
34 {-# TERMINATING #-}
35 move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) 35 move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
36 move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] )
37 move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R
38 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH 36 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH
39 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT ) 37 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT )
40 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) ) 38 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) )
41 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) ) 39 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) )
42 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT ) 40 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT )
43 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) ) 41 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) )
44 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) ) 42 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) )
45 {-# TERMINATING #-} 43 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) [] with tδ q LH
46 move-loop : {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } 44 ... | nq , write x , left = ( nq , ( tnone ∷ x ∷ LT ) , [] )
45 ... | nq , write x , right = ( nq , LT , ( x ∷ tnone ∷ [] ) )
46 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( tnone ∷ [] ) )
47 ... | nq , wnone , left = ( nq , ( tnone ∷ LH ∷ LT ) , [] )
48 ... | nq , wnone , right = ( nq , LT , ( LH ∷ tnone ∷ [] ) )
49 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( tnone ∷ [] ) )
50 move {Q} {Σ} {tnone} {tδ} q [] ( RH ∷ RT ) with tδ q tnone
51 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ [] ) , RT )
52 ... | nq , write x , right = ( nq , [] , ( x ∷ RH ∷ RT ) )
53 ... | nq , write x , mnone = ( nq , ( x ∷ [] ) , ( RH ∷ RT ) )
54 ... | nq , wnone , left = ( nq , ( RH ∷ tnone ∷ [] ) , RT )
55 ... | nq , wnone , right = ( nq , [] , ( tnone ∷ RH ∷ RT ) )
56 ... | nq , wnone , mnone = ( nq , ( tnone ∷ [] ) , ( RH ∷ RT ) )
57 move {Q} {Σ} {tnone} {tδ} q [] [] with tδ q tnone
58 ... | nq , write x , left = ( nq , ( tnone ∷ x ∷ [] ) , [] )
59 ... | nq , write x , right = ( nq , [] , ( x ∷ tnone ∷ [] ) )
60 ... | nq , write x , mnone = ( nq , ( x ∷ [] ) , ( tnone ∷ [] ) )
61 ... | nq , wnone , left = ( nq , ( tnone ∷ tnone ∷ [] ) , [] )
62 ... | nq , wnone , right = ( nq , [] , ( tnone ∷ tnone ∷ [] ) )
63 ... | nq , wnone , mnone = ( nq , ( tnone ∷ [] ) , ( tnone ∷ [] ) )
64
65 move-loop : (i : ℕ) {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move }
47 → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) 66 → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
48 move-loop {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q 67 move-loop zero {Q} {Σ} {tend} {tnone} {tδ} q L R = ( q , L , R )
68 move-loop (suc i) {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q
49 ... | true = ( q , L , R ) 69 ... | true = ( q , L , R )
50 ... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) 70 ... | flase = move-loop i {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) )
51 where 71 where
52 next = move {Q} {Σ} {tnone} {tδ} q L R 72 next = move {Q} {Σ} {tnone} {tδ} q L R
53 73
54 {-# TERMINATING #-}
55 move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q → Σ → Q × ( Write Σ ) × Move) 74 move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q → Σ → Q × ( Write Σ ) × Move)
56 (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) 75 (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
57 move0 tend tnone tδ q L R with tend q 76 move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH
58 ... | true = ( q , L , R ) 77 ... | nq , write x , left = nq , ( RH ∷ x ∷ LT ) , RT
59 move0 tend tnone tδ q L [] | false = move0 tend tnone tδ q L ( tnone ∷ [] ) 78 ... | nq , write x , right = nq , LT , ( x ∷ RH ∷ RT )
60 move0 tend tnone tδ q [] R | false = move0 tend tnone tδ q ( tnone ∷ [] ) R 79 ... | nq , write x , mnone = nq , ( x ∷ LT ) , ( RH ∷ RT )
61 move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH 80 ... | nq , wnone , left = nq , ( RH ∷ LH ∷ LT ) , RT
62 ... | nq , write x , left = move0 tend tnone tδ nq ( RH ∷ x ∷ LT ) RT 81 ... | nq , wnone , right = nq , LT , ( LH ∷ RH ∷ RT )
63 ... | nq , write x , right = move0 tend tnone tδ nq LT ( x ∷ RH ∷ RT ) 82 ... | nq , wnone , mnone = ( q , ( LH ∷ LT ) , ( RH ∷ RT ) )
64 ... | nq , write x , mnone = move0 tend tnone tδ nq ( x ∷ LT ) ( RH ∷ RT ) 83 move0 tend tnone tδ q ( LH ∷ LT ) [] with tδ q LH
65 ... | nq , wnone , left = move0 tend tnone tδ nq ( RH ∷ LH ∷ LT ) RT 84 ... | nq , write x , left = nq , ( tnone ∷ x ∷ LT ) , []
66 ... | nq , wnone , right = move0 tend tnone tδ nq LT ( LH ∷ RH ∷ RT ) 85 ... | nq , write x , right = nq , LT , ( x ∷ tnone ∷ [] )
67 ... | nq , wnone , mnone = move0 tend tnone tδ nq ( LH ∷ LT ) ( RH ∷ RT ) 86 ... | nq , write x , mnone = nq , ( x ∷ LT ) , ( tnone ∷ [] )
87 ... | nq , wnone , left = nq , ( tnone ∷ LH ∷ LT ) , []
88 ... | nq , wnone , right = nq , LT , ( LH ∷ tnone ∷ [] )
89 ... | nq , wnone , mnone = nq , ( LH ∷ LT ) , ( tnone ∷ [] )
90 move0 tend tnone tδ q [] ( RH ∷ RT ) with tδ q tnone
91 ... | nq , write x , left = nq , ( RH ∷ x ∷ [] ) , RT
92 ... | nq , write x , right = nq , [] , ( x ∷ RH ∷ RT )
93 ... | nq , write x , mnone = nq , ( x ∷ [] ) , ( RH ∷ RT )
94 ... | nq , wnone , left = nq , ( RH ∷ tnone ∷ [] ) , RT
95 ... | nq , wnone , right = nq , [] , ( tnone ∷ RH ∷ RT )
96 ... | nq , wnone , mnone = nq , ( tnone ∷ [] ) , ( RH ∷ RT )
97 move0 tend tnone tδ q [] [] with tδ q tnone
98 ... | nq , write x , left = nq , ( tnone ∷ x ∷ [] ) , []
99 ... | nq , write x , right = nq , [] , ( x ∷ tnone ∷ [] )
100 ... | nq , write x , mnone = nq , ( x ∷ [] ) , ( tnone ∷ [] )
101 ... | nq , wnone , left = nq , ( tnone ∷ tnone ∷ [] ) , []
102 ... | nq , wnone , right = nq , [] , ( tnone ∷ tnone ∷ [] )
103 ... | nq , wnone , mnone = nq , ( tnone ∷ [] ) , ( tnone ∷ [] )
68 104
69 record Turing ( Q : Set ) ( Σ : Set ) 105 record Turing ( Q : Set ) ( Σ : Set )
70 : Set where 106 : Set where
71 field 107 field
72 tδ : Q → Σ → Q × ( Write Σ ) × Move 108 tδ : Q → Σ → Q × ( Write Σ ) × Move
73 tstart : Q 109 tstart : Q
74 tend : Q → Bool 110 tend : Q → Bool
75 tnone : Σ 111 tnone : Σ
76 taccept : List Σ → ( Q × List Σ × List Σ ) 112 taccept : (i : ℕ ) → List Σ → ( Q × List Σ × List Σ )
77 taccept L = move0 tend tnone tδ tstart L [] 113 taccept i L = tloop i tstart [] [] where
114 tloop : (i : ℕ) (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
115 tloop zero q L R = ( q , L , R )
116 tloop (suc i) q L R with tend q
117 ... | true = ( q , L , R )
118 ... | false with move0 tend tnone tδ q L R
119 ... | nq , L , R = tloop i nq L R
78 120
79 open import automaton 121 open import automaton
80 122
81 -- ATuring : {Σ : Set } → Automaton (List Σ) Σ 123 -- ATuring : {Σ : Set } → Automaton (List Σ) Σ
82 -- ATuring = record { δ = {!!} ; aend = {!!} } 124 -- ATuring = record { δ = {!!} ; aend = {!!} }
83 125
84 open import automaton 126 open import automaton
85 open Automaton 127 open Automaton
86 128
87 {-# TERMINATING #-} 129 move1 : {Q Σ : Set } (tnone : Σ ) (δ : Q → Σ → Q ) (tδ : Q → Σ → Write Σ × Move)
88 move1 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (δ : Q → Σ → Q ) (tδ : Q → Σ → Write Σ × Move)
89 (q : Q ) ( L : List Σ ) ( R : List Σ ) → Q × List Σ × List Σ 130 (q : Q ) ( L : List Σ ) ( R : List Σ ) → Q × List Σ × List Σ
90 move1 tend tnone δ tδ q L R with tend q 131 move1 tnone δ tδ q ( LH ∷ LT ) ( RH ∷ RT ) with tδ (δ q LH) LH
91 ... | true = ( q , L , R ) 132 ... | write x , left = (δ q LH) , ( RH ∷ x ∷ LT ) , RT
92 move1 tend tnone δ tδ q L [] | false = move1 tend tnone δ tδ q L ( tnone ∷ [] ) 133 ... | write x , right = (δ q LH) , LT , ( x ∷ RH ∷ RT )
93 move1 tend tnone δ tδ q [] R | false = move1 tend tnone δ tδ q ( tnone ∷ [] ) R 134 ... | write x , mnone = (δ q LH) , ( x ∷ LT ) , ( RH ∷ RT )
94 move1 tend tnone δ tδ q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ (δ q LH) LH 135 ... | wnone , left = (δ q LH) , ( RH ∷ LH ∷ LT ) , RT
95 ... | write x , left = move1 tend tnone δ tδ (δ q LH) ( RH ∷ x ∷ LT ) RT 136 ... | wnone , right = (δ q LH) , LT , ( LH ∷ RH ∷ RT )
96 ... | write x , right = move1 tend tnone δ tδ (δ q LH) LT ( x ∷ RH ∷ RT ) 137 ... | wnone , mnone = (δ q LH) , ( LH ∷ LT ) , ( RH ∷ RT )
97 ... | write x , mnone = move1 tend tnone δ tδ (δ q LH) ( x ∷ LT ) ( RH ∷ RT ) 138 move1 tnone δ tδ q ( LH ∷ LT ) [] with tδ (δ q LH) LH
98 ... | wnone , left = move1 tend tnone δ tδ (δ q LH) ( RH ∷ LH ∷ LT ) RT 139 ... | write x , left = (δ q LH) , ( tnone ∷ x ∷ LT ) , []
99 ... | wnone , right = move1 tend tnone δ tδ (δ q LH) LT ( LH ∷ RH ∷ RT ) 140 ... | write x , right = (δ q LH) , LT , ( x ∷ tnone ∷ [] )
100 ... | wnone , mnone = move1 tend tnone δ tδ (δ q LH) ( LH ∷ LT ) ( RH ∷ RT ) 141 ... | write x , mnone = (δ q LH) , ( x ∷ LT ) , ( tnone ∷ [] )
142 ... | wnone , left = (δ q LH) , ( tnone ∷ LH ∷ LT ) , []
143 ... | wnone , right = (δ q LH) , LT , ( LH ∷ tnone ∷ [] )
144 ... | wnone , mnone = (δ q LH) , ( LH ∷ LT ) , ( tnone ∷ [] )
145 move1 tnone δ tδ q [] ( RH ∷ RT ) with tδ (δ q tnone) tnone
146 ... | write x , left = (δ q tnone) , ( RH ∷ x ∷ [] ) , RT
147 ... | write x , right = (δ q tnone) , [] , ( x ∷ RH ∷ RT )
148 ... | write x , mnone = (δ q tnone) , ( x ∷ [] ) , ( RH ∷ RT )
149 ... | wnone , left = (δ q tnone) , ( RH ∷ tnone ∷ [] ) , RT
150 ... | wnone , right = (δ q tnone) , [] , ( tnone ∷ RH ∷ RT )
151 ... | wnone , mnone = (δ q tnone) , ( tnone ∷ [] ) , ( RH ∷ RT )
152 move1 tnone δ tδ q [] [] with tδ (δ q tnone) tnone
153 ... | write x , left = (δ q tnone) , ( tnone ∷ x ∷ [] ) , []
154 ... | write x , right = (δ q tnone) , [] , ( x ∷ tnone ∷ [] )
155 ... | write x , mnone = (δ q tnone) , ( x ∷ [] ) , ( tnone ∷ [] )
156 ... | wnone , left = (δ q tnone) , ( tnone ∷ tnone ∷ [] ) , []
157 ... | wnone , right = (δ q tnone) , [] , ( tnone ∷ tnone ∷ [] )
158 ... | wnone , mnone = (δ q tnone) , ( tnone ∷ [] ) , ( tnone ∷ [] )
101 159
102 record TM ( Q : Set ) ( Σ : Set ) 160 record TM ( Q : Set ) ( Σ : Set )
103 : Set where 161 : Set where
104 field 162 field
105 automaton : Automaton Q Σ 163 automaton : Automaton Q Σ
106 tδ : Q → Σ → Write Σ × Move 164 tδ : Q → Σ → Write Σ × Move
107 tnone : Σ 165 tnone : Σ
108 taccept : Q → List Σ → ( Q × List Σ × List Σ ) 166 taccept : (i : ℕ) → Q → List Σ → ( Q × List Σ × List Σ )
109 taccept q L = move1 (aend automaton) tnone (δ automaton) tδ q L [] 167 taccept i q L = tloop i q L [] where
168 tloop : (i : ℕ) → (q : Q ) ( L : List Σ ) ( R : List Σ ) → Q × List Σ × List Σ
169 tloop i q L R with aend automaton q
170 ... | true = ( q , L , R )
171 tloop zero q L R | false = ( q , L , R )
172 tloop (suc i) q L R | false with move1 tnone (δ automaton) tδ q L R
173 ... | q' , L' , R' = tloop i q' L' R'
110 174
111 data CopyStates : Set where 175 data CopyStates : Set where
112 s1 : CopyStates 176 s1 : CopyStates
113 s2 : CopyStates 177 s2 : CopyStates
114 s3 : CopyStates 178 s3 : CopyStates
151 tend : CopyStates → Bool 215 tend : CopyStates → Bool
152 tend H = true 216 tend H = true
153 tend _ = false 217 tend _ = false
154 218
155 test1 : CopyStates × ( List ℕ ) × ( List ℕ ) 219 test1 : CopyStates × ( List ℕ ) × ( List ℕ )
156 test1 = Turing.taccept copyMachine ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) 220 test1 = Turing.taccept copyMachine 10 ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] )
157 221
158 test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ ) 222 test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ )
159 test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) [] 223 test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) []
160 where 224 where
161 loop : ℕ → CopyStates → ( List ℕ ) → ( List ℕ ) → CopyStates × ( List ℕ ) × ( List ℕ ) 225 loop : ℕ → CopyStates → ( List ℕ ) → ( List ℕ ) → CopyStates × ( List ℕ ) × ( List ℕ )