Networks

Computational Networks

Computational networks are defined using the following grammar

\[ \begin{array}{rl} \verb+NETWORK:+ & \verb+<COMPOSITION>+\ |\ \verb+<MONOIDAL>+\ |\ \verb+<TRACE>+\ |\ \verb+<ATOMIC>+ \\ \verb+COMPOSITION:+ & \verb+composition(<NETWORK>, <NETWORK>)+\\ \verb+MONOIDAL:+ & \verb+monoidal(<NETWORK>, <NETWORK>)+\\ \verb+TRACE:+ & \verb+trace(<NETWORK>)+\\ \verb+ATOMIC:+ & \verb+var(<IDENTIFIER>)+ \\ & |\ \verb+const(<NUMBER>)+ \\ & |\ \verb+add+ \\ & |\ \verb+convolution(<NATURAL_NUMBER>)+ \\ & |\ \verb+id+ \\ & |\ \verb+multiplication+ \\ & |\ \verb+scalar(<NUMBER>)+ \\ & |\ \verb+split+ \\ & |\ \verb+deregister(<NATURAL_NUMBER>)+ \\ & |\ \verb+register(<NATURAL_NUMBER>)+ \\ \verb+IDENTIFIER:+ & \verb%[a-zA-Z][a-zA-Z0-9_]*% \\ \verb+NUMBER:+ & x \in \mathbb{R} \\ \verb+NATURAL_NUMBER:+ & x \in \mathbb{N} \\ \end{array} \]

Networks are categories

Computational networks form a category over the domain and targets calculi. More precisely, they form a traced monoidal category extended with a few special atomic morphisms, from which all morphisms within the category is formed.

Proof system

This categorical view of computational networks give rise to an associated proof system, that can be used construct, reasons and rewrite computational networks. This is very similar to a Curry-Howard approach to reason about programs defined in standard lambda calculus.

This proof systems is essentially just a representation of the standard axioms of a traced monoidcal category extended with a set of axioms for each of the atomic morphisms. We can then use these rewrite computational networks into new forms, either to simplify them before simulation or to rewrite to simpler forms, like closed-form solutions to equational systems.