Index: doc/aaron_comp_II/comp_II.tex
===================================================================
--- doc/aaron_comp_II/comp_II.tex	(revision b44a7c55503ed27eacb384667c4cd4b0fa353e66)
+++ doc/aaron_comp_II/comp_II.tex	(revision a2565a2f9fc3ca215c85073f0fb206336d01c765)
@@ -245,39 +245,101 @@
 
 \section{Expression Resolution}
-
-\subsection{Argument-Directed}
-
-
-\subsection{Parameter-Directed}
-\textbf{TODO: Richard's algorithm isn't Baker (Cormack?), disentangle from this section \ldots}. 
-The expression resolution algorithm used by the existing iteration of {CFA-CC} is based on Baker's\cite{Baker82} algorithm for overload resolution in Ada. 
-The essential idea of this algorithm is to first find the possible interpretations of the most deeply nested subexpressions, then to use these interpretations to recursively generate valid interpretations of their superexpressions. 
-To simplify matters, the only expressions considered in this discussion of the algorithm are function application and literal expressions; other expression types can generally be considered to be variants of one of these for the purposes of the resolver, \eg variables are essentially zero-argument functions. 
-If we consider expressions as graph nodes with arcs connecting them to their subexpressions, these expressions form a DAG, generated by the algorithm from the bottom up.
-Literal expressions are represented by leaf nodes, annotated with the type of the expression, while a function application will have a reference to the function declaration chosen, as well as arcs to the interpretation nodes for its argument expressions; functions are annotated with their return type (or types, in the case of multiple return values).
-
-\textbf{TODO: Figure}
-
-Baker's algorithm was designed to account for name overloading; Richard Bilson\cite{Bilson03} extended this algorithm to also handle polymorphic functions, implicit conversions \& multiple return types when designing the original \CFA compiler. 
-The core of the algorithm is a function which Baker refers to as $gen\_calls$. 
-$gen\_calls$ takes as arguments the name of a function $f$ and a list containing the set of possible subexpression interpretations $S_j$ for each argument of the function and returns a set of possible interpretations of calling that function on those arguments. 
-The subexpression interpretations are generally either singleton sets generated by the single valid interpretation of a literal expression, or the results of a previous call to $gen\_calls$. 
-If there are no valid interpretations of an expression, the set returned by $gen\_calls$ will be empty, at which point resolution can cease, since each subexpression must have at least one valid interpretation to produce an interpretation of the whole expression. 
-On the other hand, if for some type $T$ there is more than one valid interpretation of an expression with type $T$, all interpretations of that expression with type $T$ can be collapsed into a single \emph{ambiguous expression} of type $T$, since the only way to disambiguate expressions is by their return types. 
-If a subexpression interpretation is ambiguous, than any expression interpretation containing it will also be ambiguous. 
-In the variant of this algorithm including implicit conversions, the interpretation of an expression as type $T$ is ambiguous only if there is more than one \emph{minimal-cost} interpretation of the expression as type $T$, as cheaper expressions are always chosen in preference to more expensive ones.
-
-Given this description of the behaviour of $gen\_calls$, its implementation is quite straightforward: for each function declaration $f_i$ matching the name of the function, consider each of the parameter types $p_j$ of $f_i$, attempting to match the type of an element of $S_j$ to $p_j$ (this may include checking of implicit conversions).
-If no such element can be found, there is no valid interpretation of the expression using $f_i$, while if more than one such (minimal-cost) element is found than an ambiguous interpretation with the result type of $f_i$ is produced. 
-In the \CFA variant, which includes polymorphic functions, it is possible that a single polymorphic function definition $f_i$ can produce multiple valid interpretations by different choices of type variable bindings; these interpretations are unambiguous so long as the return type of $f_i$ is different for each type binding. 
-If all the parameters $p_j$ of $f_i$ can be uniquely matched to a candidate interpretation, then a valid interpretation based on $f_i$ and those $p_j$ is produced. 
-$gen\_calls$ collects the produced interpretations for each $f_i$ and returns them; a top level expression is invalid if this list is empty, ambiguous if there is more than one (minimal-cost) result, or if this single result is ambiguous, and valid otherwise.
-
-In this implementation, resolution of a single top-level expression takes time $O(\ldots)$, where \ldots. \textbf{TODO:} \textit{Look at 2.3.1 in Richard's thesis when working out complexity; I think he does get the Baker algorithm wrong on combinations though, maybe\ldots}
-
-\textbf{TODO: Basic Lit Review} \textit{Look at 2.4 in Richard's thesis for any possible more-recent citations of Baker\ldots} \textit{Look back at Baker's related work for other papers that look similar to what you're doing, then check their citations as well\ldots} \textit{Look at Richard's citations in 2.3.2 w.r.t. type data structures\ldots}
-\textit{CormackWright90 seems to describe a solution for the same problem, mostly focused on how to find the implicit parameters}
+The expression resolution problem is essentially to determine an optimal matching between some combination of argument interpretations and the parameter list of some overloaded instance of a function; the argument interpretations are produced by recursive invocations of expression resolution, where the base case is zero-argument functions (which are, for purposes of this discussion, semantically equivalent to named variables or constant literal expressions). 
+Assuming that the matching between a function's parameter list and a combination of argument interpretations can be done in $O(p^k)$ time, where $p$ is the number of parameters and $k$ is some positive number, if there are $O(i)$ valid interpretations for each subexpression, there will be $O(i)$ candidate functions and $O(i^p)$ possible argument combinations for each expression, so a single recursive call to expression resolution will take $O(i^{p+1} \cdot p^k)$ time if it compares all combinations. 
+Given this bound, resolution of a single top-level expression tree of depth $d$ takes $O(i^{p+1} \cdot p^{k \cdot d})$ time\footnote{The call tree will have leaves at depth $O(d)$, and each internal node will have $O(p)$ fan-out, producing $O(p^d)$ total recursive calls.}.
+Expression resolution is somewhat unavoidably exponential in $p$, the number of function parameters, and $d$, the depth of the expression tree, but these values are fixed by the user programmer, and generally bounded by reasonably small constants. 
+$k$, on the other hand, is mostly dependent on the representation of types in the system and the efficiency of type assertion checking; if a candidate argument combination can be compared to a function parameter list in linear time in the length of the list (\ie $k = 1$), then the $p^{k \cdot d}$ term is linear in the input size of the source code for the expression, otherwise the resolution algorithm will exibit sub-linear performance scaling on code containing more-deeply nested expressions.
+The number of valid interpretations of any subexpression, $i$, is bounded by the number of types in the system, which is possibly infinite, though practical resolution algorithms for \CFA must be able to place some finite bound on $i$, possibly at the expense of type system completeness. 
+
+The research goal of this project is to develop a performant expression resolver for \CFA; this analysis suggests two primary areas of investigation to accomplish that end. 
+The first is efficient argument-parameter matching; Bilson\cite{Bilson03} mentions significant optimization opportunities available in the current literature to improve on the existing {CFA-CC} compiler \textbf{TODO:} \textit{look up and lit review}. 
+The second, and likely more fruitful, area of investigation is heuristics and algorithmic approaches to reduce the number of argument interpretations considered in the common case; given the large ($p+1$) exponent on number of interpretations considered in the runtime analysis, even small reductions here could have a significant effect on overall resolver runtime. 
+The discussion below presents a number of largely orthagonal axes for expression resolution algorithm design to be investigated, noting prior work where applicable. 
+
+\subsection{Argument-Parameter Matching}
+The first axis we consider is argument-parameter matching - whether the type matching for a candidate function to a set of candidate arguments is directed by the argument types or the parameter types. 
+
+\subsubsection{Argument-directed (``Bottom-up'')}
+Baker's algorithm for expression resolution\cite{Baker82} pre-computes argument candidates, from the leaves of the expression tree up.
+For each candidate function, Baker attempts to match argument types to parameter types in sequence, failing if any parameter cannot be matched.
+
+Bilson\cite{Bilson03} similarly pre-computes argument candidates in the original \CFA compiler, but then explicitly enumerates all possible argument combinations for a multi-parameter function; these argument combinations are matched to the parameter types of the candidate function as a unit rather than individual arguments.
+This is less efficient than Baker's approach, as the same argument may be compared to the same parameter many times, but allows a more straightforward handling of polymorphic type binding and multiple return types.
+It is possible the efficiency losses here relative to Baker could be significantly reduced by application of memoization to the argument-parameter type comparisons.
+
+\subsubsection{Parameter-directed (``Top-down'')}
+Unlike Baker and Bilson, Cormack's algorithm\cite{Cormack81} requests argument candidates which match the type of each parameter of each candidate function, from the top-level expression down; memoization of these requests is presented as an optimization.
+As presented, this algorithm requires the result of the expression to have a known type, though an algorithm based on Cormack's could reasonably request a candidate set of any return type, though such a set may be quite large.
+
+\subsubsection{Hybrid}
+This proposal includes the investigation of hybrid top-down/bottom-up argument-parameter matching.
+A reasonable hybrid approach might be to take a top-down approach when the expression to be matched is known to have a fixed type, and a bottom-up approach in untyped contexts.
+This may include switches from one type to another at different levels of the expression tree, for instance:
+\begin{lstlisting}
+forall(otype T)
+int f(T x);  // (1)
+
+void* f(char y);  // (2)
+
+int x = f( f( '!' ) );
+\end{lstlisting}
+Here, the outer call to ©f© must have a return type that is (implicitly convertable to) ©int©, so a top-down approach could be used to select \textit{(1)} as the proper interpretation of ©f©. \textit{(1)}'s parameter ©x© here, however, is an unbound type variable, and can thus take a value of any complete type, providing no guidance for the choice of candidate for the inner ©f©. The leaf expression ©'!'©, however, gives us a zero-cost interpretation of the inner ©f© as \textit{(2)}, providing a minimal-cost expression resolution where ©T© is bound to ©void*©.
+
+Deciding when to switch between bottom-up and top-down resolution in a hybrid algorithm is a necessarily heuristic process, and though finding good heuristics for it is an open question, one reasonable approach might be to switch from top-down to bottom-up when the number of candidate functions exceeds some threshold.
+
+\subsection{Implicit Conversion Application}
+Baker's\cite{Baker82} and Cormack's\cite{Cormack81} algorithms do not account for implicit conversions\footnote{Baker does briefly comment on an approach for handling implicit conversions.}; both assume that there is at most one valid interpretation of a given expression for each distinct type.
+Integrating implicit conversion handling into their algorithms provides some choice of implementation approach. 
+
+\subsubsection{On Parameters}
+Bilson\cite{Bilson03} did account for implicit conversions in his algorithm, but it is not clear his approach is optimal. 
+His algorithm integrates checking for valid implicit conversions into the argument-parameter matching step, essentially trading more expensive matching for a smaller number of argument interpretations. 
+This approach may result in the same subexpression being checked for a type match with the same type multiple times, though again memoization may mitigate this cost, and this approach will not generate implicit conversions that are not useful to match the containing function. 
+
+\subsubsection{On Arguments}
+Another approach would be to generate a set of possible implicit conversions for each set of interpretations of a given argument. 
+This would have the benefit of detecting ambiguous interpretations of arguments at the level of the argument rather than its containing call, and would also never find more than one interpretation of the argument with a given type. 
+On the other hand, this approach may unncessarily generate argument interpretations that will never match a parameter, wasting work.
+
+\subsection{Candidate Set Generation}
+
+\subsubsection{Eager}
+
+\subsubsection{Lazy}
+
+\subsubsection{Stepwise Lazy}
+
+%\subsection{Parameter-Directed}
+%\textbf{TODO: Richard's algorithm isn't Baker (Cormack?), disentangle from this section \ldots}. 
+%The expression resolution algorithm used by the existing iteration of {CFA-CC} is based on Baker's\cite{Baker82} algorithm for overload resolution in Ada. 
+%The essential idea of this algorithm is to first find the possible interpretations of the most deeply nested subexpressions, then to use these interpretations to recursively generate valid interpretations of their superexpressions. 
+%To simplify matters, the only expressions considered in this discussion of the algorithm are function application and literal expressions; other expression types can generally be considered to be variants of one of these for the purposes of the resolver, \eg variables are essentially zero-argument functions. 
+%If we consider expressions as graph nodes with arcs connecting them to their subexpressions, these expressions form a DAG, generated by the algorithm from the bottom up.
+%Literal expressions are represented by leaf nodes, annotated with the type of the expression, while a function application will have a reference to the function declaration chosen, as well as arcs to the interpretation nodes for its argument expressions; functions are annotated with their return type (or types, in the case of multiple return values).
+%
+%\textbf{TODO: Figure}
+%
+%Baker's algorithm was designed to account for name overloading; Richard Bilson\cite{Bilson03} extended this algorithm to also handle polymorphic functions, implicit conversions \& multiple return types when designing the original \CFA compiler. 
+%The core of the algorithm is a function which Baker refers to as $gen\_calls$. 
+%$gen\_calls$ takes as arguments the name of a function $f$ and a list containing the set of possible subexpression interpretations $S_j$ for each argument of the function and returns a set of possible interpretations of calling that function on those arguments. 
+%The subexpression interpretations are generally either singleton sets generated by the single valid interpretation of a literal expression, or the results of a previous call to $gen\_calls$. 
+%If there are no valid interpretations of an expression, the set returned by $gen\_calls$ will be empty, at which point resolution can cease, since each subexpression must have at least one valid interpretation to produce an interpretation of the whole expression. 
+%On the other hand, if for some type $T$ there is more than one valid interpretation of an expression with type $T$, all interpretations of that expression with type $T$ can be collapsed into a single \emph{ambiguous expression} of type $T$, since the only way to disambiguate expressions is by their return types. 
+%If a subexpression interpretation is ambiguous, than any expression interpretation containing it will also be ambiguous. 
+%In the variant of this algorithm including implicit conversions, the interpretation of an expression as type $T$ is ambiguous only if there is more than one \emph{minimal-cost} interpretation of the expression as type $T$, as cheaper expressions are always chosen in preference to more expensive ones.
+%
+%Given this description of the behaviour of $gen\_calls$, its implementation is quite straightforward: for each function declaration $f_i$ matching the name of the function, consider each of the parameter types $p_j$ of $f_i$, attempting to match the type of an element of $S_j$ to $p_j$ (this may include checking of implicit conversions).
+%If no such element can be found, there is no valid interpretation of the expression using $f_i$, while if more than one such (minimal-cost) element is found than an ambiguous interpretation with the result type of $f_i$ is produced. 
+%In the \CFA variant, which includes polymorphic functions, it is possible that a single polymorphic function definition $f_i$ can produce multiple valid interpretations by different choices of type variable bindings; these interpretations are unambiguous so long as the return type of $f_i$ is different for each type binding. 
+%If all the parameters $p_j$ of $f_i$ can be uniquely matched to a candidate interpretation, then a valid interpretation based on $f_i$ and those $p_j$ is produced. 
+%$gen\_calls$ collects the produced interpretations for each $f_i$ and returns them; a top level expression is invalid if this list is empty, ambiguous if there is more than one (minimal-cost) result, or if this single result is ambiguous, and valid otherwise.
+%
+%In this implementation, resolution of a single top-level expression takes time $O(\ldots)$, where \ldots. \textbf{TODO:} \textit{Look at 2.3.1 in Richard's thesis when working out complexity; I think he does get the Baker algorithm wrong on combinations though, maybe\ldots}
+%
+%\textbf{TODO: Basic Lit Review} \textit{Look at 2.4 in Richard's thesis for any possible more-recent citations of Baker\ldots} \textit{Look back at Baker's related work for other papers that look similar to what you're doing, then check their citations as well\ldots} \textit{Look at Richard's citations in 2.3.2 w.r.t. type data structures\ldots}
+%\textit{CormackWright90 seems to describe a solution for the same problem, mostly focused on how to find the implicit parameters}
 
 \section{Proposal}
+\textbf{TODO:} Talk about experimental setup here.
 
 \section{Completion Timeline}