diff options
Diffstat (limited to 'chapters/core/soundness-proof')
3 files changed, 83 insertions, 55 deletions
diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex index 800e085..4477581 100644 --- a/chapters/core/soundness-proof/02-soundness-of-translation.tex +++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex @@ -20,8 +20,7 @@ Which is identical to the ONNX definition. \end{lemma} \begin{lemma} -The ONNX Gemm (General Matrix Multiplication) operator for input tensors A, B, C, input $\alpha$ -and $\beta$ and output tensor Y is defined as: +The ONNX Gemm operator for input tensors A, B, C, input $\alpha$ and $\beta$ and output tensor Y is defined as: $$ Y = \alpha \cdot A \cdot B + \beta \cdot C $$ diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex index 26f7e13..6957c3c 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -1,6 +1,8 @@ \subsection{Soundness of Interaction Rules} \label{sec:soundness-of-interaction-rules} +We need to prove that each interaction rule does not alter the semantics of the IN. + \begin{lemma} For the \textit{Linear} and \textit{Add} agents we have the interaction rule: $$ @@ -146,8 +148,7 @@ & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\ & \Rightarrow \mathit{out} = q \cdot x + (r + s \cdot y + t) \end{aligned} \\ - & \begin{aligned} - \text{RHS: } + & \text{RHS: } \resizebox{0.85\linewidth}{!}{$ \begin{cases} \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r,s,t = 0 \\ \llbracket \mathit{out} \sim \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{if } s,t = 0 \\ @@ -161,7 +162,7 @@ \end{aligned}\\ \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise} \end{cases} - \end{aligned} + $} \end{aligned} $$ Since: @@ -200,8 +201,7 @@ & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\ & \Rightarrow \mathit{out} = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) \end{aligned} \\ - & \begin{aligned} - \text{RHS: } + & \text{RHS: } \resizebox{0.85\linewidth}{!}{$ \begin{cases} \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ \begin{aligned} @@ -213,15 +213,17 @@ \end{aligned}\\ \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 & \text{otherwise} \end{cases} - \end{aligned} + $} \end{aligned} $$ Since: $$ + \resizebox{0.95\linewidth}{!}{$ \begin{cases} 0 \cdot (s \cdot y + t) \cdot x + 0 \cdot (s \cdot y + t) = 0 \lor q \cdot (0 \cdot y + 0) \cdot x + r \cdot (0 \cdot y + 0) = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) & \text{otherwise} \end{cases} + $} $$ the rule is sound. \end{lemma} @@ -317,11 +319,13 @@ \begin{lemma} For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule: $$ - \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow - \begin{cases} - \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\ - \mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise} - \end{cases} + \begin{aligned} + & \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise} + \end{cases} + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ @@ -353,12 +357,14 @@ \begin{lemma} For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule: $$ - \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow - \begin{cases} - \mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\ - \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\ - \mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise} - \end{cases} + \begin{aligned} + & \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\ + \mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise} + \end{cases} + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ @@ -458,13 +464,13 @@ $$ \begin{aligned} & \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\ - & \quad \begin{cases} + & \quad \resizebox{0.85\linewidth}{!}{$ \begin{cases} \mathit{out} \sim \mathit{TermConcrete}(r); x \sim \mathit{Eraser} & \text{if } q = 0 \\ \mathit{out} \sim x & \text{if } q = 1, r = 0 \\ \mathit{out} \sim \mathit{TermAdd}(x, \mathit{TermConcrete}(r)) & \text{if } q = 1 \\ \mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) & \text{if } r = 0 \\ \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) & \text{otherwise} - \end{cases} + \end{cases} $} \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -477,13 +483,16 @@ \end{aligned} \\ & \begin{aligned} \text{RHS: } - \begin{cases} + \resizebox{0.9\linewidth}{!}{$ \begin{cases} \llbracket \mathit{out} \sim \mathit{TermConcrete}(r); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = r & \text{if } q = 0 \\ \llbracket \mathit{out} \sim x \rrbracket \Rightarrow \mathit{out} = x & \text{if } q = 1, r = 0 \\ \llbracket \mathit{out} \sim \mathit{TermAdd}(x, \mathit{TermConcrete}(r)) \rrbracket \Rightarrow \mathit{out} = x + r & \text{if } q = 1 \\ \llbracket \mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) \rrbracket \Rightarrow \mathit{out} = q \cdot x & \text{if } r = 0 \\ - \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{otherwise} \\ - \end{cases} + \begin{aligned} + & \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot x + r + \end{aligned} & \text{otherwise} \\ + \end{cases} $} \end{aligned} \end{aligned} $$ @@ -526,9 +535,10 @@ For the \textit{Linear} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow - & \mathit{Linear}(z_1, q, r) \sim x; \mathit{Linear}(z_2, q, r) \sim y; \\ - & \mathit{Dup}(z_1, z_2) \sim z + & \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{Linear}(z_1, q, r) \sim x; \\ + & \quad \mathit{Linear}(z_2, q, r) \sim y; \\ + & \quad \mathit{Dup}(z_1, z_2) \sim z \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -620,8 +630,11 @@ For the \textit{TermAdd} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermAdd}(a_1, b_1) \sim x; \mathit{TermAdd}(a_2, b_2) \sim y; \\ - & \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\ + & \mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermAdd}(a_1, b_1) \sim x; \\ + & \quad \mathit{TermAdd}(a_2, b_2) \sim y; \\ + & \quad \mathit{Dup}(a_1, a_2) \sim a; \\ + & \quad \mathit{Dup}(b_1, b_2) \sim b \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -671,9 +684,11 @@ For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow - & \mathit{TermMul}(a_1, b_1) \sim x; \mathit{TermMul}(a_2, b_2) \sim y; \\ - & \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b + & \mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermMul}(a_1, b_1) \sim x; \\ + & \quad \mathit{TermMul}(a_2, b_2) \sim y; \\ + & \quad \mathit{Dup}(a_1, a_2) \sim a; \\ + & \quad \mathit{Dup}(b_1, b_2) \sim b \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -723,10 +738,10 @@ For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow - & \mathit{TermReLU}(z_1) \sim x; \\ - &\mathit{TermReLU}(z_2) \sim y; \\ - & \mathit{Dup}(z_1, z_2) \sim z + & \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermReLU}(z_1) \sim x; \\ + & \quad \mathit{TermReLU}(z_2) \sim y; \\ + & \quad \mathit{Dup}(z_1, z_2) \sim z \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -774,9 +789,9 @@ For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow - & \mathit{TermConcrete}(k) \sim x; \\ - & \mathit{TermConcrete}(k) \sim y + & \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermConcrete}(k) \sim x; \\ + & \quad \mathit{TermConcrete}(k) \sim y \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -822,9 +837,9 @@ For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow - & \mathit{TermSymbolic}(id) \sim x; \\ - & \mathit{TermSymbolic}(id) \sim y + & \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermSymbolic}(id) \sim x; \\ + & \quad \mathit{TermSymbolic}(id) \sim y \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex index d0cec53..15cc4f4 100644 --- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex +++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex @@ -1,7 +1,7 @@ \subsection{Soundness of Reduction} \label{sec:soundness-of-reduction} -\begin{lemma} +\begin{property} A valid IN satisfies the following properties: \begin{itemize} \item \textbf{DAG}: the net forms a DAG where the roots are the free wires representing the network @@ -15,7 +15,7 @@ carrier nor operator agents interact with agents of the same type. Terminal agents do not interact with computational operators because they are wrapped in a \textit{Linear} agent. \end{itemize} -\end{lemma} +\end{property} \begin{theorem} Let $\text{IN}_0$ be the valid IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be @@ -65,9 +65,9 @@ \Phi(\text{IN}_n) = \sum_{a \in \text{Agents}(\text{IN}_n)} \begin{cases} 4 + 3^{D-d(a)} & \text{ if }a\text{ is of type computational operator} \\ 3 + 3^{D-d(a)} & \text{ if }a\text{ is of type intermediate} \\ - 1 + 3^{D-d(a)} & \text{ if }a\text{ is a Materialize agent} \\ + 1 + 3^{D-d(a)} & \text{ if }a\text{ is a \textit{Materialize} agent} \\ 3^{D-d(a)} & \text{ if }a\text{ is of type structural operator} \\ - 0 & \text{ if }a\text{ is a Carrier, Terminal} + 0 & \text{ if }a\text{ is a carrier, terminal} \end{cases} \end{equation} where $d(a)$ is the distance of the agent $a$ from the nearest output wire and $D$ the maximum depth @@ -88,30 +88,44 @@ \begin{equation} \Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1}) \end{equation} - or temporary Linear agents are wired with Materialize agents, which are then forced to - interact to produce terminal agents, then wrapped into a new Linear agent: + or temporary Linear agents are wired with \textit{Materialize} agents, which are then forced to + interact to produce terminal agents, then wrapped into a new \textit{Linear} agent: \begin{equation} - \Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 1 + 3^{D-d(i)-2} + 1 + 3^{D-d(i)-2} = 2 + 2 \cdot 3^{D-d(i)-2} = \Phi(\text{IN}_{n+1}) + \begin{aligned} + \Phi(\text{IN}_n) &= 3 + 3^{D-d(i)} \\ + &> 1 + 3^{D-d(i)-2} + 1 + 3^{D-d(i)-2} \\ + &= 2 + 2 \cdot 3^{D-d(i)-2} = \Phi(\text{IN}_{n+1}) + \end{aligned} \end{equation} - If the carrier $c$ interacts with a Materialize agent $i$: + If the carrier $c$ interacts with a \textit{Materialize} agent $i$: \begin{equation} \Phi(\text{IN}_n) = 1 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1}) \end{equation} - \item \textbf{Carrier with Structural Operator}: If a carrier $c$ is duplicated with the \textit{Dup} or \textit{Eraser} + \item \textbf{Carrier with Structural Operator}: If a carrier $c$ interacts with a \textit{Dup} or \textit{Eraser} agent $a$, it traverses the agent structure: \begin{equation} \Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) \end{equation} - if the Dup or Eraser agent interacts with a TermAdd or TermMul, two new agents are created at - each auxillary port: + if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermAdd} or \textit{TermMul}, two new agents are created at + each auxiliary port: \begin{equation} \Phi(\text{IN}_n) = 3^{D-d(a)} > 2 * 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) \end{equation} + if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermReLU}, one new agent is created at the + auxiliary port: + \begin{equation} + \Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) + \end{equation} + if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermConcrete} or \textit{TermSymbolic}, no new agents are + created: + \begin{equation} + \Phi(\text{IN}_n) = 3^{D-d(a)} > 0 = \Phi(\text{IN}_{n+1}) + \end{equation} \end{itemize} Since $\Phi$ is a non-negative strictly decreasing function, the reduction process must terminate in a finite number of steps $n$. - Additionally, since each active pair has exactly one applicable rule the reduction is + Additionally, since each active pair has exactly one applicable rule, the reduction is deterministic. Strong confluence follows immediately, meaning that the normal form is unique - regardless of order in which rules are applied. + regardless of the order in which rules are applied. \end{proof} |