algorithm.tex 7.51 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
16
17
18
19
20
21
22
23
24
25
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}
Optimization of a theory itself happens in two separate passes. In the first pass superfluous inclusions are detected and eliminated. In the second pass cleans up any remaining simply redundant inclusions. Both of these algorithms can be found below.

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}

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

Michael Banken's avatar
Michael Banken committed
26
\section{Pseudo Code}
Michael Banken's avatar
Michael Banken committed
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
\subsection{Finding simply redundant inclusions}
\label{sec:alg_sri}
The following pseudo code is for finding simply redundant inclusions (see: \autoref{sec:redinc}).

\begin{algorithm}[H]
 \KwData{$theory$ = theory from our theory graph\\
 pass changes that were already applied to the graph}
 \KwResult{$redundantIncludes$ = set of simply redundant inclusions}
 \Begin{
 $subIncludes := \emptyset$\
 $redundantIncludes := \emptyset$\;
 \For{$i \leftarrow directIncludes(theory)$}{
	$subIncludes := subIncludes \cup includes(i)$\; 
 }
 \For{$i \leftarrow directIncludes(theory)$}{
 	\If{$i \in subIncludes$} {
		$redundantIncludes := redundantIncludes \cup \{i\}$\;
	}
 }
 \KwRet $redundantIncludes$\;
 }
 \caption{simplyRedundantIncludes(theory, futureUse)}
\end{algorithm}

The basic idea behind this algorithm 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:\\
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.\\

Since theories are partially ordered by inclusion and inclusion paths are of finite depth, all indirect inclusions must ultimately be the result of a direct inclusion, so all relevant direct inclusions are still in the set.

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

\subsection{Optimizing theory}

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

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

\subsection{Optimizing graph}

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

\begin{algorithm}[H]
\label{alg:graph}
 \KwData{theoryGraph = theory graph to be optimized}
 \KwResult{replacements = map from theories to maps of theory inclusions to their replacement}
 \Begin{
 	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 \;
 	}
 }
 \caption{optimizeGraph(theorygraph)}
\end{algorithm}

Michael Banken's avatar
Michael Banken committed
129
130
\section{Complexity analysis}
\subsection{Runtime}
Michael Banken's avatar
Michael Banken committed
131
132
\label{sec:runtime}
\subsection{Memory}