{ "cells": [ { "cell_type": "markdown", "source": [ "# Wiring diagrams and syntactic expressions\n", "\n", "\n", "Morphisms in a monoidal category can be represented as syntactic expressions,\n", "such as $f \\cdot g$ and $f \\otimes g$, and also as [wiring\n", "diagrams](@ref wiring_diagram_basics), aka *string diagrams*. Catlab provides\n", "facilities for transforming between these two representations." ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "show_diagram (generic function with 1 method)" }, "metadata": {}, "execution_count": 1 } ], "cell_type": "code", "source": [ "using Catlab.Theories, Catlab.WiringDiagrams\n", "using Catlab.Graphics\n", "\n", "function show_diagram(d::WiringDiagram)\n", " to_graphviz(d, orientation=LeftToRight, labels=false)\n", "end" ], "metadata": {}, "execution_count": 1 }, { "cell_type": "markdown", "source": [ "## Expressions to diagrams\n", "\n", "Converting a morphism expression to a wiring diagram is conceptually and\n", "algorithmically simple, because every expression determines a unique diagram.\n", "\n", "As a simple example, here is the monoidal product of two generators, $f$ and\n", "$g$, first as an expression (displayed using LaTeX) and then as a wiring\n", "diagram (displayed using Graphviz)." ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "f⊗g: A⊗B → B⊗C", "text/latex": "$f \\otimes g : A \\otimes B \\to B \\otimes C$" }, "metadata": {}, "execution_count": 2 } ], "cell_type": "code", "source": [ "A, B, C, D, E = Ob(FreeCartesianCategory, :A, :B, :C, :D, :E)\n", "f = Hom(:f, A, B)\n", "g = Hom(:g, B, C)\n", "\n", "expr = f ⊗ g" ], "metadata": {}, "execution_count": 2 }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "Catlab.Graphics.Graphviz.Graph(\"G\", true, \"dot\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0in1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in1\")), Catlab.Graphics.Graphviz.Node(\"n0in2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"source\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0out1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out1\")), Catlab.Graphics.Graphviz.Node(\"n0out2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"sink\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Node(\"n1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"f\", :fillcolor => \"white\", :id => \"n1\", :label => Catlab.Graphics.Graphviz.Html(\"\\n\\n\\n\\n\\n\\n
f
\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"g\", :fillcolor => \"white\", :id => \"n2\", :label => Catlab.Graphics.Graphviz.Html(\"\\n\\n\\n\\n\\n\\n
g
\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n1\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e1\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n2\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e3\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"C\", :id => \"e4\"))], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :rankdir => \"LR\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :shape => \"none\", :width => \"0\", :height => \"0\", :margin => \"0\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:arrowsize => \"0.5\", :fontname => \"Serif\"))", "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "n1\n", "\n", "f\n", "\n", "\n", "\n", "\n", "n0in1:e->n1:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n2\n", "\n", "g\n", "\n", "\n", "\n", "\n", "n0in2:e->n2:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "n1:e->n0out1:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n2:e->n0out2:w\n", "\n", "\n", "\n", "\n", "\n" ] }, "metadata": {}, "execution_count": 3 } ], "cell_type": "code", "source": [ "show_diagram(to_wiring_diagram(expr))" ], "metadata": {}, "execution_count": 3 }, { "cell_type": "markdown", "source": [ "Here is a monoidal product of compositions:" ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "(f⋅g)⊗(h⋅k): A⊗C → C⊗E", "text/latex": "$\\left(f \\cdot g\\right) \\otimes \\left(h \\cdot k\\right) : A \\otimes C \\to C \\otimes E$" }, "metadata": {}, "execution_count": 4 } ], "cell_type": "code", "source": [ "h = Hom(:h, C, D)\n", "k = Hom(:k, D, E)\n", "\n", "expr = (f ⋅ g) ⊗ (h ⋅ k)" ], "metadata": {}, "execution_count": 4 }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "Catlab.Graphics.Graphviz.Graph(\"G\", true, \"dot\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0in1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in1\")), Catlab.Graphics.Graphviz.Node(\"n0in2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"source\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0out1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out1\")), Catlab.Graphics.Graphviz.Node(\"n0out2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"sink\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Node(\"n1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"f\", :fillcolor => \"white\", :id => \"n1\", :label => Catlab.Graphics.Graphviz.Html(\"\\n\\n\\n\\n\\n\\n
f
\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"g\", :fillcolor => \"white\", :id => \"n2\", :label => Catlab.Graphics.Graphviz.Html(\"\\n\\n\\n\\n\\n\\n
g
\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n3\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"h\", :fillcolor => \"white\", :id => \"n3\", :label => Catlab.Graphics.Graphviz.Html(\"\\n\\n\\n\\n\\n\\n
h
\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Node(\"n4\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:color => \"black\", :comment => \"k\", :fillcolor => \"white\", :id => \"n4\", :label => Catlab.Graphics.Graphviz.Html(\"\\n\\n\\n\\n\\n\\n
k
\"), :style => \"solid\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n1\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e1\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n3\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"C\", :id => \"e2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n2\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e3\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n3\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n4\", \"in1\", \"w\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"D\", :id => \"e4\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"C\", :id => \"e5\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n4\", \"out1\", \"e\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"E\", :id => \"e6\"))], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :rankdir => \"LR\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :shape => \"none\", :width => \"0\", :height => \"0\", :margin => \"0\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:arrowsize => \"0.5\", :fontname => \"Serif\"))", "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "n1\n", "\n", "f\n", "\n", "\n", "\n", "\n", "n0in1:e->n1:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n3\n", "\n", "h\n", "\n", "\n", "\n", "\n", "n0in2:e->n3:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "n2\n", "\n", "g\n", "\n", "\n", "\n", "\n", "n1:e->n2:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n2:e->n0out1:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n4\n", "\n", "k\n", "\n", "\n", "\n", "\n", "n3:e->n4:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n4:e->n0out2:w\n", "\n", "\n", "\n", "\n", "\n" ] }, "metadata": {}, "execution_count": 5 } ], "cell_type": "code", "source": [ "show_diagram(to_wiring_diagram(expr))" ], "metadata": {}, "execution_count": 5 }, { "cell_type": "markdown", "source": [ "## Diagrams to expressions\n", "\n", "Converting a wiring diagram to a syntactic expression is algorithmically more\n", "challenging, due to the fact that a single wiring diagram generally admits\n", "many different representations as an expression. Thus, a particular expression\n", "must be singled out.\n", "\n", "To bring this out, we define a function that round-trips a morphism expression\n", "to a wiring diagram and then back to an expression." ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "roundtrip_expr (generic function with 1 method)" }, "metadata": {}, "execution_count": 6 } ], "cell_type": "code", "source": [ "function roundtrip_expr(expr::FreeCartesianCategory.Hom)\n", " d = to_wiring_diagram(expr)\n", " to_hom_expr(FreeCartesianCategory, d)\n", "end" ], "metadata": {}, "execution_count": 6 }, { "cell_type": "markdown", "source": [ "We can recover the expression just considered above:" ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "(f⋅g)⊗(h⋅k): A⊗C → C⊗E", "text/latex": "$\\left(f \\cdot g\\right) \\otimes \\left(h \\cdot k\\right) : A \\otimes C \\to C \\otimes E$" }, "metadata": {}, "execution_count": 7 } ], "cell_type": "code", "source": [ "roundtrip_expr((f ⋅ g) ⊗ (h ⋅ k))" ], "metadata": {}, "execution_count": 7 }, { "cell_type": "markdown", "source": [ "But here is a different expression that round-trips to the same thing:" ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "(f⋅g)⊗(h⋅k): A⊗C → C⊗E", "text/latex": "$\\left(f \\cdot g\\right) \\otimes \\left(h \\cdot k\\right) : A \\otimes C \\to C \\otimes E$" }, "metadata": {}, "execution_count": 8 } ], "cell_type": "code", "source": [ "roundtrip_expr((f ⊗ h) ⋅ (g ⊗ k))" ], "metadata": {}, "execution_count": 8 }, { "cell_type": "markdown", "source": [ "The equality of these two expressions,\n", "\n", "$$\n", "(f \\cdot g) \\otimes (h \\cdot k) = (f \\otimes h) \\cdot (g \\otimes k),\n", "$$\n", "\n", "is the *interchange law* in a monoidal category. It says that composition and\n", "monoidal products can be interchanged. As this example shows, the conversion\n", "algorithm in Catlab favors products over composition, placing products towards\n", "the root of the expression tree wherever possible.\n", "Other laws can be discovered by this procedure. Since we are working in a\n", "[cartesian monoidal\n", "category](https://ncatlab.org/nlab/show/cartesian+monoidal+category),\n", "operations of copying, $\\Delta_A: A \\to A \\otimes A$, and deleting,\n", "$\\lozenge_A: A \\to I$, are available.\n", "\n", "Consider the operation of copying the product $A \\otimes B$." ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "mcopy{A⊗B}: A⊗B → A⊗B⊗A⊗B", "text/latex": "$\\Delta_{A \\otimes B} : A \\otimes B \\to A \\otimes B \\otimes A \\otimes B$" }, "metadata": {}, "execution_count": 9 } ], "cell_type": "code", "source": [ "expr = mcopy(A ⊗ B)" ], "metadata": {}, "execution_count": 9 }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "Catlab.Graphics.Graphviz.Graph(\"G\", true, \"dot\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0in1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in1\")), Catlab.Graphics.Graphviz.Node(\"n0in2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"in2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"source\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Subgraph(\"\", Catlab.Graphics.Graphviz.Statement[Catlab.Graphics.Graphviz.Node(\"n0out1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out1\")), Catlab.Graphics.Graphviz.Node(\"n0out2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out2\")), Catlab.Graphics.Graphviz.Node(\"n0out3\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out3\")), Catlab.Graphics.Graphviz.Node(\"n0out4\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:id => \"out4\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out3\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out4\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}())], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:rank => \"sink\", :rankdir => \"TB\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\", :shape => \"none\", :label => \"\", :width => \"0\", :height => \"0.333\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:style => \"invis\")), Catlab.Graphics.Graphviz.Node(\"n1\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"junction\", :fillcolor => \"black\", :height => \"0.05\", :id => \"n1\", :label => \"\", :shape => \"circle\", :style => \"filled\", :width => \"0.05\")), Catlab.Graphics.Graphviz.Node(\"n2\", OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"junction\", :fillcolor => \"black\", :height => \"0.05\", :id => \"n2\", :label => \"\", :shape => \"circle\", :style => \"filled\", :width => \"0.05\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in1\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n1\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e1\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n0in2\", \"e\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n2\", \"\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e2\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out1\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e3\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n1\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out3\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"A\", :id => \"e4\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out2\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e5\")), Catlab.Graphics.Graphviz.Edge(Catlab.Graphics.Graphviz.NodeID[Catlab.Graphics.Graphviz.NodeID(\"n2\", \"\", \"\"), Catlab.Graphics.Graphviz.NodeID(\"n0out4\", \"w\", \"\")], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:comment => \"B\", :id => \"e6\"))], OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :rankdir => \"LR\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:fontname => \"Serif\", :shape => \"none\", :width => \"0\", :height => \"0\", :margin => \"0\"), OrderedCollections.OrderedDict{Symbol, Union{String, Catlab.Graphics.Graphviz.Html}}(:arrowsize => \"0.5\", :fontname => \"Serif\"))", "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n", "\n", "G\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "n1\n", "\n", "\n", "\n", "\n", "\n", "n0in1:e->n1\n", "\n", "\n", "\n", "\n", "\n", "\n", "n2\n", "\n", "\n", "\n", "\n", "\n", "n0in2:e->n2\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "\n", "n1->n0out1:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n1->n0out3:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n2->n0out2:w\n", "\n", "\n", "\n", "\n", "\n", "\n", "n2->n0out4:w\n", "\n", "\n", "\n", "\n", "\n" ] }, "metadata": {}, "execution_count": 10 } ], "cell_type": "code", "source": [ "show_diagram(add_junctions!(to_wiring_diagram(expr)))" ], "metadata": {}, "execution_count": 10 }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "(mcopy{A}⊗mcopy{B})⋅(id{A}⊗(AσB)⊗id{B}): A⊗B → A⊗B⊗A⊗B", "text/latex": "$\\left(\\Delta_{A} \\otimes \\Delta_{B}\\right) \\cdot \\left(\\mathrm{id}_{A} \\otimes \\sigma_{A,B} \\otimes \\mathrm{id}_{B}\\right) : A \\otimes B \\to A \\otimes B \\otimes A \\otimes B$" }, "metadata": {}, "execution_count": 11 } ], "cell_type": "code", "source": [ "roundtrip_expr(expr)" ], "metadata": {}, "execution_count": 11 }, { "cell_type": "markdown", "source": [ "The equation just witnessed,\n", "\n", "$$\n", "\\Delta_{A \\otimes B} = (\\Delta_A \\otimes \\Delta_B) \\cdot (1_A \\otimes \\sigma_{A,B} \\otimes 1_B),\n", "$$\n", "\n", "is one of the *coherence laws* for cartesian products\n", "([arXiv:0908.3347](https://arxiv.org/abs/0908.3347), Table 7). Another\n", "coherence law for products is\n", "\n", "$$\n", "\\lozenge_{A \\otimes B} = \\lozenge_A \\otimes \\lozenge_B.\n", "$$" ], "metadata": {} }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "delete{A⊗B}: A⊗B → I", "text/latex": "$\\lozenge_{A \\otimes B} : A \\otimes B \\to I$" }, "metadata": {}, "execution_count": 12 } ], "cell_type": "code", "source": [ "expr = delete(A ⊗ B)" ], "metadata": {}, "execution_count": 12 }, { "outputs": [ { "output_type": "execute_result", "data": { "text/plain": "delete{A}⊗delete{B}: A⊗B → I", "text/latex": "$\\lozenge_{A} \\otimes \\lozenge_{B} : A \\otimes B \\to I$" }, "metadata": {}, "execution_count": 13 } ], "cell_type": "code", "source": [ "roundtrip_expr(expr)" ], "metadata": {}, "execution_count": 13 } ], "nbformat_minor": 3, "metadata": { "language_info": { "file_extension": ".jl", "mimetype": "application/julia", "name": "julia", "version": "1.7.3" }, "kernelspec": { "name": "julia-1.7", "display_name": "Julia 1.7.3", "language": "julia" } }, "nbformat": 4 }