@@ -8,8 +8,7 @@ For something to be declared a candidates we will only require that the theory i
...
@@ -8,8 +8,7 @@ For something to be declared a candidates we will only require that the theory i
Notably optimization candidates will not necessarily preserve the flattened graph. This is only the case for simply redundant inclusions(see below).
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}
\section{Simply redundant inclusion}
\subsection{Simply redundant inclusion}
\label{sec:redinc}
\label{sec:redinc}
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}).
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}).
...
@@ -74,7 +73,7 @@ where $Includes(I)$ are the transitively included theories in I and $DirectInclu
...
@@ -74,7 +73,7 @@ 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)$.\\
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.
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}
\section{Superfluous Inclusion}
\label{sec:superinc}
\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}.\\
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.\\
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.\\
...
@@ -82,9 +81,9 @@ In both of these cases the inclusion can be replaced or removed entirely, while
...
@@ -82,9 +81,9 @@ In both of these cases the inclusion can be replaced or removed entirely, while
The superfluous inclusions in a theory T are the set $I_{S}(T)=$\\$\{ I \in DirectInludes(T) | I \notin UsedTheories(T)\}$,\\
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.
where $DirectIncludes(T)$ are the theories included directly in the theory T and UsedTheories(T) are those theories whose terms are used in T.
\subsubsection{Purely Superfluous Inclusion}
\subsection{Purely Superfluous Inclusion}
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}
\label{sec:puresi}
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$.\\
@@ -126,29 +125,31 @@ Purely superfluous inclusions can be removed while still retaining a valid theor
...
@@ -126,29 +125,31 @@ Purely superfluous inclusions can be removed while still retaining a valid theor
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\}$,\\
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.
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.
\subsubsection{Partially Superfluous Inclusion}
\subsection{Partially Superfluous Inclusion}
\label{sec:partiallysi}
\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. We describe theories that have declarations being used in a theory A, which includes them, as \underline{theories used by A}.\\
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}.\\
\node[below = 0.2cm of bottom] (dots) {\begin{tabular}{l}
\node[thy, right of = dots] (bottomn) {\begin{tabular}{l}
.\\.\\.\\
\end{tabular}};
\node[thy, below = 0.2cm of dots] (bottomn) {\begin{tabular}{l}
\textsf{$bottom_n$}\\\hline
\textsf{$bottom_n$}\\\hline
$X_n$\\\hline
$X_n$\\\hline
...
...
\end{tabular}};
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
\node[thy, right = 1.5cm of dots] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
\textsf{middle}\\\hline
Y\\\hline
Y\\\hline
...
...
\end{tabular}};
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
\node[thy, right = 1.2 of middle, node distance=4.3cm ] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
\textsf{top}\\\hline
...\\\hline
...\\\hline
$X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
$X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
...
@@ -190,7 +193,7 @@ Partially superfluous inclusions can be optimized by identifying the used subset
...
@@ -190,7 +193,7 @@ Partially superfluous inclusions can be optimized by identifying the used subset
\draw[include] (bottom) -- (middle);
\draw[include] (bottom) -- (middle);
\draw[include] (bottomn) -- (middle);
\draw[include] (bottomn) -- (middle);
\draw[include] (bottomn) -- (top);
\draw[include] (bottomn) -- (top);
\draw[include, bend left] (bottom) edge (top);
\draw[include] (bottom) -- (top);
\end{tikzpicture}
\end{tikzpicture}
\caption{Example of partially superfluous inclusion optimized}
\caption{Example of partially superfluous inclusion optimized}
\label{fig:partiallysuperfluousoptimized}
\label{fig:partiallysuperfluousoptimized}
...
@@ -208,18 +211,18 @@ The danger of performing the proposed optimizations varies between the type of c
...
@@ -208,18 +211,18 @@ The danger of performing the proposed optimizations varies between the type of c
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.\\
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.\\
