hws/Der.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Mon, 03 Feb 2025 13:25:59 +0000
changeset 980 0c491eff5b01
parent 943 5365ef60707e
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
980
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
     5
\title{Derivative for the NOT-Regular Expression}
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
     6
942
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
     7
\begin{document}
980
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
     8
\maketitle
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
     9
\begin{abstract}
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    10
  \noindent
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    11
  This short note explains why the derivative for the NOT-regular
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    12
  expression is defined as
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    13
  \[
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    14
  der\,c(\sim r) \;\dn\; \sim (der\,c\,r)
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    15
  \]
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    16
  The explanation goes via complement sets, the semantic derivative (\textit{Der})
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    17
  and how the derivative relates to the semantic derivative.
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    18
\end{abstract}
942
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    19
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    20
\section*{Complement Sets}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    21
980
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    22
To start with, consider the following picture:
942
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
\begin{center}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    25
\begin{tikzpicture}[fill=gray]
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    26
% left hand
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    27
\scope
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    28
\fill (0,0) circle (1);
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    29
\endscope
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    30
% outline
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    31
\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
    32
      (2,0) node [text=black,above] {$\neg P(s)$}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    33
      (-2,-2) rectangle (3,2) node [text=black,above] {$\Sigma^*$};
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    34
\end{tikzpicture}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    35
\end{center}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    36
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    37
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    38
\noindent
980
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
    39
where $\Sigma^*$ is in our case the set of all strings (what follows in this section
942
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    40
also holds for any kind of ``domain'', like the set of all integers or
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    41
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
    42
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
    43
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
    44
\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
    45
$\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
    46
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
    47
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    48
\begin{equation}\label{set}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    49
\{s \in \Sigma^*\;|\; P(s) \}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    50
\end{equation}
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
\noindent
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    53
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
    54
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
    55
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
    56
sometimes the property $P(s)$ holds for every string in
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    57
$\Sigma^*$. Then the grey area would fill out the whole rectangle and
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    58
the set where $\neg P(s)$ holds is empty. Similarly, if the property $P(s)$
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    59
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
    60
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    61
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
    62
This complement set is often written as
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    63
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    64
\[
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    65
\overline{\{s \in \Sigma^*\;|\; P(s) \}}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    66
\]
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
\noindent
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    69
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
    70
minus $\{s \in \Sigma^*\;|\; P(s) \}$, \textbf{or} written differently
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    71
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
    72
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
    73
for any complement set the equation:
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
\begin{equation}\label{eq}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    76
\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
    77
\end{equation}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    78
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    79
\section*{Semantic Derivative}
942
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
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
    82
a subset of strings (inside $\Sigma^*$). The corresponding
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    83
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
    84
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    85
\[
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    86
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
    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
\noindent
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    90
That means $Der\;c\;A$ is some grey area inside $\Sigma^*$. Obviously
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    91
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
    92
choose for $c$ and $A$.\bigskip
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    93
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    94
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    95
\noindent
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
    96
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
    97
$\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
    98
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
    99
(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
   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
  \Sigma^* = \left\{\begin{array}{l}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   103
    $\ensuremath{[]}$\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   104
    $\ensuremath{[a], [b]}$\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   105
    $\ensuremath{[aa], [ab], [ba], [bb]}$\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   106
    $\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   107
    \end{array}\right\}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   108
\] 
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
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   111
\noindent
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   112
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
   113
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   114
\[
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   115
Der\;a\;A = \{[aa], [bb], [a]\}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   116
\]  
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   117
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   118
\noindent
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   119
which is given by the definition of
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   120
$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
   121
the complement of this set looks like:
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   122
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   123
\begin{equation}\label{Der}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   124
  \overline{Der\;a\;A} = \left\{\begin{array}{l}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   125
    $\ensuremath{[]}$\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   126
    $\ensuremath{[b]}$\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   127
    $\ensuremath{[ab], [ba]}$\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   128
    $\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   129
    \end{array}\right\}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   130
\end{equation}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   131
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   132
\noindent
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   133
This can be calculated by ``subtracting'' $\{[aa], [bb], [a]\}$ from
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   134
$\Sigma^*$. I let you check whether I did this correctly.  According
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   135
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
   136
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   137
\[
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   138
\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
   139
\]  
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   140
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   141
\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
   142
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
   143
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   144
\[\{[aaa], [abb], [aa], [bb], []\}\]
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   145
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   146
\noindent
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   147
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
   148
the strings of $\Sigma^*$ and in the second whether $a::s \in A$ holds. The third column
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   149
is the negated version of the second, namely $\neg(a::s\in A)$ which is the same as
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   150
$a::s\not\in A$.
942
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   151
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   152
\begin{center}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   153
\begin{tabular}{r|c|l}
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   154
  $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
   155
  \hline
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   156
  $[]$    & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   157
  $[a]$   & yes& no\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   158
  $[b]$   & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   159
  $[aa]$  & yes& no\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   160
  $[ab]$  & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   161
  $[ba]$  & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   162
  $[bb]$  & yes& no\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   163
  $[aaa]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   164
  $[aab]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   165
  $[aba]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   166
  $[abb]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   167
  $[baa]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   168
  $[bab]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   169
  $[bba]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   170
  $[bbb]$ & no & yes\\
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   171
\end{tabular}    
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   172
\end{center}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   173
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   174
\noindent
943
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   175
Collecting all the yes in the third column gives you the set in
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   176
\eqref{Der}. So it works out in this example. The idea is that this always works out. ;o)
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   177
\bigskip
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   178
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   179
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   180
BTW, notice that all three properties are the same
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   181
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   182
\[
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   183
  \neg(a::s \in A) \quad\Leftrightarrow\quad  a::s \not\in A
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   184
  \quad\Leftrightarrow\quad a::s \in \overline{A}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   185
\]  
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   186
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   187
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   188
This means we have
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   189
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   190
\begin{equation}\label{D}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   191
\overline{Der\;a\;A} = Der\;a\;\overline{A}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   192
\end{equation}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   193
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   194
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   195
I let you check whether this makes sense.
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   196
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   197
\section*{Not-Regular Expression}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   198
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   199
With the equation in \eqref{D} we can also very quickly verify that the
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   200
$der$-definition for the not-regular expression satisfies the property
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   201
of derivatives, namely
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   202
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   203
\begin{equation}\label{derprop}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   204
\forall c\,r.\;\;\;L(der\;c\;r) = Der\;c\;(L(r))
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   205
\end{equation}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   206
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   207
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   208
holds. We defined the language of a not-regular expression as
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   209
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   210
\[
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   211
L(\sim r) \;\dn\; \Sigma^* - L(r)
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   212
\]  
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   213
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   214
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   215
Using the overline notation, maybe I should have defined this equivalently as
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   216
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   217
\[
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   218
L(\sim r) \;\dn\; \overline{L(r)}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   219
\] 
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   220
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   221
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   222
meaning all the strings that $r$ \emph{cannot} match. We defined the derivative for
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   223
the not-regular expression as
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   224
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   225
\[
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   226
der\;c\;(\sim r) \;\dn\; \sim(der\;c\;r)
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   227
\]  
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   228
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   229
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   230
The big question is now does this definition satisfy the property in
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   231
\eqref{derprop}? Lets see: We would have to prove this by induction on regular
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   232
expressions. When we are in the case for $\sim r$ the reasoning is as follows:
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   233
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   234
\begin{center}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   235
  \def\arraystretch{1.5}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   236
\begin{tabular}{llll}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   237
  $L(der\;c\;(\sim r))$ & $\dn$ & $L(\sim (der\;c\;r))$ & by definition of $der$\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   238
                        & $\dn$ & $\overline{L(der\;c\;r)}$ & by definition of $L$\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   239
                        & $=$ & $\overline{Der\;c\;(L(r))}$ & by IH\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   240
                        & $=$ & $Der\;c\;\overline{(L(r))}$ & by \eqref{D}\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   241
                        & $\dn$ & $Der\;c\;(L(\sim r))$ & by definition of $L$\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   242
\end{tabular}    
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   243
\end{center}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   244
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   245
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   246
That means we have established the property of derivatives in the $\sim r$-case\dots{}yippee~;o)
980
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   247
\medskip
942
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   248
980
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   249
\noindent
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   250
The conclusion is: if we want the property $L(der\,c\,r) = Der\,c\,(L(r))$ to hold and the
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   251
semantics of $\sim r$ is defined as $\overline{L(r)}$, then the definition for the derivative
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   252
for the NOT-regular expression must be:
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   253
\[
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   254
der\,c(\sim r) \;\dn\; \sim (der\,c\,r)
0c491eff5b01 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 943
diff changeset
   255
\]  
942
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   256
\end{document}
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   257
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   258
%%% Local Variables: 
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   259
%%% mode: latex
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   260
%%% TeX-master: t
c82a45f48bfc added complement note
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff changeset
   261
%%% End: