Commit 3b1a911f authored by Michael Banken's avatar Michael Banken

fixed some remaining lite codes

parent 3fb4dec8
No preview for this file type
......@@ -7,7 +7,7 @@ Since our approach to identifying candidates is largely based on set theory, the
\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.
It may seem counter intuitive, since we are changing the theories before modifying the theories they depend upon, however our use of future light cone (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.
......@@ -145,7 +145,7 @@ The following pseudo code applies 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\\
futureUse = set of theories used by theories including $theory$ in future light cone\\
pass changes that were already applied to the graph}
\KwResult{replacements = map from theory inclusions to their replacement}
\Begin{
......@@ -164,7 +164,7 @@ The following pseudo code is for finding superfluous inclusions (see: \autoref{s
\begin{algorithm}[H]
\KwData{theory = theory from our theory graph\\
futureUse = set of theories used by theories including $theory$ in future lite code\\
futureUse = set of theories used by theories including $theory$ in future light cone\\
pass changes that were already applied to the graph}
\KwResult{replacements = map from theory inclusions to their replacement}
\Begin{
......@@ -342,7 +342,7 @@ Assuming none of the library functions need larger memory, the overall memory us
\subsubsection{Theory optimization}
\begin{algorithm}[H]
\KwData{theory = theory from our theory graph\\
futureUse = set of theories used by theories including $theory$ in future lite code\\
futureUse = set of theories used by theories including $theory$ in future light cone\\
pass changes that were already applied to the graph}
\KwResult{\\
replacements = O($t^2$)\\
......
......@@ -356,4 +356,4 @@ It should be noted that all the cases discussed in this chapter assume the relat
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}.
In addition structures have proven to be especially difficult to consider for our future light cone, for reasons that will be discussed in \autoref{sec:futurelite}.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment