diff options
| author | ericmarin <maarin.eric@gmail.com> | 2026-03-31 16:43:47 +0200 |
|---|---|---|
| committer | ericmarin <maarin.eric@gmail.com> | 2026-04-01 15:08:27 +0200 |
| commit | 81d4d604aa43660b732b3538734a52d509d7c5df (patch) | |
| tree | e0341280c3c3f10752aab7fccb2ddd5ed795c889 /proof.norg | |
| parent | d1b25fbde6b01529fd1bcfdd5778b6cb378eb865 (diff) | |
| download | vein-81d4d604aa43660b732b3538734a52d509d7c5df.tar.gz vein-81d4d604aa43660b732b3538734a52d509d7c5df.zip | |
refactored examples
Diffstat (limited to 'proof.norg')
| -rw-r--r-- | proof.norg | 10 |
1 files changed, 6 insertions, 4 deletions
@@ -48,13 +48,15 @@ version: 1.1.1 $Y = alpha * A * B + beta * C$ *** Flatten - Just identity mapping. + Just identity mapping because the wires are always Flatten. + $o_i ~ i_i$ *** MatMul - Equal to Gemm with $alpha=1$ and $beta=0$. + Equal to Gemm with $alpha=1$, $beta=0$ and $C=0$. *** Reshape - Just identity mapping. + Just identity mapping because the wires always Flatten. + $o_i ~ i_i$ *** Add ONNX Add node is defined as: @@ -491,7 +493,7 @@ version: 1.1.1 $IF false THEN k ELSE 0 = 0 => 0 = 0$ $$ -** Soundness of Reduction +** Soundness of Reduction Let $IN_0$ be the Interaction Net translated from a Neural Network $NN$. Let $IN_n$ be the state of the net after $n$ reduction steps. Then $\forall n \in N$, $[IN_n] = [NN]$. |