In the first pass we first take a selection of optimization candidates, namely those theories that are directly included, but not used in the current theory. These are the theories that need to be replaced.

The algorithm then computes all the necessary replacements by looking at all indirect inclusions that result from the inclusion to be replaced. The necessary replacements are those that are used by the theory or its future and are not already included by the theory or by one of its necessary dependencies.

For this algorithm it is not necessary to make a distinction between purely and partially superfluous inclusions, as the pure case is entirely subsumed by the partial case with an empty set of necessary inclusions.

As we discussed in \autoref{sec:puresivia} this pass cannot be expected to remove all the inclusions that are unneeded for retaining a valid graph, but what we do expect it to leave a valid graph valid.

Proof sketch:

\begin{itemize}

\item Any theory used by the current theory or its future is either directly included by the current theory or indirectly.

\item Any directly included theory that is necessary isn't a candidate and will therefore remain.

\item Any indirectly included theory is either included by a theory that is retained or by one that is being replaced. Since the replacement of a theory inclusion is the necessary subset of its included theories, all necessary dependencies will remain included.

The basic idea behind the second pass is to collect all those theories that are included indirectly by the current theory and throwing away all of those direct inclusions that are part of this set. This will leave us exactly with those inclusions that are not simply redundant, without changing the flattened theory graph.

The idea behind the second pass is to collect all those theories that are included indirectly by the current theory and throwing away all of those direct inclusions that are part of this set. This will leave us exactly with those inclusions that are not simply redundant, without changing the flattened theory graph.

Proof sketch:\\

Simply redundant inclusions are those, that are both directly and indirectly included.

Proof sketch:

\begin{itemize}

\item Simply redundant inclusions are those, that are both directly and indirectly included.

We get rid of those direct inclusions that are also indirect, so clearly all simply redundant inclusions must be gone.

\item For the invariance of the flattened theory graph, we must first assume that theories are partially ordered by inclusion and inclusion paths are of finite depth, ie. that cyclic inclusions are not present.\\

If we do so, all indirect inclusions must ultimately be the result of a direct inclusion, so all relevant direct inclusions are still in the set.\\

If these assumptions are wrong however, not only could we run into problems, but we will inevitably do so if the current theory is part of the cycle. It is therefore best to only perform this operation on a graph that satisfies our assumption.

\end{itemize}

\subsection{Future Lite Code}

\label{sec:futurelite}

In \autoref{sec:viability} we already mentioned the problem of future lite code. The obvious method for aquiring the future lite code is traversing the entire theory graph and whenever we find a theory inclusion, we make a note for the included theory that the theory we are currently traversing is part of its future code. Unfortunately this requires traversing the graph in its entirety.

For the actual algorithm we skip this part and instead put create a map of used theories in the future code, since this is the part we actually require. Since this means potentially going over every theory for every theory (or at least reasonably close to it), our runtime worst case for this part is quadratic in the number of theories in the graph.

For the actual algorithm we skip this part and instead put create a map of used theories in the future code, since this is the part we actually require. Since this means potentially going over every theory for every theory (or at least reasonably close to it), our worst case runtime for this part of the algorithm is quadratic in the number of theories in the graph.

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.

\node[thy, above of = bottom] (middle) {\begin{tabular}{l}

\textsf{middle}\\\hline

Y\\\hline

not X

\end{tabular}};

\node[thy, above of = middle] (top) {\begin{tabular}{l}

\textsf{top}\\\hline

...\\\hline

X, but not Y

\end{tabular}};

\draw[include] (bottom) -- (middle);

\draw[include] (middle) -- (top);

\end{tikzpicture}

\caption{Example of a graph where optimizing changes the future.}

\label{fig:changeablefuture}

\end{figure}

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}.

\node[thy, above of = bottom] (middle) {\begin{tabular}{l}

\textsf{middle}\\\hline

Y\\\hline

not X

\end{tabular}};

\node[thy, above of = middle] (top) {\begin{tabular}{l}

\textsf{top}\\\hline

...\\\hline

X, but not Y

\end{tabular}};

\draw[include] (bottom) -- (middle);

\draw[include, bend left] (bottom) edge (top);

\end{tikzpicture}

\caption{Example of a graph where optimizing changes the future.}

\label{fig:changedfuture}

\end{figure}

In the changed graph we can now optimize the purely superfluous inclusion of bottom in the theory middle. We could not have done this in the earlier graph, since X and therefore bottom was used in middle's future. Thus we need an updated version of the future to make full use of earlier optimizations.

To somewhat mitigate the effect this has on the performance, the future is created step by step, as we work our way from the outer edges of the graph towards the core.

\section{Pseudo Code}

\subsection{Optimizing graph}

The following code applies the earlier optimizations to the entire theory graph.

The following code applies the optimizations to the entire theory graph.

\begin{algorithm}[H]

\label{alg:graph}

...

...

@@ -66,7 +138,7 @@ The following code applies the earlier optimizations to the entire theory graph.

\subsection{Optimizing theory}

The following pseudo code combines the two earlier routines to apply optimizations to a given theory.

The following pseudo code applies optimizations to a given theory.

\begin{algorithm}[H]

\KwData{theory = theory from our theory graph\\

...

...

@@ -136,4 +208,6 @@ The following pseudo code is for finding simply redundant inclusions (see: \auto

@@ -224,6 +224,7 @@ As noted in \autoref{sec:puresi} there is very little that speaks against removi

\label{fig:redundantoverlap}

\end{figure}

\subsection{Purely superfluous inclusion}

\label{sec:puresivia}

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}).\\

...

...

@@ -257,8 +258,46 @@ However theory unions are not the only cases where optimization may be misplaced

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}.

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}).

\node[thy, above right of = bottom] (right) {\begin{tabular}{l}

\textsf{right}\\\hline

Y\\\hline

not X

\end{tabular}};

\node[thy, above left of = bottom] (left) {\begin{tabular}{l}

\textsf{left}\\\hline

Z\\\hline

not X

\end{tabular}};

\node[thy, above left of = right] (top) {\begin{tabular}{l}

\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.

\subsection{Partially superfluous inclusion}

Unsurprisingly this isn't the only case where this optimization can have unfortunate results. 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.

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.

\begin{figure}[h]

\begin{tikzpicture}[node distance=2cm]\myfontsize

...

...

@@ -284,7 +323,7 @@ Unsurprisingly this isn't the only case where this optimization can have unfortu

\label{fig:elalg}

\end{figure}

The considerations about theories including the candidate in the future lite code also apply to the partially superfluous case.

This problem is not entirely unlike the problem of the theory unions and other variations may apply to purely superfluous inclusions.

\section{Structures}

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.