Mercurial > hg > Members > kono > Proof > automaton1

comparison turing.agda @ 18:e168140d15b0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Nov 2020 19:18:15 +0900
parents
children
comparison
equal deleted inserted replaced
17:5f97e5606e7e 18:e168140d15b0
1 {-# OPTIONS --allow-unsolved-metas #-}
2 module turing where
3
4 open import Level renaming ( suc to succ ; zero to Zero )
5 open import Data.Nat -- hiding ( erase )
6 open import Data.List
7 open import Data.Maybe
8 open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate )
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
10 open import Relation.Nullary using (¬_; Dec; yes; no)
11 open import Level renaming ( suc to succ ; zero to Zero )
12 open import Data.Product
13
14
15 data Write ( Σ : Set ) : Set where
16 write : Σ → Write Σ
17 wnone : Write Σ
18 -- erase write tnone
19
20 data Move : Set where
21 left : Move
22 right : Move
23 mnone : Move
24
25 -- at tδ both stack is poped
26
27 -- write S push S , push SR
28 -- erase push SL , push tone
29 -- none push SL , push SR
30 -- left push SR , pop
31 -- right pop , push SL
32
33 {-# TERMINATING #-}
34 move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
35 move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] )
36 move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R
37 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH
38 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT )
39 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) )
40 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) )
41 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT )
42 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) )
43 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) )
44 {-# TERMINATING #-}
45 move-loop : {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move }
46 → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
47 move-loop {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q
48 ... | true = ( q , L , R )
49 ... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) )
50 where
51 next = move {Q} {Σ} {tnone} {tδ} q L R
52
53 {-# TERMINATING #-}
54 move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q → Σ → Q × ( Write Σ ) × Move)
55 (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
56 move0 tend tnone tδ q L R with tend q
57 ... | true = ( q , L , R )
58 move0 tend tnone tδ q L [] | false = move0 tend tnone tδ q L ( tnone ∷ [] )
59 move0 tend tnone tδ q [] R | false = move0 tend tnone tδ q ( tnone ∷ [] ) R
60 move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH
61 ... | nq , write x , left = move0 tend tnone tδ nq ( RH ∷ x ∷ LT ) RT
62 ... | nq , write x , right = move0 tend tnone tδ nq LT ( x ∷ RH ∷ RT )
63 ... | nq , write x , mnone = move0 tend tnone tδ nq ( x ∷ LT ) ( RH ∷ RT )
64 ... | nq , wnone , left = move0 tend tnone tδ nq ( RH ∷ LH ∷ LT ) RT
65 ... | nq , wnone , right = move0 tend tnone tδ nq LT ( LH ∷ RH ∷ RT )
66 ... | nq , wnone , mnone = move0 tend tnone tδ nq ( LH ∷ LT ) ( RH ∷ RT )
67
68 record Turing ( Q : Set ) ( Σ : Set )
69 : Set where
70 field
71 tδ : Q → Σ → Q × ( Write Σ ) × Move
72 tstart : Q
73 tend : Q → Bool
74 tnone : Σ
75 taccept : List Σ → ( Q × List Σ × List Σ )
76 taccept L = move0 tend tnone tδ tstart L []
77
78 data CopyStates : Set where
79 s1 : CopyStates
80 s2 : CopyStates
81 s3 : CopyStates
82 s4 : CopyStates
83 s5 : CopyStates
84 H : CopyStates
85
86
87 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move
88 Copyδ s1 0 = H , wnone , mnone
89 Copyδ s1 1 = s2 , write 0 , right
90 Copyδ s2 0 = s3 , write 0 , right
91 Copyδ s2 1 = s2 , write 1 , right
92 Copyδ s3 0 = s4 , write 1 , left
93 Copyδ s3 1 = s3 , write 1 , right
94 Copyδ s4 0 = s5 , write 0 , left
95 Copyδ s4 1 = s4 , write 1 , left
96 Copyδ s5 0 = s1 , write 1 , right
97 Copyδ s5 1 = s5 , write 1 , left
98 Copyδ H _ = H , wnone , mnone
99 Copyδ _ (suc (suc _)) = H , wnone , mnone
100
101 copyMachine : Turing CopyStates ℕ
102 copyMachine = record {
103 tδ = Copyδ
104 ; tstart = s1
105 ; tend = tend
106 ; tnone = 0
107 } where
108 tend : CopyStates → Bool
109 tend H = true
110 tend _ = false
111
112 test1 : CopyStates × ( List ℕ ) × ( List ℕ )
113 test1 = Turing.taccept copyMachine ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] )
114
115 test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ )
116 test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) []
117 where
118 loop : ℕ → CopyStates → ( List ℕ ) → ( List ℕ ) → CopyStates × ( List ℕ ) × ( List ℕ )
119 loop zero q L R = ( q , L , R )
120 loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) ) ( proj₂ ( proj₂ t1 ) )
121 where
122 t1 = move {CopyStates} {ℕ} {0} {Copyδ} q L R
123
124 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
125 open import Function.Bijection
126
127 -- turing-stepiwize-eq : {Q1 Q2 : Set} → {S1 S2 : Set} → (t1 : Turing Q1 S1) → (t2 : Turing Q2 S2) → Bijection S1 (List S2) →
128 -- turing-stepiwize-eq = {!!}
129
130 -- turing→01 : Turing {!!} {!!} → Turing {!!} Bool
131 -- turing→01 = {!!}
132