From a8bb7736e2e86963bd5761cc05079447abeeaba6 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Tue, 23 Jun 2026 15:26:01 +0200 Subject: using official template + fixing language errors --- .../core/implementation/02-interaction-rules.tex | 56 +++++++++++----------- 1 file changed, 28 insertions(+), 28 deletions(-) (limited to 'chapters/core/implementation/02-interaction-rules.tex') 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 -- cgit v1.2.3