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}).
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.
\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}
\subsection{Superfluous Inclusion}
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.\\
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$.\\
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}.
\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.\\
\node[thy, right of = dots] (bottomn) {\begin{tabular}{l}
\textsf{$bottom_n$}\\\hline
$X_n$\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
Y\\\hline
...
...
@@ -54,7 +123,24 @@
\node[thy, above of = middle] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
X, but not Y
$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}.
\node[thy, right of = dots] (bottomn) {\begin{tabular}{l}
...
...
@@ -62,8 +148,56 @@
$X_n$\\\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\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
\end{tabular}};
\draw[include] (bottom) -- (middle);
\draw[include] (bottomn) -- (middle);
\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}
The candidates discussed earlier are cases in which inclusions can be changed, not necessarily where they should be changed.\\
There are multiple reasons for not
\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.\\
