@@ -55,7 +55,8 @@ For the actual algorithm we skip this part and instead put create a map of used
...
@@ -55,7 +55,8 @@ For the actual algorithm we skip this part and instead put create a map of used
This runtime is especially problematic, since we need to update the the information after every step of the optimization to make proper use of any improvements of the graph. We can demonstrate this by considering the following example.
This runtime is especially problematic, since we need to update the the information after every step of the optimization to make proper use of any improvements of the graph. We can demonstrate this by considering the following example.
@@ -81,7 +82,8 @@ This runtime is especially problematic, since we need to update the the informat
...
@@ -81,7 +82,8 @@ This runtime is especially problematic, since we need to update the the informat
As we can immediately see in \autoref{fig:changeablefuture}, it is possible to replace the partially superfluous inclusion of middle in top with bottom. The result is the changed graph in \autoref{fig:changedfuture}.
As we can immediately see in \autoref{fig:changeablefuture}, it is possible to replace the partially superfluous inclusion of middle in top with bottom. The result is the changed graph in \autoref{fig:changedfuture}.
@@ -41,6 +42,7 @@ An inclusion of a theory $A\hookrightarrow{}C$ is \underline{simply redundant},
...
@@ -41,6 +42,7 @@ An inclusion of a theory $A\hookrightarrow{}C$ is \underline{simply redundant},
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.
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.
@@ -83,6 +85,7 @@ where $DirectIncludes(T)$ are the theories included directly in the theory T and
...
@@ -83,6 +85,7 @@ where $DirectIncludes(T)$ are the theories included directly in the theory T and
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$.\\
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$.\\
@@ -102,6 +105,7 @@ An inclusion of a theory $A\hookrightarrow{}B$ is \underline{purely superfluous}
...
@@ -102,6 +105,7 @@ An inclusion of a theory $A\hookrightarrow{}B$ is \underline{purely superfluous}
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}.
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}.
@@ -125,6 +129,7 @@ where $Includes(I)$ are the transitively included theories in I, $DirectIncludes
...
@@ -125,6 +129,7 @@ where $Includes(I)$ are the transitively included theories in I, $DirectIncludes
\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}.\\
@@ -158,6 +163,7 @@ An inclusion of a theory $A\hookrightarrow{}B$ is \underline{partially superfluo
...
@@ -158,6 +163,7 @@ An inclusion of a theory $A\hookrightarrow{}B$ is \underline{partially superfluo
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}.
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}.
@@ -199,7 +205,8 @@ The danger of performing the proposed optimizations varies between the type of c
...
@@ -199,7 +205,8 @@ The danger of performing the proposed optimizations varies between the type of c
\subsection{Simply redundant inclusion}
\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.\\
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.\\
@@ -230,7 +237,8 @@ Purely superfluous includes are a little trickier, as their removal can fundamen
...
@@ -230,7 +237,8 @@ Purely superfluous includes are a little trickier, as their removal can fundamen
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}).\\
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.
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.
@@ -260,7 +268,8 @@ If this content is required by a theory that originally included it via an inclu
...
@@ -260,7 +268,8 @@ If this content is required by a theory that originally included it via an inclu
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}).
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}).
@@ -299,7 +308,8 @@ Due to the inherent similarities many of the prior considerations also apply to
...
@@ -299,7 +308,8 @@ Due to the inherent similarities many of the prior considerations also apply to
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.
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.