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