Attention: Maintenance on monday 19.04.2021 from 07:00 - 13:00 (Gitlab and Mattermost are offline!)

algorithm.tex 7.58 KB
Newer Older
Michael Banken's avatar
Michael Banken committed
1
\chapter{Algorithm}
Michael Banken's avatar
Michael Banken committed
2

Michael Banken's avatar
Michael Banken committed
3
\section{Idea}
Michael Banken's avatar
Michael Banken committed
4 5 6 7 8 9 10 11 12 13 14 15
Since our approach to identifying candidates is large based on set theory, the algorithms for finding are also making heavy use of set operations, using essentially the same construction method for creating the set of optimization candidates as the definitions presented in \autoref{chap:candidates}.

\subsection{Graph Optimization}
Optimization of the theory graph happens one theory at a time, beginning at the outer most edges of the theory graphs, i.e. those theories that are not included by any other theory.

It may seem counter intuitive, since we are changing the theories before modifying the theories they depend upon, however our use of future lite code (see \autoref{sec:futurelite}) means that any change that might affect the outer theories should be discarded anyway, as it may be a desired part of the theory, even if it is not referenced in the theory itself, resulting in no effective gain for resolving inner theories first.

This is not true for the other direction, as removing unnecessary inclusions may significantly reduce the amount of dependencies that might limit our pruning of the inner theories.

As a result of these observations, it is a strictly better option to always prioritize outer theories and since the runtime will already will already be dominating the time needed for a sort, we can do so with little additional cost (see \autoref{sec:runtime}).

\subsection{Theory Optimization}
Michael Banken's avatar
Michael Banken committed
16
Optimization of a theory itself happens in two separate passes. The first pass detects and eliminates superfluous inclusions. The second pass cleans up any remaining simply redundant inclusions.
Michael Banken's avatar
Michael Banken committed
17 18 19

The reason for separating these passes is to avoid the removal of simply redundant inclusions, that will later have to be reinserted when eliminating a partially superfluous inclusion. An example for such a hazard is the example of an overlap between the two types of candidates in \autoref{fig:redundantoverlap}

Michael Banken's avatar
Michael Banken committed
20 21 22 23 24 25 26 27 28 29 30 31 32 33
\subsubsection{First pass - Eliminating superfluous inclusions}

%TODO

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.

\subsubsection{Second pass - Eliminating simply redundant inclusions}

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.

Proof sketch:\\
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.

Michael Banken's avatar
Michael Banken committed
34 35 36 37
\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.

Michael Banken's avatar
Michael Banken committed
38
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.
Michael Banken's avatar
Michael Banken committed
39

Michael Banken's avatar
Michael Banken committed
40
\section{Pseudo Code}
Michael Banken's avatar
Michael Banken committed
41 42 43 44

\subsection{Optimizing graph}

The following code applies the earlier optimizations to the entire theory graph.
Michael Banken's avatar
Michael Banken committed
45 46

\begin{algorithm}[H]
Michael Banken's avatar
Michael Banken committed
47 48 49
\label{alg:graph}
 \KwData{theoryGraph = theory graph to be optimized}
 \KwResult{replacements = map from theories to maps of theory inclusions to their replacement}
Michael Banken's avatar
Michael Banken committed
50
 \Begin{
Michael Banken's avatar
Michael Banken committed
51 52 53 54 55 56 57 58 59 60 61 62
 	futureUses := empty map\;
 	replacements := empty map\;
 	theoryGraph := sort(theoryGraph)\;
 	theoryGraphRev := reverse(theoryGraph)\;
 	\For{theory $\leftarrow$ theoryGraph}{
 		add include $\rightarrow$ usedTheories(theory) $\cup$ futureUses(theory) to futureUses\;
 		add theory $\rightarrow$ optimize(theory, futureUses(theory)) to replacements\;
 		\For{include $\leftarrow$ includes(theory)}{
 			replace include $\rightarrow$ futureUses(include)$\cup$usedTheories(include)$\cup$futureUses(theory) in futureUses\;
 		}
 		\KwRet replacements \;
 	}
Michael Banken's avatar
Michael Banken committed
63
 }
Michael Banken's avatar
Michael Banken committed
64
 \caption{optimizeGraph(theorygraph)}
Michael Banken's avatar
Michael Banken committed
65 66
\end{algorithm}

Michael Banken's avatar
Michael Banken committed
67
\subsection{Optimizing theory}
Michael Banken's avatar
Michael Banken committed
68

Michael Banken's avatar
Michael Banken committed
69
The following pseudo code combines the two earlier routines to apply optimizations to a given theory.
Michael Banken's avatar
Michael Banken committed
70

Michael Banken's avatar
Michael Banken committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84
\begin{algorithm}[H]
 \KwData{theory = theory from our theory graph\\
 futureUse = set of theories used by theories including $theory$ in future lite code\\
 pass changes that were already applied to the graph}
 \KwResult{replacements = map from theory inclusions to their replacement}
 \Begin{
 	replacements = superfluousIncludes(theory, futureUse)\;
 	\For{removal $\leftarrow$ redundantIncludes(theory, futureUse)}{
 		add removal $\rightarrow$ $\emptyset$ to replacements\;
 	}
 	\KwRet replacements\;
 } 
 \caption{optimize(theory, futureUse)}
\end{algorithm}
Michael Banken's avatar
Michael Banken committed
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111

\subsection{Finding superfluous inclusions}
\label{sec:alg_si}
The following pseudo code is for finding superfluous inclusions (see: \autoref{sec:superinc}).

\begin{algorithm}[H]
 \KwData{theory = theory from our theory graph\\
 futureUse = set of theories used by theories including $theory$ in future lite code\\
 pass changes that were already applied to the graph}
 \KwResult{replacements = map from theory inclusions to their replacement}
 \Begin{
 replacements := empty map\;
 futureUsedTheories := usedTheories(theory) $\cup$ futureUse\;
 candidates := DirectInludes(theory) $\setminus$ futureUsedTheories\;
 \For{candidate $\leftarrow$ candidates}{
 		neededCandidateIncludes := Includes(candidate) $\cap$ futureUsedTheories \;
		remainingIncludes := Includes((directIncludes(theory) $\cap$ futureUsedTheories))$\cup$ (directIncludes(theory) $\cap$ futureUsedTheories) \;
		neededCandidateIncludes := neededCandidateIncludes $\setminus$ remainingIncludes\;
		add candidate $\rightarrow$ neededCandidateIncludes to replacements\;
 }
 \KwRet superfluousIncludes\;
 \caption{superfluousIncludes(theory, futureUse)}
 }
\end{algorithm}

Note that in \autoref{sec:superinc} we made a destinction between purely and partially superfluous inclusions. However we do not need to make this distinction while searching for them, as we can search for them by using the criteria for generally superfluous inclusion. Since they only differ in the set of inclusions that needs to be retained and we write that set in our result anyway, both can be accomplished by the same routine.

Michael Banken's avatar
Michael Banken committed
112 113 114
\subsection{Finding simply redundant inclusions}
\label{sec:alg_sri}
The following pseudo code is for finding simply redundant inclusions (see: \autoref{sec:redinc}).
Michael Banken's avatar
Michael Banken committed
115 116

\begin{algorithm}[H]
Michael Banken's avatar
Michael Banken committed
117
 \KwData{$theory$ = theory from our theory graph\\
Michael Banken's avatar
Michael Banken committed
118
 pass changes that were already applied to the graph}
Michael Banken's avatar
Michael Banken committed
119
 \KwResult{$redundantIncludes$ = set of simply redundant inclusions}
Michael Banken's avatar
Michael Banken committed
120
 \Begin{
Michael Banken's avatar
Michael Banken committed
121 122 123 124
 $subIncludes := \emptyset$\
 $redundantIncludes := \emptyset$\;
 \For{$i \leftarrow directIncludes(theory)$}{
	$subIncludes := subIncludes \cup includes(i)$\; 
Michael Banken's avatar
Michael Banken committed
125
 }
Michael Banken's avatar
Michael Banken committed
126 127 128 129 130 131 132 133
 \For{$i \leftarrow directIncludes(theory)$}{
 	\If{$i \in subIncludes$} {
		$redundantIncludes := redundantIncludes \cup \{i\}$\;
	}
 }
 \KwRet $redundantIncludes$\;
 }
 \caption{simplyRedundantIncludes(theory, futureUse)}
Michael Banken's avatar
Michael Banken committed
134 135
\end{algorithm}

Michael Banken's avatar
Michael Banken committed
136 137
\section{Complexity analysis}
\subsection{Runtime}
Michael Banken's avatar
Michael Banken committed
138 139
\label{sec:runtime}
\subsection{Memory}