candidates.tex 10.1 KB
Newer Older
Michael Banken's avatar
Michael Banken committed
1
\chapter{Candidates}
Michael Banken's avatar
Michael Banken committed
2

Michael Banken's avatar
Michael Banken committed
3
4
\section{Types of optimization candidates}
\subsection{Simply redundant inclusion}
Michael Banken's avatar
Michael Banken committed
5
6
An inclusion of a theory $A\hookrightarrow{}C$ is \underline{simply redundant}, if $C$ includes a theory $B$, such that $B\hookrightarrow{}C$ (see \autoref{fig:redundantbasic}).

7
8
9
\providecommand\myxscale{3.9}
\providecommand\myyscale{2.2}
\providecommand\myfontsize{\footnotesize}
Michael Banken's avatar
Michael Banken committed
10
11
\begin{figure}[!htb]
\begin{tikzpicture}[node distance=3cm]\footnotesize
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
\node[thy,  above of = bottom] (middle) {\begin{tabular}{l}
                             \textsf{middle}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
                             \textsf{top}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
\draw[include] (bottom) -- (middle);                          
\draw[include, bend left] (bottom) edge (top);                          
\draw[include] (middle)  -- (top);
\end{tikzpicture}
Michael Banken's avatar
Michael Banken committed
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
\caption{Simply redundant inclusion example}
\label{fig:redundantbasic}
\end{figure}

Simply redundant inclusions can be safely optimized by simply removing the redundant inclusion, as seen in \autoref{fig:redundantoptimized}, without changing the flattened graph due to the transitive nature of inclusions.
\begin{figure}[!htb]
\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
\node[thy,  above of = bottom] (middle) {\begin{tabular}{l}
                             \textsf{middle}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
                             \textsf{top}\\\hline
                             ...\\\hline
                             ...
                           \end{tabular}};
\draw[include] (bottom) -- (middle);                         
\draw[include] (middle)  -- (top);
\end{tikzpicture}
\caption{Example of simply redundant inclusion optimized}
\label{fig:redundantoptimized}
\end{figure}

Michael Banken's avatar
Michael Banken committed
60
\subsection{Superfluous Inclusion}
Michael Banken's avatar
Michael Banken committed
61
62
An inclusion of a theory $A\hookrightarrow{}B$ is \underline{superfluous}, if $B$ uses none of the constants declared in $A$. Such an inclusion can be \underline{purely superfluous} (\autoref{sec:puresi}) if it can be entirely removed, or \underline{partially superfluous} if it can be reduced to a subset of the theory inclusions in $A$ \autoref{sec:partiallysi}.\\
In both of these cases the inclusion can be replaced or removed entirely, while still yielding a well formed theory. However this changes the resulting flattened theory graph and can invalidate theories that include the optimized theory.\\
Michael Banken's avatar
Michael Banken committed
63
\subsubsection{Purely Superfluous Inclusion}
Michael Banken's avatar
Michael Banken committed
64
65
66
67
An inclusion of a theory $A\hookrightarrow{}B$ is \underline{purely superfluous}, if $B$ uses none of the constants in $A$, not even if they were declared in a theory $C$ such that $C\hookrightarrow{}A$.\\
\label{sec:puresi}
\begin{figure}[!htb]
\begin{tikzpicture}[node distance=3cm]\footnotesize
68
69
70
71
72
73
74
75
76
77
78
79
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             X\\\hline
                             ...
                           \end{tabular}};
\node[thy, above of = bottom] (top) {\begin{tabular}{l}
                             \textsf{top}\\\hline
                             ...\\\hline
                             no X
                           \end{tabular}};
\draw[include] (bottom) -- (top);
\end{tikzpicture}
Michael Banken's avatar
Michael Banken committed
80
81
82
83
84
85
86
\caption{Purely superfluous inclusion example}
\label{fig:purelysuperfluousbasic}
\end{figure}

Purely superfluous inclusions can be removed while still retaining a valid theory, however this will change the resulting theory graph. These changes may or may not be what is desired. An example for such an optimization can be seen in \autoref{fig:purelysuperfluousoptimized}.
\begin{figure}[!htb]
\begin{tikzpicture}[node distance=3cm]\footnotesize
87
\node[thy] (bottom) {\begin{tabular}{l}
88
                             \textsf{bottom}\\\hline
89
90
                             X\\\hline
                             ...
91
                           \end{tabular}};
Michael Banken's avatar
Michael Banken committed
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
\node[thy, above of = bottom] (top) {\begin{tabular}{l}
                             \textsf{top}\\\hline
                             ...\\\hline
                             no X
                           \end{tabular}};
\end{tikzpicture}
\caption{Example of purely superfluous inclusion optimized}
\label{fig:purelysuperfluousoptimized}
\end{figure}

\subsubsection{Partially Superfluous Inclusion}
\label{sec:partiallysi}
An inclusion of a theory $A\hookrightarrow{}B$ is \underline{partially superfluous}, if $B$ uses none of the constants in $A$, but uses some declarations that were declared in one or more theory $C$ such that C is (transitively) included in A.\\
\begin{figure}[!htb]
\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             $X_1$\\\hline
                             ...
                           \end{tabular}};
\node[right of = bottom] (dots) {...};
\node[thy, right of = dots] (bottomn) {\begin{tabular}{l}
                             \textsf{$bottom_n$}\\\hline
                             $X_n$\\\hline
                             ...
                          \end{tabular}};
118
\node[thy,  above of = bottom] (middle) {\begin{tabular}{l}
119
120
121
122
123
124
                             \textsf{middle}\\\hline
                             Y\\\hline
                             ...
                           \end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
                             \textsf{top}\\\hline
125
                             ...\\\hline
Michael Banken's avatar
Michael Banken committed
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
                             $X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
                           \end{tabular}};
\draw[include] (bottom) -- (middle);
\draw[include] (bottomn) -- (middle);                       
\draw[include] (middle)  -- (top);
\end{tikzpicture}
\caption{Partially superfluous inclusion example}
\label{fig:partiallysuperfluousbasic}
\end{figure}

Partially superfluous inclusions can be optimized by identifying the used subset of (transitive) inclusions and replacing the superfluous inclusion with these inclusions. As seen in \autoref{fig:partiallysuperfluousoptimized}.

\begin{figure}[!htb]
\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             $X_1$\\\hline
                             ...
144
                           \end{tabular}};
145
146
147
148
149
150
\node[right of = bottom] (dots) {...};
\node[thy, right of = dots] (bottomn) {\begin{tabular}{l}
                             \textsf{$bottom_n$}\\\hline
                             $X_n$\\\hline
                             ...
                          \end{tabular}};
Michael Banken's avatar
Michael Banken committed
151
152
153
154
155
156
157
158
159
160
\node[thy,  above of = bottom] (middle) {\begin{tabular}{l}
                             \textsf{middle}\\\hline
                             Y\\\hline
                             ...
                           \end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
                             \textsf{top}\\\hline
                             ...\\\hline
                             $X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
                           \end{tabular}};
161
\draw[include] (bottom) -- (middle);
Michael Banken's avatar
Michael Banken committed
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
\draw[include] (bottomn) -- (middle);
\draw[include] (bottomn) -- (top);                       
\draw[include, bend left] (bottom)  edge (top);
\end{tikzpicture}
\caption{Example of partially superfluous inclusion optimized}
\label{fig:partiallysuperfluousoptimized}
\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 
\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.\\
\begin{figure}[h]
\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
                             \textsf{bottom}\\\hline
                             X\\\hline
                             ...
                           \end{tabular}};
\node[thy,  above of = bottom] (middle) {\begin{tabular}{l}
                             \textsf{middle}\\\hline
                             Y\\\hline
                             ...
                           \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);                     
194
195
\draw[include] (middle)  -- (top);
\end{tikzpicture}
Michael Banken's avatar
Michael Banken committed
196
197
198
199
200
201
202
203
\caption{Example of overlap between simply redundant inclusion and superfluous inclusion}
\label{fig:redundantoverlap}
\end{figure}
\subsection{Purely superfluous inclusion}

\subsection{Partially superfluous inclusion}

\section{Structures}