Grammar pass over Rewriting

chapters/3_rewriting.tex

@@ -17,15 +17,15 @@ To create an efficient \gls{slv-mod} the \gls{rewriting} process uses many simpl
 \begin{itemize}
 	\item continuously updating \variable{} \domains{},
 	\item \gls{propagation} for known \constraints{},
-	\item specialised \glspl{decomp} when variables get \gls{fixed},
+	\item specialized \glspl{decomp} when variables get \gls{fixed},
 	\item \gls{aggregation},
 	\item common sub-expression elimination,
 	\item and removing \variables{} and \constraints{} that are no longer required.
 \end{itemize}
 
 We now present a new architecture for the \gls{rewriting} process that has been designed for the modern day needs of \minizinc{}.
-At the core of our \gls{rewriting} process lie formalised rewriting rules.
-As such, this architecture represent an abstract machine model for \minizinc{}.
+At the core of our \gls{rewriting} process lie formalized rewriting rules.
+As such, this architecture represents an abstract machine model for \minizinc{}.
 These rules allow us to reason about the system and about the simplifications both to the process and the resulting \gls{slv-mod}.
 The process can even be made incremental: in \cref{ch:incremental} we discuss how when making incremental changes to the \minizinc{} model, no recompilation is required for the unchanged parts.
 
@@ -73,7 +73,7 @@ In \microzinc{} it is specifically used to mark functions that are \gls{native}
 We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
 While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
 This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
-In \minizinc{} the use of \variables{} in these positions is allowed and these expressions are rewritten to function calls.
+In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls.
 We will discuss how the same transformation takes place in when translating \minizinc{} to \microzinc{}.
 
 \begin{figure}
@@ -168,7 +168,7 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
 		In contrast to \minizinc{}, a \microzinc{} expression must be total.
 		\textcite{stuckey-2013-functions} have extensively examined these problems and describe how to transform any partial function into a total function while maintaining the relational semantics of the original \cmodel{}.
 		A general approach for describing the partiality in \microzinc{} functions is to make the function return an additional Boolean \variable{}.
-		This \variable{} indicates whether the result of the function call is defined with regards to the function parameters.
+		This \variable{} indicates whether the result of the function call is defined \wrt{} the function arguments.
 		The resulting value of the function is then adjusted to return a predefined value when it would normally be undefined.
 		For example, the \mzninline{element} function in \minizinc{} is declared as follows.
 
@@ -214,10 +214,10 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
 		\end{mzn}
 
 	\item Transform all function definitions so that they do not refer to \variables{} and \parameters{} defined outside the scope of the function.
-		Instead they are added as extra arguments to the function definition and each call.
+		Instead, they are added as extra arguments to the function definition and each call.
 
 	\item Move all top-level \variable{} declarations and \constraints{} into a let expression in the body of a new function called \mzninline{main}.
-		The arguments to this function are the top-level \parameters{} of the \minizinc{} model and it returns a fresh Boolean \variable{}.
+		The arguments to this function are the top-level \parameters{} of the \minizinc{} model, and it returns a fresh Boolean \variable{}.
 
 \end{enumerate}
 
@@ -236,7 +236,7 @@ The translation from \minizinc{} to \microzinc{} involves the following steps.
 
 	\begin{listing}
 		\mznfile{assets/listing/rew_pigeon_uzn.mzn}
-		\caption{\label{lst:rew-pigeon-uzn} The \microzinc{} tranlation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
+		\caption{\label{lst:rew-pigeon-uzn} The \microzinc{} translation of the pigeonhole problem in \cref{lst:rew-pigeon-mzn}.}
 	\end{listing}
 
 	For an \instance{} of the \cmodel{}, we can then create a simple \nanozinc{} program that calls \mzninline{main}.
@@ -275,7 +275,7 @@ In this case, the \constraint{} introduced in the \gls{let} may be enforced glob
 However, the introduced \mzninline{int_abs} \constraint{} is only needed so long as any other \constraint{} refers to \mzninline{z}.
 If \mzninline{z} is unused in the rest of the model, both \mzninline{z} and the \mzninline{int_abs} \constraint{} can be removed.
 
-As we shall see in \cref{sec:rew-simplification}, certain optimisations and simplifications during the evaluation can lead to many expressions becoming unused.
+As we shall see in \cref{sec:rew-simplification}, certain optimizations and simplifications during the evaluation can lead to many expressions becoming unused.
 It is therefore important to track which \constraints{} were merely introduced to define results of function calls.
 In order to track these dependencies, \nanozinc{} attaches \constraints{} that define a variable to the item that introduces the \variable{}.
 
@@ -399,8 +399,7 @@ Since these are directly supported by the \solver{}, they simply need to be tran
 
 The rules in \cref{fig:rew-rewrite-to-nzn-let} consider \glspl{let}.
 Starting from the main rule, (Let), the let items \textbf{I} are evaluated one at a time.
-\Glspl{constraint} that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \(\phi{}\)
-, of the evaluation arguments.
+\Glspl{constraint} that follow from the evaluation of the let expression, by the (ItemC) rule, are collected in the third component, \(\phi{}\), of the evaluation arguments.
 When all inner items have been evaluated, the captured \constraints{} are attached to the literal returned by the body of the let expression \textbf{X} in (Item0).
 The (ItemT) rule handles introduction of new \variables{} by adding them to the context.
 The (ItemTE) rule handles introduction of new \variables{} with a defining equation by evaluating them in the current context and substituting the name of the new \variable{} by the result of evaluation in the entire scope of the variable.
@@ -481,15 +480,15 @@ The compiler currently supports a significant subset of the full \minizinc{} lan
 The \gls{interpreter} evaluates \microzinc{} \gls{byte-code} and \nanozinc{} programs based on the \gls{rewriting} system introduced in this section.
 It can read \parameters{} from a file or via an \gls{api}.
 The \gls{interpreter} constructs the call to the \mzninline{main} function, and then performs the \gls{rewriting} into \gls{slv-mod} \nanozinc{}.
-Memory management is implemented using reference counting, which lends itself well to the optimisations discussed in the next section.
+Memory management is implemented using reference counting, which lends itself well to the simplifications discussed in the next section.
 The interpreter is written in around 3.5kLOC of C++ to enable easy embedding into applications and other programming languages.
 
 The framework has the ability to support multiple \solvers{}.
 It can pretty-print the \nanozinc{} code to standard \flatzinc{}, so that any solver currently compatible with \minizinc{} can be used.
 Additionally, a direct C++ \gls{api} can be used to connect solvers directly, in order to enable incremental solving.
 We revisit this topic in \cref{ch:incremental}.
-The source code for the complete system will be made available under an open source license.
-\todo{actually make source available}
+The source code for the complete system will be made available under an open source licence.
+\todo{Actually make source available}
 
 \section{NanoZinc Simplification}\label{sec:rew-simplification}
 
@@ -575,7 +574,8 @@ In this thesis we will follow the same naming standard as \minizinc{}, where a \
 
 	The \gls{rewriting} of this \minizinc{} model will initially create the \mzninline{n} elements for the \gls{array} \gls{comprehension}.
 	Each element is evaluated as a new \variable{} \mzninline{y} and a \constraint{} to ensure that \mzninline{y} is the multiplication of \mzninline{x} and \mzninline{i}.
-	Although \mzninline{n} variables are created, only the last \variable{} is constrained to be 10. All other \variables{} can thus be removed and the model will stay \gls{eqsat}.
+	Although \mzninline{n} variables are created, only the last \variable{} is constrained to take the value ten.
+	All other \variables{} can thus be removed, and the model will stay \gls{eqsat}.
 
 	In the \nanozinc{} version of this model, each of the multiplications \constraints{} will be added to the list of attached \constraints{} of its corresponding \mzninline{y} \variable{}.
 	When, after evaluating the \gls{array} access, all of those \variables{} except the last are detected to be unused, their removal triggers the removal of the subtraction \constraints{}.
@@ -666,7 +666,7 @@ It is set when the \domain{} of a \variable{} is tightened by a \constraint{} th
 When the flag is set, the \variable{} cannot be removed, even when the reference count is zero.
 This \constraint{} may then become subsumed after \gls{propagation} and can then be removed.
 Its meaning is now completely captured by the \domains{} of the \variables{}.
-However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is is no longer \gls{binding}.
+However, if any defining \constraint{} can later determine the same, or a strictly tighter, \domain{}, then it is no longer \gls{binding}.
 It is again fully implied by its defining \constraints{}.
 The flag can then be unset and the \variable{} can potentially be removed.
 
@@ -680,7 +680,7 @@ In our \microzinc{}/\nanozinc{} system, we allow functions to be annotated as po
 Any annotated \constraint{} is handled by the (CallNative) rule rather than the (Call) rule, which means that it is simply added as a call into the \nanozinc{} code, without evaluating its body.
 When \gls{propagation} reaches a \gls{fixpoint}, all annotations are removed from the current \nanozinc{} program, and evaluation resumes with the function bodies.
 
-This crucial optimisation enables rewriting in multiple phases.
+This crucial optimization enables rewriting in multiple phases.
 For example, a \cmodel{} targeted at a \gls{mip} \solver{} is rewritten into Boolean and reified \constraints{}, whose definitions are annotated to be delayed.
 The \nanozinc{} program can then be fully simplified by \gls{propagation}, before the Boolean and reified \constraints{} are rewritten into \gls{native} linear \constraints{} suitable for \gls{mip}.
 
@@ -690,7 +690,7 @@ The \nanozinc{} program can then be fully simplified by \gls{propagation}, befor
 As shown in \cref{subsec:back-cse}, \gls{cse} is a crucial technique to avoid duplications in a \gls{model}.
 In our architecture \gls{cse} is performed on two levels.
 
-The \microzinc{} \interpreter{} performs \gls{cse} through memoisation.
+The \microzinc{} \interpreter{} performs \gls{cse} through memoization.
 It maintains a table that maps a function identifier and the call arguments to its result for each call instruction that is executed.
 Before it executes a call instruction, it searches the table for an entry with identical function identifier and call arguments.
 Since functions in \microzinc{} are guaranteed to be pure and total, whenever the table search succeeds, the result can be used instead of executing the call instruction.
@@ -715,7 +715,7 @@ Earlier in the process, however, the \minizinc{} to \microzinc{} \compiler{} can
 \end{example}
 
 As such, the \compiler{} can enforce sharing of common sub-expressions before evaluation begins.
-It is worth noting that, although the \gls{cse} approach based on memorisation would also cover the static example above, this method can potentially avoid many dynamic table look-ups.
+It is worth noting that, although the \gls{cse} approach based on memoization would also cover the static example above, this method can potentially avoid many dynamic table look-ups.
 Since the static analysis is cheap, it is valuable to combine both approaches.
 The static approach can be further improved by inlining function calls, since that may expose more calls as being syntactically equal.
 
@@ -744,7 +744,7 @@ Although this structure offers flexibility when defining \minizinc{} libraries,
 	\caption{\label{lst:rew-knapsack} The definition of \mzninline{knapsack} in the \minizinc{} standard library.}
 \end{listing}
 
-Therefore, we have added an additional flag to our call instruction.
+Therefore, we have added a flag to our call instruction.
 This flag controls whether the call is subject to \gls{cse}.
 This allows us to disable the \gls{cse} when it is guaranteed to be unnecessary.
 
@@ -788,10 +788,10 @@ When the \gls{avar} become unused, they will be removed using the normal mechani
 We have created a prototype implementation of the architecture presented in the preceding sections.
 It consists of a \compiler{} from \minizinc{} to \microzinc{}, and a \microzinc{} \interpreter{} producing \nanozinc{}.
 The system supports a significant subset of the full \minizinc{} language; notable features that are missing are support for set and float variables, option types, and compilation of model output expressions and annotations.
-We will release our implementation under an open-source license and can make it available to the reviewers upon request.
+We will release our implementation under an open-source licence and can make it available to the reviewers upon request.
 \todo{I suppose it is time to release the prototype.}
 
-The implementation is not optimised for performance yet, but was created as a faithful implementation of the developed concepts, in order to evaluate their suitability and provide a solid baseline for future improvements.
+The implementation is not optimized for performance yet, but was created as a faithful implementation of the developed concepts, in order to evaluate their suitability and provide a solid baseline for future improvements.
 In the following we present experimental results on basic \gls{rewriting} performance as well as a comparison with \glspl{interpreter} of other programming languages to demonstrate the efficiency gains that are possible thanks to the new architecture.
 A description of the used computational environment, \minizinc{} instances, and versioned software has been included in \cref{ch:benchmarks}.
 
@@ -802,7 +802,7 @@ Times are averages of 10 runs.
 
 \Cref{sfig:rew-compareruntime} compares the \gls{rewriting} time for each of \instances{}.
 Points below the line indicate that the new system is faster.
-On average, the new system achieves a speed-up of 5.5, with every \instance{} achieving at least 2.5 speedup and multiple \instances{} with a speedup of over 100.
+On average, the new system achieves a speed-up of 5.5, with every \instance{} achieving at least 2.5 speed-up and multiple \instances{} with a speed-up of over 100.
 In terms of memory performance (\cref{sfig:rew-comparemem}), version 2.5.5 can sometimes still outperform the new prototype.
 We have identified that the main memory bottlenecks are our currently unoptimised implementations of \gls{cse} lookup tables and argument vectors.
 These are very encouraging results, given that we are comparing a largely unoptimised prototype to a mature piece of software.
@@ -829,7 +829,7 @@ Our second experiment considers three well-known computational recursive functio
 These functions are often used as a benchmark for implementations of functional programming languages.
 Since the \minizinc{} language includes a strong functional programming component, we use these same functions as a benchmark for our prototype \interpreter{}.
 In addition to \minizinc{} 2.5.5, we also compare our \interpreter{} to Python 3.8.5 \autocite{rossum-2009-python3} and OCaml 4.10.0 \autocite{leroy-2020-ocaml}.
-The chosen function arguments try to exercise the \glspl{interpreter}, but without running into limitations of any of them. 
+The chosen function arguments try to exercise the \glspl{interpreter}, but without running into their limitations. 
 Times are averages of 1000 runs.
 
 The results of the experiment are shown in \cref{fig:rew-interpreter-comp}.
@@ -840,8 +840,8 @@ For all experiments there is a clear ordering in the results:
 	\item Python is a close third,
 	\item and finally \minizinc{} 2.5.5.
 \end{itemize}
-Our protoype performs well in this test.
-It clearly outperforms \minizinc{} 2.5.5 with about 10 times speedup and it slightly outperforms Python, an optimised \interpreter{} for a general programming language.
+Our prototype performs well in this test.
+It clearly outperforms \minizinc{} 2.5.5 with about 10 times speed-up, and it slightly outperforms Python, an optimized \interpreter{} for a general programming language.
 It is clear though that OCaml, a language that is dedicated to these types of programs, still outperforms our prototype.
 We are convinced, however, that we can get closer to its performance given the right improvements in our prototype.
 

chapters/3_rewriting_preamble.tex

@@ -6,16 +6,16 @@ We show how this tool chain allows us to:
 
 	\item efficiently rewrite \cmodels{} with \textbf{minimal overhead},
 
-	\item easily integrate a range of \textbf{optimisation and simplification} techniques,
+	\item easily integrate a range of \textbf{optimization and simplification} techniques,
 
 	\item and effectively \textbf{detect and eliminate dead code} introduced by functional definitions.
 
 \end{itemize}
 
-\noindent{}In addition to providing the first formalisation and systematic description of rewriting MiniZinc, we will see that the resulting architecture is also significantly more efficient and flexible than the current \minizinc{} system.
+\noindent{}In addition to providing the first formalization and systematic description of rewriting MiniZinc, we will see that the resulting architecture is also significantly more efficient and flexible than the current \minizinc{} system.
 
-This chapter is organised as follows.
-\Cref{sec:rew-arch} provides an quick overview of the proposed architecture.
+This chapter is organized as follows.
+\Cref{sec:rew-arch} provides a quick overview of the proposed architecture.
 \Cref{sec:rew-micronano} introduces the core of our \gls{rewriting} system using the \microzinc{} and \nanozinc{} languages. These new languages provide a new intermediate representation that enables more efficient \gls{rewriting}.
 \Cref{sec:rew-simplification} describes how we can perform various processing and simplification steps on this representation
 Finally, in \cref{sec:rew-experiments} we report on the experimental results of the prototype implementation.