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

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.

\section{Types of optimization candidates}

\subsection{Simply redundant inclusion}

...

...

@@ -168,12 +173,13 @@ Partially superfluous inclusions can be optimized by identifying the used subset

\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

The candidates discussed earlier are cases in which inclusions can be changed, not necessarily where they should be changed, as the only criterion that makes a theory an optimization candidate is that an optimization can be performed while still retaining a valid theory. There is nothing that guarantees that this theory is also preferable to the original or even desirable at all to have.\\

The danger of performing the proposed optimizations varies between the type of candidate and the context, but overall application without at least some user guidance is not recommended.

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

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

\label{fig:redundantoverlap}

\end{figure}

\subsection{Purely superfluous inclusion}

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

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.

\node[thy, below left of = union] (A) {\begin{tabular}{l}

\textsf{A}\\\hline

...\\\hline

...

\end{tabular}};

\node[thy, below right of = union] (B) {\begin{tabular}{l}

\textsf{B}\\\hline

...\\\hline

...

\end{tabular}};

\draw[include] (A) -- (union);

\draw[include] (B) -- (union);

\end{tikzpicture}

\caption{Example of a simple theory union}

\label{fig:theoryunion}

\end{figure}

However theory unions are not the only cases where optimization may be misplaced. When culling seemingly superfluous inclusions of non-empty theories we fundamentally change the theory graph, by cutting the content of the included theory from our candidate. This means that unlike the simply redundant case, this optimization should be carefully considered.

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

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

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

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

As a rule of thumb we can assume that anything that was declared as a named structure is there for a reason and should therefore not be touched by our optimizations. Obviously this reasoning does not apply in all cases, but it is reason enough to avoid them in an automated tool.

In addition structures have proven to be especially difficult to consider for our future lite code, for reasons that will be discussed in \autoref{sec:futurelite}.