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