|
1 A student who is attempting to prove the pumping lemma for regular |
|
2 languages came across the following problem. Suppose a DFA is |
|
3 represented by a record <| init ; trans ; accept |> where |
|
4 |
|
5 init : 'state |
|
6 trans : 'state -> 'symbol -> 'state |
|
7 accept : 'state -> bool |
|
8 |
|
9 Execution of a DFA on a string: |
|
10 |
|
11 (Execute machine [] s = s) |
|
12 (Execute machine (h::t) s = Execute machine t (machine.trans s h)) |
|
13 |
|
14 Language recognized by a machine D: |
|
15 |
|
16 Lang(D) = {x | D.accept (Execute D x D.init)} |
|
17 |
|
18 These are all accepted by HOL with no problem. In then trying to define |
|
19 the |
|
20 set of regular languages, namely those accepted by some DFA, the |
|
21 following |
|
22 is natural to try |
|
23 |
|
24 Regular (L:'symbol list -> bool) = ?D. L = Lang(D) |
|
25 |
|
26 But this fails, since D has two type variables ('state and 'symbol) but |
|
27 Regular is a predicate on 'symbol lists. So the principle of definition |
|
28 rejects. |
|
29 |
|
30 So now my questions. |
|
31 |
|
32 1. Is there a work-around (other than not attempting to define Regular, |
|
33 or defining regularity through some other device, like regular |
|
34 expressions). |
|
35 |
|
36 2. I'm aware that examples of this kind have cropped up from time to |
|
37 time, |
|
38 and I'd like to hear of any others you've encountered. |
|
39 |
|
40 Thanks, |
|
41 Konrad. |
|
42 |
|
43 |
|
44 |
|
45 ----------------------------------------- |
|
46 Hi Konrad, |
|
47 |
|
48 | Regular (L:'symbol list -> bool) = ?D. L = Lang(D) |
|
49 | |
|
50 | But this fails, since D has two type variables ('state and 'symbol) but |
|
51 | Regular is a predicate on 'symbol lists. So the principle of definition |
|
52 | rejects. |
|
53 |
|
54 This is a classic case where adding quantifiers over type variables, as |
|
55 once suggested by Tom Melham, would really help. |
|
56 |
|
57 | 2. I'm aware that examples of this kind have cropped up from time to |
|
58 | time, and I'd like to hear of any others you've encountered. |
|
59 |
|
60 The metatheory of first order logic (this is close to Hasan's example). |
|
61 In the work I reported at TPHOLs'98 I wanted to define the notion of |
|
62 "satisfiable" for first order formulas, but this cannot be done in the |
|
63 straightforward way you'd like. See the end of section 3 of: |
|
64 |
|
65 http://www.cl.cam.ac.uk/users/jrh/papers/model.html |
|
66 |
|
67 | 1. Is there a work-around (other than not attempting to define Regular, |
|
68 | or defining regularity through some other device, like regular |
|
69 | expressions). |
|
70 |
|
71 You could define it over some type you "know" to be adequate, such |
|
72 as numbers (Rob) or equivalence classes of symbol lists (Ching Tsun). |
|
73 Then you could validate the definition by proving that it implies |
|
74 the analogous thing over any type. In first-order logic, this was |
|
75 precisely one of the key things I wanted to prove anyway (the |
|
76 downward Loewenheim-Skolem theorem) so it wasn't wasted effort. |
|
77 |
|
78 |- (?M:(A)model. M satisfies p) ==> (?M:(num)model. M satisfies p) |
|
79 |
|
80 Where "A" is a type variable. That's an abstraction of the actual |
|
81 statement proved, which is given towards the end of section 4. |
|
82 |
|
83 John. |
|
84 |
|
85 ----------------------------------------------------- |
|
86 |
|
87 On Apr 21, 2005, at 1:10 PM, Rob Arthan wrote: |
|
88 >> |
|
89 >> So now my questions. |
|
90 >> |
|
91 >> 1. Is there a work-around (other than not attempting to define |
|
92 >> Regular, |
|
93 >> or defining regularity through some other device, like regular |
|
94 >> expressions). |
|
95 > |
|
96 > I was going to say: instantiate 'state to num in the definition - |
|
97 > after all, DFAs only have finitely many states so the states can |
|
98 > always be represented by numbers. |
|
99 |
|
100 Good idea. |
|
101 |
|
102 > |
|
103 > But your student's definitions don't captured the tiniteness |
|
104 > requirement. And they need to! As things stand every language L is |
|
105 > regular via the machine with states being lists of symbols and with |
|
106 > |
|
107 > init = [] |
|
108 > trans st sym = st @ [sym] |
|
109 > accept = L |
|
110 |
|
111 Good example, sorry about my shoddy presentation: I gave an overly |
|
112 simplified |
|
113 version. A better version would be something like the following: |
|
114 |
|
115 Hol_datatype `dfa = <| states : 'a -> bool ; |
|
116 symbols : 'b -> bool ; |
|
117 init : 'a ; |
|
118 trans : 'a->'b->'a ; |
|
119 accept : 'a -> bool |>`; |
|
120 |
|
121 Define |
|
122 `DFA(M) = |
|
123 FINITE M.states /\ |
|
124 FINITE M.symbols /\ |
|
125 ~(M.states = {}) /\ |
|
126 ~(M.symbols = {}) /\ |
|
127 M.accept SUBSET M.states /\ |
|
128 M.init IN M.states /\ |
|
129 !(a:'symbol) (s:'state). |
|
130 a IN M.symbols /\ s IN M.states ==> (M.trans s a) IN |
|
131 M.states`; |
|
132 |
|
133 |
|
134 Define `(Exec D [] s = s) /\ |
|
135 (Exec D (h::t) s = Exec D t (D.trans s h))`; |
|
136 |
|
137 Define `Lang D = {x | D.accept (Exec D x D.init)}`; |
|
138 |
|
139 (* Urk! *) |
|
140 |
|
141 Define `Regular L = ?D::DFA. L = Lang D`; |
|
142 |
|
143 > |
|
144 > if you take account of finiteness properly, then instantiating 'state |
|
145 > to num will give the right answer.; And it gives another proof |
|
146 > opportunity! (Namely to prove that the instantiated definition is |
|
147 > equivalent to the definition you really wanted). |
|
148 |
|
149 That's a nice bit of spin: a proof opportunity! |
|
150 |
|
151 > |
|
152 >> |
|
153 >> 2. I'm aware that examples of this kind have cropped up from time to |
|
154 >> time, |
|
155 >> and I'd like to hear of any others you've encountered. |
|
156 >> |
|
157 > |
|
158 > Free algebraic structures provide a vast set of examples. |
|
159 > |
|
160 > |
|
161 Very interesting. Can you give some specific examples? |
|
162 |
|
163 Thanks, |
|
164 Konrad. |
|
165 |