Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/extended-automaton.agda @ 392:23db567b4098
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Jul 2023 09:03:13 +0900 |
| parents | 6f3636fbc481 |
| children | af8f630b7e60 |
| rev | line source |
|---|---|
| 139 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 332 | 2 module extended-automaton where |
| 17 | 3 |
| 4 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 139 | 5 open import Data.Nat -- hiding ( erase ) |
| 17 | 6 open import Data.List |
| 164 | 7 open import Data.Maybe hiding ( map ) |
| 318 | 8 -- open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate ) |
| 17 | 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 ) | |
| 164 | 12 open import Data.Product hiding ( map ) |
| 318 | 13 open import logic |
| 17 | 14 |
| 332 | 15 record Automaton ( Q : Set ) ( Σ : Set ) : Set where |
| 16 field | |
| 17 δ : Q → Σ → Q | |
| 18 aend : Q → Bool | |
| 19 | |
| 20 open Automaton | |
| 21 | |
| 22 accept : { Q : Set } { Σ : Set } | |
| 23 → Automaton Q Σ | |
| 24 → Q | |
| 25 → List Σ → Bool | |
| 26 accept M q [] = aend M q | |
| 27 accept M q ( H ∷ T ) = accept M ( δ M q H ) T | |
| 28 | |
| 29 NAutomaton : ( Q : Set ) ( Σ : Set ) → Set | |
| 30 NAutomaton Q Σ = Automaton ( Q → Bool ) Σ | |
| 31 | |
| 32 Naccept : { Q : Set } { Σ : Set } | |
| 33 → Automaton (Q → Bool) Σ | |
| 34 → (exists : ( Q → Bool ) → Bool) | |
| 35 → (Nstart : Q → Bool) → List Σ → Bool | |
| 36 Naccept M exists sb [] = exists ( λ q → sb q /\ aend M sb ) | |
| 37 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( δ M sb i q ) ))) t | |
| 38 | |
| 39 PDA : ( Q : Set ) ( Σ : Set ) → Set | |
| 40 PDA Q Σ = Automaton ( List Q ) Σ | |
| 17 | 41 |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
42 data Write ( Σ : Set ) : Set where |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
43 write : Σ → Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
44 wnone : Write Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
45 -- erase write tnone |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
46 |
| 20 | 47 data Move : Set where |
| 48 left : Move | |
| 49 right : Move | |
| 50 mnone : Move | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
51 |
| 332 | 52 record OTuring ( Q : Set ) ( Σ : Set ) |
| 17 | 53 : Set where |
| 54 field | |
| 20 | 55 tδ : Q → Σ → Q × ( Write Σ ) × Move |
| 17 | 56 tstart : Q |
| 57 tend : Q → Bool | |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
58 tnone : Σ |
|
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
59 taccept : List Σ → ( Q × List Σ × List Σ ) |
| 332 | 60 taccept L = ? |
|
18
6ec8e933ab43
turing wrote but not yet worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
61 |
| 332 | 62 open import bijection |
| 63 | |
| 64 b0 : ( Q : Set ) ( Σ : Set ) → Bijection (List Q) (( Q × ( Write Σ ) × Move ) ∧ ( Q × List Σ × List Σ )) | |
| 65 b0 = ? | |
| 318 | 66 |
| 332 | 67 Turing : ( Q : Set ) ( Σ : Set ) → Set |
| 68 Turing Q Σ = Automaton ( List Q ) Σ | |
| 69 | |
| 70 NDTM : ( Q : Set ) ( Σ : Set ) → Set | |
| 71 NDTM Q Σ = Automaton ( List Q → Bool ) Σ | |
| 318 | 72 |
| 332 | 73 UTM : ( Q : Set ) ( Σ : Set ) → Set |
| 74 UTM Q Σ = Automaton ( List Q ) Σ | |
| 318 | 75 |
| 332 | 76 SuperTM : ( Q : Set ) ( Σ : Set ) → Set |
| 77 SuperTM Q Σ = Automaton ( List Q ) Σ | |
| 17 | 78 |
| 79 | |
| 80 |