hmillerbakewell
commented
6 years ago Adding constraints to connections doesn't feel like Quantomatic's job: Starting with a valid graph and applying valid rules gives you valid graphs. If the user ends up with something connected in a manner it shouldn't be then either the starting graph or the rules are incorrect (barring bugs.) The theory shouldn't have to put any constraints on the user.
Specifying border-thickness is now working, see #232
My understanding of the string rewriting system is that we cannot generally have a statement like "G = H" where G is doubled and H isn't, because they have different numbers of boundary nodes. That said, you can have a pseudo-version of this by introducing a "zip" node which acts as a mediator between doubled and undoubled wires, but this requires non-commutative operations. (In particular the zip node needs to know which wires go left and which go right.)
[Updated to remove commutative version, since it was probably more misleading than helpful.]
It would be nice if Quantomatic could deal with doubled wires and systems. Ideally, it'd have some awareness of the rules of doubling (i.e. support conversion between two single wires/nodes and one doubled wire/node, and allow all purely-single theorems to be applied in doubled form), but realistically, it's probably more achievable and already a huge benefit to be able to allow vertices to indicate what types of edge are allowed to connect to them. That would let the Theory enforce the constraints, and axioms can cover the rules that need unpacking of doubled wires to prove.
Also, if the vertex-edge legality check is implemented, it would be nice if the border thickness of vertex types could be specified.
This should probably be turned into several feature issues (border thickness, vertex-edge legality, rule doubling, double single/single double conversion), but I'll come back to that later and close this if everything has its own issue.