|
1 \documentclass{article} |
|
2 \usepackage[utf8]{inputenc} |
|
3 \usepackage[english]{babel} |
|
4 \usepackage{listings} |
|
5 \usepackage{amsthm} |
|
6 \usepackage[margin=0.5in]{geometry} |
|
7 |
|
8 \theoremstyle{theorem} |
|
9 \newtheorem{theorem}{Theorem} |
|
10 |
|
11 \theoremstyle{lemma} |
|
12 \newtheorem{lemma}{Lemma} |
|
13 |
|
14 \theoremstyle{definition} |
|
15 \newtheorem{definition}{Definition} |
|
16 \begin{document} |
|
17 This is a sketch proof for the correctness of the algorithm ders\_simp. |
|
18 \section{Function Definitions} |
|
19 |
|
20 \begin{definition}{Bits} |
|
21 \begin{verbatim} |
|
22 abstract class Bit |
|
23 case object Z extends Bit |
|
24 case object S extends Bit |
|
25 case class C(c: Char) extends Bit |
|
26 |
|
27 type Bits = List[Bit] |
|
28 \end{verbatim} |
|
29 \end{definition} |
|
30 |
|
31 \begin{definition}{Annotated Regular Expressions} |
|
32 \begin{verbatim} |
|
33 abstract class ARexp |
|
34 case object AZERO extends ARexp |
|
35 case class AONE(bs: Bits) extends ARexp |
|
36 case class ACHAR(bs: Bits, f: Char) extends ARexp |
|
37 case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp |
|
38 case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp |
|
39 case class ASTAR(bs: Bits, r: ARexp) extends ARexp |
|
40 \end{verbatim} |
|
41 \end{definition} |
|
42 |
|
43 \begin{definition}{bnullable} |
|
44 \begin{verbatim} |
|
45 def bnullable (r: ARexp) : Boolean = r match { |
|
46 case AZERO => false |
|
47 case AONE(_) => true |
|
48 case ACHAR(_,_) => false |
|
49 case AALTS(_, rs) => rs.exists(bnullable) |
|
50 case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2) |
|
51 case ASTAR(_, _) => true |
|
52 } |
|
53 \end{verbatim} |
|
54 \end{definition} |
|
55 |
|
56 \begin{definition}{ders\_simp} |
|
57 \begin{verbatim} |
|
58 def ders_simp(r: ARexp, s: List[Char]): ARexp = { |
|
59 s match { |
|
60 case Nil => r |
|
61 case c::cs => ders_simp(bsimp(bder(c, r)), cs) |
|
62 } |
|
63 }\end{verbatim} |
|
64 \end{definition} |
|
65 |
|
66 \begin{definition}{bder} |
|
67 \begin{verbatim} |
|
68 def bder(c: Char, r: ARexp) : ARexp = r match { |
|
69 case AZERO => AZERO |
|
70 case AONE(_) => AZERO |
|
71 case ACHAR(bs, f) => if (c == f) AONE(bs:::List(C(c))) else AZERO |
|
72 case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _))) |
|
73 case ASEQ(bs, r1, r2) => { |
|
74 if (bnullable(r1)) AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(mkepsBC(r1), bder(c, r2))) |
|
75 else ASEQ(bs, bder(c, r1), r2) |
|
76 } |
|
77 case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r)) |
|
78 } |
|
79 \end{verbatim} |
|
80 \end{definition} |
|
81 |
|
82 \begin{definition}{bsimp} |
|
83 \begin{verbatim} |
|
84 def bsimp(r: ARexp): ARexp = r match { |
|
85 case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match { |
|
86 case (AZERO, _) => AZERO |
|
87 case (_, AZERO) => AZERO |
|
88 case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) |
|
89 case (r1s, r2s) => ASEQ(bs1, r1s, r2s) |
|
90 } |
|
91 case AALTS(bs1, rs) => { |
|
92 val rs_simp = rs.map(bsimp) |
|
93 val flat_res = flats(rs_simp) |
|
94 val dist_res = distinctBy(flat_res, erase) |
|
95 dist_res match { |
|
96 case Nil => AZERO |
|
97 case s :: Nil => fuse(bs1, s) |
|
98 case rs => AALTS(bs1, rs) |
|
99 } |
|
100 } |
|
101 //case ASTAR(bs, r) => ASTAR(bs, bsimp(r)) |
|
102 case r => r |
|
103 } |
|
104 \end{verbatim} |
|
105 \end{definition} |
|
106 |
|
107 \begin{definition}{sub-parts of bsimp} |
|
108 \begin{itemize} |
|
109 \item{flats}\\ |
|
110 flattens the list. |
|
111 \item{dB}\\ |
|
112 means distinctBy |
|
113 \item{Co}\\ |
|
114 The last matching clause of the function bsimp, namely |
|
115 dist\_res match { |
|
116 case Nil => AZERO |
|
117 case s :: Nil => fuse(bs1, s) |
|
118 case rs => AALTS(bs1, rs) |
|
119 } |
|
120 \end{itemize} |
|
121 \end{definition} |
|
122 |
|
123 \begin{definition}{fuse} |
|
124 \begin{verbatim} |
|
125 def fuse(bs: Bits, r: ARexp) : ARexp = r match { |
|
126 case AZERO => AZERO |
|
127 case AONE(cs) => AONE(bs ++ cs) |
|
128 case ACHAR(cs, f) => ACHAR(bs ++ cs, f) |
|
129 case AALTS(cs, rs) => AALTS(bs ++ cs, rs) |
|
130 case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2) |
|
131 case ASTAR(cs, r) => ASTAR(bs ++ cs, r) |
|
132 } |
|
133 \end{verbatim} |
|
134 \end{definition} |
|
135 |
|
136 |
|
137 \begin{definition}{mkepsBC} |
|
138 \begin{verbatim} |
|
139 def mkepsBC(r: ARexp) : Bits = r match { |
|
140 case AONE(bs) => bs |
|
141 case AALTS(bs, rs) => { |
|
142 val n = rs.indexWhere(bnullable) |
|
143 bs ++ mkepsBC(rs(n)) |
|
144 } |
|
145 case ASEQ(bs, r1, r2) => bs ++ mkepsBC(r1) ++ mkepsBC(r2) |
|
146 case ASTAR(bs, r) => bs ++ List(Z) |
|
147 } |
|
148 \end{verbatim} |
|
149 \end{definition} |
|
150 |
|
151 \begin{definition}{mkepsBC equicalence} |
|
152 \\ |
|
153 Given 2 nullable annotated regular expressions r1, r2, if mkepsBC(r1) == mkepsBC(r2) |
|
154 then r1 and r2 are mkepsBC equivalent, denoted as r1 $\sim_{m\epsilon}$ r2 |
|
155 \end{definition} |
|
156 |
|
157 \begin{definition}{shorthand notation for ders} |
|
158 \\For the sake of reducing verbosity, we sometimes use the shorthand notation |
|
159 $d_{c}(r)$ for the function application bder(c, r) and $s(r)$(s here stands for simplification) for the function application bsimp(r) . |
|
160 \\We omit the subscript when it is clear from context what that character is and write $d(r)$ instead of $d_{c}(r)$. |
|
161 \\And we omit the parentheses when no confusion can be caused. For example ders\_simp(c, r) can be written as $s(d_{c}(r))$ or even $s d r$ as we know the derivative operation is w.r.t the character c. Here the s and d are more like operators that take an annotated regular expression as an input and return an annotated regular expression as an output |
|
162 |
|
163 \end{definition} |
|
164 |
|
165 \begin{definition}{mkepsBC invariant manipulation of bits and notation}\\ |
|
166 ALTS(bs, ALTS(bs1, rs1), ALTS(bs2, rs2)) $\sim_{m\epsilon}$ ALTS(bs, rs1.map(fuse(bs1, \_)) ++ rs2.map(fuse(bs2, \_)) ). \\ |
|
167 We also use $bs2>>rs2 $ as a shorthand notation for rs2.map(fuse(bs2,\_)). |
|
168 |
|
169 \end{definition} |
|
170 |
|
171 \begin{definition}{distinctBy operation expressed in a different way--how it transforms the list}\\ |
|
172 Given two lists rs1 and rs2, we define the operation $--$:\\ |
|
173 $rs1 -- rs2 := [r \in rs1 | r \notin rs2]$ |
|
174 Note that the order is preserved as in the original list. |
|
175 \end{definition} |
|
176 |
|
177 |
|
178 \section{Main Result} |
|
179 \begin{lemma}{simplification function does not simplify an already simplified regex}\\ |
|
180 bsimp(r) == bsimp(bsimp(r)) holds for any annotated regular expression r. |
|
181 \end{lemma} |
|
182 |
|
183 \begin{lemma}{simp and mkeps}\\ |
|
184 When r is nullable, we have that |
|
185 mkeps(bsimp(r)) == mkeps(r) |
|
186 \end{lemma} |
|
187 |
|
188 \begin{lemma}{mkeps equivalence w.r.t some syntactically different regular expressions(1 ALTS)}\\ |
|
189 When one of the 2 regular expressions $s(r_1)$ and $s(r_2)$ is ALTS(bs1, rs1), we have that $ds(ALTS(bs, r1, r2)) \sim_{m\epsilon} d(ALTS(bs, sr_1, sr_2))$ |
|
190 \end{lemma} |
|
191 \begin{proof} |
|
192 By opening up one of the alts and show no additional changes are made. |
|
193 \end{proof} |
|
194 |
|
195 \begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS)}\\ |
|
196 $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have $ d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ |
|
197 \end{lemma} |
|
198 \begin{proof} |
|
199 We are just fusing bits inside here, there is no other structural change. |
|
200 \end{proof} |
|
201 |
|
202 \begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS+ some deletion)}\\ |
|
203 $d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2))) \sim_{m\epsilon} d Co(ALTS(bs, dB(bs1>>rs1 ++ ((bs2>>rs2)--rs1) ))) $ |
|
204 \end{lemma} |
|
205 \begin{proof} |
|
206 The removed parts have already appeared before in $rs_1$, so if any of them is truly nullable and is chosen as the mkeps path, it will have been traversed through in its previous counterpart.\\ |
|
207 (We probably need to switch the position of lemma5 and lemma6) |
|
208 \end{proof} |
|
209 |
|
210 \begin{lemma}{after opening two previously simplified alts up into terms, length must exceed 2}\\ |
|
211 $d Co(ALTS(bs, rs )) \sim_{m\epsilon} d(ALTS(bs, rs))$ if $rs$ is a list of length greater than or equal to 2. |
|
212 \end{lemma} |
|
213 \begin{proof} |
|
214 As suggested by the title of this lemma |
|
215 \end{proof} |
|
216 |
|
217 |
|
218 |
|
219 |
|
220 |
|
221 |
|
222 \begin{theorem}{Correctness Result} |
|
223 |
|
224 \begin{itemize} |
|
225 |
|
226 \item{} |
|
227 When s is a string in the language L(ar), \\ |
|
228 ders\_simp(ar, s) $\sim_{m\epsilon}$ ders(ar, s), \\ |
|
229 \item{} |
|
230 when s is not a string of the language L(ar) |
|
231 ders\_simp(ar, s) is not nullable |
|
232 \end{itemize} |
|
233 \end{theorem} |
|
234 |
|
235 \begin{proof}{Split into 2 parts.} |
|
236 \begin{itemize} |
|
237 \item |
|
238 |
|
239 When we have an annotated regular expression ar and a string s that matches ar, by the correctness of the algorithm ders, we have that ders(ar, s) is nullable, and that mkepsBC will extract the desired bits for decoding the correct value v for the matching, and v is a POSIX value. Now we prove that mkepsBC(ders\_simp(ar, s)) yields the same bitsequence. |
|
240 \\ |
|
241 We first open up the ders\_simp function into nested alternating sequences of ders and simp. |
|
242 Assume that s = $c_1...c_n$($n \geq 1$ ) where each of the $c_i$ are characters. |
|
243 Then $ders\_simp(ar, s)$ = $s(d_{c_n}(...s(d_{c_1}(r))...))$ = $sdsd......sdr$. If we can prove that |
|
244 $sdr \sim_{m\epsilon} dsr$ holds for any regular expression and any character, then we are done. This is because then we can push ders operation inside and move simp operation outside and have that $sdsd...sdr \sim_{m\epsilon} ssddsdsd...sdr \sim_{m\epsilon} ... \sim_{m\epsilon} s....sd....dr$ and using lemma1 we have that $s...sd....dr = sd...dr$. By lemma2, we have $RHS \sim_{m\epsilon} d...dr$.\\ |
|
245 Now we proceed to prove that $sdr \sim_{m\epsilon} dsr$. This can be reduced to proving $dr \sim_{m\epsilon} dsr$ as we know that $dr \sim_{m\epsilon} sdr$ by lemma2.\\ |
|
246 |
|
247 we use an induction proof. Base cases are omitted. Here are the 3 inductive cases. |
|
248 \begin{itemize} |
|
249 |
|
250 \item{$r_1+r_2$} |
|
251 $r_1+r_2$\\ |
|
252 The most difficult case is when $sr1$ and $sr2$ are both ALTS, so that they will be opened up in the flats function and some terms in sr2 might be deleted. Or otherwise we can use the argument that $d(r_1+r_2) = dr_1 + dr_2 \sim_{m\epsilon} dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$, |
|
253 the last equivalence being established by lemma3. |
|
254 When $s(r_1), s(r_2)$ are both ALTS, we have to be more careful for the last equivalence step, namelly, $dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$. \\ |
|
255 We have that $LHS = dsr_1 + dsr_2 = d(sr_1 +sr_2)$. Since $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have $ d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ by lemma4. |
|
256 On the other hand, $RHS = ds(ALTS(bs, r1, r2)) \sim_{m\epsilon}d Co(ALTS(bs, dB(flats(s(r1), s(r2))))) == d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2)))$ by definition of bsimp and flats.\\ $d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2))) \sim_{m\epsilon} d Co(ALTS(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1) ))) $ by lemma5.\\ $d Co(ALTS(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1) ))) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1))$ by lemma6. \\ |
|
257 Using lemma5 again, we have $d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$.\\ |
|
258 This completes the proof. |
|
259 \item{$r*$}\\ |
|
260 s(r*) = s(r). |
|
261 \item{$r1.r2$}\\ |
|
262 using previous. |
|
263 |
|
264 \end{itemize} |
|
265 \item |
|
266 Proof of second part of the theorem: use a similar structure of argument as in the first part. |
|
267 \end{itemize} |
|
268 \end{proof} |
|
269 |
|
270 \end{document} |
|
271 |
|
272 %The second part might still need some more development. |
|
273 %When s is not in the set L(ar), we have that s = s1@s2 s.t. s1 $\in$ L(ar), and any longer string that is a prefix of s does not belong to L(ar).\\ |
|
274 %By first part of proof, we have ders(ar, s1) $\sim_{m\epsilon}$ ders\_simp(ar, s1) |
|
275 %.....somehow show that by correctness, der(c, ders\_simp(ar, s1)) must be not nullable. But this will need that L(ders(ar, s1)) == L(ders\_simp(ar, s1)). By part 1 of proof we only have that for any string s1c s.t. s1c $\in$ L(ar) (which is equivalent to s $\in$ L(ders(ar, s1))), s is also in L(ders\_simp(ar, s1)). That is an inclusion, not an equality. c not in L(ders(ar, s1)) does not imply c not in L(ders\_simp(ar, s1)) |
|
276 %So this path stuck here. |