Index: doc/theses/jiada_liang_MMath/background.tex
===================================================================
--- doc/theses/jiada_liang_MMath/background.tex	(revision ab11ab1beb9d10d00e4dab6b43817c7e9271e435)
+++ doc/theses/jiada_liang_MMath/background.tex	(revision 7568e5ca6e5718e97f473656ac2d190bb2a13f6a)
@@ -1,5 +1,5 @@
 \chapter{Background}
 
-This chapter covers background material for C enumerations and \CFA features used in later discussion.
+This chapter covers background material for C enumerations and \CFA features used in later discussions.
 
 
@@ -14,9 +14,9 @@
 \begin{enumerate}[leftmargin=*]
 \item
-For @#define@, the programmer has to explicitly manage the constant name and value.
-Furthermore, these C preprocessor macro names are outside of the C type-system and can incorrectly change random text in a program.
+For @#define@, the programmer must explicitly manage the constant name and value.
+Furthermore, these C preprocessor macro names are outside the C type system and can incorrectly change random text in a program.
 \item
 The same explicit management is true for the @const@ declaration, and the @const@ variable cannot appear in constant-expression locations, like @case@ labels, array dimensions,\footnote{
-C allows variable-length array-declarations (VLA), so this case does work, but it fails in \CC, which does not support VLAs, unless it is \lstinline{g++}.} immediate oper\-ands of assembler instructions, and occupies storage.
+C allows variable-length array declarations (VLA), so this case does work. Still, it fails in \CC, which does not support VLAs, unless it is \lstinline{g++}.} immediate oper\-ands of assembler instructions and occupies storage.
 \begin{clang}
 $\$$ nm test.o
@@ -87,13 +87,13 @@
 enum { Size = 20, Max = 10, MaxPlus10 = Max + 10, @Max10Plus1@, Fred = -7 };
 \end{clang}
-Here, the aliased constants are: 20, 10, 20, 21, and -7.
-Direct initialization is by a compile-time expression generating a constant value.
+Here, the aliased constants are 20, 10, 20, 21, and -7.
+Direct initialization is achieved by a compile-time expression that generates a constant value.
 Indirect initialization (without an initializer, @Max10Plus1@) is called \newterm{auto-initialization}, where enumerators are assigned values from left to right, starting at zero or the next explicitly initialized constant, incrementing by @1@.
 Because multiple independent enumerators can be combined, enumerators with the same values can occur.
-The enumerators are rvalues, so assignment is disallowed.
+The enumerators are @rvalues@, so the assignment is disallowed.
 Finally, enumerators are \newterm{unscoped}, \ie enumerators declared inside of an @enum@ are visible (projected) outside into the enclosing scope of the @enum@ type.
-For unnamed enumerations, this semantic is required because there is no type name for scoped qualification.
-
-As noted, this kind of aliasing declaration is not an enumeration, even though it is declared using an @enum@ in C.
+This semantic is required for unnamed enumerations because there is no type name for scoped qualification.
+
+As noted, this aliasing declaration is not an enumeration, even though it is declared using an @enum@ in C.
 While the semantics is misleading, this enumeration form matches with aggregate types:
 \begin{cfa}
@@ -121,5 +121,5 @@
 };
 \end{clang}
-Note, the comma in the enumerator list can be a terminator or a separator, allowing the list to end with a dangling comma.\footnote{
+Note the comma in the enumerator list can be a terminator or a separator, allowing the list to end with a dangling comma.\footnote{
 A terminating comma appears in other C syntax, \eg the initializer list.}
 This feature allows enumerator lines to be interchanged without moving a comma.
@@ -130,5 +130,5 @@
 \label{s:CenumImplementation}
 
-In theory, a C enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
+Theoretically, a C enumeration \emph{variable} is an implementation-defined integral type large enough to hold all enumerator values.
 In practice, C defines @int@~\cite[\S~6.4.4.3]{C11} as the underlying type for enumeration variables, restricting initialization to integral constants, which have type @int@ (unless qualified with a size suffix).
 However, type @int@ is defined as:
@@ -137,7 +137,7 @@
 \end{quote}
 However, @int@ means 4 bytes on both 32/64-bit architectures, which does not seem like the ``natural'' size for a 64-bit architecture.
-Whereas, @long int@ means 4 bytes on a 32-bit and 8 bytes on 64-bit architectures, and @long long int@ means 8 bytes on both 32/64-bit architectures, where 64-bit operations are simulated on 32-bit architectures.
-\VRef[Figure]{f:gccEnumerationStorageSize} shows both @gcc@ and @clang@ partially ignore this specification and type the integral size of an enumerator based its initialization.
-Hence, initialization in the range @INT_MIN@..@INT_MAX@ results in a 4-byte enumerator, and outside this range the enumerator is 8 bytes.
+Whereas @long int@ means 4 bytes on a 32-bit and 8 bytes on 64-bit architectures, and @long long int@ means 8 bytes on both 32/64-bit architectures, where 64-bit operations are simulated on 32-bit architectures.
+\VRef[Figure]{f:gccEnumerationStorageSize} shows both @gcc@ and @clang@ partially ignore this specification and type the integral size of an enumerator based on its initialization.
+Hence, initialization in the range @INT_MIN@..@INT_MAX@ results in a 4-byte enumerator, and outside this range, the enumerator is 8 bytes.
 Note that @sizeof( typeof( IMin ) ) != sizeof( E )@, making the size of an enumerator different than is containing enumeration type, which seems inconsistent, \eg @sizeof( typeof( 3 ) ) == sizeof( int )@.
 
@@ -168,5 +168,5 @@
 \label{s:Usage}
 
-C proves an implicit \emph{bidirectional} conversion between an enumeration and its integral type, and between two different enumerations.
+C proves an implicit \emph{bidirectional} conversion between an enumeration and its integral type and between two different enumerations.
 \begin{clang}
 enum Week week = Mon;				$\C{// week == 0}$
@@ -178,5 +178,5 @@
 @week = Winter;@					$\C{// UNDEFINED! implicit conversion to Week}$
 \end{clang}
-While converting an enumerator to its underlying type is useful, the implicit conversion from the base or another enumeration type to an enumeration is a common source of error.
+While converting an enumerator to its underlying type is sound, the implicit conversion from the base or another enumeration type to an enumeration is a common source of error.
 
 Enumerators can appear in @switch@ and looping statements.
@@ -194,14 +194,14 @@
 \end{cfa}
 For iterating using arithmetic to make sense, the enumerator values \emph{must} have a consecutive ordering with a fixed step between values.
-For example, a previous gap introduced by @Thu = 10@, results in iterating over the values 0--13, where values 3--9 are not @Week@ values.
-Note, it is the bidirectional conversion that allows incrementing @day@: @day@ is converted to @int@, integer @1@ is added, and the result is converted back to @Week@ for the assignment to @day@.
+For example, a previous gap introduced by @Thu = 10@ results in iterating over the values 0--13, where values 3--9 are not @Week@ values.
+Note that the bidirectional conversion allows incrementing @day@: @day@ is converted to @int@, integer @1@ is added, and the result is converted back to @Week@ for the assignment to @day@.
 For safety, \CC does not support the bidirectional conversion, and hence, an unsafe cast is necessary to increment @day@: @day = (Week)(day + 1)@.
 
-There is a C idiom to automatically compute the number of enumerators in an enumeration.
+There is a C idiom that computes the number of enumerators in an enumeration automatically.
 \begin{cfa}
 enum E { A, B, C, D, @N@ };  // N == 4
 for ( enum E e = A; e < @N@; e += 1 ) ...
 \end{cfa}
-Here, serendipitously the auto-incrementing counts the number of enumerators and puts the total into the last enumerator @N@.
+Serendipitously, the auto-incrementing counts the number of enumerators and puts the total into the last enumerator @N@.
 This @N@ is often used as the dimension for an array associated with the enumeration.
 \begin{cfa}
@@ -226,21 +226,21 @@
 \end{cfa}
 However, the companion idiom results in the \emph{harmonizing} problem because an update to the enumeration @Integral_Type@ often requires a corresponding update to the companion array \snake{Integral_Name}.
-The requirement to harmonize is at best indicated by a comment before the enumeration.
+The requirement to harmonize is, at best, indicated by a comment before the enumeration.
 This issue is exacerbated if enumeration and companion array are in different translation units.
 
 \bigskip
-While C provides a true enumeration, it is restricted, has unsafe semantics, and does not provide useful/advanced enumeration features found in other programming languages.
+While C provides a true enumeration, it is restricted, has unsafe semantics, and does not provide helpful/advanced enumeration features in other programming languages.
 
 
 \section{\texorpdfstring{\CFA}{Cforall}}
 
-\CFA in \emph{not} an object-oriented programming-language, \ie functions cannot be nested in aggregate types, and hence, there is no \newterm{receiver} notation for calling functions, \eg @obj.method(...)@, where the first argument proceeds the call and becomes an implicit first (\lstinline[language=C++]{this}) parameter.
+\CFA in \emph{not} an object-oriented programming language, \ie functions cannot be nested in aggregate types, and hence, there is no \newterm{receiver} notation for calling functions, \eg @obj.method(...)@, where the first argument proceeds the call and becomes an implicit first (\lstinline[language=C++]{this}) parameter.
 The following sections provide short descriptions of \CFA features needed further in the thesis.
-Other \CFA features are presented in-situ with short explanations, or no explanation because the feature is obvious to C programmers.
+Other \CFA features are presented in situ with short or no explanation because the feature is obvious to C programmers.
 
 
 \subsection{Overloading}
 
-Overloading allows programmers to use the most meaningful names without fear of name clashes within a program or from external sources, like include files.
+Overloading allows programmers to use the most meaningful names without fear of name clashes within a program or from external sources like included files.
 \begin{quote}
 There are only two hard things in Computer Science: cache invalidation and naming things. --- Phil Karlton
@@ -269,5 +269,5 @@
 \subsection{Function Overloading}
 
-Both \CFA and \CC allow function names to be overloaded, as long as their prototypes differ in the number and type of parameters and returns.
+Both \CFA and \CC allow function names to be overloaded as long as their prototypes differ in the number and type of parameters and returns.
 \begin{cfa}
 void f( void );			$\C[1.75in]{// (1): no parameter}$
@@ -277,8 +277,8 @@
 \end{cfa}
 In this case, the name @f@ is overloaded depending on the number and parameter types.
-The type system examines each call size and selects the best match based on the number and types of the arguments.
-Here, there is a perfect match for the call, @f( 'A' )@ with the number and parameter type of function (2).
-
-Ada, Scala, and \CFA type-systems also use the return type in resolving a call, to pinpoint the best overloaded name.
+The type system examines each call size and selects the best match based on the number and types of arguments.
+Here, the call @f( 'A' )@ is a perfect match for the number and parameter type of function (2).
+
+Ada, Scala, and \CFA type-systems also use the return type to pinpoint the best-overloaded name in resolving a call.
 \begin{cfa}
 int f( void );			$\C[1.75in]{// (4); overloaded on return type}$
@@ -302,5 +302,5 @@
 }
 \end{cfa}
-The \CFA type system simply treats overloaded variables as an overloaded function returning a value with no parameters.
+The \CFA type system treats overloaded variables as an overloaded function returning a value with no parameters.
 Hence, no significant effort is required to support this feature.
 
@@ -312,9 +312,9 @@
 
 All objects in \CFA are initialized by @constructors@ \emph{after} allocation and de-initialized \emph{before} deallocation.
-\CC cannot have constructors for basic-types because they have no aggregate type \lstinline[language=C++]{struct/class} in which to insert a constructor definition.
+\CC cannot have constructors for basic types because they have no aggregate type \lstinline[language=C++]{struct/class} in which to insert a constructor definition.
 Like \CC, \CFA has multiple auto-generated constructors for every type.
 
 The prototype for the constructor/destructor are @void ?{}( T &, ... )@ and @void ^?{}( T &, ... )@, respectively.
-The first parameter is logically the \lstinline[language=C++]{this} or \lstinline[language=Python]{self} in other object-oriented languages, and implicitly passed.
+The first parameter is logically the \lstinline[language=C++]{this} or \lstinline[language=Python]{self} in other object-oriented languages and implicitly passed.
 \VRef[Figure]{f:CFAConstructorDestructor} shows an example of creating and using a constructor and destructor.
 Both constructor and destructor can be explicitly called to reuse a variable.
@@ -350,5 +350,5 @@
 
 The C constants @0@ and @1@ have special meaning.
-@0@ is the null pointer and used in conditional expressions, where @if ( p )@ is rewritten @if ( p != 0 )@;
+@0@ is the null pointer and is used in conditional expressions, where @if ( p )@ is rewritten @if ( p != 0 )@;
 @1@ is an additive identity in unary operators @++@ and @--@.
 Aware of their significance, \CFA provides a special type @zero_t@ and @one_t@ for custom types.
@@ -385,5 +385,5 @@
 bar( s );
 \end{cfa}
-The assertion on @T@ restricts the range of types that can be manipulated by @bar@ to only those that have an implementation of @foo@ with the matching signature, allowing @bar@'s call to @foo@ in its body.
+The assertion on @T@ restricts the range of types that can be manipulated by @bar@ to only those that implement @foo@ with the matching signature, allowing @bar@'s call to @foo@ in its body.
 Unlike templates in \CC, which are macro expansions at the call site, \CFA polymorphic functions are compiled, passing the call-site assertion functions as hidden parameters.
 
@@ -392,5 +392,5 @@
 
 A @forall@ clause can assert many restrictions on multiple types.
-A common practice is to refactor the assertions into a named \newterm{trait}, similar to other languages, like Go and Rust.
+A common practice is refactoring the assertions into a named \newterm{trait}, similar to other languages like Go and Rust.
 \begin{cfa}
 forall(T) trait @Bird@ {
@@ -407,5 +407,5 @@
 bird_fly( 23, robin );
 \end{cfa}
-Grouping type assertions into a named trait effectively creates a reusable interface for parametric-polymorphic types.
+Grouping type assertions into a named trait effectively creates a reusable interface for parametric polymorphic types.
 
 
@@ -417,5 +417,5 @@
 
 The \CFA resolver attempts to identify the best candidate based on: first, the number of parameters and types, and second, when no exact match exists, the fewest implicit conversions and polymorphic variables.
-Finding an exact match is not discussed here, because the mechanism is fairly straightforward, even when the search space is large;
+Finding an exact match is not discussed here, because the mechanism is fairly straightforward, even when the search space is ample;
 only finding a non-exact match is discussed in detail.
 
@@ -425,8 +425,8 @@
 
 Most programming languages perform some implicit conversions among basic types to facilitate mixed-mode arithmetic;
-otherwise, the program becomes littered with many explicit casts, which does not match with programmer's expectations.
-C is an aggressive language as it provides conversions among almost all of the basic types, even when the conversion is potentially unsafe or not meaningful, \ie @float@ to @bool@.
+otherwise, the program becomes littered with many explicit casts which do not match the programmer's expectations.
+C is an aggressive language, providing conversions among almost all basic types, even when the conversion is potentially unsafe or not meaningful, \ie @float@ to @bool@.
 C defines the resolution pattern as ``usual arithmetic conversion''~\cite[\S~6.3.1.8]{C11}, in which C looks for a \newterm{common type} between operands, and converts one or both operands to the common type.
-Loosely defined, a common type is the smallest type in terms of the size of representation that both operands can be converted into without losing their precision, called a \newterm{widening} or \newterm{safe conversion}.
+A common type is the smallest type in terms of the size of representation that both operands can be converted into without losing their precision, called a \newterm{widening} or \newterm{safe conversion}.
 
 \CFA generalizes ``usual arithmetic conversion'' to \newterm{conversion cost}.
@@ -438,16 +438,16 @@
 @poly@ is the number of polymorphic function parameters, and
 \item
-@safe@ is sum of the degree of safe (widening) conversions.
+@safe@ is the sum of the degree of safe (widening) conversions.
 \end{enumerate}
 Sum of degree is a method to quantify C's integer and floating-point rank.
 Every pair of widening conversion types is assigned a \newterm{distance}, and the distance between the two same types is 0.
-For example, the distance from @char@ to @int@ is 2, the distance from @int@ to @long@ is 1, and the distance from @int@ to @long long int@ is 2.
+For example, the distance from @char@ to @int@ is 2, from @int@ to @long@ is 1, and from @int@ to @long long int@ is 2.
 This distance does not mirror C's rank system.
-For example, the rank of @char@ and @signed char@ are the same in C, but the distance from @char@ to @signed char@ is assigned 1.
+For example, the @char@ and @signed char@ ranks are the same in C, but the distance from @char@ to @signed char@ is assigned 1.
 @safe@ cost is summing all pairs of arguments to parameter safe conversion distances.
-Among the three costs in Bilson's model, @unsafe@ is the most significant cost and @safe@ is the least significant, with an implication that \CFA always choose a candidate with the lowest @unsafe@, if possible.
-
-For example, assume the overloaded function @foo@ is called with two @int@ parameter.
-The cost for every overloaded @foo@ has been listed along:
+Among the three costs in Bilson's model, @unsafe@ is the most significant cost, and @safe@ is the least significant, implying that \CFA always chooses a candidate with the lowest @unsafe@, if possible.
+
+For example, assume the overloaded function @foo@ is called with two @int@ parameters.
+The cost for every overloaded @foo@ has been listed along with the following:
 \begin{cfa}
 void foo( char, char );				$\C[2.5in]{// (1) (2, 0, 0)}$
@@ -479,13 +479,13 @@
 \CFA favours candidates with more restrictions on polymorphism, so @forall( T ) void foo( T, T )@ has lower cost.
 @specialization@ is an arbitrary count-down value starting at zero.
-For every type assertion in @forall@ clause (no assertions in the above example), \CFA subtracts one from @specialization@.
-More type assertions means more constraints on argument types, making the function less generic.
+For every type assertion in the @forall@ clause (no assertions in the above example), \CFA subtracts one from @specialization@.
+More type assertions mean more constraints on argument types, making the function less generic.
 
 \CFA defines two special cost values: @zero@ and @infinite@.
-A conversion cost is @zero@ when the argument and parameter have an exact match, and a conversion cost is @infinite@ when there is no defined conversion between two types.
+A conversion cost is @zero@ when the argument and parameter have an exact match, and a conversion cost is @infinite@ when there is no defined conversion between the two types.
 For example, the conversion cost from @int@ to a @struct S@ is @infinite@.
 
 In \CFA, the meaning of a C-style cast is determined by its @Cast Cost@.
-For most cast-expression resolutions, a cast cost is equal to a conversion cost.
-Cast cost exists as an independent matrix for conversion that cannot happen implicitly, while being possible with an explicit cast.
-These conversions are often defined to have a infinite conversion cost and a non-infinite cast cost.
+For most cast-expression resolutions, a cast cost equals a conversion cost.
+Cast cost exists as an independent matrix for conversion that cannot happen implicitly while being possible with an explicit cast.
+These conversions are often defined as having an infinite conversion cost and a non-infinite cast cost.
