Mercurial > hg > Members > kono > Proof > automaton

comparison agda/turing.agda @ 139:3be1afb87f82

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add utm
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Mar 2020 17:34:54 +0900
parents 964e4bd0272a
children b3f05cd08d24
comparison
equal deleted inserted replaced
138:7a0634a7c25a 139:3be1afb87f82
1 {-# OPTIONS --allow-unsolved-metas #-}
1 module turing where 2 module turing where
2 3
3 open import Level renaming ( suc to succ ; zero to Zero ) 4 open import Level renaming ( suc to succ ; zero to Zero )
4 open import Data.Nat hiding ( erase ) 5 open import Data.Nat -- hiding ( erase )
5 open import Data.List 6 open import Data.List
6 open import Data.Maybe 7 open import Data.Maybe
7 open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate ) 8 open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate )
8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
9 open import Relation.Nullary using (¬_; Dec; yes; no) 10 open import Relation.Nullary using (¬_; Dec; yes; no)
28 -- none push SL , push SR 29 -- none push SL , push SR
29 -- left push SR , pop 30 -- left push SR , pop
30 -- right pop , push SL 31 -- right pop , push SL
31 32
32 {-# TERMINATING #-} 33 {-# TERMINATING #-}
33 move : {Q Σ : Set } → { tone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) 34 move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
34 move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] ) 35 move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] )
35 move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R 36 move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R
36 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH 37 move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH
37 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT ) 38 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT )
38 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) ) 39 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) )
39 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) ) 40 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) )
40 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT ) 41 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT )
41 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) ) 42 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) )
42 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) ) 43 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) )
43 {-# TERMINATING #-} 44 {-# TERMINATING #-}
44 move-loop : {Q Σ : Set } → {tend : Q → Bool} → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) 45 move-loop : {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move }
45 move-loop {Q} {Σ} {tend} q L R with tend q 46 → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
47 move-loop {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q
46 ... | true = ( q , L , R ) 48 ... | true = ( q , L , R )
47 ... | flase = move-loop {Q} {Σ} {tend} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) 49 ... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) )
48 where 50 where
49 next = move {Q} {Σ} {{!!}} {{!!}} q L R 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 )
50 67
51 record Turing ( Q : Set ) ( Σ : Set ) 68 record Turing ( Q : Set ) ( Σ : Set )
52 : Set where 69 : Set where
53 field 70 field
54 tδ : Q → Σ → Q × ( Write Σ ) × Move 71 tδ : Q → Σ → Q × ( Write Σ ) × Move
55 tstart : Q 72 tstart : Q
56 tend : Q → Bool 73 tend : Q → Bool
57 tnone : Σ 74 tnone : Σ
58 {-# TERMINATING #-}
59 move0 : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
60 move0 q L R with tend q
61 ... | true = ( q , L , R )
62 move0 q L [] | false = move0 q L ( tnone ∷ [] )
63 move0 q [] R | false = move0 q ( tnone ∷ [] ) R
64 move0 q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH
65 ... | nq , write x , left = move0 nq ( RH ∷ x ∷ LT ) RT
66 ... | nq , write x , right = move0 nq LT ( x ∷ RH ∷ RT )
67 ... | nq , write x , mnone = move0 nq ( x ∷ LT ) ( RH ∷ RT )
68 ... | nq , wnone , left = move0 nq ( RH ∷ LH ∷ LT ) RT
69 ... | nq , wnone , right = move0 nq LT ( LH ∷ RH ∷ RT )
70 ... | nq , wnone , mnone = move0 nq ( LH ∷ LT ) ( RH ∷ RT )
71 taccept : List Σ → ( Q × List Σ × List Σ ) 75 taccept : List Σ → ( Q × List Σ × List Σ )
72 taccept L = move0 tstart L [] 76 taccept L = move0 tend tnone tδ tstart L []
73 77
74 data CopyStates : Set where 78 data CopyStates : Set where
75 s1 : CopyStates 79 s1 : CopyStates
76 s2 : CopyStates 80 s2 : CopyStates
77 s3 : CopyStates 81 s3 : CopyStates
79 s5 : CopyStates 83 s5 : CopyStates
80 H : CopyStates 84 H : CopyStates
81 85
82 86
83 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move 87 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move
84 Copyδ s1 0 = (H , wnone , mnone ) 88 Copyδ s1 0 = H , wnone , mnone
85 Copyδ s1 1 = (s2 , write 0 , right ) 89 Copyδ s1 1 = s2 , write 0 , right
86 Copyδ s2 0 = (s3 , write 0 , right ) 90 Copyδ s2 0 = s3 , write 0 , right
87 Copyδ s2 1 = (s2 , write 1 , right ) 91 Copyδ s2 1 = s2 , write 1 , right
88 Copyδ s3 0 = (s4 , write 1 , left ) 92 Copyδ s3 0 = s4 , write 1 , left
89 Copyδ s3 1 = (s3 , write 1 , right ) 93 Copyδ s3 1 = s3 , write 1 , right
90 Copyδ s4 0 = (s5 , write 0 , left ) 94 Copyδ s4 0 = s5 , write 0 , left
91 Copyδ s4 1 = (s4 , write 1 , left ) 95 Copyδ s4 1 = s4 , write 1 , left
92 Copyδ s5 0 = (s1 , write 1 , right ) 96 Copyδ s5 0 = s1 , write 1 , right
93 Copyδ s5 1 = (s5 , write 1 , left ) 97 Copyδ s5 1 = s5 , write 1 , left
94 Copyδ H _ = (H , wnone , mnone ) 98 Copyδ H _ = H , wnone , mnone
95 Copyδ _ (suc (suc _)) = (H , wnone , mnone ) 99 Copyδ _ (suc (suc _)) = H , wnone , mnone
96 100
97 copyMachine : Turing CopyStates ℕ 101 copyMachine : Turing CopyStates ℕ
98 copyMachine = record { 102 copyMachine = record {
99 tδ = Copyδ 103 tδ = Copyδ
100 ; tstart = s1 104 ; tstart = s1