jpfairbanks
commented
4 years ago This is a good example of how we should be tracking some higher level structure in wiring diagrams that mathematicians keep in their head. Like when you do F = ocompose(f, i, g) it creates an subdiagram containing g within F. The semantics of F don't depend on that grouping, and the wiring diagram data structure doesn't track it, but in order to do layout and rewriting the way a human would, you need to remember that the nodes of F corresponding to g came hung together in f.
In the same way the trace operator creates a subdiagram, ie. that which is traced over. In order to do conversion of wiring diagrams with trace, we need to keep track of the subdiagrams. I think the same will be true for internal homs. I guess this is another argument in favor of point free notation. If you want to have a new type of formula that is parameterized by formulas like tr for trace, you can always introduce a term type that takes terms as an argument: (tr((f ⊗ g) ⋅ h) ⊗ g) ⋅ h. Or for example the keeping track of the ocompose structure ⊙(⊙(⊙(f,1,g), 2, h), 1, f). The formula keeps track of how you got there by composition, in a way that wiring diagrams don't. I guess that is why wiring diagrams are a "normalizing form" for a lot of variation in the hom expressions.
Wiring diagrams are great for visualization, but the more I think about the future of Catlab, the more I think we will be building on the GATExpr and @program functionality because it is more scalable for manipulation and input respectively. I think the paradigm of @program for input, GATExpr for manipulation and WiringDiagram for output/visualization is the right way to think about Catlab. Of course the ability to go WiringDiagram --> GATExpr is critical for usability, so we can't ignore things that are hard to do with WDs.
The machinery for converting wiring diagrams to morphism expressions should support traced monoidal categories.
This is not a purely mechanical job; some thinking will be needed. At the very least, self-loops must be detected. Also, some parts of the existing algorithm use a topological sort and so assume that the underlying graph is a DAG. This assumption must be relaxed.