diff options
Diffstat (limited to 'chapters/core/soundness-proof/01-mathematical-definitions.tex')
| -rw-r--r-- | chapters/core/soundness-proof/01-mathematical-definitions.tex | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/chapters/core/soundness-proof/01-mathematical-definitions.tex b/chapters/core/soundness-proof/01-mathematical-definitions.tex index 19059ad..4bcb9df 100644 --- a/chapters/core/soundness-proof/01-mathematical-definitions.tex +++ b/chapters/core/soundness-proof/01-mathematical-definitions.tex @@ -27,10 +27,18 @@ The agents are defined as: where $x, \mathit{out}$ are wires. \item $\llbracket \mathit{Materialize}(\mathit{out}) \sim x \rrbracket \iff \mathit{out} = x$\\ where $x, \mathit{out}$ are wires. - \item $\llbracket \mathit{TermAdd}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a + b$\\ + \item $\llbracket \mathit{TermAdd}(a, b) \sim \mathit{out} \rrbracket \iff \mathit{out} = a + b$\\ where $a, b, \mathit{out}$ are wires. - \item $\llbracket \mathit{TermMul}(a, b) \sim \mathit{out} \rrbracket \Rightarrow \mathit{out} = a \cdot b$\\ + \item $\llbracket \mathit{TermMul}(a, b) \sim \mathit{out} \rrbracket \iff \mathit{out} = a \cdot b$\\ where $a, b, \mathit{out}$ are wires. \item $\llbracket \mathit{TermReLU}(x) \sim \mathit{out} \rrbracket \iff \mathit{out} = \max(0, x)$\\ where $x, \mathit{out}$ are wires. + \item $\llbracket \mathit{TermSymbolic}(id) \sim \mathit{out} \rrbracket \iff \mathit{out} = x_{id}$\\ + where $\mathit{out}$ is a wire and $id$ is a variable identifier. + \item $\llbracket \mathit{TermConcrete}(k) \sim \mathit{out} \rrbracket \iff \mathit{out} = k$\\ + where $\mathit{out}$ is a wire and $k \in \mathbb{R}$ is an attribute. + \item $\llbracket \mathit{Dup}(x, y) \sim z \rrbracket \iff z = x = y$\\ + where $x, y, z$ are wires. + \item $\llbracket \mathit{Eraser} \sim x \rrbracket \iff x \in \mathbb{R}$\\ + where $x$ is a wire. \textit{Eraser} effectively removes any constraints. \end{itemize} |