| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Fri, 22 Nov 2024 12:42:07 +0000 | |
| changeset 973 | db987b9717a4 | 
| parent 942 | 7f52427568ff | 
| child 979 | 15e49c674b46 | 
| permissions | -rw-r--r-- | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 1 | \documentclass{article}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 2 | \usepackage{../style}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 3 | \usepackage{../graphics}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 4 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 5 | \begin{document}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 6 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 7 | \section*{Complement Sets}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 8 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 9 | Consider the following picture: | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 10 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 11 | \begin{center}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 12 | \begin{tikzpicture}[fill=gray]
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 13 | % left hand | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 14 | \scope | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 15 | \fill (0,0) circle (1); | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 16 | \endscope | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 17 | % outline | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 18 | \draw (0,0) circle (1) (0,1)  node [text=white,below] {$P(s)$}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 19 |       (2,0) node [text=black,above] {$\neg P(s)$}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 20 |       (-2,-2) rectangle (3,2) node [text=black,above] {$\Sigma^*$};
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 21 | \end{tikzpicture}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 22 | \end{center}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 23 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 24 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 25 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 26 | where $\Sigma^*$ is in our case the set of all strings (what follows | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 27 | also holds for any kind of ``domain'', like the set of all integers or | 
| 942 | 28 | the set of all binary trees, etc). Let us assume $P(s)$ is a property that | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 29 | is about strings, for example $P(s)$ could be ``the string $s$ has | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 30 | an even length'', or ``the string $s$ starts with the letter | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 31 | \texttt{a}''. Every such property carves out a subset of strings from
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 32 | $\Sigma^*$, which in the picture above is depicted as a grey | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 33 | circle. This subset of strings is often written as a comprehension like | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 34 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 35 | \begin{equation}\label{set}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 36 | \{s \in \Sigma^*\;|\; P(s) \}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 37 | \end{equation}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 38 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 39 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 40 | meaning all the $s$ (out of $\Sigma^*$) for which the property $P(s)$ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 41 | is true. If $P(s)$ would not be true then the corresponding string $s$ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 42 | would be outside the grey area where $\neg P(s)$ holds. Notice that | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 43 | sometimes the property $P(s)$ holds for every string in | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 44 | $\Sigma^*$. Then the grey area would fill out the whole rectangle and | 
| 942 | 45 | the set where $\neg P(s)$ holds is empty. Similarly, if the property $P(s)$ | 
| 46 | holds for no string, then the grey circle is empty. | |
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 47 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 48 | Now, we are looking for the complement of the set defined in \eqref{set}.
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 49 | This complement set is often written as | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 50 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 51 | \[ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 52 | \overline{\{s \in \Sigma^*\;|\; P(s) \}}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 53 | \] | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 54 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 55 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 56 | It is the area of $\Sigma^*$ which isn't grey, that is $\Sigma^*$ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 57 | minus $\{s \in \Sigma^*\;|\; P(s) \}$, \textbf{or} written differently
 | 
| 942 | 58 | it is the set $\{s \in \Sigma^*\;|\; \neg P(s) \}$. That means it is the
 | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 59 | set of all the strings where $\neg P(s)$ holds. Consequently we have | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 60 | for any complement set the equation: | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 61 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 62 | \begin{equation}\label{eq}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 63 | \overline{\{s \in \Sigma^*\;|\; P(s) \}} = \{s \in \Sigma^*\;|\; \neg P(s) \}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 64 | \end{equation}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 65 | |
| 942 | 66 | \section*{Semantic Derivative}
 | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 67 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 68 | Our semantic derivative $Der\;c\;A$ is nothing else than a property that defines | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 69 | a subset of strings (inside $\Sigma^*$). The corresponding | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 70 | property $P(s)$ is $c::s \in A$ because we defined $Der\;c\;A$ as | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 71 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 72 | \[ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 73 | Der\;c\;A \;\dn\; \{s \in \Sigma^*\;|\; c::s \in A\}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 74 | \] | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 75 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 76 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 77 | That means $Der\;c\;A$ is some grey area inside $\Sigma^*$. Obviously | 
| 942 | 78 | which subset, or which grey area, we are carving out from $\Sigma^*$ depends on what we | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 79 | choose for $c$ and $A$.\bigskip | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 80 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 81 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 82 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 83 | Let us see how this pans out in a concrete example. For this let | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 84 | $\Sigma^*$ not be the set of all strings, but only the set of strings | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 85 | upto a length of 3 over the alphabet $\{a, b\}$. That means $\Sigma^*$
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 86 | (or the rectangle in the picture above) consists of the strings | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 87 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 88 | \[ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 89 |   \Sigma^* = \left\{\begin{array}{l}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 90 |     $\ensuremath{[]}$\\
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 91 |     $\ensuremath{[a], [b]}$\\
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 92 |     $\ensuremath{[aa], [ab], [ba], [bb]}$\\
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 93 |     $\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 94 |     \end{array}\right\}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 95 | \] | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 96 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 97 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 98 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 99 | If we set $A$ to $\{[aaa], [abb], [aa], [bb], []\}$, then $Der\;a\;A$ is the subset
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 100 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 101 | \[ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 102 | Der\;a\;A = \{[aa], [bb], [a]\}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 103 | \] | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 104 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 105 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 106 | which is given by the definition of | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 107 | $Der\;a\;A \dn \{s \in \Sigma^*\;|\;a::s\in A\}$. Now lets look at what
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 108 | the complement of this set looks like: | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 109 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 110 | \begin{equation}\label{Der}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 111 |   \overline{Der\;a\;A} = \left\{\begin{array}{l}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 112 |     $\ensuremath{[]}$\\
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 113 |     $\ensuremath{[b]}$\\
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 114 |     $\ensuremath{[ab], [ba]}$\\
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 115 |     $\ensuremath{[aaa], [aab], [aba], [abb], [baa], [bab], [bba], [bbb]}$
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 116 |     \end{array}\right\}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 117 | \end{equation}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 118 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 119 | \noindent | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 120 | This can be calculated by ``subtracting'' $\{[aa], [bb], [a]\}$ from
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 121 | $\Sigma^*$. I let you check whether I did this correctly. According | 
| 942 | 122 | to the equation in \eqref{eq} this should also be equal to
 | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 123 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 124 | \[ | 
| 942 | 125 | \overline{Der\;a\;A} = \{s \in \Sigma^*\;|\;\neg(a::s\in A)\}
 | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 126 | \] | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 127 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 128 | \noindent Let us test in turn every string in $\Sigma^*$ and see | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 129 | whether $a::s$ is in $A$ which we set above to | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 130 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 131 | \[\{[aaa], [abb], [aa], [bb], []\}\]
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 132 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 133 | \noindent | 
| 942 | 134 | This gives rise to the following table where in the first column are all | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 135 | the strings of $\Sigma^*$ and in the second whether $a::s \in A$ holds. The third column | 
| 942 | 136 | is the negated version of the second, namely $\neg(a::s\in A)$ which is the same as | 
| 137 | $a::s\not\in A$. | |
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 138 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 139 | \begin{center}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 140 | \begin{tabular}{r|c|l}
 | 
| 942 | 141 | $s\in\Sigma^*$ & is $a::s \in A$? & $\neg(a::s \in A) \Leftrightarrow a::s \not\in A$\\ | 
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 142 | \hline | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 143 | $[]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 144 | $[a]$ & yes& no\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 145 | $[b]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 146 | $[aa]$ & yes& no\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 147 | $[ab]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 148 | $[ba]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 149 | $[bb]$ & yes& no\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 150 | $[aaa]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 151 | $[aab]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 152 | $[aba]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 153 | $[abb]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 154 | $[baa]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 155 | $[bab]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 156 | $[bba]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 157 | $[bbb]$ & no & yes\\ | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 158 | \end{tabular}    
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 159 | \end{center}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 160 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 161 | \noindent | 
| 942 | 162 | Collecting all the yes in the third column gives you the set in | 
| 163 | \eqref{Der}. So it works out in this example. The idea is that this always works out. ;o)
 | |
| 164 | \bigskip | |
| 165 | ||
| 166 | \noindent | |
| 167 | BTW, notice that all three properties are the same | |
| 168 | ||
| 169 | \[ | |
| 170 | \neg(a::s \in A) \quad\Leftrightarrow\quad a::s \not\in A | |
| 171 |   \quad\Leftrightarrow\quad a::s \in \overline{A}
 | |
| 172 | \] | |
| 173 | ||
| 174 | \noindent | |
| 175 | This means we have | |
| 176 | ||
| 177 | \begin{equation}\label{D}
 | |
| 178 | \overline{Der\;a\;A} = Der\;a\;\overline{A}
 | |
| 179 | \end{equation}
 | |
| 180 | ||
| 181 | \noindent | |
| 182 | I let you check whether this makes sense. | |
| 183 | ||
| 184 | \section*{Not-Regular Expression}
 | |
| 185 | ||
| 186 | With the equation in \eqref{D} we can also very quickly verify that the
 | |
| 187 | $der$-definition for the not-regular expression satisfies the property | |
| 188 | of derivatives, namely | |
| 189 | ||
| 190 | \begin{equation}\label{derprop}
 | |
| 191 | \forall c\,r.\;\;\;L(der\;c\;r) = Der\;c\;(L(r)) | |
| 192 | \end{equation}
 | |
| 193 | ||
| 194 | \noindent | |
| 195 | holds. We defined the language of a not-regular expression as | |
| 196 | ||
| 197 | \[ | |
| 198 | L(\sim r) \;\dn\; \Sigma^* - L(r) | |
| 199 | \] | |
| 200 | ||
| 201 | \noindent | |
| 202 | Using the overline notation, maybe I should have defined this equivalently as | |
| 203 | ||
| 204 | \[ | |
| 205 | L(\sim r) \;\dn\; \overline{L(r)}
 | |
| 206 | \] | |
| 207 | ||
| 208 | \noindent | |
| 209 | meaning all the strings that $r$ \emph{cannot} match. We defined the derivative for
 | |
| 210 | the not-regular expression as | |
| 211 | ||
| 212 | \[ | |
| 213 | der\;c\;(\sim r) \;\dn\; \sim(der\;c\;r) | |
| 214 | \] | |
| 215 | ||
| 216 | \noindent | |
| 217 | The big question is now does this definition satisfy the property in | |
| 218 | \eqref{derprop}? Lets see: We would have to prove this by induction on regular
 | |
| 219 | expressions. When we are in the case for $\sim r$ the reasoning is as follows: | |
| 220 | ||
| 221 | \begin{center}
 | |
| 222 |   \def\arraystretch{1.5}
 | |
| 223 | \begin{tabular}{llll}
 | |
| 224 | $L(der\;c\;(\sim r))$ & $\dn$ & $L(\sim (der\;c\;r))$ & by definition of $der$\\ | |
| 225 |                         & $\dn$ & $\overline{L(der\;c\;r)}$ & by definition of $L$\\
 | |
| 226 |                         & $=$ & $\overline{Der\;c\;(L(r))}$ & by IH\\
 | |
| 227 |                         & $=$ & $Der\;c\;\overline{(L(r))}$ & by \eqref{D}\\
 | |
| 228 | & $\dn$ & $Der\;c\;(L(\sim r))$ & by definition of $L$\\ | |
| 229 | \end{tabular}    
 | |
| 230 | \end{center}
 | |
| 231 | ||
| 232 | \noindent | |
| 233 | That means we have established the property of derivatives in the $\sim r$-case\dots{}yippee~;o)
 | |
| 941 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 234 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 235 | \end{document}
 | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 236 | |
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 237 | %%% Local Variables: | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 238 | %%% mode: latex | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 239 | %%% TeX-master: t | 
| 
38456acd29f3
added complement note
 Christian Urban <christian.urban@kcl.ac.uk> parents: diff
changeset | 240 | %%% End: |