Mercurial > hg > Members > kono > Proof > automaton

annotate agda/pushdown.agda @ 38:ab265470c2d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
push down automaton example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 12 Dec 2018 17:50:42 +0900
parents 08b589172493
children 7a0634a7c25a
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 Γ )
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 pstart : Q
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
24 pok : Q → Bool
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
25 pempty : Γ
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
26 pmoves : Q → List Γ → Σ → ( Q × List Γ )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
27 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
28 pmoves q [] i | qn , pop = ( qn , [] )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
29 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
30 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
31 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
32 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
33
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
34 paccept : List Σ → Bool
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
35 paccept L = move pstart L []
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 where
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
37 move : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
38 move q [] [] = pok q
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
39 move q ( H ∷ T) [] with pδ q H pempty
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
40 move q (H ∷ T) [] | qn , pop = move qn T []
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
41 move q (H ∷ T) [] | qn , push x = move qn T (x ∷ [] )
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 move q [] (_ ∷ _ ) = false
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 ... | (nq , pop ) = move nq T ST
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST )
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
48 -- 0011
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
49 -- 00000111111
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
50 inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
51 inputnn {zero} {_} _ _ s = s
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
52 inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) )
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 States0 : Set where
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
55 sr : States0
17
08b589172493 add pushdown and turing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
38
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
57 data In2 : Set where
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
58 i0 : In2
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
59 i1 : In2
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
60
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
61 pnn : PushDownAutomaton States0 In2 States0
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
62 pnn = record {
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
63 pδ = pδ
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
64 ; pstart = sr
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
65 ; pempty = sr
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
66 ; pok = λ q → true
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
67 } where
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
68 pδ : States0 → In2 → States0 → States0 × PushDown States0
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
69 pδ sr i0 _ = (sr , push sr)
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
70 pδ sr i1 _ = (sr , pop )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
71
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
72 test1 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
73 test2 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] )
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
74 test3 = PushDownAutomaton.pmoves pnn sr [] i0
ab265470c2d0 push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
75