author | Christian Urban <christian.urban@kcl.ac.uk> |
Tue, 28 Nov 2023 11:42:31 +0000 | |
changeset 956 | ae9782e62bdd |
parent 943 | 5365ef60707e |
permissions | -rw-r--r-- |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1 |
\documentclass{article} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
2 |
\usepackage{../style} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
3 |
\usepackage{../graphics} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
4 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
5 |
\begin{document} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
6 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
7 |
\section*{Complement Sets} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
8 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
9 |
Consider the following picture: |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
10 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
11 |
\begin{center} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
12 |
\begin{tikzpicture}[fill=gray] |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
13 |
% left hand |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
14 |
\scope |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
15 |
\fill (0,0) circle (1); |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
16 |
\endscope |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
17 |
% outline |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
18 |
\draw (0,0) circle (1) (0,1) node [text=white,below] {$P(s)$} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
19 |
(2,0) node [text=black,above] {$\neg P(s)$} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
20 |
(-2,-2) rectangle (3,2) node [text=black,above] {$\Sigma^*$}; |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
21 |
\end{tikzpicture} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
22 |
\end{center} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
23 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
24 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
25 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
26 |
where $\Sigma^*$ is in our case the set of all strings (what follows |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
27 |
also holds for any kind of ``domain'', like the set of all integers or |
943 | 28 |
the set of all binary trees, etc). Let us assume $P(s)$ is a property that |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
29 |
is about strings, for example $P(s)$ could be ``the string $s$ has |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
30 |
an even length'', or ``the string $s$ starts with the letter |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
31 |
\texttt{a}''. Every such property carves out a subset of strings from |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
32 |
$\Sigma^*$, which in the picture above is depicted as a grey |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
33 |
circle. This subset of strings is often written as a comprehension like |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
34 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
35 |
\begin{equation}\label{set} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
36 |
\{s \in \Sigma^*\;|\; P(s) \} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
37 |
\end{equation} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
38 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
39 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
40 |
meaning all the $s$ (out of $\Sigma^*$) for which the property $P(s)$ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
41 |
is true. If $P(s)$ would not be true then the corresponding string $s$ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
42 |
would be outside the grey area where $\neg P(s)$ holds. Notice that |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
43 |
sometimes the property $P(s)$ holds for every string in |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
44 |
$\Sigma^*$. Then the grey area would fill out the whole rectangle and |
943 | 45 |
the set where $\neg P(s)$ holds is empty. Similarly, if the property $P(s)$ |
46 |
holds for no string, then the grey circle is empty. |
|
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
47 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
48 |
Now, we are looking for the complement of the set defined in \eqref{set}. |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
49 |
This complement set is often written as |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
50 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
51 |
\[ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
52 |
\overline{\{s \in \Sigma^*\;|\; P(s) \}} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
53 |
\] |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
54 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
55 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
56 |
It is the area of $\Sigma^*$ which isn't grey, that is $\Sigma^*$ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
57 |
minus $\{s \in \Sigma^*\;|\; P(s) \}$, \textbf{or} written differently |
943 | 58 |
it is the set $\{s \in \Sigma^*\;|\; \neg P(s) \}$. That means it is the |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
59 |
set of all the strings where $\neg P(s)$ holds. Consequently we have |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
60 |
for any complement set the equation: |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
61 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
62 |
\begin{equation}\label{eq} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
63 |
\overline{\{s \in \Sigma^*\;|\; P(s) \}} = \{s \in \Sigma^*\;|\; \neg P(s) \} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
64 |
\end{equation} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
65 |
|
943 | 66 |
\section*{Semantic Derivative} |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
67 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
68 |
Our semantic derivative $Der\;c\;A$ is nothing else than a property that defines |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
69 |
a subset of strings (inside $\Sigma^*$). The corresponding |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
70 |
property $P(s)$ is $c::s \in A$ because we defined $Der\;c\;A$ as |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
71 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
72 |
\[ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
73 |
Der\;c\;A \;\dn\; \{s \in \Sigma^*\;|\; c::s \in A\} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
74 |
\] |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
75 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
76 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
77 |
That means $Der\;c\;A$ is some grey area inside $\Sigma^*$. Obviously |
943 | 78 |
which subset, or which grey area, we are carving out from $\Sigma^*$ depends on what we |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
79 |
choose for $c$ and $A$.\bigskip |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
80 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
81 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
82 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
83 |
Let us see how this pans out in a concrete example. For this let |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
84 |
$\Sigma^*$ not be the set of all strings, but only the set of strings |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
85 |
upto a length of 3 over the alphabet $\{a, b\}$. That means $\Sigma^*$ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
86 |
(or the rectangle in the picture above) consists of the strings |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
87 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
88 |
\[ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
89 |
\Sigma^* = \left\{\begin{array}{l} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
90 |
$\ensuremath{[]}$\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
91 |
$\ensuremath{[a], [b]}$\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
92 |
$\ensuremath{[aa], [ab], [ba], [bb]}$\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
93 |
$\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
94 |
\end{array}\right\} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
95 |
\] |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
96 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
97 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
98 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
99 |
If we set $A$ to $\{[aaa], [abb], [aa], [bb], []\}$, then $Der\;a\;A$ is the subset |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
100 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
101 |
\[ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
102 |
Der\;a\;A = \{[aa], [bb], [a]\} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
103 |
\] |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
104 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
105 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
106 |
which is given by the definition of |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
107 |
$Der\;a\;A \dn \{s \in \Sigma^*\;|\;a::s\in A\}$. Now lets look at what |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
108 |
the complement of this set looks like: |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
109 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
110 |
\begin{equation}\label{Der} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
111 |
\overline{Der\;a\;A} = \left\{\begin{array}{l} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
112 |
$\ensuremath{[]}$\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
113 |
$\ensuremath{[b]}$\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
114 |
$\ensuremath{[ab], [ba]}$\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
115 |
$\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
116 |
\end{array}\right\} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
117 |
\end{equation} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
118 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
119 |
\noindent |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
120 |
This can be calculated by ``subtracting'' $\{[aa], [bb], [a]\}$ from |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
121 |
$\Sigma^*$. I let you check whether I did this correctly. According |
943 | 122 |
to the equation in \eqref{eq} this should also be equal to |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
123 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
124 |
\[ |
943 | 125 |
\overline{Der\;a\;A} = \{s \in \Sigma^*\;|\;\neg(a::s\in A)\} |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
126 |
\] |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
127 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
128 |
\noindent Let us test in turn every string in $\Sigma^*$ and see |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
129 |
whether $a::s$ is in $A$ which we set above to |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
130 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
131 |
\[\{[aaa], [abb], [aa], [bb], []\}\] |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
132 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
133 |
\noindent |
943 | 134 |
This gives rise to the following table where in the first column are all |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
135 |
the strings of $\Sigma^*$ and in the second whether $a::s \in A$ holds. The third column |
943 | 136 |
is the negated version of the second, namely $\neg(a::s\in A)$ which is the same as |
137 |
$a::s\not\in A$. |
|
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
138 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
139 |
\begin{center} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
140 |
\begin{tabular}{r|c|l} |
943 | 141 |
$s\in\Sigma^*$ & is $a::s \in A$? & $\neg(a::s \in A) \Leftrightarrow a::s \not\in A$\\ |
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
142 |
\hline |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
143 |
$[]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
144 |
$[a]$ & yes& no\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
145 |
$[b]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
146 |
$[aa]$ & yes& no\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
147 |
$[ab]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
148 |
$[ba]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
149 |
$[bb]$ & yes& no\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
150 |
$[aaa]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
151 |
$[aab]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
152 |
$[aba]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
153 |
$[abb]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
154 |
$[baa]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
155 |
$[bab]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
156 |
$[bba]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
157 |
$[bbb]$ & no & yes\\ |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
158 |
\end{tabular} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
159 |
\end{center} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
160 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
161 |
\noindent |
943 | 162 |
Collecting all the yes in the third column gives you the set in |
163 |
\eqref{Der}. So it works out in this example. The idea is that this always works out. ;o) |
|
164 |
\bigskip |
|
165 |
||
166 |
\noindent |
|
167 |
BTW, notice that all three properties are the same |
|
168 |
||
169 |
\[ |
|
170 |
\neg(a::s \in A) \quad\Leftrightarrow\quad a::s \not\in A |
|
171 |
\quad\Leftrightarrow\quad a::s \in \overline{A} |
|
172 |
\] |
|
173 |
||
174 |
\noindent |
|
175 |
This means we have |
|
176 |
||
177 |
\begin{equation}\label{D} |
|
178 |
\overline{Der\;a\;A} = Der\;a\;\overline{A} |
|
179 |
\end{equation} |
|
180 |
||
181 |
\noindent |
|
182 |
I let you check whether this makes sense. |
|
183 |
||
184 |
\section*{Not-Regular Expression} |
|
185 |
||
186 |
With the equation in \eqref{D} we can also very quickly verify that the |
|
187 |
$der$-definition for the not-regular expression satisfies the property |
|
188 |
of derivatives, namely |
|
189 |
||
190 |
\begin{equation}\label{derprop} |
|
191 |
\forall c\,r.\;\;\;L(der\;c\;r) = Der\;c\;(L(r)) |
|
192 |
\end{equation} |
|
193 |
||
194 |
\noindent |
|
195 |
holds. We defined the language of a not-regular expression as |
|
196 |
||
197 |
\[ |
|
198 |
L(\sim r) \;\dn\; \Sigma^* - L(r) |
|
199 |
\] |
|
200 |
||
201 |
\noindent |
|
202 |
Using the overline notation, maybe I should have defined this equivalently as |
|
203 |
||
204 |
\[ |
|
205 |
L(\sim r) \;\dn\; \overline{L(r)} |
|
206 |
\] |
|
207 |
||
208 |
\noindent |
|
209 |
meaning all the strings that $r$ \emph{cannot} match. We defined the derivative for |
|
210 |
the not-regular expression as |
|
211 |
||
212 |
\[ |
|
213 |
der\;c\;(\sim r) \;\dn\; \sim(der\;c\;r) |
|
214 |
\] |
|
215 |
||
216 |
\noindent |
|
217 |
The big question is now does this definition satisfy the property in |
|
218 |
\eqref{derprop}? Lets see: We would have to prove this by induction on regular |
|
219 |
expressions. When we are in the case for $\sim r$ the reasoning is as follows: |
|
220 |
||
221 |
\begin{center} |
|
222 |
\def\arraystretch{1.5} |
|
223 |
\begin{tabular}{llll} |
|
224 |
$L(der\;c\;(\sim r))$ & $\dn$ & $L(\sim (der\;c\;r))$ & by definition of $der$\\ |
|
225 |
& $\dn$ & $\overline{L(der\;c\;r)}$ & by definition of $L$\\ |
|
226 |
& $=$ & $\overline{Der\;c\;(L(r))}$ & by IH\\ |
|
227 |
& $=$ & $Der\;c\;\overline{(L(r))}$ & by \eqref{D}\\ |
|
228 |
& $\dn$ & $Der\;c\;(L(\sim r))$ & by definition of $L$\\ |
|
229 |
\end{tabular} |
|
230 |
\end{center} |
|
231 |
||
232 |
\noindent |
|
233 |
That means we have established the property of derivatives in the $\sim r$-case\dots{}yippee~;o) |
|
942
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
234 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
235 |
\end{document} |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
236 |
|
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
237 |
%%% Local Variables: |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
238 |
%%% mode: latex |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
239 |
%%% TeX-master: t |
c82a45f48bfc
added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
240 |
%%% End: |