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}.
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.
Notably optimization candidates will not necessarily preserve the flattened graph. This is only the case for simply redundant inclusions(see below).
\section{Types of optimization candidates}
\subsection{Simply redundant inclusion}
\label{sec:redinc}
...
...
@@ -22,12 +24,12 @@ An inclusion of a theory $A\hookrightarrow{}C$ is \underline{simply redundant},
...\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
\node[thy, right of = bottom] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
...\\\hline
...
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
\node[thy, right of = middle] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
...
...
...
@@ -49,12 +51,12 @@ Simply redundant inclusions can be safely optimized by simply removing the redun
...\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
\node[thy, right of = bottom] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
...\\\hline
...
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
\node[thy, right of = middle] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
...
...
...
@@ -72,7 +74,6 @@ where $Includes(I)$ are the transitively included theories in I and $DirectInclu
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.
\subsection{Superfluous Inclusion}
\label{sec:superinc}
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}.\\
...
...
@@ -92,7 +93,7 @@ An inclusion of a theory $A\hookrightarrow{}B$ is \underline{purely superfluous}
X\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (top) {\begin{tabular}{l}
\node[thy, right of = bottom] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
no X
...
...
@@ -112,7 +113,7 @@ Purely superfluous inclusions can be removed while still retaining a valid theor
X\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (top) {\begin{tabular}{l}
\node[thy, right of = bottom] (top) {\begin{tabular}{l}
