candidates.tex 20.9 KB
Newer Older
Michael Banken's avatar
Michael Banken committed
1 2
\chapter{Optimization Candidates}
\label{chap:candidates}
Michael Banken's avatar
Michael Banken committed
3
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}.
Michael Banken's avatar
Michael Banken committed
4 5 6 7

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's avatar
Michael Banken committed
8

Michael Banken's avatar
Michael Banken committed
9 10
Notably optimization candidates will not necessarily preserve the flattened graph. This is only the case for simply redundant inclusions(see below). 

Michael Banken's avatar
Michael Banken committed
11
\section{Simply redundant inclusion}
Michael Banken's avatar
Michael Banken committed
12
\label{sec:redinc}
Michael Banken's avatar
Michael Banken committed
13 14
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}).

15 16 17
\providecommand\myxscale{3.9}
\providecommand\myyscale{2.2}
\providecommand\myfontsize{\footnotesize}
Michael Banken's avatar
Michael Banken committed
18
\begin{figure}[!htb]
19
\centering
Michael Banken's avatar
Michael Banken committed
20
\begin{tikzpicture}[node distance=3cm]\footnotesize
21 22 23 24 25
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
26
\node[thy,  right of = bottom] (middle) {\begin{tabular}{l}
27 28 29 30
                             \textsf{middle}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
31
\node[thy, right of = middle] (top) {\begin{tabular}{l}
32 33 34 35 36 37 38 39
                             \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's avatar
Michael Banken committed
40 41 42 43 44 45
\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]
46
\centering
Michael Banken's avatar
Michael Banken committed
47 48 49 50 51 52
\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
53
\node[thy,  right of = bottom] (middle) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
54 55 56 57
                             \textsf{middle}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
58
\node[thy, right of = middle] (top) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
59 60 61 62 63 64 65 66 67 68 69
                             \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's avatar
Michael Banken committed
70 71 72 73 74 75
The simply redundant inclusions in a theory T are the set $I_R(T) =$\\ $ (\bigcup_{I \in DirectIncludes(T)}Includes(I)) \cap DirectIncludes(T)$,\\
where $Includes(I)$ are the transitively included theories in I and $DirectIncludes(T)$ are the theories included directly in the theory T.

It is immediately obvious that removing a simply redundant inclusion I from a theory T also removes it from the above set via the intersection with $DirectIncludes(T)$.\\
Slightly less obvious is that doing so neither adds nor removes any other inclusions. This is because by design the set $\bigcup_{I \in DirectIncludes(T)}Includes(I))$ still includes I and any of its children and thus remains unchanged.

Michael Banken's avatar
Michael Banken committed
76
\section{Superfluous Inclusion}
Michael Banken's avatar
Michael Banken committed
77
\label{sec:superinc}
Michael Banken's avatar
Michael Banken committed
78 79
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's avatar
Michael Banken committed
80 81 82 83

The superfluous inclusions in a theory T are the set $I_{S}(T) =$\\ $ \{ I \in DirectInludes(T) | I \notin UsedTheories(T) \}$,\\
where $DirectIncludes(T)$ are the theories included directly in the theory T and UsedTheories(T) are those theories whose terms are used in T.

Michael Banken's avatar
Michael Banken committed
84
\subsection{Purely Superfluous Inclusion}
Michael Banken's avatar
Michael Banken committed
85
\label{sec:puresi}
Michael Banken's avatar
Michael Banken committed
86
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$.\\
Michael Banken's avatar
Michael Banken committed
87
\begin{figure}[!htb]
88
\centering
Michael Banken's avatar
Michael Banken committed
89
\begin{tikzpicture}[node distance=3cm]\footnotesize
90 91 92 93 94
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             X\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
95
\node[thy, right of = bottom] (top) {\begin{tabular}{l}
96 97 98 99 100 101
                             \textsf{top}\\\hline
                             ...\\\hline
                             no X
                           \end{tabular}};
\draw[include] (bottom) -- (top);
\end{tikzpicture}
Michael Banken's avatar
Michael Banken committed
102 103 104 105 106 107
\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]
108
\centering
Michael Banken's avatar
Michael Banken committed
109
\begin{tikzpicture}[node distance=3cm]\footnotesize
110
\node[thy] (bottom) {\begin{tabular}{l}
111
                             \textsf{bottom}\\\hline
112 113
                             X\\\hline
                             ...
114
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
115
\node[thy, right of = bottom] (top) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
116 117 118 119 120 121 122 123 124
                             \textsf{top}\\\hline
                             ...\\\hline
                             no X
                           \end{tabular}};
\end{tikzpicture}
\caption{Example of purely superfluous inclusion optimized}
\label{fig:purelysuperfluousoptimized}
\end{figure}

Michael Banken's avatar
Michael Banken committed
125 126 127
The purely superfluous inclusions in a theory T are the set $I_{PuS}(T) =$\\ $ \{ I \in DirectInludes(T) | I \notin UsedTheories(T) \land Includes(I) \cap UsedTheories(T) \setminus Includes(UsedTheories(T)\setminus \{ T \}) = \emptyset \}$,\\
where $Includes(I)$ are the transitively included theories in I, $DirectIncludes(T)$ are the theories included directly in the theory T and $UsedTheories(T)$ are those theories whose terms are used in T.

Michael Banken's avatar
Michael Banken committed
128
\subsection{Partially Superfluous Inclusion}
Michael Banken's avatar
Michael Banken committed
129
\label{sec:partiallysi}
Michael Banken's avatar
Michael Banken committed
130
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. We describe theories that have declarations being used in a theory A, which includes them, as \underline{theories used by A}.\\
Michael Banken's avatar
Michael Banken committed
131
\begin{figure}[!htb]
132
\centering
Michael Banken's avatar
Michael Banken committed
133
\begin{tikzpicture}[node distance=2cm]\footnotesize
Michael Banken's avatar
Michael Banken committed
134 135 136 137 138
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             $X_1$\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
139 140 141 142
\node[below = 0.2cm of bottom] (dots) {\begin{tabular}{l}
								.\\.\\.\\
								\end{tabular}};
\node[thy, below = 0.2cm of dots] (bottomn) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
143 144 145 146
                             \textsf{$bottom_n$}\\\hline
                             $X_n$\\\hline
                             ...
                          \end{tabular}};
Michael Banken's avatar
Michael Banken committed
147
\node[thy,  right = 1.5cm of dots] (middle) {\begin{tabular}{l}
148 149 150 151
                             \textsf{middle}\\\hline
                             Y\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
152
\node[thy, right = 1.2cm of middle, node distance=4.3cm ] (top) {\begin{tabular}{l}
153
                             \textsf{top}\\\hline
154
                             ...\\\hline
Michael Banken's avatar
Michael Banken committed
155 156 157 158 159 160 161 162 163 164 165 166 167
                             $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]
168
\centering
Michael Banken's avatar
Michael Banken committed
169
\begin{tikzpicture}[node distance=2cm]\footnotesize
Michael Banken's avatar
Michael Banken committed
170 171 172 173
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             $X_1$\\\hline
                             ...
174
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
175 176 177 178
\node[below = 0.2cm of bottom] (dots) {\begin{tabular}{l}
								.\\.\\.\\
								\end{tabular}};
\node[thy, below = 0.2cm of dots] (bottomn) {\begin{tabular}{l}
179 180 181 182
                             \textsf{$bottom_n$}\\\hline
                             $X_n$\\\hline
                             ...
                          \end{tabular}};
Michael Banken's avatar
Michael Banken committed
183
\node[thy,  right = 1.5cm of dots] (middle) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
184 185 186 187
                             \textsf{middle}\\\hline
                             Y\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
188
\node[thy, right = 1.2 of middle, node distance=4.3cm ] (top) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
189 190 191 192
                             \textsf{top}\\\hline
                             ...\\\hline
                             $X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
                           \end{tabular}};
193
\draw[include] (bottom) -- (middle);
Michael Banken's avatar
Michael Banken committed
194 195
\draw[include] (bottomn) -- (middle);
\draw[include] (bottomn) -- (top);                       
Michael Banken's avatar
Michael Banken committed
196
\draw[include] (bottom)  -- (top);
Michael Banken's avatar
Michael Banken committed
197 198 199 200 201
\end{tikzpicture}
\caption{Example of partially superfluous inclusion optimized}
\label{fig:partiallysuperfluousoptimized}
\end{figure}

Michael Banken's avatar
Michael Banken committed
202 203 204
The partially superfluous inclusions in a theory T are the set $I_{PaS}(T) =$\\ $\{ I \in DirectInludes(T) | I \notin UsedTheories(T) \land Includes(I) \cap UsedTheories(T) \setminus Includes(UsedTheories(T)\setminus \{ T \}) \neq \emptyset \}$,\\
where $Includes(I)$ are the transitively included theories in I, $DirectIncludes(T)$ are the theories included directly in the theory T and $UsedTheories(T)$ are those theories whose terms are used in T.

Michael Banken's avatar
Michael Banken committed
205
\section{Viability and dangers of candidate optimizations}
Michael Banken's avatar
Michael Banken committed
206
\label{sec:viability}
Michael Banken's avatar
Michael Banken committed
207 208 209
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's avatar
Michael Banken committed
210 211
\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.\\
212 213
\begin{figure}[!htb]
\centering
Michael Banken's avatar
Michael Banken committed
214
\begin{tikzpicture}[node distance=3cm]\footnotesize
Michael Banken's avatar
Michael Banken committed
215 216 217 218 219
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             X\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
220
\node[thy,  right of = bottom] (middle) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
221 222 223 224
                             \textsf{middle}\\\hline
                             Y\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
225
\node[thy, right of = middle] (top) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
226 227 228 229 230 231
                             \textsf{top}\\\hline
                             ...\\\hline
                             X, but not Y
                           \end{tabular}};
\draw[include] (bottom) -- (middle);
\draw[include, bend left] (bottom) edge (top);                     
232 233
\draw[include] (middle)  -- (top);
\end{tikzpicture}
Michael Banken's avatar
Michael Banken committed
234 235 236 237
\caption{Example of overlap between simply redundant inclusion and superfluous inclusion}
\label{fig:redundantoverlap}
\end{figure}
\subsection{Purely superfluous inclusion}
238
\label{sec:puresivia}
Michael Banken's avatar
Michael Banken committed
239 240 241 242 243
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.

244 245
\begin{figure}[!htb]
\centering
Michael Banken's avatar
Michael Banken committed
246 247 248 249
\begin{tikzpicture}[node distance=2cm]\footnotesize
\node[thy] (union) {\begin{tabular}{l}
                             \textsf{union}\\\hline
                             \\\hline
Michael Banken's avatar
Michael Banken committed
250
                             \hfill
Michael Banken's avatar
Michael Banken committed
251
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
252
\node[thy,  above left = -0.2cm and 1.2cm of union] (A) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
253 254 255 256
                             \textsf{A}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
257
\node[thy, below left = -0.2cm and 1.2cm of union] (B) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
258 259 260 261 262 263 264 265 266 267 268 269 270 271
                             \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's avatar
Michael Banken committed
272

273 274
Another problem arises were inclusion paths branch of before eventually meeting again. Ideally optimizing superfluous inclusions should retain exactly those theory inclusions that are necessary for keeping a valid theory graph with no undeclared objects. Unfortunately this is complicated by the requirement to keep a theory's future valid. Specifically the problem arises if a future theory indirectly includes a theory over more than one path (see \autoref{fig:doubleinclusion}).

275 276
\begin{figure}[!htb]
\centering
277 278 279 280 281 282
\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             X\\\hline
                             ...
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
283
\node[thy,  below right = 0cm and 1 cm of bottom] (right) {\begin{tabular}{l}
284 285 286 287
                             \textsf{right}\\\hline
                             Y\\\hline
                             not X
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
288
\node[thy,  above right = 0cm and 1 cm of bottom] (left) {\begin{tabular}{l}
289 290 291 292
                             \textsf{left}\\\hline
                             Z\\\hline
                             not X
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
293
\node[thy, above right =  0cm and 1 cm of right] (top) {\begin{tabular}{l}
294 295 296 297 298 299 300 301 302 303 304 305 306 307 308
                             \textsf{top}\\\hline
                             ...\\\hline
                             X, Y, Z
                           \end{tabular}};
\draw[include] (bottom) -- (right);
\draw[include] (bottom) -- (left);                 
\draw[include] (right)  -- (top);                
\draw[include] (left)  -- (top);
\end{tikzpicture}
\caption{Example of a graph where optimization leaves ambiguous choice.}
\label{fig:doubleinclusion}
\end{figure}

As we can see the branched inclusion leaves us with two paths for top to include bottom. Either via inclusion of left or right. Therefore we could remove one of the inclusions of bottom in left or right, but not both of them. However recognizing such a case is difficult and even if one of the inclusions should be removed it is not easily deducible which one is truly superfluous. Thus it seems prudent to err on the side of caution and ignore such a case entirely and treat it like a regular case of a use of bottom in left and right's respective futures.

Michael Banken's avatar
Michael Banken committed
309
\subsection{Partially superfluous inclusion}
310 311 312 313

Due to the inherent similarities many of the prior considerations also apply to partially superfluous inclusions.

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. Again this problem can be somewhat alleviated by looking at the future lite code.
Michael Banken's avatar
Michael Banken committed
314

315 316
\begin{figure}[!htb]
\centering
Michael Banken's avatar
Michael Banken committed
317
\begin{tikzpicture}[node distance=3cm]\myfontsize
Michael Banken's avatar
Michael Banken committed
318 319 320 321 322
\node[thy] (magma) {\begin{tabular}{l}
                             \textsf{Magma}\\\hline
                             $G,\circ$\\\hline
                             $\scriptstyle x\circ y\in G$
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
323
\node[thy, right of=magma] (sg) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
324 325 326 327
                             \textsf{SemiGrp}\\\hline
                             \\\hline
                             $\scriptstyle (x\circ y)\circ z=x\circ (y\circ z)$
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
328
\node[thy, right of=sg] (m) {\begin{tabular}{l}
Michael Banken's avatar
Michael Banken committed
329 330 331 332 333 334 335 336 337 338 339
                             \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}

340
This problem is not entirely unlike the problem of the theory unions and other variations may apply to purely superfluous inclusions. 
Michael Banken's avatar
Michael Banken committed
341 342

\section{Structures}
Michael Banken's avatar
Michael Banken committed
343 344 345 346
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.

Michael Banken's avatar
Michael Banken committed
347
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}.