Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision 104a13ea5d327bb08e0c9d3d988a704b095aa283)
+++ doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision e451c0f0917272e92aac63fa7493aba98ca92c69)
@@ -164,4 +164,9 @@
 Accordingly, the cost of a single argument-parameter unification is $O(d)$, where !d! is the depth of the expression tree, and the cost of argument-parameter unification for a single candidate for a given function call expression is $O(pd)$, where $p$ is the number of parameters. 
 
+Implicit conversions are also checked in argument-parameter matching, but the cost of checking for the existence of an implicit conversion is again proportional to the complexity of the type, $O(d)$. 
+Polymorphism again introduces a potential expense here; for a monomorphic function there is only one potential implicit conversion from argument type to parameter type, while if the parameter type is an unbound polymorphic type variable then any implicit conversion from the argument type could potentially be considered a valid binding for that type variable. 
+\CFA{}, however, requires exact matches for the bound type of polymorphic parameters, removing this problem. 
+An interesting question for future work is whether loosening this requirement incurs significant runtime cost in practice.
+
 Considering the recursive traversal of the expression tree, polymorphism again greatly expands the worst-case runtime. 
 Letting $i$ be the number of candidate declarations for each function call, if all of these candidates are monomorphic then there are no more than $i$ unambiguous interpretations of the subexpression rooted at that function call. 
@@ -174,11 +179,23 @@
 Given these calculations of number of subexpression interpretations and matching costs, the upper bound on runtime for generating candidates for a single subexpression $d$ levels up from the leaves is $O( i^{p^d} \cdot pd )$. 
 Since there are $O(p^d)$ subexpressions in a single top-level expression, the total worst-case cost of argument-parameter matching with the overloading and polymorphism features of \CFA{} is $O( i^{p^d} \cdot pd \cdot p^d )$. 
+Since the size of the expression is $O(p^d)$, letting $n = p^d$ this simplifies to $O(i^n \cdot n^2)$
 
 This already high bound does not yet account for the cost of assertion resolution, though. 
-% continue from here
-
-% need to discuss that n == p^d, that that i^p^d bound is **super** rare, and will usually be closer to $i$
-
-% missing a +1 somewhere in these bounds; also, pd is O(n) ()
+\CFA{} uses type unification on the assertion type and the candidate declaration type to test assertion satisfaction; this unification calculation has cost proportional to the complexity of the declaration type after substitution of bound type variables; as discussed above, this cost is $O(d)$. 
+If there are $O(a)$ type assertions on each declaration, there are $O(i)$ candidates to satisfy each assertion, for a total of $O(ai)$ candidates to check for each declaration. 
+However, each assertion candidate may generate another $O(a)$ assertions, recursively until the assertion recursion limit $r$ is reached, for a total cost of $O((ai)^r \cdot d)$. 
+Now, $a$, $i$, and $r$ are properties of the set of declarations in scope, or the language spec in the case of $r$, so $(ai)^r$ is essentially a constant, albeit a very large one. 
+It is not uncommon in \CFA{} to have functions with dozens of assertions, and common function names (\eg{} !?{}!, the constructor) can have hundreds of overloads.
+
+It is clear that assertion resolution costs can be very large, and in fact a method for heuristically reducing them is one of the key contributions of this thesis, but it should be noted that the worst-case analysis is a particularly poor match for actual code in the case of assertions. 
+It is reasonable to assume that most code compiles without errors, as in an actively-developed project the code will be compiled many times, generally with relatively few new errors introduced between compiles. 
+However, the worst-case bound for assertion resolution is based on recursive assertion satisfaction exceeding the limit, which is an error case.
+In practice, then, the depth of recursive assertion satisfaction should be bounded by a small constant for error-free code, which will account for the vast majority of problem instances.
+
+Similarly, uses of polymorphism like those that generate the $O(d)$ bound on unification or the $O(i^{p^d})$ bound on number of candidates are particular enough to be rare, but not completely absent. 
+This analysis points to type unification, argument-parameter matching, and assertion satisfaction as potentially costly elements of expression resolution, and thus potentially profitable targets for tuning on realistic data. 
+Type unification is discussed in Chapter~\ref{env-chap}, while the other aspects are covered below.
+
+% also, unification of two classes is not particularly cheap ... the bounds above may be optimistic
 
 \subsection{Related Work}