1 \documentclass{article} |
1 \documentclass{article} |
2 \usepackage{charter} |
2 \usepackage{../style} |
3 \usepackage{hyperref} |
3 |
4 \usepackage{amssymb} |
|
5 \usepackage{amsmath} |
|
6 |
|
7 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions |
|
8 \begin{document} |
4 \begin{document} |
9 |
5 |
10 \section*{Proof} |
6 \section*{Proof} |
11 |
7 |
12 Recall the definitions for regular expressions and the language associated with a regular expression: |
8 Recall the definitions for regular expressions and the language associated with a regular expression: |
13 |
9 |
14 \begin{center} |
10 \begin{center} |
15 \begin{tabular}{c} |
11 \begin{tabular}{c} |
16 \begin{tabular}[t]{rcl} |
12 \begin{tabular}[t]{rcl} |
17 $r$ & $::=$ & $\varnothing$ \\ |
13 $r$ & $::=$ & $\ZERO$ \\ |
18 & $\mid$ & $\epsilon$ \\ |
14 & $\mid$ & $\ONE$ \\ |
19 & $\mid$ & $c$ \\ |
15 & $\mid$ & $c$ \\ |
20 & $\mid$ & $r_1 \cdot r_2$ \\ |
16 & $\mid$ & $r_1 \cdot r_2$ \\ |
21 & $\mid$ & $r_1 + r_2$ \\ |
17 & $\mid$ & $r_1 + r_2$ \\ |
22 & $\mid$ & $r^*$ \\ |
18 & $\mid$ & $r^*$ \\ |
23 \end{tabular}\hspace{10mm} |
19 \end{tabular}\hspace{10mm} |
24 \begin{tabular}[t]{r@{\hspace{1mm}}c@{\hspace{1mm}}l} |
20 \begin{tabular}[t]{r@{\hspace{1mm}}c@{\hspace{1mm}}l} |
25 $L(\varnothing)$ & $\dn$ & $\varnothing$ \\ |
21 $L(\ZERO)$ & $\dn$ & $\varnothing$ \\ |
26 $L(\epsilon)$ & $\dn$ & $\{\texttt{""}\}$ \\ |
22 $L(\ONE)$ & $\dn$ & $\{\texttt{""}\}$ \\ |
27 $L(c)$ & $\dn$ & $\{\texttt{"}c\texttt{"}\}$ \\ |
23 $L(c)$ & $\dn$ & $\{\texttt{"}c\texttt{"}\}$ \\ |
28 $L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ \\ |
24 $L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ \\ |
29 $L(r_1 + r_2)$ & $\dn$ & $L(r_1) \cup L(r_2)$ \\ |
25 $L(r_1 + r_2)$ & $\dn$ & $L(r_1) \cup L(r_2)$ \\ |
30 $L(r^*)$ & $\dn$ & $\bigcup_{n\ge 0} L(r)^n$ \\ |
26 $L(r^*)$ & $\dn$ & $\bigcup_{n\ge 0} L(r)^n$ \\ |
31 \end{tabular} |
27 \end{tabular} |
35 \noindent |
31 \noindent |
36 We also defined the notion of a derivative of a regular expression (the derivative with respect to a character): |
32 We also defined the notion of a derivative of a regular expression (the derivative with respect to a character): |
37 |
33 |
38 \begin{center} |
34 \begin{center} |
39 \begin{tabular}{lcl} |
35 \begin{tabular}{lcl} |
40 $der\, c\, (\varnothing)$ & $\dn$ & $\varnothing$ \\ |
36 $der\, c\, (\ZERO)$ & $\dn$ & $\ZERO$ \\ |
41 $der\, c\, (\epsilon)$ & $\dn$ & $\varnothing$ \\ |
37 $der\, c\, (\ONE)$ & $\dn$ & $\ZERO$ \\ |
42 $der\, c\, (d)$ & $\dn$ & if $c = d$ then $\epsilon$ else $\varnothing$\\ |
38 $der\, c\, (d)$ & $\dn$ & if $c = d$ then $\ONE$ else $\ZERO$\\ |
43 $der\, c\, (r_1 + r_2)$ & $\dn$ & $(der\, c\, r_1) + (der\, c\, r_2)$ \\ |
39 $der\, c\, (r_1 + r_2)$ & $\dn$ & $(der\, c\, r_1) + (der\, c\, r_2)$ \\ |
44 $der\, c\, (r_1 \cdot r_2)$ & $\dn$ & if $nullable(r_1)$\\ |
40 $der\, c\, (r_1 \cdot r_2)$ & $\dn$ & if $nullable(r_1)$\\ |
45 & & then $((der\, c\, r_1) \cdot r_2) + (der\, c\, r_2)$\\ |
41 & & then $((der\, c\, r_1) \cdot r_2) + (der\, c\, r_2)$\\ |
46 & & else $(der\, c\, r_1) \cdot r_2$\\ |
42 & & else $(der\, c\, r_1) \cdot r_2$\\ |
47 $der\, c\, (r^*)$ & $\dn$ & $(der\, c\, r) \cdot (r^*)$\\ |
43 $der\, c\, (r^*)$ & $\dn$ & $(der\, c\, r) \cdot (r^*)$\\ |
51 \noindent |
47 \noindent |
52 With our definition of regular expressions comes an induction principle. Given a property $P$ over |
48 With our definition of regular expressions comes an induction principle. Given a property $P$ over |
53 regular expressions. We can establish that $\forall r.\; P(r)$ holds, provided we can show the following: |
49 regular expressions. We can establish that $\forall r.\; P(r)$ holds, provided we can show the following: |
54 |
50 |
55 \begin{enumerate} |
51 \begin{enumerate} |
56 \item $P(\varnothing)$, $P(\epsilon)$ and $P(c)$ all hold, |
52 \item $P(\ZERO)$, $P(\ONE)$ and $P(c)$ all hold, |
57 \item $P(r_1 + r_2)$ holds under the induction hypotheses that |
53 \item $P(r_1 + r_2)$ holds under the induction hypotheses that |
58 $P(r_1)$ and $P(r_2)$ hold, |
54 $P(r_1)$ and $P(r_2)$ hold, |
59 \item $P(r_1 \cdot r_2)$ holds under the induction hypotheses that |
55 \item $P(r_1 \cdot r_2)$ holds under the induction hypotheses that |
60 $P(r_1)$ and $P(r_2)$ hold, and |
56 $P(r_1)$ and $P(r_2)$ hold, and |
61 \item $P(r^*)$ holds under the induction hypothesis that $P(r)$ holds. |
57 \item $P(r^*)$ holds under the induction hypothesis that $P(r)$ holds. |
84 \newpage |
80 \newpage |
85 \noindent |
81 \noindent |
86 {\bf Proof} |
82 {\bf Proof} |
87 |
83 |
88 \noindent |
84 \noindent |
89 According to 1.~above we need to prove $P(\varnothing)$, $P(\epsilon)$ and $P(d)$. Lets do this in turn. |
85 According to 1.~above we need to prove $P(\ZERO)$, $P(\ONE)$ and $P(d)$. Lets do this in turn. |
90 |
86 |
91 \begin{itemize} |
87 \begin{itemize} |
92 \item First Case: $P(\varnothing)$ is $L(der\,c\,\varnothing) = Der\,c\,(L(\varnothing))$ (a). We have $der\,c\,\varnothing = \varnothing$ |
88 \item First Case: $P(\ZERO)$ is $L(der\,c\,\ZERO) = Der\,c\,(L(\ZERO))$ (a). We have $der\,c\,\ZERO = \ZERO$ |
93 and $L(\varnothing) = \varnothing$. We also have $Der\,c\,\varnothing = \varnothing$. Hence we have $\varnothing = \varnothing$ in (a). |
89 and $L(\ZERO) = \ZERO$. We also have $Der\,c\,\ZERO = \ZERO$. Hence we have $\ZERO = \ZERO$ in (a). |
94 |
90 |
95 \item Second Case: $P(\epsilon)$ is $L(der\,c\,\epsilon) = Der\,c\,(L(\epsilon))$ (b). We have $der\,c\,\epsilon = \varnothing$, |
91 \item Second Case: $P(\ONE)$ is $L(der\,c\,\ONE) = Der\,c\,(L(\ONE))$ (b). We have $der\,c\,\ONE = \ZERO$, |
96 $L(\varnothing) = \varnothing$ and $L(\epsilon) = \{\texttt{""}\}$. We also have $Der\,c\,\{\texttt{""}\} = \varnothing$. Hence we have |
92 $L(\ZERO) = \ZERO$ and $L(\ONE) = \{\texttt{""}\}$. We also have $Der\,c\,\{\texttt{""}\} = \ZERO$. Hence we have |
97 $\varnothing = \varnothing$ in (b). |
93 $\ZERO = \ZERO$ in (b). |
98 |
94 |
99 \item Third Case: $P(d)$ is $L(der\,c\,d) = Der\,c\,(L(d))$ (c). We need to treat the cases $d = c$ and $d \not= c$. |
95 \item Third Case: $P(d)$ is $L(der\,c\,d) = Der\,c\,(L(d))$ (c). We need to treat the cases $d = c$ and $d \not= c$. |
100 |
96 |
101 $d = c$: We have $der\,c\,c = \epsilon$ and $L(\epsilon) = \{\texttt{""}\}$. |
97 $d = c$: We have $der\,c\,c = \ONE$ and $L(\ONE) = \{\texttt{""}\}$. |
102 We also have $L(c) = \{\texttt{"}c\texttt{"}\}$ and $Der\,c\,\{\texttt{"}c\texttt{"}\} = \{\texttt{""}\}$. Hence we have |
98 We also have $L(c) = \{\texttt{"}c\texttt{"}\}$ and $Der\,c\,\{\texttt{"}c\texttt{"}\} = \{\texttt{""}\}$. Hence we have |
103 $\{\texttt{""}\} = \{\texttt{""}\}$ in (c). |
99 $\{\texttt{""}\} = \{\texttt{""}\}$ in (c). |
104 |
100 |
105 $d \not=c$: We have $der\,c\,d = \varnothing$. |
101 $d \not=c$: We have $der\,c\,d = \ZERO$. |
106 We also have $Der\,c\,\{\texttt{"}d\texttt{"}\} = \varnothing$. Hence we have |
102 We also have $Der\,c\,\{\texttt{"}d\texttt{"}\} = \ZERO$. Hence we have |
107 $\varnothing = \varnothing$ in (c). |
103 $\ZERO = \ZERO$ in (c). |
108 \end{itemize} |
104 \end{itemize} |
109 |
105 |
110 \noindent |
106 \noindent |
111 These were the easy base cases. Now come the inductive cases. |
107 These were the easy base cases. Now come the inductive cases. |
112 |
108 |
194 |
190 |
195 \begin{center} |
191 \begin{center} |
196 $Der\,c\,(L(r^*)) = Der\,c\,(L(r)^0 \cup \bigcup_{n \ge 1} L(r)^n) = (Der\,c\,L(r)^0) \cup Der\,c\,(\bigcup_{n \ge 1} L(r)^n)$ |
192 $Der\,c\,(L(r^*)) = Der\,c\,(L(r)^0 \cup \bigcup_{n \ge 1} L(r)^n) = (Der\,c\,L(r)^0) \cup Der\,c\,(\bigcup_{n \ge 1} L(r)^n)$ |
197 \end{center} |
193 \end{center} |
198 |
194 |
199 The first union ``disappears'' since $Der\,c\,(L(r)^0) = \varnothing$. |
195 The first union ``disappears'' since $Der\,c\,(L(r)^0) = \ZERO$. |
200 |
196 |
201 |
197 |
202 \end{document} |
198 \end{document} |
203 |
199 |
204 %%% Local Variables: |
200 %%% Local Variables: |