candidates.tex 16 KB
 Michael Banken committed Dec 19, 2017 1 2 3 4 5 6 \chapter{Optimization .Candidates} In order to optimize the theory graph we must first identify cases where it is possible to apply any optimizations. We call such theories \underline{optimization candidates} or just \underline{candidates}. All candidates have in common that they are theories where inclusions can be removed or replaced with weaker inclusions, while still yielding a valid theory as a result without any undeclared symbols (assuming of course a valid theory graph at the start). For something to be declared a candidates we will only require that the theory itself must remain valid, but not necessarily the stronger case that replacing the candidate with the optimized theory will result in a graph that is still valid as a whole. Of course these considerations will still be applied elsewhere.  Michael Banken committed Oct 25, 2017 7   Michael Banken committed Oct 16, 2017 8 9 \section{Types of optimization candidates} \subsection{Simply redundant inclusion}  Michael Banken committed Oct 25, 2017 10 11 An inclusion of a theory $A\hookrightarrow{}C$ is \underline{simply redundant}, if $C$ includes a theory $B$, such that $B\hookrightarrow{}C$ (see \autoref{fig:redundantbasic}).  Michael Banken committed Oct 16, 2017 12 13 14 \providecommand\myxscale{3.9} \providecommand\myyscale{2.2} \providecommand\myfontsize{\footnotesize}  Michael Banken committed Oct 25, 2017 15 16 \begin{figure}[!htb] \begin{tikzpicture}[node distance=3cm]\footnotesize  Michael Banken committed Oct 16, 2017 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline ...\\\hline ... \end{tabular}}; \node[thy, above of = bottom] (middle) {\begin{tabular}{l} \textsf{middle}\\\hline ...\\\hline ... \end{tabular}}; \node[thy, above of = middle] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline ... \end{tabular}}; \draw[include] (bottom) -- (middle); \draw[include, bend left] (bottom) edge (top); \draw[include] (middle) -- (top); \end{tikzpicture}  Michael Banken committed Oct 25, 2017 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 \caption{Simply redundant inclusion example} \label{fig:redundantbasic} \end{figure} Simply redundant inclusions can be safely optimized by simply removing the redundant inclusion, as seen in \autoref{fig:redundantoptimized}, without changing the flattened graph due to the transitive nature of inclusions. \begin{figure}[!htb] \begin{tikzpicture}[node distance=3cm]\footnotesize \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline ...\\\hline ... \end{tabular}}; \node[thy, above of = bottom] (middle) {\begin{tabular}{l} \textsf{middle}\\\hline ...\\\hline ... \end{tabular}}; \node[thy, above of = middle] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline ... \end{tabular}}; \draw[include] (bottom) -- (middle); \draw[include] (middle) -- (top); \end{tikzpicture} \caption{Example of simply redundant inclusion optimized} \label{fig:redundantoptimized} \end{figure}  Michael Banken committed Oct 16, 2017 65 \subsection{Superfluous Inclusion}  Michael Banken committed Oct 25, 2017 66 67 An inclusion of a theory $A\hookrightarrow{}B$ is \underline{superfluous}, if $B$ uses none of the constants declared in $A$. Such an inclusion can be \underline{purely superfluous} (\autoref{sec:puresi}) if it can be entirely removed, or \underline{partially superfluous} if it can be reduced to a subset of the theory inclusions in $A$ \autoref{sec:partiallysi}.\\ In both of these cases the inclusion can be replaced or removed entirely, while still yielding a well formed theory. However this changes the resulting flattened theory graph and can invalidate theories that include the optimized theory.\\  Michael Banken committed Oct 16, 2017 68 \subsubsection{Purely Superfluous Inclusion}  Michael Banken committed Oct 25, 2017 69 70 71 72 An inclusion of a theory $A\hookrightarrow{}B$ is \underline{purely superfluous}, if $B$ uses none of the constants in $A$, not even if they were declared in a theory $C$ such that $C\hookrightarrow{}A$.\\ \label{sec:puresi} \begin{figure}[!htb] \begin{tikzpicture}[node distance=3cm]\footnotesize  Michael Banken committed Oct 16, 2017 73 74 75 76 77 78 79 80 81 82 83 84 \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline X\\\hline ... \end{tabular}}; \node[thy, above of = bottom] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline no X \end{tabular}}; \draw[include] (bottom) -- (top); \end{tikzpicture}  Michael Banken committed Oct 25, 2017 85 86 87 88 89 90 91 \caption{Purely superfluous inclusion example} \label{fig:purelysuperfluousbasic} \end{figure} Purely superfluous inclusions can be removed while still retaining a valid theory, however this will change the resulting theory graph. These changes may or may not be what is desired. An example for such an optimization can be seen in \autoref{fig:purelysuperfluousoptimized}. \begin{figure}[!htb] \begin{tikzpicture}[node distance=3cm]\footnotesize  Michael Banken committed Oct 16, 2017 92 \node[thy] (bottom) {\begin{tabular}{l}  Michael Banken committed Oct 16, 2017 93  \textsf{bottom}\\\hline  Michael Banken committed Oct 16, 2017 94 95  X\\\hline ...  Michael Banken committed Oct 16, 2017 96  \end{tabular}};  Michael Banken committed Oct 25, 2017 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 \node[thy, above of = bottom] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline no X \end{tabular}}; \end{tikzpicture} \caption{Example of purely superfluous inclusion optimized} \label{fig:purelysuperfluousoptimized} \end{figure} \subsubsection{Partially Superfluous Inclusion} \label{sec:partiallysi} An inclusion of a theory $A\hookrightarrow{}B$ is \underline{partially superfluous}, if $B$ uses none of the constants in $A$, but uses some declarations that were declared in one or more theory $C$ such that C is (transitively) included in A.\\ \begin{figure}[!htb] \begin{tikzpicture}[node distance=3cm]\footnotesize \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline $X_1$\\\hline ... \end{tabular}}; \node[right of = bottom] (dots) {...}; \node[thy, right of = dots] (bottomn) {\begin{tabular}{l} \textsf{$bottom_n$}\\\hline $X_n$\\\hline ... \end{tabular}};  Michael Banken committed Oct 16, 2017 123 \node[thy, above of = bottom] (middle) {\begin{tabular}{l}  Michael Banken committed Oct 16, 2017 124 125 126 127 128 129  \textsf{middle}\\\hline Y\\\hline ... \end{tabular}}; \node[thy, above of = middle] (top) {\begin{tabular}{l} \textsf{top}\\\hline  Michael Banken committed Oct 16, 2017 130  ...\\\hline  Michael Banken committed Oct 25, 2017 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148  $X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y \end{tabular}}; \draw[include] (bottom) -- (middle); \draw[include] (bottomn) -- (middle); \draw[include] (middle) -- (top); \end{tikzpicture} \caption{Partially superfluous inclusion example} \label{fig:partiallysuperfluousbasic} \end{figure} Partially superfluous inclusions can be optimized by identifying the used subset of (transitive) inclusions and replacing the superfluous inclusion with these inclusions. As seen in \autoref{fig:partiallysuperfluousoptimized}. \begin{figure}[!htb] \begin{tikzpicture}[node distance=3cm]\footnotesize \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline $X_1$\\\hline ...  Michael Banken committed Oct 16, 2017 149  \end{tabular}};  Michael Banken committed Oct 16, 2017 150 151 152 153 154 155 \node[right of = bottom] (dots) {...}; \node[thy, right of = dots] (bottomn) {\begin{tabular}{l} \textsf{$bottom_n$}\\\hline $X_n$\\\hline ... \end{tabular}};  Michael Banken committed Oct 25, 2017 156 157 158 159 160 161 162 163 164 165 \node[thy, above of = bottom] (middle) {\begin{tabular}{l} \textsf{middle}\\\hline Y\\\hline ... \end{tabular}}; \node[thy, above of = middle] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline $X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y \end{tabular}};  Michael Banken committed Oct 16, 2017 166 \draw[include] (bottom) -- (middle);  Michael Banken committed Oct 25, 2017 167 168 169 170 171 172 173 174 175 \draw[include] (bottomn) -- (middle); \draw[include] (bottomn) -- (top); \draw[include, bend left] (bottom) edge (top); \end{tikzpicture} \caption{Example of partially superfluous inclusion optimized} \label{fig:partiallysuperfluousoptimized} \end{figure} \section{Viability and dangers of candidate optimizations}  Michael Banken committed Dec 19, 2017 176 177 178 The candidates discussed earlier are cases in which inclusions can be changed, not necessarily where they should be changed, as the only criterion that makes a theory an optimization candidate is that an optimization can be performed while still retaining a valid theory. There is nothing that guarantees that this theory is also preferable to the original or even desirable at all to have.\\ The danger of performing the proposed optimizations varies between the type of candidate and the context, but overall application without at least some user guidance is not recommended.  Michael Banken committed Oct 25, 2017 179 180 181 \subsection{Simply redundant inclusion} As noted in \autoref{sec:puresi} there is very little that speaks against removing simply redundant inclusions, since the flattened graph is preserved. However there are some cases where they might do more harm than good, particularly when they overlap with superfluous inclusions, as seen in \autoref{fig:redundantoverlap}.\\ Removing the redundant edge will not change the flattened graph, but it will complicate the changes needed to remove the superfluous edge between middle and top. A simple solution to avoiding this problem is to relegate the removal of simple redundancies until after other optimizations have been performed on the theory.\\ \begin{figure}[h]  Michael Banken committed Dec 19, 2017 182 \begin{tikzpicture}[node distance=2cm]\footnotesize  Michael Banken committed Oct 25, 2017 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 \node[thy] (bottom) {\begin{tabular}{l} \textsf{bottom}\\\hline X\\\hline ... \end{tabular}}; \node[thy, above of = bottom] (middle) {\begin{tabular}{l} \textsf{middle}\\\hline Y\\\hline ... \end{tabular}}; \node[thy, above of = middle] (top) {\begin{tabular}{l} \textsf{top}\\\hline ...\\\hline X, but not Y \end{tabular}}; \draw[include] (bottom) -- (middle); \draw[include, bend left] (bottom) edge (top);  Michael Banken committed Oct 16, 2017 200 201 \draw[include] (middle) -- (top); \end{tikzpicture}  Michael Banken committed Oct 25, 2017 202 203 204 205 \caption{Example of overlap between simply redundant inclusion and superfluous inclusion} \label{fig:redundantoverlap} \end{figure} \subsection{Purely superfluous inclusion}  Michael Banken committed Dec 19, 2017 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 Purely superfluous includes are a little trickier, as their removal can fundamentally change the underlying theory graph. Removing a purely superfluous inclusion. A trivial example for a purely superfluous inclusion that should not be optimized is any theory union, ie. a theory that consists entirely of theory inclusions (\autoref{fig:theoryunion}).\\ Removing purely superfluous includes from a theory union will leave behind an entirely empty theory. Since an empty theory is rarely a desired outcome an easy fix is to skip theory unions for this or in fact any kind of optimization. \begin{figure}[h] \begin{tikzpicture}[node distance=2cm]\footnotesize \node[thy] (union) {\begin{tabular}{l} \textsf{union}\\\hline \\\hline \end{tabular}}; \node[thy, below left of = union] (A) {\begin{tabular}{l} \textsf{A}\\\hline ...\\\hline ... \end{tabular}}; \node[thy, below right of = union] (B) {\begin{tabular}{l} \textsf{B}\\\hline ...\\\hline ... \end{tabular}}; \draw[include] (A) -- (union); \draw[include] (B) -- (union); \end{tikzpicture} \caption{Example of a simple theory union} \label{fig:theoryunion} \end{figure} However theory unions are not the only cases where optimization may be misplaced. When culling seemingly superfluous inclusions of non-empty theories we fundamentally change the theory graph, by cutting the content of the included theory from our candidate. This means that unlike the simply redundant case, this optimization should be carefully considered. If this content is required by a theory that originally included it via an inclusion of the candidate, this may even break the entire theory graph. To avoid this problem it makes sense to not only watch what the candidate theory itself uses, but to look further ahead and also consider the symbols used by theories which include the candidate. We call these theories the \underline{future lite code}.  Michael Banken committed Oct 25, 2017 238 239  \subsection{Partially superfluous inclusion}  Michael Banken committed Dec 19, 2017 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 Unsurprisingly this isn't the only case where this optimization can have unfortunate results. Let us consider the following example from elementary Algebra (\autoref{fig:elalg}). It is easy to define a monoid as a semigroup with the addition of a neutral element. The problem this poses for our optimizations is that our definition doesn't make use of associativity in any way. If all the symbols needed for defining the neutral element are delivered through a theory included by semi groups called Magma, then replacing the inclusion of semigroups with magma is a perfectly valid optimization. This is however a vastly different theory then we would expect of something that calls itself a monoid and can lead to complications if a theory including this theory expects it to contain the associativity rule, as it should. \begin{figure}[h] \begin{tikzpicture}[node distance=2cm]\myfontsize \node[thy] (magma) {\begin{tabular}{l} \textsf{Magma}\\\hline $G,\circ$\\\hline $\scriptstyle x\circ y\in G$ \end{tabular}}; \node[thy, above of=magma] (sg) {\begin{tabular}{l} \textsf{SemiGrp}\\\hline \\\hline $\scriptstyle (x\circ y)\circ z=x\circ (y\circ z)$ \end{tabular}}; \node[thy, above of=sg] (m) {\begin{tabular}{l} \textsf{Monoid}\\\hline $e$\\\hline $\scriptstyle e\circ x=x\circ e=x$ \end{tabular}}; \draw[include] (magma) -- (sg); \draw[include] (sg) -- (m); \end{tikzpicture} \caption{Simple example from elementary Algebra} \label{fig:elalg} \end{figure} The considerations about theories including the candidate in the future lite code also apply to the partially superfluous case.  Michael Banken committed Oct 25, 2017 267 268  \section{Structures}  Michael Banken committed Dec 19, 2017 269 270 271 272 273 It should be noted that all the cases discussed in this chapter assume the relationship between these theories to be one of simple theory inclusion, while ignoring the existence of named structures entirely. As a rule of thumb we can assume that anything that was declared as a named structure is there for a reason and should therefore not be touched by our optimizations. Obviously this reasoning does not apply in all cases, but it is reason enough to avoid them in an automated tool. In addition structures have proven to be especially difficult to consider for our future lite code, for reasons that will be discussed in \autoref{sec:futurelite}.