hws/Der.tex
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--
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
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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    45
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
    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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
    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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   136
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
   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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   162
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
   163
\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
   164
\bigskip
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   165
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   166
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   167
BTW, notice that all three properties are the same
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   168
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   169
\[
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   170
  \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
   171
  \quad\Leftrightarrow\quad a::s \in \overline{A}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   172
\]  
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   173
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   174
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   175
This means we have
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   176
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   177
\begin{equation}\label{D}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   178
\overline{Der\;a\;A} = Der\;a\;\overline{A}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   179
\end{equation}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   180
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   181
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   182
I let you check whether this makes sense.
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   183
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   184
\section*{Not-Regular Expression}
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
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
   187
$der$-definition for the not-regular expression satisfies the property
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   188
of derivatives, namely
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{derprop}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   191
\forall c\,r.\;\;\;L(der\;c\;r) = Der\;c\;(L(r))
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
holds. We defined the language of a not-regular expression as
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
\[
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   198
L(\sim r) \;\dn\; \Sigma^* - L(r)
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   199
\]  
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   200
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   201
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   202
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
   203
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   204
\[
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   205
L(\sim r) \;\dn\; \overline{L(r)}
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
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   208
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   209
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
   210
the not-regular expression as
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   211
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
der\;c\;(\sim r) \;\dn\; \sim(der\;c\;r)
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   214
\]  
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   215
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   216
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   217
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
   218
\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
   219
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
   220
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   221
\begin{center}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   222
  \def\arraystretch{1.5}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   223
\begin{tabular}{llll}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   224
  $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
   225
                        & $\dn$ & $\overline{L(der\;c\;r)}$ & by definition of $L$\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   226
                        & $=$ & $\overline{Der\;c\;(L(r))}$ & by IH\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   227
                        & $=$ & $Der\;c\;\overline{(L(r))}$ & by \eqref{D}\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   228
                        & $\dn$ & $Der\;c\;(L(\sim r))$ & by definition of $L$\\
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   229
\end{tabular}    
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   230
\end{center}
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   231
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   232
\noindent
5365ef60707e updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 942
diff changeset
   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: