Index: doc/theses/fangren_yu_MMath/intro.tex
===================================================================
--- doc/theses/fangren_yu_MMath/intro.tex	(revision 597ddfeb10fef2c06e63efb640839e2647564036)
+++ doc/theses/fangren_yu_MMath/intro.tex	(revision 2572addbb8aee3c5431c49eb112bb76eed2c97b2)
@@ -903,5 +903,6 @@
 						& O\footnote{except assignment}/F	& O/F/M	& V/O/F	& M\footnote{not universal}	& O/M	& O/F/M	& no	& no	\\
 general constraints\footnote{T $\Rightarrow$ parameter type, \# $\Rightarrow$ parameter number, N $\Rightarrow$ parameter name; R $\Rightarrow$ return type}
-						& T/\#/N/R	& T/\#	& T/\#/R	& T/\#	& T/\#/N/R	& T/\#/N/R	& T/\#/N	& T/R \\
+						& T/\#//R\footnote{parameter names can be used to disambiguate among overloads but not create overloads}
+									& T/\#	& T/\#/R	& T/\#	& T/\#/N/R	& T/\#/N/R	& T/\#/N	& T/R \\
 univ. type constraints\footnote{A $\Rightarrow$ concept, T $\Rightarrow$ interface/trait/type-class, B $\Rightarrow$ type bounds}
 						& no\footnote{generic cannot be overloaded}		& C		& T			& B		& B			& T			& T			& T \\
Index: doc/theses/fangren_yu_MMath/resolution.tex
===================================================================
--- doc/theses/fangren_yu_MMath/resolution.tex	(revision 597ddfeb10fef2c06e63efb640839e2647564036)
+++ doc/theses/fangren_yu_MMath/resolution.tex	(revision 2572addbb8aee3c5431c49eb112bb76eed2c97b2)
@@ -159,31 +159,16 @@
 In \CFA, trying to use such a system is problematic because of the presence of return-type overloading of functions and variable.
 Specifically, \CFA expression resolution considers multiple interpretations of argument subexpressions with different types, \eg:
-\begin{cfa}
-@generate a CFA example here@
-
-read more
-\end{cfa}
 so it is possible that both the selected function and the set of arguments are different, and cannot be compared with a partial-ordering system.
-This situation arises often in \CFA, even in the simple expression @f(x)@, where both the function name @f@ and variable name @x@ are overloaded.
+This situation arises often in \CFA, even in the simple expression @f(x)@, where both the function name @f@ and variable name @x@ are overloaded (examples to follow).
 
 Ada is another programming language that has overloading based on return type.
-Although Ada also allows implicit type conversions of function arguments, it is fairly conservative on resolving ambiguities~\cite[\S~8.6]{Ada22}.
-\begin{cfa}
-@generate an Ada example here@
-
-section 8.6 the context of overload resolution
-page 468, item number 28 - 30 
-\end{cfa}
-There are only two preference rules in Ada overload resolution, one for primitive arithmetic operators and one for universal access types (pointer type);
-\begin{ada}
-Function "-"( L, R : Float ) return Integer is begin
-	return Integer(L) + (-Integer(R)); --  prevent infinite recursion
-end;
-Integer i;
-i := 7 - 3; -- prefer 
-i := 7.2 - 3.5
-\end{ada}
-any other cases where an expression has multiple legal interpretations are considered ambiguous.
-The current overload resolution system for \CFA is on the other end of the spectrum, as it tries to order every legal interpretations of an expression and chooses the best one according to cost, occasionally giving unexpected results rather than an ambiguity.
+Ada has no type conversions but has subtyping so subtypes are convertible to supertypes.
+There are only two preference rules in Ada overload resolution:
+\begin{quote}
+There is a preference for the primitive operators (and ranges) of the root numeric types @root_integer@ and @root_real@.
+In particular, if two acceptable interpretations of a constituent of a complete context differ only in that one is for a primitive operator (or range) of the type @root_integer@ or @root_real@, and the other is not,
+\end{quote}
+However, I was unable to generate any Ada example program that demonstrates this preference.
+In contrast, the \CFA overload resolution-system is at the other end of the spectrum, as it tries to order every legal interpretations of an expression and chooses the best one according to cost, occasionally giving unexpected results rather than an ambiguity.
 
 Interestingly, the \CFA cost-based model can sometimes make expression resolution too permissive because it always attempts to select the lowest cost option, and only when there are multiple options tied at the lowest cost does it report the expression is ambiguous.
@@ -378,18 +363,18 @@
 This is demonstrated in the following example, adapted from the C standard library:
 \begin{cfa}
-	unsigned long long x;
-	(unsigned)( x >> 32 );
+unsigned long long x;
+(unsigned)( x >> 32 );
 \end{cfa}
 \vspace{5pt}
 In C semantics, this example is unambiguously upcasting 32 to @unsigned long long@, performing the shift, then downcasting the result to @unsigned@, at cost (1, 0, 3, 1, 0, 0, 0).
 If ascription were allowed to be a first-class interpretation of a cast expression, it would be cheaper to select the @unsigned@ interpretation of @?>>?@ by downcasting @x@ to @unsigned@ and upcasting 32 to @unsigned@, at a total cost of (1, 0, 1, 1, 0, 0, 0).
-\PAB{This example feels incorrect. Assume a word size of 4 bits (long long). Given the value 1001, shift it >> 2, gives 10, which fits in a half word (int). Now truncate 1001 to a halfword 01 and shift it >> 2, gives 00. So the lower-cost alternative does generate the correct result. Basically truncation is an unsafe operation and hence has a huge negative cost.}
-However, this break from C semantics is not backwards compatible, so to maintain C compatibility, the \CFA resolver selects the lowest-cost interpretation of the cast argument for which a conversion or coercion to the target type exists (upcasting to @unsigned long long@ in the example above, due to the lack of unsafe downcasts), using the cost of the conversion itself only as a tie-breaker.\cite[pp.~46-47]{Moss19}
+\PAB{[Note, this alternate interpretation is semantically incorrect, because the downcasting \lstinline{x} to from \lstinline{long long} to \lstinline{unsigned} is unsafe (truncation).]}
+However, this break from C semantics is not backwards compatible, so to maintain C compatibility, the \CFA resolver selects the lowest-cost interpretation of the cast argument for which a conversion or coercion to the target type exists (upcasting to @unsigned long long@ in the example above, due to the lack of unsafe downcasts), using the cost of the conversion itself only as a tie-breaker.~\cite[pp.~46-47]{Moss19}
 \end{cquote}
 However, a cast expression is unnecessary to have such inconsistency to C semantics.
 An implicit argument-parameter type conversion in a function calls can replicate this issue without an explicit cast.
 \begin{cfa}
-unsigned long long x;
-void f( unsigned );
+	unsigned long long x;
+	void f( unsigned );
 f( x >> 32 );
 \end{cfa}
@@ -619,7 +604,7 @@
 \end{enumerate}
 
-\CFA does attempt to incorporate upstream type information propagated from variable declaration with initializer, since the type of the variable being initialized is definitely known.
+\CFA does attempt to incorporate upstream type information propagated from variable a declaration with initializer, since the type of the variable being initialized is known.
 However, the current type-environment representation is flawed in handling such type inferencing, when the return type in the initializer is polymorphic.
-Currently, an inefficient workaround is performed to efficiency the necessary effect.
+Currently, an inefficient workaround is performed to create the necessary effect.
 The following is an annotated example of the workaround.
 \begin{cfa}
@@ -629,5 +614,4 @@
 const char * x = "hello world";
 int ch = x[0];
-// Fails with simple return type binding (xxx -- check this!) as follows:
 // * T is bound to int
 // * (x: const char *) is unified with int *, which fails