Mercurial > hg > Members > kono > Proof > automaton

annotate agda/pushdown.agda @ 143:f896c112f01f

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 Tue, 29 Dec 2020 15:32:57 +0900
parents b3f05cd08d24
children 26407ce19d66
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module pushdown where
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level renaming ( suc to succ ; zero to Zero )
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.List
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Maybe
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Data.Bool using ( Bool ; true ; false )
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary using (¬_; Dec; yes; no)
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Level renaming ( suc to succ ; zero to Zero )
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Product
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 data PushDown ( Γ : Set ) : Set where
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 pop : PushDown Γ
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 push : Γ → PushDown Γ
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 record PushDownAutomaton ( Q : Set ) ( Σ : Set ) ( Γ : Set )
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 : Set where
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 field
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 pδ : Q → Σ → Γ → Q × ( PushDown Γ )
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
23 pok : Q → Bool
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
24 pempty : Γ
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
25 pmoves : Q → List Γ → Σ → ( Q × List Γ )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
26 pmoves q [] i with pδ q i pempty
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
27 pmoves q [] i | qn , pop = ( qn , [] )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
28 pmoves q [] i | qn , push x = ( qn , ( x ∷ [] ) )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
29 pmoves q ( H ∷ T ) i with pδ q i H
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
30 pmoves q (H ∷ T) i | qn , pop = ( qn , T )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
31 pmoves q (H ∷ T) i | qn , push x = ( qn , ( x ∷ H ∷ T) )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
32
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
33 paccept : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
34 paccept q [] [] = pok q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
35 paccept q ( H ∷ T) [] with pδ q H pempty
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
36 paccept q (H ∷ T) [] | qn , pop = paccept qn T []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
37 paccept q (H ∷ T) [] | qn , push x = paccept qn T (x ∷ [] )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
38 paccept q [] (_ ∷ _ ) = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
39 paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
40 ... | (nq , pop ) = paccept nq T ST
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
41 ... | (nq , push ns ) = paccept nq T ( ns ∷ SH ∷ ST )
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
44 -- 0011
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
45 -- 00000111111
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
46 inputnn : ( n : ℕ ) → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
47 inputnn zero {_} _ _ s = s
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
48 inputnn (suc n) x y s = x ∷ ( inputnn n x y ( y ∷ s ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
49
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
51 data States0 : Set where
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
52 sr : States0
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
54 data In2 : Set where
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
55 i0 : In2
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
56 i1 : In2
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
57
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
58 test0 = inputnn 5 i0 i1 []
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
59
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
60 pnn : PushDownAutomaton States0 In2 States0
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
61 pnn = record {
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
62 pδ = pδ
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
63 ; pempty = sr
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
64 ; pok = λ q → true
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
65 } where
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
66 pδ : States0 → In2 → States0 → States0 × PushDown States0
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
67 pδ sr i0 _ = (sr , push sr)
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
68 pδ sr i1 _ = (sr , pop )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
69
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
70 data States1 : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
71 ss : States1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
72 st : States1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
73
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
74 pn1 : PushDownAutomaton States1 In2 States1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
75 pn1 = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
76 pδ = pδ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
77 ; pempty = ss
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
78 ; pok = pok1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
79 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
80 pok1 : States1 → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
81 pok1 ss = false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
82 pok1 st = true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
83 pδ : States1 → In2 → States1 → States1 × PushDown States1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
84 pδ ss i0 _ = (ss , push ss)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
85 pδ ss i1 _ = (st , pop)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
86 pδ st i0 _ = (st , push ss)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
87 pδ st i1 _ = (st , pop )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
89 test1 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
90 test2 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) []
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
91 test3 = PushDownAutomaton.pmoves pnn sr [] i0
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
92 test4 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
93
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
94 test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
95 test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
96
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
97 test7 : (n : ℕ ) → PushDownAutomaton.paccept pnn sr (inputnn n i0 i1 []) [] ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
98 test7 zero = refl
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
99 test7 (suc n) with test7 n
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
100 ... | t = test7lem [] t where
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
101 test7lem : (x : List States0) → PushDownAutomaton.paccept pnn sr (inputnn n i0 i1 []) x ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
102 → PushDownAutomaton.paccept pnn sr (inputnn n i0 i1 (i1 ∷ [])) (sr ∷ x) ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
103 test7lem x with PushDownAutomaton.paccept pnn sr (inputnn (suc n) i0 i1 []) (sr ∷ x)
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 138
diff changeset
104 ... | t2 = {!!}