| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Fri, 17 Oct 2025 11:20:49 +0100 | |
| changeset 1009 | 7fd1997bd14c | 
| parent 995 | 5056d7de44af | 
| permissions | -rw-r--r-- | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 1 | \documentclass{article}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 2 | \usepackage{../style}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 3 | \usepackage{../graphics}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 4 | |
| 979 | 5 | \title{Derivative for the NOT-Regular Expression}
 | 
| 6 | ||
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 7 | \begin{document}
 | 
| 979 | 8 | \maketitle | 
| 9 | \begin{abstract}
 | |
| 10 | \noindent | |
| 11 | This short note explains why the derivative for the NOT-regular | |
| 12 | expression is defined as | |
| 13 | \[ | |
| 14 | der\,c(\sim r) \;\dn\; \sim (der\,c\,r) | |
| 15 | \] | |
| 16 |   The explanation goes via complement sets, the semantic derivative (\textit{Der})
 | |
| 17 | and how the derivative relates to the semantic derivative. | |
| 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 | 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 | 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 | 
| 995 | 41 | the set of all binary trees, etc).\footnote{NOTE: In the videos and slides I use \textit{UNIV} as notation for $\Sigma^*$. } 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 | 58 | the set where $\neg P(s)$ holds is empty. Similarly, if the property $P(s)$ | 
| 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 | 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 | 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 | 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 | 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 | 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 | 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 | 149 | is the negated version of the second, namely $\neg(a::s\in A)$ which is the same as | 
| 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 | 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 | 175 | Collecting all the yes in the third column gives you the set in | 
| 176 | \eqref{Der}. So it works out in this example. The idea is that this always works out. ;o)
 | |
| 177 | \bigskip | |
| 178 | ||
| 179 | \noindent | |
| 180 | BTW, notice that all three properties are the same | |
| 181 | ||
| 182 | \[ | |
| 183 | \neg(a::s \in A) \quad\Leftrightarrow\quad a::s \not\in A | |
| 184 |   \quad\Leftrightarrow\quad a::s \in \overline{A}
 | |
| 185 | \] | |
| 186 | ||
| 187 | \noindent | |
| 188 | This means we have | |
| 189 | ||
| 190 | \begin{equation}\label{D}
 | |
| 191 | \overline{Der\;a\;A} = Der\;a\;\overline{A}
 | |
| 192 | \end{equation}
 | |
| 193 | ||
| 194 | \noindent | |
| 195 | I let you check whether this makes sense. | |
| 196 | ||
| 197 | \section*{Not-Regular Expression}
 | |
| 198 | ||
| 199 | With the equation in \eqref{D} we can also very quickly verify that the
 | |
| 200 | $der$-definition for the not-regular expression satisfies the property | |
| 201 | of derivatives, namely | |
| 202 | ||
| 203 | \begin{equation}\label{derprop}
 | |
| 204 | \forall c\,r.\;\;\;L(der\;c\;r) = Der\;c\;(L(r)) | |
| 205 | \end{equation}
 | |
| 206 | ||
| 207 | \noindent | |
| 208 | holds. We defined the language of a not-regular expression as | |
| 209 | ||
| 210 | \[ | |
| 211 | L(\sim r) \;\dn\; \Sigma^* - L(r) | |
| 212 | \] | |
| 213 | ||
| 214 | \noindent | |
| 215 | Using the overline notation, maybe I should have defined this equivalently as | |
| 216 | ||
| 217 | \[ | |
| 218 | L(\sim r) \;\dn\; \overline{L(r)}
 | |
| 219 | \] | |
| 220 | ||
| 221 | \noindent | |
| 222 | meaning all the strings that $r$ \emph{cannot} match. We defined the derivative for
 | |
| 223 | the not-regular expression as | |
| 224 | ||
| 225 | \[ | |
| 226 | der\;c\;(\sim r) \;\dn\; \sim(der\;c\;r) | |
| 227 | \] | |
| 228 | ||
| 229 | \noindent | |
| 230 | The big question is now does this definition satisfy the property in | |
| 231 | \eqref{derprop}? Lets see: We would have to prove this by induction on regular
 | |
| 232 | expressions. When we are in the case for $\sim r$ the reasoning is as follows: | |
| 233 | ||
| 234 | \begin{center}
 | |
| 235 |   \def\arraystretch{1.5}
 | |
| 236 | \begin{tabular}{llll}
 | |
| 237 | $L(der\;c\;(\sim r))$ & $\dn$ & $L(\sim (der\;c\;r))$ & by definition of $der$\\ | |
| 238 |                         & $\dn$ & $\overline{L(der\;c\;r)}$ & by definition of $L$\\
 | |
| 239 |                         & $=$ & $\overline{Der\;c\;(L(r))}$ & by IH\\
 | |
| 240 |                         & $=$ & $Der\;c\;\overline{(L(r))}$ & by \eqref{D}\\
 | |
| 241 | & $\dn$ & $Der\;c\;(L(\sim r))$ & by definition of $L$\\ | |
| 242 | \end{tabular}    
 | |
| 243 | \end{center}
 | |
| 244 | ||
| 245 | \noindent | |
| 246 | That means we have established the property of derivatives in the $\sim r$-case\dots{}yippee~;o)
 | |
| 979 | 247 | \medskip | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 248 | |
| 979 | 249 | \noindent | 
| 250 | The conclusion is: if we want the property $L(der\,c\,r) = Der\,c\,(L(r))$ to hold and the | |
| 251 | semantics of $\sim r$ is defined as $\overline{L(r)}$, then the definition for the derivative
 | |
| 252 | for the NOT-regular expression must be: | |
| 253 | \[ | |
| 254 | der\,c(\sim r) \;\dn\; \sim (der\,c\,r) | |
| 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: |