using official template + fixing language errorsthesis

1 files changed, 28 insertions, 28 deletions

diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex
index 8b02c3c..433989d 100644
--- a/chapters/core/implementation/02-interaction-rules.tex
+++ b/chapters/core/implementation/02-interaction-rules.tex
@@ -17,7 +17,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 			\item \textbf{ReLU}: Unary operator for rectified linear unit.
 		\end{itemize}
 	\item
-		\textbf{Structural Operators}: Agents that perform some kind of operation on net structure.
+		\textbf{Structural Operators}: Agents that perform some kind of operation on the net structure.
 		\begin{itemize}
 			\item \textbf{Eraser}: Built-in INPLA unary operator to delete other agents.
 			\item \textbf{Dup}: Built-in INPLA unary operator to duplicate other agents.
@@ -34,9 +34,9 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 	\item
 		\textbf{Terminals}: Agents that compose the normal form.
 		\begin{itemize}
-			\item \textbf{TermAdd}: This agent is parsed as addition for the SMT solver.
-			\item \textbf{TermMul}: This agent is parsed as multiplication for the SMT solver.
-			\item \textbf{TermReLU}: This agent is parsed as rectified linear unit for the SMT solver.
+			\item \textbf{TermAdd}: This agent is parsed as an addition for the SMT solver.
+			\item \textbf{TermMul}: This agent is parsed as a multiplication for the SMT solver.
+			\item \textbf{TermReLU}: This agent is parsed as a rectified linear unit for the SMT solver.
 			\item \textbf{TermSymbolic}: This agent is parsed as a specific variable for the SMT solver.
 			\item \textbf{TermConcrete}: This agent is parsed as a real value for the SMT solver.
 		\end{itemize}
@@ -184,10 +184,10 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f
 \end{figure}
 
 \paragraph{Linear with Add/Mul}
-The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents as illustrated in
+The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents, as illustrated in
 \textbf{\Cref{fig:rule-linear-add}} and \textbf{\Cref{fig:rule-linear-mul}}. Because interactions are local, the binary
-operators need to check one operand a time. For this reason \textit{Add} and \textit{Mul} agents are replaced by
-\textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$ and their
+operators need to check one operand at a time. For this reason, \textit{Add} and \textit{Mul} agents are replaced by
+\textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$, and their
 principal port faces the other operand.
 
 % Linear >< Add
@@ -235,11 +235,11 @@ principal port faces the other operand.
 \end{figure}
 
 \paragraph{Concrete with Add/Mul}
-The same logic is applied to the \textit{Concrete} carrier agent, but here analyzing the attribute $k$
-enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}} we can see that when summing a \textit{Concrete}
-with $k=0$ we do not need to check the other operand and we simply wire it to the output.
+The same logic is applied to the \textit{Concrete} carrier agent, but here, analyzing the attribute $k$
+enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}}, we can see that when summing a \textit{Concrete}
+with $k=0$, we do not need to check the other operand, and we simply wire it to the output.
 This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1$, as shown in
-\textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$ the other operand is deleted
+\textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$, the other operand is deleted
 before it is even invoked.
 
 % Concrete >< Add
@@ -339,14 +339,14 @@ before it is even invoked.
 \end{figure}
 
 \paragraph{Linear with AddCheckLinear/MulCheckLinear}
-If both operands are \textit{Linear} agents they need to be materialized before being wrapped in another
+If both operands are \textit{Linear} agents, they need to be materialized before being wrapped in another
 \textit{Linear} to allow further simplification. This is done because multiplying two linear packets
 gives a non-linear result.
-While adding two linear packets gives a linear result, it depends on two free variables and the
+While adding two linear packets gives a linear result, it depends on two free variables, and the
 \textit{Linear} agent only supports keeping track of one; consequently, the addition of two linear packets
 results in their materialization.
 This is illustrated in \textbf{\Cref{fig:rule-linear-addchecklinear}}
-and \textbf{\Cref{fig:rule-linear-mulchecklinear}} where the result of the materialization is passed
+and \textbf{\Cref{fig:rule-linear-mulchecklinear}}, where the result of the materialization is passed
 to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Linear} with attributes
 $q=1,r=0$.
 
@@ -491,11 +491,11 @@ $q=1,r=0$.
 \end{figure}
 
 \paragraph{Concrete with AddCheckLinear/MulCheckLinear}
-If, instead, the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent different rules
-are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) the system adds the
+If, instead, the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent, different rules
+are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}), the system adds the
 attribute of the \textit{Concrete} agent to the attribute that represents the constant of the \textit{Linear} agent.
-For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) the system multiplies the attribute of
-the \textit{Concrete} agent to both the attributes of the \textit{Linear}.
+For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}), the system multiplies the attribute of
+the \textit{Concrete} agent by both the attributes of the \textit{Linear}.
 
 % Concrete >< AddCheckLinear
 \begin{figure}[H]
@@ -538,8 +538,8 @@ the \textit{Concrete} agent to both the attributes of the \textit{Linear}.
 \end{figure}
 
 \paragraph{Linear with AddCheckConcrete/MulCheckConcrete}
-In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}}
-we follow the exact same logic except the first operand is a \textit{Concrete} and the second is a \textit{Linear}.
+In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}},
+we follow the exact same logic, except the first operand is a \textit{Concrete} and the second is a \textit{Linear}.
 
 % Linear >< AddCheckConcrete
 \begin{figure}[H]
@@ -582,9 +582,9 @@ we follow the exact same logic except the first operand is a \textit{Concrete} a
 \end{figure}
 
 \paragraph{Concrete with AddCheckConcrete/MulCheckConcrete}
-Finally if both operands are \textit{Concrete} agents they are either merged into a single \textit{Concrete}
+Finally, if both operands are \textit{Concrete} agents, they are either merged into a single \textit{Concrete}
 or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckconcrete}} and
-\textbf{\Cref{fig:rule-concrete-mulcheckconcrete}} following a similar logic to the previous rules.
+\textbf{\Cref{fig:rule-concrete-mulcheckconcrete}}, following a similar logic to the previous rules.
 
 % Concrete >< AddCheckConcrete
 \begin{figure}[H]
@@ -672,10 +672,10 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 \end{figure}
 
 \paragraph{Linear/Concrete with ReLU}
-When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is not
-enough information to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}},
-the agent is just materialized, passed to a \textit{TermReLU} and then wrapped in a \textit{Linear}.
-In \textbf{\Cref{fig:rule-concrete-relu}} is illustrated that when the \textit{Concrete} carrier agent
+When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents, there is not
+enough information to perform any simplification, so, as shown in \textbf{\Cref{fig:rule-linear-relu}},
+the agent is just materialized, passed to a \textit{TermReLU}, and then wrapped in a \textit{Linear}.
+In \textbf{\Cref{fig:rule-concrete-relu}}, it is illustrated that when the \textit{Concrete} carrier agent
 meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either with attribute $k$
 if $k>0$ or with attribute equal $0$ otherwise.
 
@@ -742,9 +742,9 @@ if $k>0$ or with attribute equal $0$ otherwise.
 \end{figure}
 
 \paragraph{Linear/Concrete with Materialize}
-When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd}, \textit{TermMul} and \textit{TermConcrete}
+When a \textit{Linear} is materialized, it explicitly builds an AST using \textit{TermAdd}, \textit{TermMul}, and \textit{TermConcrete}
 to recreate $q*x+r$ as shown in \textbf{\Cref{fig:rule-linear-materialize}}.
-When a \textit{Concrete} needs to be materialized it is converted into \textit{TermConcrete} as illustrated in
+When a \textit{Concrete} needs to be materialized, it is converted into \textit{TermConcrete} as illustrated in
 \textbf{\Cref{fig:rule-concrete-materialize}}.
 
 % Linear >< Materialize