Index: doc/theses/fangren_yu_MMath/features.tex
===================================================================
--- doc/theses/fangren_yu_MMath/features.tex	(revision 98c77b23c65a940cf9e4e2811e0737d6305418e2)
+++ doc/theses/fangren_yu_MMath/features.tex	(revision 8fe7a8559944d6ddee57c207f975f15dd8ddfb45)
@@ -13,5 +13,5 @@
 Here, manipulating the pointer address is the primary operation, while dereferencing the pointer to its value is the secondary operation.
 For example, \emph{within} a data structure, \eg stack or queue, all operations involve pointer addresses and the pointer may never be dereferenced because the referenced object is opaque.
-Alternatively, use a reference when its primary purpose is to alias a value, \eg a function parameter that does not copy the argument (performance reason).
+Alternatively, use a reference when its primary purpose is to alias a value, \eg a function parameter that does not copy the argument, for performance reasons.
 Here, manipulating the value is the primary operation, while changing the pointer address is the secondary operation.
 Succinctly, if the address changes often, use a pointer;
@@ -64,5 +64,5 @@
 The call applies an implicit dereference once to @x@ so the call is typed @f( int & )@ with @T = int@, rather than with @T = int &@.
 
-As for a pointer type, a reference type may have qualifiers, where @const@ is most common.
+As with a pointer type, a reference type may have qualifiers, where @const@ is most common.
 \begin{cfa}
 int x = 3; $\C{// mutable}$
@@ -188,5 +188,5 @@
 @[x, y, z]@ = foo( 3, 4 );  // return 3 values into a tuple
 \end{cfa}
-Along with making returning multiple values a first-class feature, tuples were extended to simplify a number of other common contexts that normally require multiple statements and/or additional declarations, all of which reduces coding time and errors.
+Along with making returning multiple values a first-class feature, tuples were extended to simplify a number of other common contexts that normally require multiple statements and/or additional declarations.
 \begin{cfa}
 [x, y, z] = 3; $\C[2in]{// x = 3; y = 3; z = 3, where types may be different}$
@@ -205,5 +205,5 @@
 Only when returning a tuple from a function is there the notion of a tuple value.
 
-Overloading in the \CFA type-system must support complex composition of tuples and C type conversions using a costing scheme giving lower cost to widening conversions that do not truncate a value.
+Overloading in the \CFA type-system must support complex composition of tuples and C type conversions using a conversion cost scheme giving lower cost to widening conversions that do not truncate a value.
 \begin{cfa}
 [ int, int ] foo$\(_1\)$( int );			$\C{// overloaded foo functions}$
@@ -223,5 +223,5 @@
 bar( foo( 3 ) ) // only one tuple returning call 
 \end{lstlisting}
-Hence, programers cannot take advantage of the full power of tuples but type match is straightforward.
+Hence, programmers cannot take advantage of the full power of tuples but type match is straightforward.
 
 K-W C also supported tuple variables, but with a strong distinction between tuples and tuple values/variables.
@@ -356,5 +356,5 @@
 \end{figure}
 
-Interestingly, in the third implementation of \CFA tuples by Robert Schluntz~\cite[\S~3]{Schluntz17}, the MVR functions revert back to structure based, where it remains in the current version of \CFA.
+Interestingly, in the third implementation of \CFA tuples by Robert Schluntz~\cite[\S~3]{Schluntz17}, the MVR functions revert back to structure based, and this remains in the current version of \CFA.
 The reason for the reversion is a uniform approach for tuple values/variables making tuples first-class types in \CFA, \ie allow tuples with corresponding tuple variables.
 This reversion was possible, because in parallel with Schluntz's work, generic types were added independently by Moss~\cite{Moss19}, and the tuple variables leveraged the same implementation techniques as for generic variables~\cite[\S~3.7]{Schluntz17}.
@@ -512,5 +512,5 @@
 looping is used to traverse the argument pack from left to right.
 The @va_list@ interface is walking up the stack (by address) looking at the arguments pushed by the caller.
-(Magic knowledge is needed for arguments pushed using registers.)
+(Compiler-specific ABI knowledge is needed for arguments pushed using registers.)
 
 \begin{figure}
@@ -683,5 +683,5 @@
 
 Nested \emph{named} aggregates are allowed in C but there is no qualification operator, like the \CC type operator `@::@', to access an inner type.
-\emph{To compensate for the missing type operator, all named nested aggregates are hoisted to global scope, regardless of the nesting depth, and type usages within the nested type are replaced with global type name.}
+To compensate for the missing type operator, all named nested aggregates are hoisted to global scope, regardless of the nesting depth, and type usages within the nested type are replaced with global type name.
 Hoisting nested types can result in name collisions among types at the global level, which defeats the purpose of nesting the type.
 \VRef[Figure]{f:NestedNamedAggregate} shows the nested type @T@ is hoisted to the global scope and the declaration rewrites within structure @S@.
@@ -729,5 +729,5 @@
 \end{figure}
 
-For good reasons, \CC chose to change this semantics:
+\CC chose to change this semantics:
 \begin{cquote}
 \begin{description}[leftmargin=*,topsep=0pt,itemsep=0pt,parsep=0pt]
@@ -769,5 +769,5 @@
 Like an anonymous nested type, a named Plan-9 nested type has its field names hoisted into @struct S@, so there is direct access, \eg @s.x@ and @s.i@.
 Hence, the field names must be unique, unlike \CC nested types, but the type names are at a nested scope level, unlike type nesting in C.
-In addition, a pointer to a structure is automatically converted to a pointer to an anonymous field for assignments and function calls, providing containment inheritance with implicit subtyping, \ie @U@ $\subset$ @S@ and @W@ $\subset$ @S@, \eg:
+In addition, a pointer to a structure is automatically converted to a pointer to an anonymous field for assignments and function calls, providing containment inheritance with implicit subtyping, \ie @U@ $<:$ @S@ and @W@ $<:$ @S@, \eg:
 \begin{cfa}
 void f( union U * u );
@@ -781,5 +781,5 @@
 Note, there is no value assignment, such as, @w = s@, to copy the @W@ field from @S@.
 
-Unfortunately, the Plan-9 designers did not lookahead to other useful features, specifically nested types.
+Unfortunately, the Plan-9 designers did not look ahead to other useful features, specifically nested types.
 This nested type compiles in \CC and \CFA.
 \begin{cfa}
@@ -808,5 +808,5 @@
 In addition, a semi-non-compatible change is made so that Plan-9 syntax means a forward declaration in a nested type.
 Since the Plan-9 extension is not part of C and rarely used, this change has minimal impact.
-Hence, all Plan-9 semantics are denoted by the @inline@ qualifier, which is good ``eye-candy'' when reading a structure definition to spot Plan-9 definitions.
+Hence, all Plan-9 semantics are denoted by the @inline@ qualifier, which clearly indicates the usage of Plan-9 definitions.
 Finally, the following code shows the value and pointer polymorphism.
 \begin{cfa}
@@ -847,5 +847,5 @@
 \end{c++}
 and again the expression @d.x@ is ambiguous.
-While \CC has no direct syntax to disambiguate @x@, \ie @d.B.x@ or @d.C.x@, it is possible with casts, @((B)d).x@ or @((C)d).x@.
+While \CC has no direct syntax to disambiguate @x@, \eg @d.B.x@ or @d.C.x@, it is possible with casts, @((B)d).x@ or @((C)d).x@.
 Like \CC, \CFA compiles the Plan-9 version and provides direct qualification and casts to disambiguate @x@.
 While ambiguous definitions are allowed, duplicate field names are poor practice and should be avoided if possible.
Index: doc/theses/fangren_yu_MMath/future.tex
===================================================================
--- doc/theses/fangren_yu_MMath/future.tex	(revision 98c77b23c65a940cf9e4e2811e0737d6305418e2)
+++ doc/theses/fangren_yu_MMath/future.tex	(revision 8fe7a8559944d6ddee57c207f975f15dd8ddfb45)
@@ -8,5 +8,5 @@
 \section{Closed Trait Types}
 
-Currently, \CFA does not have any closed types, as open type are the basis of its unique type-system, allowing new functions to be added at any time to override existing ones for trait satisfaction.
+Currently, \CFA does not have any closed types, as open types are the basis of its unique type-system, allowing new functions to be added at any time to override existing ones for trait satisfaction.
 Locally-declared nested-functions,\footnote{
 Nested functions are not a feature in C but supported by \lstinline{gcc} for multiple decades and are used heavily in \CFA.}
@@ -17,5 +17,5 @@
 Library implementers normally do not want users to override certain operations and cause the behaviour of polymorphic invocations to change.
 \item
-Caching and reusing resolution results in the compiler is effected, as newly introduced declarations can participate in assertion resolution;
+Caching and reusing resolution results in the compiler is affected, as newly introduced declarations can participate in assertion resolution;
 as a result, previously invalid subexpressions suddenly become valid, or alternatively cause ambiguity in assertions.
 \end{enumerate}
@@ -70,5 +70,5 @@
 \end{figure}
 
-A \CFA closed trait type is similar to a Haskell type class requiring an explicit instance declaration.
+A \CFA closed trait type is planned to be working similarly to a Haskell type class that requires an explicit instance declaration.
 The syntax for the closed trait might look like:
 \begin{cfa}
@@ -91,4 +91,5 @@
 
 \section{Associated Types}
+\label{s:AssociatedTypes}
 
 The analysis presented in \VRef{s:AssertionSatisfaction} shows if all type parameters have to be bound before assertion resolution, the complexity of resolving assertions becomes much lower as every assertion parameter can be resolved independently.
@@ -159,5 +160,5 @@
 \section{User-defined Conversions}
 
-Missing type-system feature is a scheme for user-defined conversions.
+A missing type-system feature in \CFA is a scheme for user-defined conversions.
 Conversion means one type goes through an arbitrary complex process of changing its value to some meaningful value in another type.
 Because the conversion process can be arbitrarily complex, it requires the power of a function.
Index: doc/theses/fangren_yu_MMath/resolution.tex
===================================================================
--- doc/theses/fangren_yu_MMath/resolution.tex	(revision 98c77b23c65a940cf9e4e2811e0737d6305418e2)
+++ doc/theses/fangren_yu_MMath/resolution.tex	(revision 8fe7a8559944d6ddee57c207f975f15dd8ddfb45)
@@ -2,5 +2,5 @@
 \label{c:content2}
 
-Recapping, the \CFA's type-system provides expressive polymorphism: variables can be overloaded, functions can be overloaded by argument and return types, tuple types, generic (polymorphic) functions and types (aggregates) can have multiple type parameters with assertion restrictions;
+Recapping, \CFA's type-system provides expressive polymorphism: variables can be overloaded, functions can be overloaded by argument and return types, tuple types, generic (polymorphic) functions and types (aggregates) can have multiple type parameters with assertion restrictions;
 in addition, C's multiple implicit type-conversions must be respected.
 This generality leads to internal complexity and correspondingly higher compilation cost directly related to type resolution.
@@ -24,5 +24,5 @@
 \end{enumerate}
 \VRef[Table]{t:SelectedFileByCompilerBuild} shows improvements for selected tests with accumulated reductions in compile time across each of the 5 fixes.
-To this day, the large reduction in compilation time significantly improves the development of the \CFA's runtime because of its frequent compilation cycles.
+The large reduction in compilation time significantly improves the development of the \CFA's runtime because of its frequent compilation cycles.
 
 \begin{table}[htb]
@@ -86,5 +86,5 @@
 
 \item \textbf{Safe} cost representing a widening conversion \eg @short@ to @int@, qualifier-adding conversions for pointer and reference types, and value conversion for enumeration constants.
-Even when conversions are safe, the fewest conversions it ranked better, \eg @short@ to @int@ versus @short@ to @long int@.
+When all conversions are safe, closer conversions are ranked better, \eg @short@ to @int@ versus @short@ to @long int@.
 \begin{cfa}
 void f( long int p ); $\C[2.5in]{// 1}$
@@ -110,10 +110,10 @@
 \end{cfa}
 \end{enumerate}
-Cost tuples are compared by lexicographical order, from unsafe (highest) to specialization (lowest), with ties moving to the next lowest item.
+Cost tuples are compared in lexicographical order, from unsafe (highest) to specialization (lowest), with ties moving to the next lowest item.
 At a subexpression level, the lowest cost candidate for each result type is included as a possible interpretation of the expression;
 at the top level, all possible interpretations of different types are considered (generating a total ordering) and the overall lowest cost is selected as the final interpretation of the expression.
 Glen Ditchfield first proposed this costing model~\cite[\S~4.4.5]{Ditchfield92} to generate a resolution behaviour that is reasonable to C programmers based on existing conversions in the C programming language.
 This model carried over into the first implementation of the \CFA type-system by Richard Bilson~\cite[\S~2.2]{Bilson03}, and was extended but not redesigned by Aaron Moss~\cite[chap.~4]{Moss19}.
-Moss's work began to show problems with the underlying costing model;
+Moss's work began to show problems with the underlying cost model;
 these design issues are part of this work.
 
@@ -171,5 +171,5 @@
 Other than the case of multiple exact matches, where all have cost zero, incomparable candidates under a partial ordering can often have different expression costs since different kinds of implicit conversions are involved, resulting in seemingly arbitrary overload selections.
 
-There are currently at least three different situations where the polymorphic cost element of the cost model does not yield a candidate selection that is clearly justifiable, and one of them is straight up wrong.
+There are currently at least three different situations where the polymorphic cost element of the cost model does not yield a candidate selection that is justifiable, and one of them is clearly wrong.
 \begin{enumerate}[leftmargin=*]
 \item Polymorphic exact match versus non-polymorphic inexact match.
@@ -193,5 +193,5 @@
 \end{itemize}
 In this example, option 1 produces the prototype @void f( int )@, which gives an exact match and therefore takes priority.
-The \CC resolution rules effectively make option 2 a specialization that only applies to type @long@ exactly,\footnote{\CC does have explicit template specializations, however they do not participate directly in overload resolution and can sometimes lead to unintuitive results.} while the current \CFA rules make option 2 apply for all integral types below @long@.
+The \CC resolution rules effectively make option 2 a specialization that only applies to type @long@ exactly,\footnote{\CC does have explicit template specializations, however they do not participate directly in overload resolution and can sometimes lead to unintuitive results.} while the current \CFA rules make option 2 apply for all integral types ranked lower than @long@ as well.
 This difference could be explained as compensating for \CFA polymorphic functions being separately compiled versus template inlining;
 hence, calling them requires passing type information and assertions increasing the runtime cost.
@@ -227,14 +227,14 @@
 Passing a @pair@ variable to @f@
 \begin{cfa}
-pair p;
+pair(int, double) p;
 f( p );
 \end{cfa}
 gives a cost of 1 poly, 2 variable for the @pair@ overload, versus a cost of 1 poly, 1 variable for the unconstrained overload.
 Programmer expectation is to select option 1 because of the exact match, but the cost model selects 2;
-while either could work, the type system should select a call that meets expectation of say the call is ambiguous, forcing the programmer to mediate.
+it is not possible to write a specialization for @f@ that works on any pair type and gets selected by the type resolver as intended.
 As a result, simply counting the number of polymorphic type variables is no longer correct to order the function candidates as being more constrained.
 \end{enumerate}
 
-These inconsistencies are not easily solvable in the current cost-model, meaning the current \CFA codebase has to workaround these defects.
+These inconsistencies are not easily solvable in the current cost-model, meaning that currently the \CFA codebase has to workaround these defects.
 One potential solution is to mix the conversion cost and \CC-like partial ordering of specializations.
 For example, observe that the first three elements (unsafe, polymorphic and safe conversions) in the \CFA cost-tuple are related to the argument/parameter types, while the other two elements (polymorphic variable and assertion counts) are properties of the function declaration.
@@ -469,5 +469,5 @@
 
 
-In previous versions of \CFA, this number was set at 4; as the compiler becomes more optimized and capable of handling more complex expressions in a reasonable amount of time, I have increased the limit to 8 and it does not lead to problems.
+In previous versions of \CFA, this number was set at 4; as the compiler has become more optimized and capable of handling more complex expressions in a reasonable amount of time, I have increased the limit to 8 and it has not led to problems.
 Only rarely is there a case where the infinite recursion produces an exponentially growing assertion set, causing minutes of time wasted before the limit is reached.
 Fortunately, it is very hard to generate this situation with realistic \CFA code, and the ones that have occurred have clear characteristics, which can be prevented by alternative approaches.
@@ -481,5 +481,5 @@
 In many cases, these problems can be avoided by examining other assertions that provide insight on the desired type binding: if one assertion parameter can only be matched by a unique option, the type bindings can be updated confidently without the need for backtracking.
 
-The Moss algorithm currently used in \CFA was developed using a simplified type system that captures most of \CFA type system features.
+The Moss algorithm currently used in \CFA was developed using a simplified type system that captures most of \CFA's type system features.
 The simulation results were then ported back to the actual language.
 The simulator used a mix of breadth- and depth-first search in a staged approach.
@@ -520,5 +520,5 @@
 Currently, type resolution cannot do enough return-type inferencing while performing eager assertion resolution: the return type information is unknown before the parent expression is resolved, unless the expression is an initialization context where the variable type is known.
 By delaying the assertion resolution until the return type becomes known, this problem can be circumvented.
-The truly problematic case occurs if a type variable does not appear in either of the parameter or return types and only appears in assertions or variables (associate types).
+The truly problematic case occurs if a type variable does not appear in either of the parameter or return types and only appears in assertions or variables (\newterm{associate types}).
 \begin{cfa}
 forall( T | { void foo( @T@ ) } ) int f( float ) {
@@ -527,5 +527,5 @@
 \end{cfa}
 This case is rare so forcing every type variable to appear at least once in parameter or return types does not limit the expressiveness of \CFA type system to a significant extent.
-The next section presents a proposal for including type declarations in traits rather than having all type variables appear in the trait parameter list, which is provides equivalent functionality to an unbound type parameter in assertion variables, and also addresses some of the variable cost issue discussed in \VRef{s:ExpressionCostModel}.
+\VRef{s:AssociatedTypes} presents a proposal for including type declarations in traits rather than having all type variables appear in the trait parameter list, which provides equivalent functionality to an unbound type parameter in assertion variables, and also addresses some of the variable cost issue discussed in \VRef{s:ExpressionCostModel}.
 
 
@@ -599,5 +599,5 @@
 \end{enumerate}
 
-\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.
+\CFA does attempt to incorporate upstream type information propagated from a variable 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 create the necessary effect.
