Translate Equation to Network¶

Translating a system of equations to a computational network happens in four stages:

Resolution: the binding of a unique variable identifier to each equation of the system
Isolation: rewriting the system to isolate each bound variable on the left side of each equation
Translation: translating the isolated system to a network according to a set of rewrite rules
Unification: unifying matching network outputs and inputs using the trace operator

Resolution¶

TODO

For each equation \(i\) we define the set of possible bounded variables \( BV \) in the following way:

\[ degree(i) = \max \{ \} \]

\[ BV(i) = \{ \} \]

To find the unique bounded variable for each equations we solve the associated boundedness problem as a simple linear equational system.

Now the isolation is pretty straightforward.

For each equation, with a bounded variable, we isolated the bounded variable through the following rewrite:

TODO: write up isolation rewrite rules

To translate from an isolated equation to a network we apply the following set of rewrite rules:

\[ \verb+<1> = <2>+ \Rightarrow \verb+composition(<2>, <1>)+ \]

\[ \verb+(<1>)+ \Rightarrow \verb+<1>+ \]

\[ \verb+<1>+ \Rightarrow \verb+var(<1>)+ \]

\[ \verb+<1>+ \Rightarrow \verb+const(<1>)+ \]

\[ \verb%<1> + <2>% \Rightarrow \verb+composition(monoidal(<1>,<2>) add)+ \]

\[ \verb%<1> - <2>% \Rightarrow \verb+composition(monoidal(<1>,composition(scalar(-1.0),<2>)) add)+ \]

\[ \verb%<1> * <2>% \Rightarrow \verb+composition(monoidal(<1>,<2>) multiplication)+ \]

\[ \verb%<1> / <2>% \Rightarrow ??? \]

\[ \verb%<1> ^ <2>% \Rightarrow ??? \]

\[ λ \verb+<1>+.\verb+<2>+ @ (\verb+<3>+) \Rightarrow \verb+composition(monoidal(<2>,<3>) convolution(<1>))+ \]

\[ \int \verb+<1>+\ \partial \verb+<2>+ \Rightarrow \verb+composition(<1>, register(<2>))+ \]

\[ \frac{\partial}{\partial} \verb+<2>+\ \verb+<1>+ \Rightarrow \verb+composition(<1>, deregister(<2>))+ \]

Unification now follows as a straightforward rewrite across input and output labels using copy and trace operators.

TODO: write up the rewrite rules