| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Mon, 30 Oct 2023 18:46:27 +0000 | |
| changeset 950 | 285da21f44c0 | 
| parent 942 | 7f52427568ff | 
| child 979 | 15e49c674b46 | 
| permissions | -rw-r--r-- | 
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
1  | 
\documentclass{article}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
2  | 
\usepackage{../style}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
3  | 
\usepackage{../graphics}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
4  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
5  | 
\begin{document}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
6  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
7  | 
\section*{Complement Sets}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
8  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
9  | 
Consider the following picture:  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
10  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
11  | 
\begin{center}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
12  | 
\begin{tikzpicture}[fill=gray]
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
13  | 
% left hand  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
14  | 
\scope  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
15  | 
\fill (0,0) circle (1);  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
16  | 
\endscope  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
17  | 
% outline  | 
| 
 
38456acd29f3
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)$}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
19  | 
      (2,0) node [text=black,above] {$\neg P(s)$}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
20  | 
      (-2,-2) rectangle (3,2) node [text=black,above] {$\Sigma^*$};
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
21  | 
\end{tikzpicture}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
22  | 
\end{center}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
23  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
24  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
25  | 
\noindent  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
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  | 
| 942 | 28  | 
the set of all binary trees, etc). Let us assume $P(s)$ is a property that  | 
| 
941
 
38456acd29f3
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  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
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
 | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
34  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
35  | 
\begin{equation}\label{set}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
36  | 
\{s \in \Sigma^*\;|\; P(s) \}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
37  | 
\end{equation}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
38  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
39  | 
\noindent  | 
| 
 
38456acd29f3
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)$  | 
| 
 
38456acd29f3
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$  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
43  | 
sometimes the property $P(s)$ holds for every string in  | 
| 
 
38456acd29f3
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  | 
| 942 | 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.  | 
|
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
47  | 
|
| 
 
38456acd29f3
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}.
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
49  | 
This complement set is often written as  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
50  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
51  | 
\[  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
52  | 
\overline{\{s \in \Sigma^*\;|\; P(s) \}}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
53  | 
\]  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
54  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
55  | 
\noindent  | 
| 
 
38456acd29f3
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^*$  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
57  | 
minus $\{s \in \Sigma^*\;|\; P(s) \}$, \textbf{or} written differently
 | 
| 942 | 58  | 
it is the set $\{s \in \Sigma^*\;|\; \neg P(s) \}$. That means it is the
 | 
| 
941
 
38456acd29f3
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  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
60  | 
for any complement set the equation:  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
61  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
62  | 
\begin{equation}\label{eq}
 | 
| 
 
38456acd29f3
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) \}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
64  | 
\end{equation}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
65  | 
|
| 942 | 66  | 
\section*{Semantic Derivative}
 | 
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
67  | 
|
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
69  | 
a subset of strings (inside $\Sigma^*$). The corresponding  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
71  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
72  | 
\[  | 
| 
 
38456acd29f3
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\}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
74  | 
\]  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
75  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
76  | 
\noindent  | 
| 
 
38456acd29f3
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  | 
| 942 | 78  | 
which subset, or which grey area, we are carving out from $\Sigma^*$ depends on what we  | 
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
79  | 
choose for $c$ and $A$.\bigskip  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
80  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
81  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
82  | 
\noindent  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
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^*$
 | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
87  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
88  | 
\[  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
89  | 
  \Sigma^* = \left\{\begin{array}{l}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
90  | 
    $\ensuremath{[]}$\\
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
91  | 
    $\ensuremath{[a], [b]}$\\
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
92  | 
    $\ensuremath{[aa], [ab], [ba], [bb]}$\\
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
93  | 
    $\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
94  | 
    \end{array}\right\}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
95  | 
\]  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
96  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
97  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
98  | 
\noindent  | 
| 
 
38456acd29f3
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
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
100  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
101  | 
\[  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
102  | 
Der\;a\;A = \{[aa], [bb], [a]\}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
103  | 
\]  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
104  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
105  | 
\noindent  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
106  | 
which is given by the definition of  | 
| 
 
38456acd29f3
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
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
108  | 
the complement of this set looks like:  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
109  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
110  | 
\begin{equation}\label{Der}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
111  | 
  \overline{Der\;a\;A} = \left\{\begin{array}{l}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
112  | 
    $\ensuremath{[]}$\\
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
113  | 
    $\ensuremath{[b]}$\\
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
114  | 
    $\ensuremath{[ab], [ba]}$\\
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
115  | 
    $\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
116  | 
    \end{array}\right\}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
117  | 
\end{equation}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
118  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
119  | 
\noindent  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
120  | 
This can be calculated by ``subtracting'' $\{[aa], [bb], [a]\}$ from
 | 
| 
 
38456acd29f3
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  | 
| 942 | 122  | 
to the equation in \eqref{eq} this should also be equal to
 | 
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
123  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
124  | 
\[  | 
| 942 | 125  | 
\overline{Der\;a\;A} = \{s \in \Sigma^*\;|\;\neg(a::s\in A)\}
 | 
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
126  | 
\]  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
127  | 
|
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
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  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
130  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
131  | 
\[\{[aaa], [abb], [aa], [bb], []\}\]
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
132  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
133  | 
\noindent  | 
| 942 | 134  | 
This gives rise to the following table where in the first column are all  | 
| 
941
 
38456acd29f3
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  | 
| 942 | 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$.  | 
|
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
138  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
139  | 
\begin{center}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
140  | 
\begin{tabular}{r|c|l}
 | 
| 942 | 141  | 
$s\in\Sigma^*$ & is $a::s \in A$? & $\neg(a::s \in A) \Leftrightarrow a::s \not\in A$\\  | 
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
142  | 
\hline  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
143  | 
$[]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
144  | 
$[a]$ & yes& no\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
145  | 
$[b]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
146  | 
$[aa]$ & yes& no\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
147  | 
$[ab]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
148  | 
$[ba]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
149  | 
$[bb]$ & yes& no\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
150  | 
$[aaa]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
151  | 
$[aab]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
152  | 
$[aba]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
153  | 
$[abb]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
154  | 
$[baa]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
155  | 
$[bab]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
156  | 
$[bba]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
157  | 
$[bbb]$ & no & yes\\  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
158  | 
\end{tabular}    
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
159  | 
\end{center}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
160  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
161  | 
\noindent  | 
| 942 | 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)
 | 
|
| 
941
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
234  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
235  | 
\end{document}
 | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
236  | 
|
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
237  | 
%%% Local Variables:  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
238  | 
%%% mode: latex  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
239  | 
%%% TeX-master: t  | 
| 
 
38456acd29f3
added complement note
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
240  | 
%%% End:  |