/
search_index.js
3 lines (3 loc) · 277 KB
/
search_index.js
1
2
3
var documenterSearchIndex = {"docs":
[{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/graphics/tikz_wiring_diagrams.jl\"","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/#Drawing-wiring-diagrams-in-TikZ","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"(Image: )","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"Catlab can draw morphism expressions as TikZ pictures. To use this feature, LaTeX must be installed and the Julia package TikzPictures.jl must be loaded.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"For best results, it is recommended to load the packages Convex.j and SCS.jl. When available they are used to optimize the layout of the outer ports.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"using Catlab.WiringDiagrams, Catlab.Graphics\n\nimport Convex, SCS\nimport TikzPictures","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/#Examples","page":"Drawing wiring diagrams in TikZ","title":"Examples","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/#Symmetric-monoidal-category","page":"Drawing wiring diagrams in TikZ","title":"Symmetric monoidal category","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"using Catlab.Theories\n\nA, B, C, D = Ob(FreeSymmetricMonoidalCategory, :A, :B, :C, :D)\nf, g = Hom(:f, A, B), Hom(:g, B, A);\nnothing #hide","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"To start, here are a few very simple examples.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(f, labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(f⋅g, labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(f⊗g, labels=true, orientation=TopToBottom)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"Here is a more complex example, involving generators with compound domains and codomains.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"h, k = Hom(:h, C, D), Hom(:k, D, C)\nm, n = Hom(:m, B⊗A, A⊗B), Hom(:n, D⊗C, C⊗D)\nq = Hom(:l, A⊗B⊗C⊗D, D⊗C⊗B⊗A)\n\nto_tikz((f⊗g⊗h⊗k)⋅(m⊗n)⋅q⋅(n⊗m)⋅(h⊗k⊗f⊗g))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"Identities and braidings appear as wires.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(id(A), labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(braid(A,B), labels=true, labels_pos=0.25)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(braid(A,B) ⋅ (g⊗f) ⋅ braid(A,B))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"The isomorphism A otimes B otimes C to C otimes B otimes A induced by the permutation (3 2 1) is a composite of braidings and identities.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"σ = (braid(A,B) ⊗ id(C)) ⋅ (id(B) ⊗ braid(A,C) ⋅ (braid(B,C) ⊗ id(A)))\n\nto_tikz(σ, arrowtip=\"Stealth\", arrowtip_pos=\"-0.1pt\",\n labels=true, labels_pos=\"0.1pt\")","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"By default, anchor points are added along identity and braiding wires to reproduce the expression structure in the layout. The anchors can be disabled to get a more \"unbiased\" layout.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(σ, anchor_wires=false, arrowtip=\"Stealth\", arrowtip_pos=\"-0.1pt\",\n labels=true, labels_pos=\"0.1pt\")","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/#Biproduct-category","page":"Drawing wiring diagrams in TikZ","title":"Biproduct category","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"A, B, C = Ob(FreeBiproductCategory, :A, :B, :C)\nf = Hom(:f, A, B)\n\nto_tikz(mcopy(A), labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(delete(A), labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(mcopy(A)⋅(f⊗f)⋅mmerge(B), labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(mcopy(A⊗B), orientation=TopToBottom, labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(mcopy(A⊗B⊗C), orientation=TopToBottom, labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/#Compact-closed-category","page":"Drawing wiring diagrams in TikZ","title":"Compact closed category","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"The unit and co-unit of a compact closed category appear as caps and cups.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"A, B = Ob(FreeCompactClosedCategory, :A, :B)\n\nto_tikz(dunit(A), arrowtip=\"Stealth\", labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(dcounit(A), arrowtip=\"Stealth\", labels=true)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"In a self-dual compact closed category, such as a bicategory of relations, every morphism f A to B has a transpose f^dagger B to A given by bending wires:","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"A, B = Ob(FreeBicategoryRelations, :A, :B)\nf = Hom(:f, A, B)\n\nto_tikz((dunit(A) ⊗ id(B)) ⋅ (id(A) ⊗ f ⊗ id(B)) ⋅ (id(A) ⊗ dcounit(B)))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/#Abelian-bicategory-of-relations","page":"Drawing wiring diagrams in TikZ","title":"Abelian bicategory of relations","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"In an abelian bicategory of relations, such as the category of linear relations, the duplication morphisms Delta_X X to X oplus X and addition morphisms blacktriangledown_X X oplus X to X belong to a bimonoid. Among other things, this means that the following two morphisms are equal.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"X = Ob(FreeAbelianBicategoryRelations, :X)\n\nto_tikz(plus(X) ⋅ mcopy(X))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz((mcopy(X)⊕mcopy(X)) ⋅ (id(X)⊕swap(X,X)⊕id(X)) ⋅ (plus(X)⊕plus(X)))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/#Custom-styles","page":"Drawing wiring diagrams in TikZ","title":"Custom styles","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"The visual appearance of wiring diagrams can be customized using the builtin options or by redefining the TikZ styles for the boxes or wires.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"A, B, = Ob(FreeSymmetricMonoidalCategory, :A, :B)\nf, g = Hom(:f, A, B), Hom(:g, B, A)\n\npic = to_tikz(f⋅g, styles=Dict(\n \"box\" => [\"draw\", \"fill\"=>\"{rgb,255: red,230; green,230; blue,250}\"],\n))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"X = Ob(FreeAbelianBicategoryRelations, :X)\n\nto_tikz(plus(X) ⋅ mcopy(X), styles=Dict(\n \"junction\" => [\"circle\", \"draw\", \"fill\"=>\"red\", \"inner sep\"=>\"0\"],\n \"variant junction\" => [\"circle\", \"draw\", \"fill\"=>\"blue\", \"inner sep\"=>\"0\"],\n))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"By default, the boxes are rectangular (:rectangle). Other available shapes include circles (:circle), ellipses (:ellipse), triangles (:triangle, :invtriangle), and trapezoids (:trapezium, :invtrapezium).","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(f⋅g, default_box_shape=:circle)","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(f⋅g, rounded_boxes=false, box_shapes=Dict(\n f => :triangle, g => :invtriangle,\n))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(f⋅g, orientation=TopToBottom, rounded_boxes=false, box_shapes=Dict(\n f => :triangle, g => :invtriangle,\n))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"to_tikz(f⋅g, box_shapes=Dict(\n f => :invtrapezium, g => :trapezium,\n))","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/#Output-formats","page":"Drawing wiring diagrams in TikZ","title":"Output formats","text":"","category":"section"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"The function to_tikz returns an object of type TikZ.Document, representing a TikZ picture and its TikZ library dependencies as an abstract syntax tree. When displayed interactively, this object is compiled by LaTeX to PDF and then converted to SVG.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"To generate the LaTeX source code, use the builtin pretty-printer. This feature does not require LaTeX or TikzPictures.jl to be installed.","category":"page"},{"location":"generated/graphics/tikz_wiring_diagrams/","page":"Drawing wiring diagrams in TikZ","title":"Drawing wiring diagrams in TikZ","text":"import Catlab.Graphics: TikZ\n\ndoc = to_tikz(f⋅g)\nTikZ.pprint(doc)","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/graphics/layouts_vs_drawings.jl\"","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/#Layouts-versus-drawings-of-wiring-diagrams","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"","category":"section"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"(Image: )","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"In Catlab, layout and drawing (rendering) of wiring diagrams are mostly decoupled. This notebook shows how to lay out diagrams using Graphviz's rank-based layout or Catlab's series-parallel layout and then render them using Compose.jl or TikZ.","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"The morphism we will visualize is:","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"using Catlab.Theories\n\nX = Ob(FreeSymmetricMonoidalCategory, :X)\nf, g, h = (Hom(sym, X, X) for sym in (:f, :g, :h))\n\nexpr = otimes(f, compose(f,g), compose(f,g,h))","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"Let's convert this expression into a wiring diagram. This yields a purely combinatorial object, as evidenced by its underlying graph.","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"using Catlab.WiringDiagrams, Catlab.Graphics\n\ndiagram = to_wiring_diagram(expr)\nWiringDiagrams.graph(diagram)","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/#Graphviz-layout","page":"Layouts versus drawings of wiring diagrams","title":"Graphviz layout","text":"","category":"section"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"Calling to_graphviz both lays out and draws the diagram, entirely within Graphviz.","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"to_graphviz(diagram, orientation=LeftToRight)","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"To get just the layout from Graphviz, we call graphviz_layout instead. We can then render this layout using Compose.jl. Note that the Graphviz layout has units in points.","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"import Compose\n\nlayout = graphviz_layout(diagram, orientation=LeftToRight)\nlayout_to_composejl(layout, base_unit=Compose.pt)","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"The same layout can be rendered in TikZ:","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"import TikzPictures\n\nlayout_to_tikz(layout, base_unit=\"1pt\")","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/#Series-parallel-layout","page":"Layouts versus drawings of wiring diagrams","title":"Series-parallel layout","text":"","category":"section"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"Catlab has its own layout system based on series-parallel decomposition. In this case, the layout exactly recovers the structure of the morphism expression created at the beginning.","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"layout = layout_diagram(FreeSymmetricMonoidalCategory, diagram,\n orientation=LeftToRight)\nlayout_to_composejl(layout)","category":"page"},{"location":"generated/graphics/layouts_vs_drawings/","page":"Layouts versus drawings of wiring diagrams","title":"Layouts versus drawings of wiring diagrams","text":"layout_to_tikz(layout)","category":"page"},{"location":"apis/programs/#programs","page":"Programs","title":"Programs","text":"","category":"section"},{"location":"apis/programs/","page":"Programs","title":"Programs","text":"Modules = [\n Programs.GenerateJuliaPrograms,\n Programs.ParseJuliaPrograms,\n Programs.RelationalPrograms,\n]\nPrivate = false","category":"page"},{"location":"apis/programs/#Catlab.Programs.GenerateJuliaPrograms","page":"Programs","title":"Catlab.Programs.GenerateJuliaPrograms","text":"Compile or evaluate morphisms as Julia programs.\n\n\n\n\n\n","category":"module"},{"location":"apis/programs/#Catlab.Programs.GenerateJuliaPrograms.Block","page":"Programs","title":"Catlab.Programs.GenerateJuliaPrograms.Block","text":"A block of Julia code with input and output variables.\n\n\n\n\n\n","category":"type"},{"location":"apis/programs/#Catlab.Programs.GenerateJuliaPrograms.CompileState","page":"Programs","title":"Catlab.Programs.GenerateJuliaPrograms.CompileState","text":"Internal state for compilation of morphism into Julia code.\n\n\n\n\n\n","category":"type"},{"location":"apis/programs/#Catlab.Programs.GenerateJuliaPrograms.compile-Tuple{Module, HomExpr}","page":"Programs","title":"Catlab.Programs.GenerateJuliaPrograms.compile","text":"Compile a morphism expression into a Julia function.\n\n\n\n\n\n","category":"method"},{"location":"apis/programs/#Catlab.Programs.GenerateJuliaPrograms.compile_block-Tuple{HomExpr, Vector{T} where T}","page":"Programs","title":"Catlab.Programs.GenerateJuliaPrograms.compile_block","text":"Compile a morphism expression into a block of Julia code.\n\n\n\n\n\n","category":"method"},{"location":"apis/programs/#Catlab.Programs.GenerateJuliaPrograms.compile_expr-Tuple{HomExpr}","page":"Programs","title":"Catlab.Programs.GenerateJuliaPrograms.compile_expr","text":"Compile a morphism expression into a Julia function expression.\n\n\n\n\n\n","category":"method"},{"location":"apis/programs/#Catlab.Programs.GenerateJuliaPrograms.evaluate-Tuple{HomExpr, Vararg{Any, N} where N}","page":"Programs","title":"Catlab.Programs.GenerateJuliaPrograms.evaluate","text":"Evaluate a morphism as a function.\n\nIf the morphism will be evaluated only once (possibly with vectorized inputs), then direct evaluation will be much faster than compiling (via compile) and evaluating a standard Julia function.\n\nCompare with functor.\n\n\n\n\n\n","category":"method"},{"location":"apis/programs/#Catlab.Programs.ParseJuliaPrograms","page":"Programs","title":"Catlab.Programs.ParseJuliaPrograms","text":"Parse Julia programs into morphisms represented as wiring diagrams.\n\n\n\n\n\n","category":"module"},{"location":"apis/programs/#Catlab.Programs.ParseJuliaPrograms.parse_wiring_diagram-Tuple{Presentation, Expr}","page":"Programs","title":"Catlab.Programs.ParseJuliaPrograms.parse_wiring_diagram","text":"Parse a wiring diagram from a Julia function expression.\n\nFor more information, see the corresponding macro @program.\n\n\n\n\n\n","category":"method"},{"location":"apis/programs/#Catlab.Programs.ParseJuliaPrograms.@program-Tuple{Any, Vararg{Any, N} where N}","page":"Programs","title":"Catlab.Programs.ParseJuliaPrograms.@program","text":"Parse a wiring diagram from a Julia program.\n\nFor the most part, this is standard Julia code but we take a few liberties with the syntax. Products are represented as tuples. So if x and y are variables of type X and Y, then (x,y) has type X otimes Y. Also, both () and nothing are interpreted as the monoidal unit I.\n\nUnlike in standard Julia, the call expressions f(x,y) and f((x,y)) are equivalent. Consequently, given morphisms f W to X otimes Y and g X otimes Y to Z, the code\n\nx, y = f(w)\ng(x,y)\n\nis equivalent to g(f(w)). In standard Julia, at most one of these calls to g would be valid, unless g had multiple signatures.\n\nThe diagonals (copying and deleting) are implicit in the Julia syntax: copying is variable reuse and deleting is variable non-use. For the codiagonals (merging and creating), a special syntax is provided, reinterpreting Julia's vector literals. The merge of x1 and x2 is represented by the vector [x1,x2] and creation by the empty vector []. For example, f([x1,x2]) translates to compose(mmerge(X),f).\n\nThis macro is a wrapper around parse_wiring_diagram.\n\n\n\n\n\n","category":"macro"},{"location":"apis/programs/#Catlab.Programs.RelationalPrograms","page":"Programs","title":"Catlab.Programs.RelationalPrograms","text":"Parse relation expressions in Julia syntax into undirected wiring diagrams.\n\n\n\n\n\n","category":"module"},{"location":"apis/programs/#Catlab.Programs.RelationalPrograms.parse_relation_diagram-Tuple{Expr}","page":"Programs","title":"Catlab.Programs.RelationalPrograms.parse_relation_diagram","text":"Parse an undirected wiring diagram from a relation expression.\n\nFor more information, see the corresponding macro @relation.\n\n\n\n\n\n","category":"method"},{"location":"apis/programs/#Catlab.Programs.RelationalPrograms.@relation-Tuple","page":"Programs","title":"Catlab.Programs.RelationalPrograms.@relation","text":"Construct an undirected wiring diagram using relation notation.\n\nUnlike the @program macro for directed wiring diagrams, this macro departs from the usual semantics of the Julia programming language. Function calls with n arguments are now interpreted as assertions that an n-ary relation holds at a particular point. For example, the composition of binary relations R ⊆ X × Y and S ⊆ Y × Z can be represented as an undirected wiring diagram by the macro call\n\n@relation (x,z) where (x::X, y::Y, z::Z) begin\n R(x,y)\n S(y,z)\nend\n\nIn general, the context in the where clause defines the set of junctions in the diagram and variable sharing defines the wiring of ports to junctions.\n\nThe ports and junctions of the diagram may be typed or untyped, and the ports may be named or unnamed. Thus four possible types of diagrams may be returned, with the type determined by the form of relation header:\n\nUntyped, unnamed: @relation (x,z) where (x,y,z) ...\nTyped, unnamed: @relation (x,z) where (x::X, y::Y, z::Z) ...\nUntyped, named: @relation (out1=x, out2=z) where (x,y,z) ...\nTyped, named: @relation (out=1, out2=z) where (x::X, y::Y, z::Z) ...\n\n\n\n\n\n","category":"macro"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/wiring_diagrams/wiring_diagram_basics.jl\"","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#wiring_diagram_basics","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"(Image: )","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"Using Catlab, you can create, manipulate, serialize, and visualize wiring diagrams, also known as string diagrams. The flexible data structure for wiring diagrams allows arbitrary data to be attached to boxes, ports, and wires, and supports recursively nested diagrams.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"You can interact with wiring diagrams using two different progamming interfaces:","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"Categorical: A high-level, functional interface expressed in terms of categorical concepts, such as composition (compose), monoidal products (otimes), duplication (mcopy), and deletion (delete).\nImperative: A lower-level, mutating interface to directly manipulate boxes, ports, and wires, via operations like adding boxes (add_box) and wires (add_wire).","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"In this notebook, we introduce both interfaces. We do not explicitly cover the visualization API, although for illustrative purposes we will draw wiring diagrams using Graphviz. Thus, you should install Graphviz if you wish to run this notebook.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"using Catlab.WiringDiagrams\n\nusing Catlab.Graphics\nimport Catlab.Graphics: Graphviz\n\nshow_diagram(d::WiringDiagram) = to_graphviz(d,\n orientation=LeftToRight,\n labels=true, label_attr=:xlabel,\n node_attrs=Graphviz.Attributes(\n :fontname => \"Courier\",\n ),\n edge_attrs=Graphviz.Attributes(\n :fontname => \"Courier\",\n )\n)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Data-structures","page":"Basics of wiring diagrams","title":"Data structures","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"The basic building blocks of a wiring diagram are boxes, ports, and wires. The top-level data structure is WiringDiagram, defined in the module Catlab.WiringDiagrams. A wiring diagram consists of boxes (usually of type Box) connected by wires (of type Wire). Each box has a sequence of input ports and a sequence of output ports, as does the wiring diagram itself. The wires have sources and targets, both of which consist of a box and a port on that box.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"The boxes in a wiring diagram are indexed by integer IDs. Boxes can be retrieved by ID, and wires refer to boxes using their IDs. Two special IDs, obtained by input_id and output_id methods, refer to the inputs and outputs of the diagram itself. In this way, wires can connect the (inner) boxes of a diagram to the diagram's \"outer box\".","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"The WiringDiagram data structure is an elaborate wrapper around a directed graph from LightGraphs.jl. The underlying DiGraph object can be accessed using the graph method. The vertices of this graph are exactly the box IDs. The graph should never be mutated directly, on pain of creating inconsistent state, but it does allow convenient access to the large array of graph algorithms supported by LightGraphs.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"All this is somewhat abstract but should become clearer as we see concrete examples.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Categorical-interface","page":"Basics of wiring diagrams","title":"Categorical interface","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"In this example, the wiring diagrams will carry symbolic expressions (of type Catlab.ObExpr and Catlab.HomExpr).","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"using Catlab.Theories\n\nA, B, C, D = Ob(FreeBiproductCategory, :A, :B, :C, :D)\nf = Hom(:f, A, B)\ng = Hom(:g, B, C)\nh = Hom(:h, C, D)\n\nf","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Generators","page":"Basics of wiring diagrams","title":"Generators","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"Convert each of the morphism generators into a diagram with a single box.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"f, g, h = to_wiring_diagram(f), to_wiring_diagram(g), to_wiring_diagram(h)\nf","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(f)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Composition","page":"Basics of wiring diagrams","title":"Composition","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"compose(f,g)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(compose(f,g))","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Monoidal-products","page":"Basics of wiring diagrams","title":"Monoidal products","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"otimes(f,h)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(otimes(f,h))","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Copy-and-merge,-delete-and-create","page":"Basics of wiring diagrams","title":"Copy and merge, delete and create","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"mcopy(codom(f),2)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(mcopy(codom(f),2))","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(compose(f, mcopy(codom(f),2)))","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(compose(mcopy(dom(f),2), otimes(f,f)))","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Imperative-interface","page":"Basics of wiring diagrams","title":"Imperative interface","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"We now show how to manipulate wiring diagrams using the low-level, imperative interface. The diagrams will carry Julia symbols.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"f = Box(:f, [:A], [:B])\ng = Box(:g, [:B], [:C])\nh = Box(:h, [:C], [:D])\n\nf","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Composition-2","page":"Basics of wiring diagrams","title":"Composition","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"For example, here is how to manually construct a composition of two boxes.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"The add_box! method adds a box to a wiring diagrams and returns the ID assigned to the box. How the boxes are indexed is an implementation detail that you should not rely on; use the IDs that the system gives you.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"d = WiringDiagram([:A], [:C])\n\nfv = add_box!(d, f)\ngv = add_box!(d, g)\n\nadd_wires!(d, [\n (input_id(d),1) => (fv,1),\n (fv,1) => (gv,1),\n (gv,1) => (output_id(d),1),\n])\n\nnboxes(d)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"nwires(d)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"d","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(d)","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/#Products","page":"Basics of wiring diagrams","title":"Products","text":"","category":"section"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"Here is how to manually construct a product of two boxes.","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"d = WiringDiagram([:A,:C], [:B,:D])\n\nfv = add_box!(d, f)\nhv = add_box!(d, h)\n\nadd_wires!(d, [\n (input_id(d),1) => (fv,1),\n (input_id(d),2) => (hv,1),\n (fv,1) => (output_id(d),1),\n (hv,1) => (output_id(d),2),\n])\n\nd","category":"page"},{"location":"generated/wiring_diagrams/wiring_diagram_basics/","page":"Basics of wiring diagrams","title":"Basics of wiring diagrams","text":"show_diagram(d)","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/sketches/meets.jl\"","category":"page"},{"location":"generated/sketches/meets/#meets","page":"meets","title":"meets","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"(Image: )","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Our first example of a concept defined by a universal mapping property is a meet respectively meet.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"The first step is our Catlab imports","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"using Core: GeneratedFunctionStub\nusing Test\n\nusing Catlab, Catlab.Theories, Catlab.CategoricalAlgebra, Catlab.CategoricalAlgebra.FinSets\nusing Catlab.Present\nusing Catlab.Graphics\nusing Catlab.Graphics.Graphviz\n\nimport Catlab.Theories: compose\nusing DataStructures","category":"page"},{"location":"generated/sketches/meets/#Defining-some-basic-preorders","page":"meets","title":"Defining some basic preorders","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"@present P(FreeSchema) begin\n (a₁,a₂,a₃,a₄)::Ob\n f::Hom(a₁, a₂)\n g::Hom(a₁, a₃)\n h::Hom(a₂, a₄)\n k::Hom(a₃, a₄)\nend","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"We can draw a picture of our preorder as a Hasse Diagram.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"to_graphviz(P)","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"It will be convenient to program with our preorders based on the Hasse Diagram represent as a labeled graph so we convert the Presentation{Schema, Symbol} into a FreeDigram. FreeDiagrams are implemented as an ACSet which you can think of as an in-memory database. ACSets are a key feature of Catlab that allow you to represent many data structures in a common framework.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"g = FreeDiagram(P)","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"To give ourselves a graph-like API for Hasse Diagrams, we define parents and children.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"parents(g, y::Int) = subpart(g, incident(g, y, :tgt), :src)\nchildren(g, x::Int) = subpart(g, incident(g, x, :src), :tgt)","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"We can compute upsets/downsets with breadth first search.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"function bfs(g, x::Int, f=children)\n explored = falses(nparts(g, :V))\n explored[x] = 1\n q = Queue{Int}()\n enqueue!(q, x)\n while !isempty(q)\n v = dequeue!(q)\n S = f(g,v)\n map(filter(s -> !explored[s], S)) do s\n enqueue!(q, s)\n end\n explored[S] .= true\n end\n return findall(explored)\nend","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"The upset of a preorder element is all the elements that come after it in the preorder.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"upset(g,x) = bfs(g,x,children)","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"The downset is the dual notion, which we compute by reversing the role of children and parents.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"downset(g,x) = bfs(g,x,parents)\n\nupset(g, 1)","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"We can use upsets to define the less than or equal two relation implied by any Hasse Diagram","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"function leq(g::FreeDiagram, x::Int, y::Int)\n return y in upset(g, x)\nend","category":"page"},{"location":"generated/sketches/meets/#Exercise-1","page":"meets","title":"Exercise 1","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Define a more efficient algorithm for checking whether two elements satisfy the leq relation.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Multiple dispatch allows us to overload the leq function with another method for symbols.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"function leq(g::FreeDiagram, x::Symbol, y::Symbol)\n leq(g, incident(g, x, :ob), incident(g, y, :ob))\nend","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"the meet of two elements is the largest element in the intersection of their downsets.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"function meet(g::FreeDiagram, x::Int, y::Int)\n U = downset(g, x) ∩ downset(g,y)\n maxima(g, U)\n return maximum(g, U)\nend\n\nfunction meet(g::FreeDiagram, x, y)\n meet(g, incident(g, x, :ob)[1], incident(g, y, :ob)[1])\nend","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"assuming that D is a downset, the maxima are those elements whose children are disjoint from D.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"function maxima(g::FreeDiagram, D::Vector{Int})\n X = Set(D)\n M = filter(D) do x\n Pₓ = children(g, x) ∩ X\n length(Pₓ) == 0\n end\n return M\nend\n\nfunction hastop(g::FreeDiagram, xs::Vector{Int})\n length(maxima(g, xs)) == 1\nend\n\nfunction maximum(g::FreeDiagram, xs::Vector{Int})\n m = maxima(g, xs::Vector{Int})\n if length(m) == 1\n return m[1]\n end\n if length(m) > 1\n all_iso = all(m) do a\n Uₐ = downset(g, a)\n a_le_allb = all(m) do b\n b in Uₐ\n end\n return a_le_allb\n end\n if all_iso\n return m[1]\n end\n end\n return nothing\nend","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"From the definition of minimum, you can see that when you want to do many leq queries in sequence, you can reuse the upsets that you compute with bfs. This is a place where mathematical abstractions don't work well with the operational needs of computer programming. In a mathematical definition you can define x ≤ y as y ∈ upset(x), but in programming, that is inefficient when you want to check a property like for all y in Y, x ≤ y. Programming requires you to reason about not only the correctness of the code, but also the performance. Much of the complexity of software engineering comes from the fact that computational performance requires the programmers to break down their clean abstractions to optimize the code.","category":"page"},{"location":"generated/sketches/meets/#Exercise-2","page":"meets","title":"Exercise 2","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"If you wanted to perform many x ≤ y queries in a loop, you might want to precompute the matrix L where L[i,j] = 1 if and only if i ≤ j in the preorder P. Implement an algorithm that performs this computation in O(V⋅E) time where V is the number of elements in P and E is the number of edges in the corresponding FreeDiagram.","category":"page"},{"location":"generated/sketches/meets/#Testing-it-out","page":"meets","title":"Testing it out","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Let's make sure we get the answers that we expect.","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"using Test\n@testset \"Upsets\" begin\n @test upset(g, 3) == [3,4]\n @test upset(g, 2) == [2,4]\n @test upset(g, 1) == [1,2,3,4]\n @test upset(g, 4) == [4]\nend\n@testset \"Downsets\" begin\n @test downset(g, 3) == [1,3]\n @test downset(g, 2) == [1,2]\n @test downset(g, 4) == [1,2,3,4]\n @test downset(g, 1) == [1]\nend\n\n@testset \"Meets\" begin\n @test meet(g, 2,3) == 1\n @test meet(g, 1,2) == 1\n @test meet(g, 3,4) == 3\n @test meet(g, 1, 4) == 1\n @test meet(g, 1, 1) == 1\n @test meet(g, 2, 2) == 2\nend","category":"page"},{"location":"generated/sketches/meets/#Another-Example:","page":"meets","title":"Another Example:","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"@present P(FreeSchema) begin\n (a₁,a₂,a₃,a₄, a₅)::Ob\n f::Hom(a₁, a₂)\n g::Hom(a₁, a₃)\n h::Hom(a₂, a₄)\n k::Hom(a₃, a₄)\n l::Hom(a₅, a₂)\nend","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Which can be viewed as a picture:","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"to_graphviz(P)","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Or, as tables:","category":"page"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"g = FreeDiagram(P)","category":"page"},{"location":"generated/sketches/meets/#Test-suite","page":"meets","title":"Test suite","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"@testset \"meets2\" begin\n @test meet(g, 2,3) == 1\n @test meet(g, 1,2) == 1\n @test meet(g, 3,4) == 3\n @test meet(g, 1, 4) == 1\n @test meet(g, 1, 1) == 1\n @test meet(g, 2, 2) == 2\n @test meet(g, 3, 5) == nothing\n @test meet(g, 2, 5) == 5\nend","category":"page"},{"location":"generated/sketches/meets/#Exercise-3","page":"meets","title":"Exercise 3","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Make bigger preorders to test corner cases in the above code. If you find an example that breaks these implementations, please report it.","category":"page"},{"location":"generated/sketches/meets/#Exercise-4","page":"meets","title":"Exercise 4","text":"","category":"section"},{"location":"generated/sketches/meets/","page":"meets","title":"meets","text":"Implement the dual constructions for joins.","category":"page"},{"location":"apis/graphs/#graphs","page":"Graphs","title":"Graphs","text":"","category":"section"},{"location":"apis/graphs/","page":"Graphs","title":"Graphs","text":"Modules = [\n Graphs.BasicGraphs,\n Graphs.PropertyGraphs,\n Graphs.GraphAlgorithms,\n]\nPrivate = false","category":"page"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs","page":"Graphs","title":"Catlab.Graphs.BasicGraphs","text":"Data structures for graphs, based on C-sets.\n\nProvides the category theorist's four basic kinds of graphs: graphs (aka directed multigraphs), symmetric graphs, reflexive graphs, and symmetric reflexive graphs. Also defines half-edge graphs. The API generally follows that of LightGraphs.jl, with some departures due to differences between the data structures.\n\n\n\n\n\n","category":"module"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.AbstractGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.AbstractGraph","text":"Abstract type for graphs, aka directed multigraphs.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.AbstractHalfEdgeGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.AbstractHalfEdgeGraph","text":"Abstract type for half-edge graphs, possibly with data attributes.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.AbstractReflexiveGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.AbstractReflexiveGraph","text":"Abstract type for reflexive graphs, possibly with data attributes.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.AbstractSymmetricGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.AbstractSymmetricGraph","text":"Abstract type for symmetric graph, possibly with data attributes.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.AbstractSymmetricReflexiveGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.AbstractSymmetricReflexiveGraph","text":"Abstract type for symmetric reflexive graphs, possibly with data attributes.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.AbstractSymmetricWeightedGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.AbstractSymmetricWeightedGraph","text":"Abstract type for symmetric weights graphs.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.AbstractWeightedGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.AbstractWeightedGraph","text":"Abstract type for weighted graphs.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.HasGraph","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.HasGraph","text":"Abstract type for C-sets that contain a graph.\n\nThis type encompasses C-sets where the schema for graphs is a subcategory of C. This includes, for example, graphs, symmetric graphs, and reflexive graphs, but not half-edge graphs.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.HasVertices","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.HasVertices","text":"Abstract type for C-sets that contain vertices.\n\nThis type encompasses C-sets where the schema C contains an object V interpreted as vertices. This includes, for example, graphs and half-edge graphs, but not bipartite graphs or wiring diagrams.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Base.inv-Tuple{AbstractHalfEdgeGraph, Vararg{Any, N} where N}","page":"Graphs","title":"Base.inv","text":"Involution on half-edge(s) in a half-edge graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Base.inv-Tuple{HasGraph, Vararg{Any, N} where N}","page":"Graphs","title":"Base.inv","text":"Involution on edge(s) in a symmetric graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.add_dangling_edge!-Tuple{AbstractHalfEdgeGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.add_dangling_edge!","text":"Add a dangling edge to a half-edge graph.\n\nA \"dangling edge\" is a half-edge that is paired with itself under the half-edge involution. They are usually interpreted differently than \"self-loops\", i.e., a pair of distinct half-edges incident to the same vertex.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.add_dangling_edges!-Tuple{AbstractHalfEdgeGraph, AbstractVector{Int64}}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.add_dangling_edges!","text":"Add multiple dangling edges to a half-edge graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.add_edge!-Tuple{HasGraph, Int64, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.add_edge!","text":"Add an edge to a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.add_edges!-Tuple{HasGraph, AbstractVector{Int64}, AbstractVector{Int64}}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.add_edges!","text":"Add multiple edges to a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.add_vertex!-Tuple{HasVertices}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.add_vertex!","text":"Add a vertex to a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.add_vertices!-Tuple{HasVertices, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.add_vertices!","text":"Add multiple vertices to a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.all_neighbors-Tuple{AbstractGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.all_neighbors","text":"Union of in-neighbors and out-neighbors in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.edges-Tuple{HasGraph}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.edges","text":"Edges in a graph, or between two vertices in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.half_edges-Tuple{AbstractHalfEdgeGraph}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.half_edges","text":"Half-edges in a half-edge graph, or incident to a vertex.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.has_edge-Tuple{HasGraph, Any}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.has_edge","text":"Whether the graph has the given edge, or an edge between two vertices.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.has_vertex-Tuple{HasVertices, Any}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.has_vertex","text":"Whether the graph has the given vertex.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.induced_subgraph-Union{Tuple{G}, Tuple{G, AbstractVector{Int64}}} where G<:ACSet","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.induced_subgraph","text":"Subgraph induced by a set of a vertices.\n\nThe induced subgraph consists of the given vertices and all edges between vertices in this set.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.inneighbors-Tuple{AbstractGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.inneighbors","text":"In-neighbors of vertex in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.ne-Tuple{HasGraph}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.ne","text":"Number of edges in a graph, or between two vertices in a graph.\n\nIn a symmetric graph, this function counts both edges in each edge pair, so that the number of edges in a symmetric graph is twice the number of edges in the corresponding undirected graph (at least when the edge involution has no fixed points).\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.neighbors-Tuple{AbstractGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.neighbors","text":"Neighbors of vertex in a graph.\n\nIn a graph, this function is an alias for outneighbors; in a symmetric graph, a vertex has the same out-neighbors and as in-neighbors, so the distinction is moot.\n\nIn the presence of multiple edges, neighboring vertices are given with multiplicity. To get the unique neighbors, call unique(neighbors(g)).\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.nv-Tuple{HasVertices}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.nv","text":"Number of vertices in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.outneighbors-Tuple{AbstractGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.outneighbors","text":"Out-neighbors of vertex in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.refl-Tuple{HasGraph, Vararg{Any, N} where N}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.refl","text":"Reflexive loop(s) of vertex (vertices) in a reflexive graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.rem_edge!-Tuple{HasGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.rem_edge!","text":"Remove an edge from a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.rem_edges!-Tuple{HasGraph, Any}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.rem_edges!","text":"Remove multiple edges from a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.rem_vertex!-Tuple{HasVertices, Int64}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.rem_vertex!","text":"Remove a vertex from a graph.\n\nWhen keep_edges is false (the default), all edges incident to the vertex are also deleted. When keep_edges is true, incident edges are preserved but their source/target vertices become undefined.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.rem_vertices!-Tuple{AbstractGraph, Any}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.rem_vertices!","text":"Remove multiple vertices from a graph.\n\nEdges incident to any of the vertices are treated as in rem_vertex!.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.src-Tuple{HasGraph, Vararg{Any, N} where N}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.src","text":"Source vertex (vertices) of edges(s) in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.tgt-Tuple{HasGraph, Vararg{Any, N} where N}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.tgt","text":"Target vertex (vertices) of edges(s) in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.vertex-Tuple{AbstractHalfEdgeGraph, Vararg{Any, N} where N}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.vertex","text":"Incident vertex (vertices) of half-edge(s) in a half-edge graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.vertices-Tuple{HasVertices}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.vertices","text":"Vertices in a graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.BasicGraphs.weight-Tuple{HasGraph, Vararg{Any, N} where N}","page":"Graphs","title":"Catlab.Graphs.BasicGraphs.weight","text":"Weight(s) of edge(s) in a weighted graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.AbstractPropertyGraph","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.AbstractPropertyGraph","text":"Abstract type for graph with properties.\n\nConcrete types are PropertyGraph and SymmetricPropertyGraph.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.PropertyGraph","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.PropertyGraph","text":"Graph with properties.\n\n\"Property graphs\" are graphs with arbitrary named properties on the graph, vertices, and edges. They are intended for applications with a large number of ad-hoc properties. If you have a small number of known properties, it is better and more efficient to create a specialized C-set type using CSetType.\n\nSee also: SymmetricPropertyGraph.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.SymmetricPropertyGraph","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.SymmetricPropertyGraph","text":"Symmetric graphs with properties.\n\nThe edge properties are preserved under the edge involution, so these can be interpreted as \"undirected\" property (multi)graphs.\n\nSee also: PropertyGraph.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.eprops-Tuple{AbstractPropertyGraph, Any}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.eprops","text":"Properties of edge in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.get_eprop-Tuple{AbstractPropertyGraph, Any, Symbol}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.get_eprop","text":"Get property of edge or edges in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.get_gprop-Tuple{AbstractPropertyGraph, Symbol}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.get_gprop","text":"Get graph-level property of a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.get_vprop-Tuple{AbstractPropertyGraph, Any, Symbol}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.get_vprop","text":"Get property of vertex or vertices in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.gprops-Tuple{AbstractPropertyGraph}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.gprops","text":"Graph-level properties of a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.set_eprop!-Tuple{AbstractPropertyGraph, Any, Symbol, Any}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.set_eprop!","text":"Set property of edge or edges in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.set_eprops!-Tuple{AbstractPropertyGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.set_eprops!","text":"Set multiple properties of an edge in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.set_gprop!-Tuple{AbstractPropertyGraph, Symbol, Any}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.set_gprop!","text":"Set graph-level property in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.set_gprops!-Tuple{AbstractPropertyGraph}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.set_gprops!","text":"Set multiple graph-level properties in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.set_vprop!-Tuple{AbstractPropertyGraph, Any, Symbol, Any}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.set_vprop!","text":"Set property of vertex or vertices in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.set_vprops!-Tuple{AbstractPropertyGraph, Int64}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.set_vprops!","text":"Set multiple properties of a vertex in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.PropertyGraphs.vprops-Tuple{AbstractPropertyGraph, Any}","page":"Graphs","title":"Catlab.Graphs.PropertyGraphs.vprops","text":"Properties of vertex in a property graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.GraphAlgorithms","page":"Graphs","title":"Catlab.Graphs.GraphAlgorithms","text":"Algorithms on graphs based on C-sets.\n\n\n\n\n\n","category":"module"},{"location":"apis/graphs/#Catlab.Graphs.GraphAlgorithms.connected_component_projection","page":"Graphs","title":"Catlab.Graphs.GraphAlgorithms.connected_component_projection","text":"Projection onto (weakly) connected components of a graph.\n\nReturns a function in FinSet{Int} from the vertex set to the set of components.\n\n\n\n\n\n","category":"function"},{"location":"apis/graphs/#Catlab.Graphs.GraphAlgorithms.connected_components-Tuple{ACSet}","page":"Graphs","title":"Catlab.Graphs.GraphAlgorithms.connected_components","text":"(Weakly) connected components of a graph.\n\nReturns a vector of vectors, which are the components of the graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.GraphAlgorithms.topological_sort-Tuple{ACSet}","page":"Graphs","title":"Catlab.Graphs.GraphAlgorithms.topological_sort","text":"Topological sort of a directed acyclic graph.\n\nThe depth-first search algorithm is adapted from the function topological_sort_by_dfs in LightGraphs.jl.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphs/#Catlab.Graphs.GraphAlgorithms.transitive_reduction!-Tuple{ACSet}","page":"Graphs","title":"Catlab.Graphs.GraphAlgorithms.transitive_reduction!","text":"Transitive reduction of a DAG.\n\nThe algorithm computes the longest paths in the DAGs and keeps only the edges corresponding to longest paths of length 1. Requires a topological sort, which is computed if it is not supplied.\n\n\n\n\n\n","category":"method"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/sketches/partitions.jl\"","category":"page"},{"location":"generated/sketches/partitions/#Partitions","page":"Partitions","title":"Partitions","text":"","category":"section"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"(Image: )","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"Partitions are a categorical construction that we derive from sets and functions. Given a set A, you can think of all of the ways to partition A into parts. These ways of partitioning are isomorphic to equivalence relations R ⊆ A × A.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"The first step is our Catlab imports","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"using Core: GeneratedFunctionStub\nusing Test\n\nusing Catlab, Catlab.Theories, Catlab.CategoricalAlgebra, Catlab.CategoricalAlgebra.FinSets\nimport Catlab.Theories: compose\nusing DataStructures\nusing PrettyTables\nPrettyTables.pretty_table(f::FinFunction, name::Symbol=:f) = pretty_table(OrderedDict(:x=>1:dom(f).set, Symbol(\"$(name)(x)\")=>collect(f)))\nusing LaTeXStrings\n\nQuiversty = L\"\"\"\n% contents of quiver.sty\n% `tikz-cd` is necessary to draw commutative diagrams.\n\\RequirePackage{tikz-cd}\n% `amssymb` is necessary for `\\lrcorner` and `\\ulcorner`.\n\\RequirePackage{amssymb}\n% `calc` is necessary to draw curved arrows.\n\\usetikzlibrary{calc}\n% `pathmorphing` is necessary to draw squiggly arrows.\n\\usetikzlibrary{decorations.pathmorphing}\n\n% A TikZ style for curved arrows of a fixed height, due to AndréC.\n\\tikzset{curve/.style={settings={#1},to path={(\\tikztostart)\n .. controls ($(\\tikztostart)!\\pv{pos}!(\\tikztotarget)!\\pv{height}!270:(\\tikztotarget)$)\n and ($(\\tikztostart)!1-\\pv{pos}!(\\tikztotarget)!\\pv{height}!270:(\\tikztotarget)$)\n .. (\\tikztotarget)\\tikztonodes}},\n settings/.code={\\tikzset{quiver/.cd,#1}\n \\def\\pv##1{\\pgfkeysvalueof{/tikz/quiver/##1}}},\n quiver/.cd,pos/.initial=0.35,height/.initial=0}\n\n% TikZ arrowhead/tail styles.\n\\tikzset{tail reversed/.code={\\pgfsetarrowsstart{tikzcd to}}}\n\\tikzset{2tail/.code={\\pgfsetarrowsstart{Implies[reversed]}}}\n\\tikzset{2tail reversed/.code={\\pgfsetarrowsstart{Implies}}}\n% TikZ arrow styles.\n\\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}\n\"\"\";\nnothing #hide","category":"page"},{"location":"generated/sketches/partitions/#FinSet:-the-category-of-Finite-Sets","page":"Partitions","title":"FinSet: the category of Finite Sets","text":"","category":"section"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"In FinSet the objects are sets n = {1...n} and the morphisms are functions between finite sets. You can wrap a plain old Int into a finite set with the FinSet(n::Int) function. These sets will serve as the domain and codomains of our functions.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"n = FinSet(3)\nm = FinSet(4)","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"once you have some sets, you can define functions between them. A FinFunction from n to m, f:n→m, can be specified as an array of length n with elements from m.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"f = FinFunction([2,4,3], n, m)\n\npretty_table(f)","category":"page"},{"location":"generated/sketches/partitions/#Surjective-maps","page":"Partitions","title":"Surjective maps","text":"","category":"section"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"In order to use a map to represent a partition, we have to make sure that it is surjective. Given a FinFunction, we can compute the preimage of any element in its codomain.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"preimage(f, 2)\n\npreimage(f, 1)","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"If the preimage is empty, then there is no element in the domain that maps to that element of the codomain. This gives us a definition of surjective functions by asserting that all the preimages are nonempty. Julia note: !p is the predicate x ↦ ¬p(x), f.(A) applies f to all of the elements in A.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"is_surjective(f::FinFunction) = all((!isempty).(preimage(f,i) for i in codom(f)))\nis_surjective(f)","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"Our function f, wasn't surjective so it can't be used to induce a partition via its preimages. Let's try again,","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"g = FinFunction([1,2,3,3], m, n)\npretty_table(g, :g)\nis_surjective(g)","category":"page"},{"location":"generated/sketches/partitions/#Refinements-of-a-Partition","page":"Partitions","title":"Refinements of a Partition","text":"","category":"section"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"When defining partitions classically as A = ∪ₚ Aₚ with p ≠ r ⟹ Aₚ ≠ Aᵣ, it is not immediately obvious how to define comparisons between partitions. With the \"a partition of A is a surjective map out of A\" definition, the comparisons are obvious. The composition of surjective maps is surjective, so we can define the refinement order in terms of a diagram in Set.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"You can see a graphical definition in quiver","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"using TikzCDs\n\ntriangle = L\"\"\"\nA &&& Q \\\\\n\\\\\n&&& P\n\\arrow[\"h\", two heads, from=1-4, to=3-4]\n\\arrow[\"f\", two heads, from=1-1, to=1-4]\n\\arrow[\"g\"', two heads, from=1-1, to=3-4]\n\"\"\";\n\nTikzCD(triangle, preamble=Quiversty)","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"Let's take a look at an example:","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"A = FinSet(4)\nQ = FinSet(3)\nP = FinSet(2)\n\nf = FinFunction([1,2,3,3], A, Q)\ng = FinFunction([1,1,2,2], A, P)\nh = FinFunction([1,1,2], Q, P)\n\n@test_throws ErrorException compose(g,h) #Catlab checks the domains match\n\npretty_table(compose(f,h), Symbol(\"(f⋅h)\"))\n\ncompose(f,h) == g","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"This triangle commutes, so f is a refinement of g equivalently g is coarser than f.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"h′ = FinFunction([1,1], P, FinSet(1))\n\npretty_table(f⋅h⋅h′, Symbol(\"f⋅h⋅h′\"))","category":"page"},{"location":"generated/sketches/partitions/#Properties-of-refinements","page":"Partitions","title":"Properties of refinements","text":"","category":"section"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"We can show that refinement gives us a preorder on partitions directly from the nice properties of surjective maps.","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"Reflexive: Any partition is a refinement of itself.\nTransitive: If f ≤ g ≤ h as partitions, then f ≤ h","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"You can read these directly off the definition of refinements as a commutative triangle in the category of (Set, Surjections). You can edit this diagram in quiver","category":"page"},{"location":"generated/sketches/partitions/","page":"Partitions","title":"Partitions","text":"refinement = L\"\"\"\nA &&& Q \\\\\n\\\\\n&&& P \\\\\n\\\\\n&&& {Q^\\prime}\n\\arrow[\"h\", from=1-4, to=3-4]\n\\arrow[\"f\", two heads, from=1-1, to=1-4]\n\\arrow[\"g\"', two heads, from=1-1, to=3-4]\n\\arrow[\"{h^\\prime}\", from=3-4, to=5-4]\n\\arrow[\"{f\\cdot h\\cdot h^\\prime = g\\cdot h^\\prime}\"', two heads, from=1-1, to=5-4]\n\"\"\";\n\nTikzCD(refinement, preamble=Quiversty)","category":"page"},{"location":"apis/theories/#Standard-library-of-theories","page":"Standard library of theories","title":"Standard library of theories","text":"","category":"section"},{"location":"apis/theories/","page":"Standard library of theories","title":"Standard library of theories","text":"Through the module Catlab.Theories, Catlab provides a standard library of generalized algebraic theories for categories, monoidal categories, and other categorical structures. The theories correspond, in most cases, to standard definitions in category theory and they are used throughout Catlab and the AlgebraicJulia ecosystem to structure programs and provide a common interface for applied category theory. The module also provides default syntax systems for many of the theories.","category":"page"},{"location":"apis/theories/","page":"Standard library of theories","title":"Standard library of theories","text":"Categorical structures for which theories are provided include:","category":"page"},{"location":"apis/theories/","page":"Standard library of theories","title":"Standard library of theories","text":"categories\nmonoidal and symmetric monoidal categories\ncartesian and cocartesian categories\nsemiadditive categories/biproduct categories\nhypergraph categories\nbicategories of relations\ncategories with two monoidal products, such as distributive monoidal categories","category":"page"},{"location":"apis/theories/","page":"Standard library of theories","title":"Standard library of theories","text":"The contents of this module can be supplemented by the user, and it is even possible to use many parts of Catlab without using this module. The user is free to create new syntax systems for the theories defined here and also to define entirely new theories.","category":"page"},{"location":"apis/theories/","page":"Standard library of theories","title":"Standard library of theories","text":"Modules = [ Theories ]\nPrivate = false","category":"page"},{"location":"apis/theories/#Catlab.Theories","page":"Standard library of theories","title":"Catlab.Theories","text":"Catlab's standard library of generalized algebraic theories.\n\nThe focus is on categories and monoidal categories, but other related structures are also included.\n\n\n\n\n\n","category":"module"},{"location":"apis/theories/#Catlab.Theories.AbelianBicategoryRelations","page":"Standard library of theories","title":"Catlab.Theories.AbelianBicategoryRelations","text":"Theory of abelian bicategories of relations\n\nUnlike BicategoryRelations, this theory uses additive notation.\n\nReferences:\n\nCarboni & Walters, 1987, \"Cartesian bicategories I\", Sec. 5\nBaez & Erbele, 2015, \"Categories in control\"\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.AdditiveCategory","page":"Standard library of theories","title":"Catlab.Theories.AdditiveCategory","text":"Theory of additive categories\n\nAn additive category is a biproduct category enriched in abelian groups. Thus, it is a semiadditive category where the hom-monoids have negatives.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.AlgebraicLattice","page":"Standard library of theories","title":"Catlab.Theories.AlgebraicLattice","text":"Theory of lattices as algebraic structures\n\nThis is one of two standard axiomatizations of a lattice, the other being Lattice. Because the partial order is not present, this theory is merely an algebraic theory (no dependent types).\n\nThe partial order is recovered as A B iff A B = A iff A B = B. This definition could be reintroduced into a generalized algebraic theory using an equality type Eq(lhs::El, rhs::El)::TYPE combined with term constructors `meet_leq(eq::Eq(A∧B, A))::(A ≤ B) and join_leq(eq::Eq(A∨B, B))::(A ≤ B). We do not employ that trick here because at that point it is more convenient to just start with the poset structure, as in Lattice.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.BicategoryRelations","page":"Standard library of theories","title":"Catlab.Theories.BicategoryRelations","text":"Theory of bicategories of relations\n\nTODO: The 2-morphisms are missing.\n\nReferences:\n\nCarboni & Walters, 1987, \"Cartesian bicategories I\"\nWalters, 2009, blog post, \"Categorical algebras of relations\", http://rfcwalters.blogspot.com/2009/10/categorical-algebras-of-relations.html\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.BiproductCategory","page":"Standard library of theories","title":"Catlab.Theories.BiproductCategory","text":"Theory of biproduct categories\n\nMathematically the same as SemiadditiveCategory but written multiplicatively, instead of additively.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CartesianCategory","page":"Standard library of theories","title":"Catlab.Theories.CartesianCategory","text":"Theory of cartesian (monoidal) categories\n\nFor the traditional axiomatization of products, see CategoryWithProducts.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CartesianClosedCategory","page":"Standard library of theories","title":"Catlab.Theories.CartesianClosedCategory","text":"Theory of cartesian closed categories, aka CCCs\n\nA CCC is a cartesian category with internal homs (aka, exponential objects).\n\nFIXME: This theory should also extend ClosedMonoidalCategory, but multiple inheritance is not yet supported.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Category","page":"Standard library of theories","title":"Catlab.Theories.Category","text":"Theory of categories (with no extra structure)\n\nWarning: We compose functions from left to right, i.e., if f:A→B and g:B→C then compose(f,g):A→C. Under this convention function are applied on the right, e.g., if a∈A then af∈B.\n\nWe retain the usual meaning of the symbol ∘ (\\circ), i.e., g∘f = compose(f,g). This usage is too entrenched to overturn, inconvenient though it may be. We use symbol ⋅ (\\cdot) for diagrammatic composition: f⋅g = compose(f,g).\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Category2","page":"Standard library of theories","title":"Catlab.Theories.Category2","text":"Theory of (strict) 2-categories\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CategoryWithCoproducts","page":"Standard library of theories","title":"Catlab.Theories.CategoryWithCoproducts","text":"Theory of a category with (finite) coproducts\n\nFinite coproducts are presented in biased style, via the nullary case (initial objects) and the binary case (binary coproducts). The axioms are dual to those of CategoryWithProducts.\n\nFor a monoidal category axiomatization, see CocartesianCategory.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CategoryWithProducts","page":"Standard library of theories","title":"Catlab.Theories.CategoryWithProducts","text":"Theory of a category with (finite) products\n\nFinite products are presented in biased style, via the nullary case (terminal objects) and the binary case (binary products). The equational axioms are standard, especially in type theory (Lambek & Scott, 1986, Section 0.5 or Section I.3). Strictly speaking, this theory is not of a \"category with finite products\" (a category in which finite products exist) but of a \"category with chosen finite products\".\n\nFor a monoidal category axiomatization, see CartesianCategory.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.ClosedMonoidalCategory","page":"Standard library of theories","title":"Catlab.Theories.ClosedMonoidalCategory","text":"Theory of (symmetric) closed monoidal categories\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CocartesianCategory","page":"Standard library of theories","title":"Catlab.Theories.CocartesianCategory","text":"Theory of cocartesian (monoidal) categories\n\nFor the traditional axiomatization of coproducts, see CategoryWithCoproducts.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CocompleteCategory","page":"Standard library of theories","title":"Catlab.Theories.CocompleteCategory","text":"Theory of a (finitely) cocomplete category\n\nFinite colimits are presented in biased style, via finite coproducts and coequalizers. The axioms are dual to those of CompleteCategory.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CompactClosedCategory","page":"Standard library of theories","title":"Catlab.Theories.CompactClosedCategory","text":"Theory of compact closed categories\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.CompleteCategory","page":"Standard library of theories","title":"Catlab.Theories.CompleteCategory","text":"Theory of a (finitely) complete category\n\nFinite limits are presented in biased style, via finite products and equalizers. The equational axioms for equalizers are obscure, but can found in (Lambek & Scott, 1986, Section 0.5), which follow \"Burroni's pioneering ideas\". Strictly speaking, this theory is not of a \"finitely complete category\" (a category in which finite limits exist) but of a \"category with chosen finite limits\".\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Copresheaf","page":"Standard library of theories","title":"Catlab.Theories.Copresheaf","text":"Theory of copresheaves.\n\nAxiomatized as a covariant category action.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DaggerCategory","page":"Standard library of theories","title":"Catlab.Theories.DaggerCategory","text":"Theory of dagger categories\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DaggerCompactCategory","page":"Standard library of theories","title":"Catlab.Theories.DaggerCompactCategory","text":"Theory of dagger compact categories\n\nIn a dagger compact category, there are two kinds of adjoints of a morphism f::Hom(A,B), the adjoint mate mate(f)::Hom(dual(B),dual(A)) and the dagger adjoint dagger(f)::Hom(B,A). In the category of Hilbert spaces, these are respectively the Banach space adjoint and the Hilbert space adjoint (Reed-Simon, Vol I, Sec VI.2). In Julia, they would correspond to transpose and adjoint in the official LinearAlegbra module. For the general relationship between mates and daggers, see Selinger's survey of graphical languages for monoidal categories.\n\nFIXME: This theory should also extend DaggerCategory, but multiple inheritance is not yet supported.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DaggerSymmetricMonoidalCategory","page":"Standard library of theories","title":"Catlab.Theories.DaggerSymmetricMonoidalCategory","text":"Theory of dagger symmetric monoidal categories\n\nAlso known as a symmetric monoidal dagger category.\n\nFIXME: This theory should also extend DaggerCategory, but multiple inheritance is not yet supported.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DisplayedCategory","page":"Standard library of theories","title":"Catlab.Theories.DisplayedCategory","text":"Theory of a displayed category.\n\nMore precisely, this is the theory of a base category C (Ob,Hom) and a displayed category (El,Act) over C. Displayed categories axiomatize lax functors C **Span** or equivalently objects in **Cat**C in a pleasant, generalized algebraic style.\n\nReference: Ahrens & Lumsdaine 2019, \"Displayed categories\", Definition 3.1.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DistributiveBicategoryRelations","page":"Standard library of theories","title":"Catlab.Theories.DistributiveBicategoryRelations","text":"Theory of a distributive bicategory of relations\n\nReferences:\n\nCarboni & Walters, 1987, \"Cartesian bicategories I\", Remark 3.7 (mention in passing only)\nPatterson, 2017, \"Knowledge representation in bicategories of relations\", Section 9.2\n\nFIXME: Should also inherit BicategoryOfRelations, but multiple inheritance is not yet supported.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DistributiveCategory","page":"Standard library of theories","title":"Catlab.Theories.DistributiveCategory","text":"Theory of a distributive category\n\nA distributive category is a distributive monoidal category whose tensor product is the cartesian product, see DistributiveMonoidalCategory.\n\nFIXME: Should also inherit CartesianCategory.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DistributiveMonoidalCategory","page":"Standard library of theories","title":"Catlab.Theories.DistributiveMonoidalCategory","text":"Theory of a distributive (symmetric) monoidal category\n\nReference: Jay, 1992, LFCS tech report LFCS-92-205, \"Tail recursion through universal invariants\", Section 3.2\n\nFIXME: Should also inherit CocartesianCategory.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DistributiveSemiadditiveCategory","page":"Standard library of theories","title":"Catlab.Theories.DistributiveSemiadditiveCategory","text":"Theory of a distributive semiadditive category\n\nThis terminology is not standard but the concept occurs frequently. A distributive semiadditive category is a semiadditive category (or biproduct) category, written additively, with a tensor product that distributes over the biproduct.\n\nFIXME: Should also inherit SemiadditiveCategory\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.DoubleCategory","page":"Standard library of theories","title":"Catlab.Theories.DoubleCategory","text":"Theory of (strict) double categories\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.HypergraphCategory","page":"Standard library of theories","title":"Catlab.Theories.HypergraphCategory","text":"Theory of hypergraph categories\n\nHypergraph categories are also known as \"well-supported compact closed categories\" and \"spidered/dungeon categories\", among other things.\n\nFIXME: Should also inherit ClosedMonoidalCategory and DaggerCategory, but multiple inheritance is not yet supported.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.HypergraphCategoryAdditive","page":"Standard library of theories","title":"Catlab.Theories.HypergraphCategoryAdditive","text":"Theory of hypergraph categories, in additive notation\n\nMathematically the same as HypergraphCategory but with different notation.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Lattice","page":"Standard library of theories","title":"Catlab.Theories.Lattice","text":"Theory of lattices as posets\n\nA (bounded) lattice is a poset with all finite meets and joins. Viewed as a thin category, this means that the category has all finite products and coproducts, hence the names for the inequality constructors in the theory. Compare with CartesianCategory and CocartesianCategory.\n\nThis is one of two standard axiomatizations of a lattice, the other being AlgebraicLattice.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.MonoidalCategory","page":"Standard library of theories","title":"Catlab.Theories.MonoidalCategory","text":"Theory of monoidal categories\n\nTo avoid associators and unitors, we assume the monoidal category is strict. By the coherence theorem there is no loss of generality, but we may add a theory for weak monoidal categories later.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.MonoidalCategoryAdditive","page":"Standard library of theories","title":"Catlab.Theories.MonoidalCategoryAdditive","text":"Theory of monoidal categories, in additive notation\n\nMathematically the same as MonoidalCategory but with different notation.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.MonoidalCategoryWithBidiagonals","page":"Standard library of theories","title":"Catlab.Theories.MonoidalCategoryWithBidiagonals","text":"Theory of monoidal categories with bidiagonals\n\nThe terminology is nonstandard (is there any standard terminology?) but is supposed to mean a monoidal category with coherent diagonals and codiagonals. Unlike in a biproduct category, the naturality axioms need not be satisfied.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.MonoidalCategoryWithBidiagonalsAdditive","page":"Standard library of theories","title":"Catlab.Theories.MonoidalCategoryWithBidiagonalsAdditive","text":"Theory of monoidal categories with bidiagonals, in additive notation\n\nMathematically the same as MonoidalCategoryWithBidiagonals but written additively, instead of multiplicatively.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.MonoidalCategoryWithCodiagonals","page":"Standard library of theories","title":"Catlab.Theories.MonoidalCategoryWithCodiagonals","text":"Theory of monoidal categories with codiagonals\n\nA monoidal category with codiagonals is a symmetric monoidal category equipped with coherent collections of merging and creating morphisms (monoids). Unlike in a cocartesian category, the naturality axioms need not be satisfied.\n\nFor references, see MonoidalCategoryWithDiagonals.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.MonoidalCategoryWithDiagonals","page":"Standard library of theories","title":"Catlab.Theories.MonoidalCategoryWithDiagonals","text":"Theory of monoidal categories with diagonals\n\nA monoidal category with diagonals is a symmetric monoidal category equipped with coherent operations of copying and deleting, also known as a supply of commutative comonoids. Unlike in a cartesian category, the naturality axioms need not be satisfied.\n\nReferences:\n\nFong & Spivak, 2019, \"Supplying bells and whistles in symmetric monoidal categories\" (arxiv:1908.02633)\nSelinger, 2010, \"A survey of graphical languages for monoidal categories\", Section 6.6: \"Cartesian center\"\nSelinger, 1999, \"Categorical structure of asynchrony\"\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.MonoidalDoubleCategory","page":"Standard library of theories","title":"Catlab.Theories.MonoidalDoubleCategory","text":"Theory of monoidal double categories\n\nTo avoid associators and unitors, we assume the monoidal double category is strict in both the horizontal and vertical directions. Apart from assuming strictness, this theory follows the definition of a monoidal double category in (Shulman, 2010, Constructing symmetric monoidal bicategories) and other recent papers, starting from an internal category (S,T: D₁ ⇉ D₀, U: D₀ → D₁, ⋆: D₁ ×_{D₀} D₁ → D₁) in Cat where\n\nthe objects of D₀ are objects\nthe morphisms of D₀ are vertical 1-cells\nthe objects of D₁ are horizontal 1-cells\nthe morphisms of D₁ are 2-cells.\n\nThe top and bottom of a 2-cell are given by domain and codomain in D₁ and the left and right are given by the functors S,T. In a monoidal double category, D₀ and D₁ are each required to be monoidal categories, subject to further axioms such as S and T being strict monoidal functors.\n\nDespite the apparent asymmetry in this setup, the definition of a monoidal double category unpacks to be nearly symmetric with respect to horizontal and vertical, except that the monoidal unit I of D₀ induces the monoidal unit of D₁ as U(I), which I think has no analogue in the vertical direction.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Poset","page":"Standard library of theories","title":"Catlab.Theories.Poset","text":"Theory of partial orders (posets)\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Preorder","page":"Standard library of theories","title":"Catlab.Theories.Preorder","text":"Theory of preorders\n\nThe generalized algebraic theory of preorders encodes inequalities AB as dependent types `Leq(AB) and the axioms of reflexivity and transitivity as term constructors.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Presheaf","page":"Standard library of theories","title":"Catlab.Theories.Presheaf","text":"Theory of presheaves.\n\nAxiomatized as a contravariant category action.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.RigCategory","page":"Standard library of theories","title":"Catlab.Theories.RigCategory","text":"Theory of a rig category, also known as a bimonoidal category\n\nRig categories are the most general in the hierarchy of distributive monoidal structures.\n\nTODO: Do we also want the distributivty and absorption isomorphisms? Usually we ignore coherence isomorphisms such as associators and unitors.\n\nFIXME: This theory should also inherit MonoidalCategory, but multiple inheritance is not supported.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.Schema","page":"Standard library of theories","title":"Catlab.Theories.Schema","text":"The GAT that parameterizes Attributed C-sets A schema is comprised of a category C, a discrete category D, and a profunctor Attr : C^op x D → Set. In GAT form, this is given by extending the theory of categories with two extra types, AttrType for objects of D, and Attr, for elements of the sets given by the profunctor.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.SemiadditiveCategory","page":"Standard library of theories","title":"Catlab.Theories.SemiadditiveCategory","text":"Theory of semiadditive categories\n\nMathematically the same as BiproductCategory but written additively, instead of multiplicatively.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.SymmetricMonoidalCategory","page":"Standard library of theories","title":"Catlab.Theories.SymmetricMonoidalCategory","text":"Theory of (strict) symmetric monoidal categories\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.SymmetricMonoidalCategoryAdditive","page":"Standard library of theories","title":"Catlab.Theories.SymmetricMonoidalCategoryAdditive","text":"Theory of symmetric monoidal categories, in additive notation\n\nMathematically the same as SymmetricMonoidalCategory but with different notation.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.SymmetricMonoidalCopresheaf","page":"Standard library of theories","title":"Catlab.Theories.SymmetricMonoidalCopresheaf","text":"Theory of a symmetric monoidal copresheaf\n\nThe name is not standard but refers to a lax symmetric monoidal functor into Set. This can be interpreted as an action of a symmetric monoidal category, just as a copresheaf (set-valued functor) is an action of a category. The theory is simpler than that of a general lax monoidal functor because (1) the domain is a strict monoidal category and (2) the codomain is fixed to the cartesian monoidal category Set.\n\nFIXME: This theory should also extend Copresheaf but multiple inheritance is not yet supported.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.SymmetricMonoidalDoubleCategory","page":"Standard library of theories","title":"Catlab.Theories.SymmetricMonoidalDoubleCategory","text":"Theory of (strict) symmetric monoidal double categories\n\nUnlike classical double categories, symmetric monoidal double categories do not treat the vertical and horizontal directions on an equal footing, even in the strict case. See MonoidalDoubleCategory for details and references.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.SymmetricRigCategory","page":"Standard library of theories","title":"Catlab.Theories.SymmetricRigCategory","text":"Theory of a symmetric rig category\n\nFIXME: Should also inherit SymmetricMonoidalCategory.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.ThinCategory","page":"Standard library of theories","title":"Catlab.Theories.ThinCategory","text":"Theory of thin categories\n\nThin categories have at most one morphism between any two objects and are isomorphic to preorders.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.ThinSymmetricMonoidalCategory","page":"Standard library of theories","title":"Catlab.Theories.ThinSymmetricMonoidalCategory","text":"Theory of thin symmetric monoidal category\n\nThin SMCs are isomorphic to commutative monoidal prosets.\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Catlab.Theories.TracedMonoidalCategory","page":"Standard library of theories","title":"Catlab.Theories.TracedMonoidalCategory","text":"Theory of traced monoidal categories\n\n\n\n\n\n","category":"type"},{"location":"apis/theories/#Base.collect-Tuple{ObExpr}","page":"Standard library of theories","title":"Base.collect","text":"Collect generators of object in monoidal category as a vector.\n\n\n\n\n\n","category":"method"},{"location":"apis/theories/#Base.ndims-Tuple{ObExpr}","page":"Standard library of theories","title":"Base.ndims","text":"Number of \"dimensions\" of object in monoidal category.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Theories,-instances,-and-expressions","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"","category":"section"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"At the core of Catlab is a system for defining generalized algebraic structures, such as categories and monoidal categories, and then creating instances of these structures in Julia code. The objects, morphisms, and even higher-order morphisms can also be represented as typed symbolic expressions, as in a computer algebra system. These expressions can be manipulated abstractly or transformed into more concrete representations, such as wiring diagrams or Julia functions.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"The basic elements of this system are:","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Generalized algebraic theories (GATs), defined using the @theory macro. Categories and other typed (multisorted) algebraic structures can be defined as GATs. Alternatively, the @signature macro can be used when only the signature (not the axioms) of the GAT are to be specified.\nInstances, or concrete implementations, of theories, defined using the @instance macro.\nSyntax systems for theories, defined using the @syntax macro. These are type-safe expression trees constructed using ordinary Julia functions.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"We'll explain each of these elements in greater detail in the following sections. From the programming perspective, theories can be thought of as interfaces and bear some resemblance to type classes in languages like Haskell. Both instances and syntax systems can then be thought of as implementations of the interface.","category":"page"},{"location":"apis/core/#gats","page":"Theories, instances, and expressions","title":"Theories","text":"","category":"section"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Generalized algebraic theories (GATs) are the natural logical system in which to define categories and related algebraic structures. GATs generalize the typed (multisorted) algebraic theories of universal algebra by incorporating a fragment of dependent type theory; they are perhaps the simplest dependently typed logics.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Catlab implements a version of the GAT formalism on top of Julia's type system, taking advantage of Julia macros to provide a pleasant syntax. GATs are defined using the @theory macro.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"For example, the theory of categories could be defined by:","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"using Catlab\nimport Catlab.Theories: Ob, Hom, ObExpr, HomExpr, dom, codom, compose, ⋅, id","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"@theory Category{Ob,Hom} begin\n @op begin\n (→) := Hom\n (⋅) := compose\n end\n\n Ob::TYPE\n Hom(dom::Ob, codom::Ob)::TYPE\n\n id(A::Ob)::(A → A)\n compose(f::(A → B), g::(B → C))::(A → C) ⊣ (A::Ob, B::Ob, C::Ob)\n\n (f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ (A::Ob, B::Ob, C::Ob, D::Ob,\n f::(A → B), g::(B → C), h::(C → D))\n f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B))\n id(A) ⋅ f == f ⊣ (A::Ob, B::Ob, f::(A → B))\nend\nnothing # hide","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"The code is simplified only slightly from the official Catlab definition of Category. The theory has two type constructors, Ob (object) and Hom (morphism). The type Hom is a dependent type, depending on two objects, named dom (domain) and codom (codomain). The theory has two term constructors, id (identity) and compose (composition).","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Notice how the return types of the term constructors depend on the argument values. For example, the term id(A) has type Hom(A,A). The term constructor compose also uses context variables, listed to the right of the ⊣ symbol. These context variables can also be defined after a where clause, but the left hand side must be surrounded by parentheses. This allows us to write compose(f,g), instead of the more verbose compose(A,B,C,f,g) (for discussion, see Cartmell, 1986, Sec 10: Informal syntax).","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Notice the @op call where we can create method aliases that can then be used throughout the rest of the theory and outside of definition. We can either use this block notation, or a single line notation such as @op (⋅) := compose to define a single alias. Here we utilize this functionality by replacing the Hom and compose methods with their equivalent Unicode characters, → and ⋅ respectively. These aliases are also automatically available to definitions that inherit a theory that already has the alias defined.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"note: Note\nIn general, a GAT consists of a signature, defining the types and terms of the theory, and a set of axioms, the equational laws satisfied by models of the theory. The theory of categories, for example, has axioms of unitality and associativity. At present, Catlab supports the specification of both signatures and the axioms, but is not currently utilizing the axiom definitions in any way, reflecting its status as a programming library, not a proof assistant. It is the programmer's responsibility to ensure any declared instances of an algebraic structure satisfy its axioms.","category":"page"},{"location":"apis/core/#References","page":"Theories, instances, and expressions","title":"References","text":"","category":"section"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Cartmell, 1986: Generalized algebraic theories and contextual categories, DOI:10.1016/0168-0072(86)90053-9\nCartmell, 1978, PhD thesis: Generalized algebraic theories and contextual categories\nPitts, 1995: Categorical logic, Sec 6: Dependent types","category":"page"},{"location":"apis/core/#instances","page":"Theories, instances, and expressions","title":"Instances","text":"","category":"section"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"A theory can have one or more instances, or instantiations by ordinary Julia types and functions. This feature builds on Julia's support for generic functions with multiple dispatch.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Instances are declared using the @instance macro. In an instance of a theory, each theory type is mapped to a Julia type and each term is mapped to a Julia method of the same name. For example, the category of matrices could be defined as an instance of the theory Category defined above:","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"using LinearAlgebra: I\n\nstruct MatrixDomain\n eltype::Type\n dim::Int\nend\n\n@instance Category{MatrixDomain, Matrix} begin\n dom(M::Matrix) = MatrixDomain(eltype(M), size(M,1))\n codom(M::Matrix) = MatrixDomain(eltype(M), size(M,2))\n\n id(m::MatrixDomain) = Matrix{m.eltype}(I, m.dim, m.dim)\n compose(M::Matrix, N::Matrix) = M*N\nend","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"A = Matrix{Float64}([0 1; 1 0])\nid(dom(A))","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"In this instance, the theory type Ob is mapped to the custom Julia type MatrixDomain. The latter type has two fields, a Julia type eltype representing a field k and an integer dim representing the dimensionality n, and so can be interpreted as the n-dimensional vector space k^n. The theory Hom is mapped to the standard Julia type Matrix.","category":"page"},{"location":"apis/core/#syntax-systems","page":"Theories, instances, and expressions","title":"Syntax systems","text":"","category":"section"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Theories can also be instantiated as systems of symbolic expressions, using the @syntax macro. The symbolic expressions are expression trees, as commonly used in computer algebra systems. They are similar to Julia's Expr type but they are instead subtyped from Catlab's GATExpr type and they have a more refined type hierarchy.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"A single theory can have different syntax systems, treating different terms as primitive or performing different simplication or normalization procedures. Catlab tries to make it easy to define new syntax systems. Many of the theories included with Catlab have default syntax systems, but the user is encouraged to define their own to suit their needs.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"To get started, you can always call the @syntax macro with an empty body. Below, we subtype from Catlab's abstract types ObExpr and HomExpr to enable LaTeX pretty-printing and other convenient features, but this is not required.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"@syntax CategoryExprs{ObExpr, HomExpr} Category begin\nend\n\nA, B, C, D = [ Ob(CategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]\nf, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)\n\ncompose(compose(f,g),h)","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"The resulting symbolic expressions perform no simplification. For example, the associativity law is not satisfied:","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"compose(compose(f,g),h) == compose(f,compose(g,h))","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Thus, unlike instances of a theory, syntactic expressions are not expected to obey all the axioms of the theory.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"However, the user may supply logic in the body of the @syntax macro to enforce the axioms or perform other kinds of simplification. Below, we use the associate function provided by Catlab to convert the binary expressions representing composition into n-ary expressions for any number n. The option strict=true tells Catlab to check that the domain and codomain objects are strictly equal and throw an error if they are not.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"@syntax SimplifyingCategoryExprs{ObExpr, HomExpr} Category begin\n compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))\nend\n\nA, B, C, D = [ Ob(SimplifyingCategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ]\nf, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, C, D)\n\ncompose(compose(f,g),h)","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Now the associativity law is satisfied:","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"compose(compose(f,g),h) == compose(f,compose(g,h))","category":"page"},{"location":"apis/core/#Primitive-versus-derived-operations","page":"Theories, instances, and expressions","title":"Primitive versus derived operations","text":"","category":"section"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"In some algebraic structures, there is a choice as to which operations should be considered primitive and which should be derived. For example, in a cartesian monoidal category, the copy operation Delta_X X to X otimes X can be defined in terms of the pairing operation langle f g rangle, or vice versa. In addition, the projections pi_XY X otimes Y to X and pi_XY X otimes Y to Y can be defined in terms of the deleting operation (terminal morphism) or left as primitive.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"In Catlab, the recommended way to deal with such situations is to define all the operations in the theory and then allow particular syntax systems to determine which operations, if any, will be derived from others. In the case of the cartesian monoidal category, we could define a signature CartesianCategory by inheriting from the builtin theory SymmetricMonoidalCategory.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"using Catlab\nimport Catlab.Theories: Ob, Hom, ObExpr, HomExpr, SymmetricMonoidalCategory,\n dom, codom, compose, id, otimes, munit, braid","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"@signature CartesianCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin\n mcopy(A::Ob)::(A → (A ⊗ A))\n delete(A::Ob)::(A → munit())\n\n pair(f::(A → B), g::(A → C))::(A → (B ⊗ C)) ⊣ (A::Ob, B::Ob, C::Ob)\n proj1(A::Ob, B::Ob)::((A ⊗ B) → A)\n proj2(A::Ob, B::Ob)::((A ⊗ B) → B)\nend\nnothing # hide","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"We could then define the copying operation in terms of the pairing.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"@syntax CartesianCategoryExprsV1{ObExpr,HomExpr} CartesianCategory begin\n mcopy(A::Ob) = pair(id(A), id(A))\nend\n\nA = Ob(CartesianCategoryExprsV1.Ob, :A)\nmcopy(A)","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Alternatively, we could define the pairing and projections in terms of the copying and deleting operations.","category":"page"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"@syntax CartesianCategoryExprsV2{ObExpr,HomExpr} CartesianCategory begin\n pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))\n proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))\n proj2(A::Ob, B::Ob) = otimes(delete(A), id(B))\nend\n\nA, B, C = [ Ob(CartesianCategoryExprsV2.Ob, X) for X in [:A, :B, :C] ]\nf, g = Hom(:f, A, B), Hom(:g, A, C)\npair(f, g)","category":"page"},{"location":"apis/core/#API","page":"Theories, instances, and expressions","title":"API","text":"","category":"section"},{"location":"apis/core/","page":"Theories, instances, and expressions","title":"Theories, instances, and expressions","text":"Modules = [\n GAT,\n Syntax,\n Rewrite,\n Present,\n]\nPrivate = false","category":"page"},{"location":"apis/core/#Catlab.GAT","page":"Theories, instances, and expressions","title":"Catlab.GAT","text":"Generalized algebraic theories (GATs) in Julia.\n\n\n\n\n\n","category":"module"},{"location":"apis/core/#Catlab.GAT.invoke_term-Tuple{Type, Tuple, Symbol, Vararg{Any, N} where N}","page":"Theories, instances, and expressions","title":"Catlab.GAT.invoke_term","text":"Invoke a term constructor by name on an instance.\n\nThis method provides reflection for GATs. In everyday use the generic method for the constructor should be called directly, not through this function.\n\nCf. Julia's builtin invoke() function.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.GAT.theory","page":"Theories, instances, and expressions","title":"Catlab.GAT.theory","text":"Retrieve generalized algebraic theory associated with abstract type.\n\nFor example, if Category is imported from Catlab.Theories, then theory(Category)returns the theory of a category.\n\n\n\n\n\n","category":"function"},{"location":"apis/core/#Catlab.GAT.@instance-Tuple{Any, Any}","page":"Theories, instances, and expressions","title":"Catlab.GAT.@instance","text":"Define an instance of a generalized algebraic theory (GAT).\n\n\n\n\n\n","category":"macro"},{"location":"apis/core/#Catlab.GAT.@signature-Tuple{Any, Any}","page":"Theories, instances, and expressions","title":"Catlab.GAT.@signature","text":"Define a signature for a generalized algebraic theory (GAT).\n\nA signature is the same as a theory, except it may not contain axioms, and therefore only three kinds of things can go in the signature body:\n\nType constructors, indicated by the special type TYPE, e.g., Hom(X::Ob,Y::Ob)::TYPE\nTerm constructors, e.g., id(X::Ob)::Hom(X,X)\nFunction aliases, e.g., @op Hom :→\n\nA signature can extend existing theories (at present only one).\n\n\n\n\n\n","category":"macro"},{"location":"apis/core/#Catlab.GAT.@theory-Tuple{Any, Any}","page":"Theories, instances, and expressions","title":"Catlab.GAT.@theory","text":"Define a generalized algebraic theory (GAT).\n\nFour kinds of things can go in the theory body:\n\nType constructors, indicated by the special type TYPE, e.g., Hom(X::Ob,Y::Ob)::TYPE\nTerm constructors, e.g., id(X::Ob)::Hom(X,X)\nFunction aliases, e.g., @op Hom :→\nEquality axioms, e.g., f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B))\n\nA theory can extend existing theories (at present only one).\n\n\n\n\n\n","category":"macro"},{"location":"apis/core/#Catlab.Syntax","page":"Theories, instances, and expressions","title":"Catlab.Syntax","text":"Syntax systems for generalized algebraic theories (GATs).\n\nIn general, a single theory may have many different syntaxes. The purpose of this module to enable the simple but flexible construction of syntax systems.\n\n\n\n\n\n","category":"module"},{"location":"apis/core/#Catlab.Syntax.GATExpr","page":"Theories, instances, and expressions","title":"Catlab.Syntax.GATExpr","text":"Base type for expression in the syntax of a GAT.\n\nWe define Julia types for each type constructor in the theory, e.g., object, morphism, and 2-morphism in the theory of 2-categories. Of course, Julia's type system does not support dependent types, so the type parameters are incorporated in the Julia types. (They are stored as extra data in the expression instances.)\n\nThe concrete types are structurally similar to the core type Expr in Julia. However, the term constructor is represented as a type parameter, rather than as a head field. This makes dispatch using Julia's type system more convenient.\n\n\n\n\n\n","category":"type"},{"location":"apis/core/#Base.Meta.show_sexpr-Tuple{GATExpr}","page":"Theories, instances, and expressions","title":"Base.Meta.show_sexpr","text":"Show the syntax expression as an S-expression.\n\nCf. the standard library function Meta.show_sexpr.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.GAT.invoke_term-Tuple{Module, Symbol, Vararg{Any, N} where N}","page":"Theories, instances, and expressions","title":"Catlab.GAT.invoke_term","text":"Invoke a term constructor by name in a syntax system.\n\nThis method provides reflection for syntax systems. In everyday use the generic method for the constructor should be called directly, not through this function.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Syntax.functor-Tuple{Tuple, GATExpr}","page":"Theories, instances, and expressions","title":"Catlab.Syntax.functor","text":"Functor from GAT expression to GAT instance.\n\nStrictly speaking, we should call these \"structure-preserving functors\" or, better, \"model homomorphisms of GATs\". But this is a category theory library, so we'll go with the simpler \"functor\".\n\nA functor is completely determined by its action on the generators. There are several ways to specify this mapping:\n\nSpecify a Julia instance type for each GAT type, using the required types tuple. For this to work, the generator constructors must be defined for the instance types.\nExplicitly map each generator term to an instance value, using the generators dictionary.\nFor each GAT type (e.g., object and morphism), specify a function mapping generator terms of that type to an instance value, using the terms dictionary.\n\nThe terms dictionary can also be used for special handling of non-generator expressions. One use case for this capability is defining forgetful functors, which map non-generators to generators.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Syntax.parse_json_sexpr-Tuple{Module, Any}","page":"Theories, instances, and expressions","title":"Catlab.Syntax.parse_json_sexpr","text":"Deserialize expression from JSON-able S-expression.\n\nIf symbols is true (the default), strings are converted to symbols.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Syntax.show_latex-Tuple{GATExpr}","page":"Theories, instances, and expressions","title":"Catlab.Syntax.show_latex","text":"Show the expression in infix notation using LaTeX math.\n\nDoes not include $ or \\[begin|end]{equation} delimiters.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Syntax.show_unicode-Tuple{GATExpr}","page":"Theories, instances, and expressions","title":"Catlab.Syntax.show_unicode","text":"Show the expression in infix notation using Unicode symbols.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Syntax.to_json_sexpr-Tuple{GATExpr}","page":"Theories, instances, and expressions","title":"Catlab.Syntax.to_json_sexpr","text":"Serialize expression as JSON-able S-expression.\n\nThe format is an S-expression encoded as JSON, e.g., \"compose(f,g)\" is represented as [\"compose\", f, g].\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Syntax.@syntax","page":"Theories, instances, and expressions","title":"Catlab.Syntax.@syntax","text":"Define a syntax system for a generalized algebraic theory (GAT).\n\nA syntax system consists of Julia types (with top type GATExpr) for each type constructor in the signature, plus Julia functions for\n\nGenerators: creating new generator terms, e.g., objects or morphisms\nAccessors: accessing type parameters, e.g., domains and codomains\nTerm constructors: applying term constructors, e.g., composition and monoidal products\n\nJulia code for all this is generated by the macro. Any of the methods can be overriden with custom simplification logic.\n\n\n\n\n\n","category":"macro"},{"location":"apis/core/#Catlab.Rewrite","page":"Theories, instances, and expressions","title":"Catlab.Rewrite","text":"Rewriting for GAT expressions.\n\nThe current content of this module is just a stopgap until I can implement a generic term rewriting system.\n\n\n\n\n\n","category":"module"},{"location":"apis/core/#Catlab.Rewrite.associate-Tuple{E} where E<:GATExpr","page":"Theories, instances, and expressions","title":"Catlab.Rewrite.associate","text":"Simplify associative binary operation.\n\nMaintains the normal form op(e1,e2,...) where e1,e2,... are expressions that are not applications of op()\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Rewrite.associate_unit-Tuple{GATExpr, Function}","page":"Theories, instances, and expressions","title":"Catlab.Rewrite.associate_unit","text":"Simplify associative binary operation with unit.\n\nReduces a freely generated (typed) monoid to normal form.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Rewrite.distribute_unary-Tuple{GATExpr, Function, Function}","page":"Theories, instances, and expressions","title":"Catlab.Rewrite.distribute_unary","text":"Distribute unary operation over binary operation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Rewrite.involute-Tuple{GATExpr}","page":"Theories, instances, and expressions","title":"Catlab.Rewrite.involute","text":"Simplify involutive unary operation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present","page":"Theories, instances, and expressions","title":"Catlab.Present","text":"Finite presentations of a model of a generalized algebraic theory (GAT).\n\nWe support two methods for defining models of a GAT: as Julia objects using the @instance macro and as syntactic objects using the @present macro. Instances are useful for casting generic data structures, such as matrices, abstract tensor systems, and wiring diagrams, in categorical language. Presentations define small categories by generators and relations and are useful in applications like knowledge representation.\n\n\n\n\n\n","category":"module"},{"location":"apis/core/#Catlab.Present.add_definition!-Tuple{Presentation, Symbol, GATExpr}","page":"Theories, instances, and expressions","title":"Catlab.Present.add_definition!","text":"Add a generator defined by an equation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.add_equation!-Tuple{Presentation, GATExpr, GATExpr}","page":"Theories, instances, and expressions","title":"Catlab.Present.add_equation!","text":"Add an equation between terms to a presentation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.add_generator!-Tuple{Presentation, Any}","page":"Theories, instances, and expressions","title":"Catlab.Present.add_generator!","text":"Add a generator to a presentation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.add_generators!-Tuple{Presentation, Any}","page":"Theories, instances, and expressions","title":"Catlab.Present.add_generators!","text":"Add iterable of generators to a presentation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.equations-Tuple{Presentation}","page":"Theories, instances, and expressions","title":"Catlab.Present.equations","text":"Get all equations of a presentation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.generator-Tuple{Presentation, Any}","page":"Theories, instances, and expressions","title":"Catlab.Present.generator","text":"Retrieve generators by name.\n\nGenerators can also be retrieved using indexing notation, so that generator(pres, name) and pres[name] are equivalent.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.generator_index-Tuple{Presentation, Symbol}","page":"Theories, instances, and expressions","title":"Catlab.Present.generator_index","text":"Get the index of a generator\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.generators-Tuple{Presentation}","page":"Theories, instances, and expressions","title":"Catlab.Present.generators","text":"Get all generators of a presentation.\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.has_generator-Tuple{Presentation, Any}","page":"Theories, instances, and expressions","title":"Catlab.Present.has_generator","text":"Does the presentation contain a generator with the given name?\n\n\n\n\n\n","category":"method"},{"location":"apis/core/#Catlab.Present.@present-Tuple{Any, Any}","page":"Theories, instances, and expressions","title":"Catlab.Present.@present","text":"Define a presentation using a convenient syntax.\n\n\n\n\n\n","category":"macro"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/graphics/graphviz_wiring_diagrams.jl\"","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Drawing-wiring-diagrams-in-Graphviz","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"(Image: )","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"Catlab can draw wiring diagrams using Graphviz. Directed wiring diagrams are drawn using the dot program and undirected wiring diagrams using neato and fdp. This feature requires that Graphviz be installed, but does not require any additional Julia packages.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"using Catlab.WiringDiagrams, Catlab.Graphics","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Directed-wiring-diagrams","page":"Drawing wiring diagrams in Graphviz","title":"Directed wiring diagrams","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Symmetric-monoidal-category","page":"Drawing wiring diagrams in Graphviz","title":"Symmetric monoidal category","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"using Catlab.Theories\n\nA, B = Ob(FreeSymmetricMonoidalCategory, :A, :B)\nf = Hom(:f, A, B)\ng = Hom(:g, B, A)\nh = Hom(:h, otimes(A,B), otimes(A,B));\nnothing #hide","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"To start, here are a few very simple examples.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(f)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(compose(f,g))","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(otimes(f,g))","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"In the next example, notice how Graphviz automatically \"untwists\" the double braiding to minimize edge crossings.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(compose(braid(A,A), otimes(f,f), braid(B,B)))","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"Here is a larger composite morphism.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"composite = compose(otimes(g,f), h, otimes(f,g))\nto_graphviz(composite)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"By default, the wiring diagram is laid out from top to bottom. Other layout orientations can be requested, such as left-to-right or bottom-to-top:","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(composite, orientation=LeftToRight)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(composite, orientation=BottomToTop)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"When working with very large diagrams (larger than the ones shown here), it is sometimes convenient to omit the ports of the outer box and any wires attached to them.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(composite, outer_ports=false)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Biproduct-category","page":"Drawing wiring diagrams in Graphviz","title":"Biproduct category","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"A, B = Ob(FreeBiproductCategory, :A, :B)\nf = Hom(:f, A, B)\ng = Hom(:g, B, A);\nnothing #hide","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"By default, copies and merges are drawn the way they are represented internally, as multiple wires.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"f1 = compose(mcopy(A), otimes(f,f))\nto_graphviz(f1)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"f2 = compose(mcopy(A), otimes(f,f), mmerge(B))\nto_graphviz(f2)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"To draw nodes for copies and merges, we need to add junctions to the wiring diagram.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(add_junctions!(to_wiring_diagram(f1)))","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(add_junctions!(to_wiring_diagram(f2)))","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Traced-monoidal-category","page":"Drawing wiring diagrams in Graphviz","title":"Traced monoidal category","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"A, B, X, Y = Ob(FreeTracedMonoidalCategory, :A, :B, :X, :Y)\nf = Hom(:f, otimes(X,A), otimes(X,B))\n\nto_graphviz(trace(X, A, B, f))","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(trace(X, A, B, f), orientation=LeftToRight)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"g, h = Hom(:g, A, A), Hom(:h, B, B)\n\ntrace_naturality = trace(X, A, B, compose(otimes(id(X),g), f, otimes(id(X),h)))\nto_graphviz(trace_naturality, orientation=LeftToRight)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Undirected-wiring-diagrams","page":"Drawing wiring diagrams in Graphviz","title":"Undirected wiring diagrams","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"The composite of two binary relations:","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"using Catlab.Programs: @relation\n\ndiagram = @relation (x,z) where (x,y,z) begin\n R(x,y)\n S(y,z)\nend\nto_graphviz(diagram, box_labels=:name)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"A \"wheel\"-shaped composition of relations:","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"diagram = @relation (x,y,z) where (w,x,y,z) begin\n R(x,w)\n S(y,w)\n T(z,w)\nend\nto_graphviz(diagram, box_labels=:name)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"As these examples show, the box_labels keyword argument specifies the data attribute of boxes to use for box labels, if any. The boolean argument port_labels controls the labeling of ports by numerical values and the argument junction_labels specifies the data attribute of junctions to use for junction labels. Note that the macro @relation creates wiring diagrams with name attribute for boxes and variable attribute for junctions.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(diagram, box_labels=:name,\n port_labels=false, junction_labels=:variable)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"By default, all junctions are shown. The keyword argument implicit_junctions omits any junctions which have exactly two incident ports.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"to_graphviz(diagram, box_labels=:name,\n port_labels=false, implicit_junctions=true)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Custom-styles","page":"Drawing wiring diagrams in Graphviz","title":"Custom styles","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"The visual appearance of wiring diagrams can be customized by setting Graphviz attributes at the graph, node, edge, and cell levels. Graph, node, and edge attributes are described in the Graphviz documentation. Cell attributes are passed to the primary cell of the HTML-like label used for the boxes.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"A, B, C = Ob(FreeSymmetricMonoidalCategory, :A, :B, :C)\nf, g = Hom(:f, A, B), Hom(:g, B, C)\n\nto_graphviz(compose(f,g),\n labels = true, label_attr=:headlabel,\n node_attrs = Dict(\n :fontname => \"Courier\",\n ),\n edge_attrs = Dict(\n :fontname => \"Courier\",\n :labelangle => \"25\",\n :labeldistance => \"2\",\n ),\n cell_attrs = Dict(\n :bgcolor => \"lavender\",\n )\n)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/#Output-formats","page":"Drawing wiring diagrams in Graphviz","title":"Output formats","text":"","category":"section"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"The function to_graphviz returns an object of a type Graphviz.Graph, representing a Graphviz graph as an abstract syntax tree. When displayed interactively, this object is automatically run through Graphviz and rendered as an SVG image. Sometimes it is convenient to perform this process manually, to change the output format or further customize the generated dot file.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"To generate a dot file, use the builtin pretty-printer. This feature does not require Graphviz to be installed.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"using Catlab.Graphics: Graphviz\n\ngraph = to_graphviz(compose(f,g))\nGraphviz.pprint(graph)","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"Catlab provides a simple wrapper around the Graphviz command-line programs. For example, here is the JSON output for the graph.","category":"page"},{"location":"generated/graphics/graphviz_wiring_diagrams/","page":"Drawing wiring diagrams in Graphviz","title":"Drawing wiring diagrams in Graphviz","text":"import JSON\n\nJSON.parse(Graphviz.run_graphviz(graph, format=\"json0\"))","category":"page"},{"location":"apis/graphics/#graphics","page":"Graphics","title":"Graphics","text":"","category":"section"},{"location":"apis/graphics/","page":"Graphics","title":"Graphics","text":"Modules = [\n Graphics.GraphvizGraphs,\n Graphics.ComposeWiringDiagrams,\n Graphics.GraphvizWiringDiagrams,\n Graphics.TikZWiringDiagrams,\n Graphics.WiringDiagramLayouts,\n]\nPrivate = false","category":"page"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizGraphs","page":"Graphics","title":"Catlab.Graphics.GraphvizGraphs","text":"Graphviz support for Catlab's graph types.\n\n\n\n\n\n","category":"module"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizGraphs.parse_graphviz-Tuple{AbstractDict}","page":"Graphics","title":"Catlab.Graphics.GraphvizGraphs.parse_graphviz","text":"Parse Graphviz output in JSON format.\n\nReturns a property graph with graph layout and other metadata. Each node has a position and size.\n\nAll units are in points. Note that Graphviz has 72 points per inch.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizGraphs.to_graphviz-Tuple{AbstractPropertyGraph}","page":"Graphics","title":"Catlab.Graphics.GraphvizGraphs.to_graphviz","text":"Convert a property graph to a Graphviz graph.\n\nThis method is usually more convenient than direct AST manipulation for creating simple Graphviz graphs. For more advanced features, like nested subgraphs, you must use the Graphviz AST.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizGraphs.to_graphviz-Tuple{Union{AbstractGraph, AbstractReflexiveGraph, AbstractSymmetricGraph, AbstractSymmetricReflexiveGraph}}","page":"Graphics","title":"Catlab.Graphics.GraphvizGraphs.to_graphviz","text":"Convert a graph to a Graphviz graph.\n\nA simple default style is applied. For more control over the visual appearance, first convert the graph to a property graph, define the Graphviz attributes as needed, and then convert to a Graphviz graph.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.ComposeWiringDiagrams","page":"Graphics","title":"Catlab.Graphics.ComposeWiringDiagrams","text":"Draw wiring diagrams using Compose.jl.\n\n\n\n\n\n","category":"module"},{"location":"apis/graphics/#Catlab.Graphics.ComposeWiringDiagrams.ComposePicture","page":"Graphics","title":"Catlab.Graphics.ComposeWiringDiagrams.ComposePicture","text":"A Compose context together with a given width and height.\n\nWe need this type because contexts have no notion of size or aspect ratio, but wiring diagram layouts have fixed aspect ratios.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphics/#Catlab.Graphics.ComposeWiringDiagrams.layout_to_composejl-Tuple{WiringDiagram}","page":"Graphics","title":"Catlab.Graphics.ComposeWiringDiagrams.layout_to_composejl","text":"Draw a wiring diagram in Compose.jl using the given layout.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.ComposeWiringDiagrams.to_composejl-Tuple","page":"Graphics","title":"Catlab.Graphics.ComposeWiringDiagrams.to_composejl","text":"Draw a wiring diagram in Compose.jl.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizWiringDiagrams","page":"Graphics","title":"Catlab.Graphics.GraphvizWiringDiagrams","text":"Lay out and draw wiring diagrams using Graphviz.\n\nThis module requires Graphviz v2.42 or higher.\n\n\n\n\n\n","category":"module"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizGraphs.to_graphviz-Tuple{CPortGraph}","page":"Graphics","title":"Catlab.Graphics.GraphvizGraphs.to_graphviz","text":"Draw a circular port graph using Graphviz.\n\nCreates a Graphviz graph. Ports are currently not respected in the image, but the port index for each box can be displayed to provide clarification.\n\nArguments\n\ngraph_name=\"G\": name of Graphviz graph\nprog=\"neato\": Graphviz program, usually \"neato\" or \"fdp\"\nbox_labels=false: whether to label boxes with their number\nport_labels=false: whether to label ports with their number\ngraph_attrs=Dict(): top-level graph attributes\nnode_attrs=Dict(): top-level node attributes\nedge_attrs=Dict(): top-level edge attributes\n\nTODO: The lack of ports might be able to be resolved by introducing an extra node per port which is connected to its box with an edge of length 0.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizGraphs.to_graphviz-Tuple{Catlab.WiringDiagrams.UndirectedWiringDiagrams.AbstractUWD}","page":"Graphics","title":"Catlab.Graphics.GraphvizGraphs.to_graphviz","text":"Draw an undirected wiring diagram using Graphviz.\n\nCreates an undirected, bipartite Graphviz graph, with the boxes and outer ports of the diagram becoming nodes of one kind and the junctions of the diagram becoming nodes of the second kind.\n\nArguments\n\ngraph_name=\"G\": name of Graphviz graph\nprog=\"neato\": Graphviz program, usually \"neato\" or \"fdp\"\nbox_labels=false: if boolean, whether to label boxes with their number; if a symbol, name of data attribute for box label\nport_labels=false: whether to label ports with their number\njunction_labels=false: if boolean, whether to label junctions with their number; if a symbol, name of data attribute for junction label\njunction_size=\"0.075\": size of junction nodes, in inches\nimplicit_junctions=false: whether to represent a junction implicity as a wire when it has exactly two incident ports\ngraph_attrs=Dict(): top-level graph attributes\nnode_attrs=Dict(): top-level node attributes\nedge_attrs=Dict(): top-level edge attributes\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizGraphs.to_graphviz-Tuple{WiringDiagram}","page":"Graphics","title":"Catlab.Graphics.GraphvizGraphs.to_graphviz","text":"Draw a wiring diagram using Graphviz.\n\nThe input can also be a morphism expression, in which case it is first converted into a wiring diagram. This function requires Graphviz v2.42 or higher.\n\nArguments\n\ngraph_name=\"G\": name of Graphviz digraph\norientation=TopToBottom: orientation of layout. One of LeftToRight, RightToLeft, TopToBottom, or BottomToTop.\nnode_labels=true: whether to label the nodes\nlabels=false: whether to label the edges\nlabel_attr=:label: what kind of edge label to use (if labels is true). One of :label, :xlabel, :headlabel, or :taillabel.\nport_size=\"24\": minimum size of ports on box, in points\njunction_size=\"0.05\": size of junction nodes, in inches\nouter_ports=true: whether to display the outer box's input and output ports. If disabled, no incoming or outgoing wires will be shown either!\nanchor_outer_ports=true: whether to enforce ordering of the outer box's input and output, i.e., ordering of the incoming and outgoing wires\ngraph_attrs=Dict(): top-level graph attributes\nnode_attrs=Dict(): top-level node attributes\nedge_attrs=Dict(): top-level edge attributes\ncell_attrs=Dict(): main cell attributes in node HTML-like label\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.GraphvizWiringDiagrams.graphviz_layout-Tuple{WiringDiagram}","page":"Graphics","title":"Catlab.Graphics.GraphvizWiringDiagrams.graphviz_layout","text":"Lay out directed wiring diagram using Graphviz.\n\nNote: At this time, only the positions and sizes of the boxes, and the positions of the outer ports, are used. The positions of the box ports and the splines for the wires are ignored.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.TikZWiringDiagrams","page":"Graphics","title":"Catlab.Graphics.TikZWiringDiagrams","text":"Draw wiring diagrams using TikZ.\n\n\n\n\n\n","category":"module"},{"location":"apis/graphics/#Catlab.Graphics.TikZWiringDiagrams.layout_to_tikz-Tuple{WiringDiagram}","page":"Graphics","title":"Catlab.Graphics.TikZWiringDiagrams.layout_to_tikz","text":"Draw a wiring diagram in TikZ using the given layout.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.TikZWiringDiagrams.to_tikz-Tuple","page":"Graphics","title":"Catlab.Graphics.TikZWiringDiagrams.to_tikz","text":"Draw a wiring diagram in TikZ.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.WiringDiagramLayouts","page":"Graphics","title":"Catlab.Graphics.WiringDiagramLayouts","text":"Backend-agnostic layout of wiring diagrams via morphism expressions.\n\nThis module lays out wiring diagrams for visualization, independent of any specific graphics system. It uses the structure of a morphism expression to determine the layout. Thus, the first step of the algorithm is to convert the wiring diagram to a symbolic expression, using the submodule WiringDiagrams.Expressions. Morphism expressions may also be given directly.\n\n\n\n\n\n","category":"module"},{"location":"apis/graphics/#Catlab.Graphics.WiringDiagramLayouts.LayoutOrientation","page":"Graphics","title":"Catlab.Graphics.WiringDiagramLayouts.LayoutOrientation","text":"Orientation of wiring diagram.\n\n\n\n\n\n","category":"type"},{"location":"apis/graphics/#Catlab.Graphics.WiringDiagramLayouts.layout_box-Tuple{Vector{T} where T, Vector{T} where T, Catlab.Graphics.WiringDiagramLayouts.LayoutOptions}","page":"Graphics","title":"Catlab.Graphics.WiringDiagramLayouts.layout_box","text":"Lay out a box and its ports.\n\nBy default the box is rectangular, but other shapes are also supported.\n\n\n\n\n\n","category":"method"},{"location":"apis/graphics/#Catlab.Graphics.WiringDiagramLayouts.layout_diagram-Tuple{Module, WiringDiagram}","page":"Graphics","title":"Catlab.Graphics.WiringDiagramLayouts.layout_diagram","text":"Lay out a wiring diagram or morphism expression for visualization.\n\nIf a wiring diagram is given, it is first to converted to a morphism expression.\n\nThe layout is calculated with respect to a cartesian coordinate system with origin at the center of the diagram and the positive y-axis pointing downwards. Box positions are relative to their centers. All positions and sizes are dimensionless (unitless).\n\n\n\n\n\n","category":"method"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/graphs/subgraphs.jl\"","category":"page"},{"location":"generated/graphs/subgraphs/#Algebra-of-subgraphs","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"","category":"section"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"(Image: )","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"using Catlab.Graphs, Catlab.Graphics\nusing Catlab.Theories, Catlab.CategoricalAlgebra","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"A subgraph of a graph G is a monomorphism A rightarrowtail G. Because the category of graphs is a presheaf topos, its subobjects have a rich algebraic structure, which we will explore in this vignette.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Throughout the vignette, we will work with subgraphs of the following graph.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"G = cycle_graph(Graph, 4) ⊕ path_graph(Graph, 2) ⊕ cycle_graph(Graph, 1)\nadd_edge!(G, 3, add_vertex!(G))\n\nto_graphviz(G, node_labels=true, edge_labels=true)","category":"page"},{"location":"generated/graphs/subgraphs/#Meet-and-join","page":"Algebra of subgraphs","title":"Meet and join","text":"","category":"section"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"The basic operations of meet or intersection (wedge), join or union (vee), top or maximum (top), bottom or minimum (bot) are all computed pointwise: separately on vertices and edges.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Consider the following two subgraphs.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"(A = Subobject(G, V=1:4, E=[1,2,4])) |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"(B = Subobject(G, V=[2,3,4,7,8], E=[2,3,6,7])) |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"The join is defined as left adjoint to the diagonal, making it the least upper bound:","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"A vee B leq C qquadtextiffqquad A leq C text and B leq C","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"A ∨ B |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Dually, the meet is defined as right adjoint to the diagonal, making it the greatest lower bound:","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"C leq A text and C leq B qquadtextiffqquad C leq A wedge B","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"A ∧ B |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/#Implication-and-negation","page":"Algebra of subgraphs","title":"Implication and negation","text":"","category":"section"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"The other operations, beginning with implication (Rightarrow) and negation (neg) are more interesting because they do not have pointwise formulas.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Implication is defined as the right adjoint to the meet:","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"C wedge A leq B qquadtextiffqquad C leq A Rightarrow B","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"(A ⟹ B) |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Negation is defined by setting B = bot in the above formula:","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"C wedge A = bot qquadtextiffqquad C leq neg A","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"¬A |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/#Induced-subgraph-as-a-double-negation","page":"Algebra of subgraphs","title":"Induced subgraph as a double negation","text":"","category":"section"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"The logic of subgraphs, and of subobjects in presheaf toposes generally, is not classical. Specifically, subobjects form a Heyting algebra but not a Boolean algebra. This means that the law of excluded middle does not hold: in general, neg neg A neq A.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Applying the double negation to a discrete subgraph gives the subgraph induced by those vertices.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"(C = Subobject(G, V=1:4)) |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"¬(¬C) |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/#Subtraction-and-non","page":"Algebra of subgraphs","title":"Subtraction and non","text":"","category":"section"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"The subojects also form co-Heyting algebra and hence a bi-Heyting algebra.","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Subtraction is defined dually to implication as the left adjoint to the join:","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"A leq B vee C qquadtextiffqquad A setminus B leq C","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"(A \\ B) |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"Non is defined by setting A = top in the above formula:","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"top = B vee C qquadtextiffqquad sim B leq C","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"~A |> to_graphviz","category":"page"},{"location":"generated/graphs/subgraphs/#Boundary-via-non","page":"Algebra of subgraphs","title":"Boundary via non","text":"","category":"section"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"A boundary operator can be defined using the non operator:","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"partial A = A wedge sim A","category":"page"},{"location":"generated/graphs/subgraphs/","page":"Algebra of subgraphs","title":"Algebra of subgraphs","text":"(A ∧ ~A) |> to_graphviz","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/wiring_diagrams/diagrams_and_expressions.jl\"","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/#Wiring-diagrams-and-syntactic-expressions","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"","category":"section"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"(Image: )","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"Morphisms in a monoidal category can be represented as syntactic expressions, such as f cdot g and f otimes g, and also as wiring diagrams, aka string diagrams. Catlab provides facilities for transforming between these two representations.","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"using Catlab.Theories, Catlab.WiringDiagrams\nusing Catlab.Graphics\n\nfunction show_diagram(d::WiringDiagram)\n to_graphviz(d, orientation=LeftToRight, labels=false)\nend","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/#Expressions-to-diagrams","page":"Wiring diagrams and syntactic expressions","title":"Expressions to diagrams","text":"","category":"section"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"Converting a morphism expression to a wiring diagram is conceptually and algorithmically simple, because every expression determines a unique diagram.","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"As a simple example, here is the monoidal product of two generators, f and g, first as an expression (displayed using LaTeX) and then as a wiring diagram (displayed using Graphviz).","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"A, B, C, D, E = Ob(FreeCartesianCategory, :A, :B, :C, :D, :E)\nf = Hom(:f, A, B)\ng = Hom(:g, B, C)\n\nexpr = f ⊗ g","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"show_diagram(to_wiring_diagram(expr))","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"Here is a monoidal product of compositions:","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"h = Hom(:h, C, D)\nk = Hom(:k, D, E)\n\nexpr = (f ⋅ g) ⊗ (h ⋅ k)","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"show_diagram(to_wiring_diagram(expr))","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/#Diagrams-to-expressions","page":"Wiring diagrams and syntactic expressions","title":"Diagrams to expressions","text":"","category":"section"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"Converting a wiring diagram to a syntactic expression is algorithmically more challenging, due to the fact that a single wiring diagram generally admits many different representations as an expression. Thus, a particular expression must be singled out.","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"To bring this out, we define a function that round-trips a morphism expression to a wiring diagram and then back to an expression.","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"function roundtrip_expr(expr::FreeCartesianCategory.Hom)\n d = to_wiring_diagram(expr)\n to_hom_expr(FreeCartesianCategory, d)\nend","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"We can recover the expression just considered above:","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"roundtrip_expr((f ⋅ g) ⊗ (h ⋅ k))","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"But here is a different expression that round-trips to the same thing:","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"roundtrip_expr((f ⊗ h) ⋅ (g ⊗ k))","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"The equality of these two expressions,","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"(f cdot g) otimes (h cdot k) = (f otimes h) cdot (g otimes k)","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"is the interchange law in a monoidal category. It says that composition and monoidal products can be interchanged. As this example shows, the conversion algorithm in Catlab favors products over composition, placing products towards the root of the expression tree wherever possible. Other laws can be discovered by this procedure. Since we are working in a cartesian monoidal category, operations of copying, Delta_A A to A otimes A, and deleting, lozenge_A A to I, are available.","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"Consider the operation of copying the product A otimes B.","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"expr = mcopy(A ⊗ B)","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"show_diagram(add_junctions!(to_wiring_diagram(expr)))","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"roundtrip_expr(expr)","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"The equation just witnessed,","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"Delta_A otimes B = (Delta_A otimes Delta_B) cdot (1_A otimes sigma_AB otimes 1_B)","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"is one of the coherence laws for cartesian products (arXiv:0908.3347, Table 7). Another coherence law for products is","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"lozenge_A otimes B = lozenge_A otimes lozenge_B","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"expr = delete(A ⊗ B)","category":"page"},{"location":"generated/wiring_diagrams/diagrams_and_expressions/","page":"Wiring diagrams and syntactic expressions","title":"Wiring diagrams and syntactic expressions","text":"roundtrip_expr(expr)","category":"page"},{"location":"apis/categorical_algebra/#categorical_algebra","page":"Categorical algebra","title":"Categorical algebra","text":"","category":"section"},{"location":"apis/categorical_algebra/#FinSet-and-FinRel","page":"Categorical algebra","title":"FinSet and FinRel","text":"","category":"section"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"The following APIs implement FinSet, the category of Finite Sets (actually the skeleton of FinSet). The objects of this category are natural numbers where n represents a set with n elements. The morphisms are functions between such sets. We use the skeleton of FinSet in order to ensure that all sets are finite and morphisms can be stored using lists of integers. Finite relations are built out of FinSet and can be used to do some relational algebra.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"Modules = [\n CategoricalAlgebra.FinSets,\n CategoricalAlgebra.FinRelations,\n ]\nPrivate = false","category":"page"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets","text":"The category of finite sets and functions, and its skeleton.\n\n\n\n\n\n","category":"module"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.FinDomFunction","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.FinDomFunction","text":"Function out of a finite set.\n\nThis class of functions is convenient because it is exactly the class that can be represented explicitly by a vector of values from the codomain.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.FinFunction","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.FinFunction","text":"Function between finite sets.\n\nThe function can be defined implicitly by an arbitrary Julia function, in which case it is evaluated lazily, or explictly by a vector of integers. In the vector representation, the function (1↦1, 2↦3, 3↦2, 4↦3), for example, is represented by the vector [1,3,2,3].\n\nThis type is mildly generalized by FinDomFunction.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.FinSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.FinSet","text":"Finite set.\n\nThis generic type encompasses the category FinSet of finite sets and functions, through types FinSet{S} where S <: AbstractSet, as well as the skeleton of this category, through the type FinSet{Int}. In the latter case, the object FinSet(n) represents the set 1n.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.HashJoin","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.HashJoin","text":"Hash join algorithm.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.JoinAlgorithm","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.JoinAlgorithm","text":"Algorithm for limit of spans or multispans out of finite sets.\n\nIn the context of relational databases, such limits are joins.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.NestedLoopJoin","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.NestedLoopJoin","text":"Nested-loop join algorithm.\n\nThis is the naive algorithm for computing joins.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.SmartJoin","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.SmartJoin","text":"Meta-algorithm for joins that attempts to pick an appropriate algorithm.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.SortMergeJoin","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.SortMergeJoin","text":"Sort-merge join algorithm.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.SubFinSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.SubFinSet","text":"Subset of a finite set.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.SubOpBoolean","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.SubOpBoolean","text":"Algorithm to compute subobject operations using elementwise boolean logic.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.force-Tuple{Catlab.CategoricalAlgebra.Sets.SetFunction{Dom, Codom} where {Dom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T), Codom}}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.force","text":"Force evaluation of lazy function or relation.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.is_indexed-Tuple{Catlab.CategoricalAlgebra.Sets.SetFunction}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.is_indexed","text":"Whether the given function is indexed, i.e., supports efficient preimages.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinSets.preimage-Tuple{Catlab.CategoricalAlgebra.Sets.SetFunctionIdentity, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinSets.preimage","text":"The preimage (inverse image) of the value y in the codomain.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinRelations","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinRelations","text":"The category of finite sets and relations, and its skeleton.\n\n\n\n\n\n","category":"module"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinRelations.BoolRig","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinRelations.BoolRig","text":"The rig of booleans.\n\nThis struct is needed because in base Julia, the product of booleans is another boolean, but the sum of booleans is coerced to an integer: true + true == 2.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinRelations.FinRel","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinRelations.FinRel","text":"Object in the category of finite sets and relations.\n\nSee also: FinSet.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinRelations.FinRelation","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinRelations.FinRelation","text":"Binary relation between finite sets.\n\nA morphism in the category of finite sets and relations. The relation can be represented implicitly by an arbitrary Julia function mapping pairs of elements to booleans or explicitly by a matrix (dense or sparse) taking values in the rig of booleans (BoolRig).\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinRelations.FinRelationCallable","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinRelations.FinRelationCallable","text":"Relation in FinRel defined by a callable Julia object.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FinRelations.FinRelationMatrix","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FinRelations.FinRelationMatrix","text":"Relation in FinRel represented by a boolean matrix.\n\nBoolean matrices are also known as logical matrices or relation matrices.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Diagrams,-Limits,-and-Colimts","page":"Categorical algebra","title":"Diagrams, Limits, and Colimts","text":"","category":"section"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"The following modules define diagrams in an arbitrary category and specify limit and colimt cones over said diagrams. Thes constructions enjoy the fullest support for FinSet and are used below to define presheaf categories as C-Sets. The general idea of these functions is that you set up a limit computation by specifying a diagram and asking for a limit or colimit cone, which is returned as a struct containing the apex object and the leg morphisms. This cone structure can be queried using the functions apex and legs. Julia's multiple dispatch feature is heavily used to specialize limit and colimit computations for various diagram shapes like product/coproduct and equalizer/coequalizer. As a consumer of this API, it is highly recommended that you use multiple dispatch to specialize your code on the diagram shape whenever possible.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"Modules = [\n CategoricalAlgebra.FreeDiagrams,\n CategoricalAlgebra.Limits,\n ]\nPrivate = false","category":"page"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams","text":"Free diagrams in a category.\n\nA free diagram in a category is a diagram whose shape is a free category. Examples include the empty diagram, pairs of objects, discrete diagrams, parallel pairs, composable pairs, and spans and cospans. Limits and colimits are most commonly taken over free diagrams.\n\n\n\n\n\n","category":"module"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.ComposableMorphisms","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.ComposableMorphisms","text":"Composable morphisms in a category.\n\nComposable morphisms are a sequence of morphisms in a category that form a path in the underlying graph of the category.\n\nFor the common special case of two morphisms, see ComposablePair.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.ComposablePair","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.ComposablePair","text":"Pair of composable morphisms in a category.\n\nComposable pairs are a common special case of ComposableMorphisms.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.Cospan","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.Cospan","text":"Cospan of morphisms in a category.\n\nA common special case of Multicospan. See also Span.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.DiscreteDiagram","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.DiscreteDiagram","text":"Discrete diagram: a diagram whose only morphisms are identities.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.FixedShapeFreeDiagram","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.FixedShapeFreeDiagram","text":"Abstract type for free diagram of fixed shape.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.Multicospan","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.Multicospan","text":"Multicospan of morphisms in a category.\n\nA multicospan is like a Cospan except that it may have a number of legs different than two. A limit of this shape is a pullback.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.Multispan","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.Multispan","text":"Multispan of morphisms in a category.\n\nA multispan is like a Span except that it may have a number of legs different than two. A colimit of this shape is a pushout.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.ParallelMorphisms","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.ParallelMorphisms","text":"Parallel morphims in a category.\n\nParallel morphisms are just morphisms with the same domain and codomain. A (co)limit of this shape is a (co)equalizer.\n\nFor the common special case of two morphisms, see ParallelPair.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.ParallelPair","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.ParallelPair","text":"Pair of parallel morphisms in a category.\n\nA common special case of ParallelMorphisms.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.Span","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.Span","text":"Span of morphims in a category.\n\nA common special case of Multispan. See also Cospan.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.apex-Tuple{Multispan}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.apex","text":"apex(span::Multispan)\n\nreturns the object at the top of the multispan, which is the domain of all the legs.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.bundle_legs-Tuple{Multispan, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.bundle_legs","text":"Bundle together legs of a multi(co)span.\n\nFor example, calling bundle_legs(span, SVector((1,2),(3,4))) on a multispan with four legs gives a span whose left leg bundles legs 1 and 2 and whose right leg bundles legs 3 and 4. Note that in addition to bundling, this function can also permute legs and discard them.\n\nThe bundling is performed using the universal property of (co)products, which assumes that these (co)limits exist.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.feet-Tuple{Multispan}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.feet","text":"feet(span::Multispan)\n\nreturns the collection of feet in the multspan, which are the codomains of the legs.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.FreeDiagrams.legs-Tuple{Multispan}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.FreeDiagrams.legs","text":"legs(span::Multispan)\n\nreturns the collection of legs in the multspan, which are the morphisms sharing a common domain.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits","text":"Limits and colimits in a category.\n\n\n\n\n\n","category":"module"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.AbstractColimit","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.AbstractColimit","text":"Abstract type for colimit in a category.\n\nThe standard concrete subtype is Colimit, although for computational reasons certain categories may use different subtypes to include extra data.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.AbstractLimit","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.AbstractLimit","text":"Abstract type for limit in a category.\n\nThe standard concrete subtype is Limit, although for computational reasons certain categories may use different subtypes to include extra data.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.Colimit","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.Colimit","text":"Colimit in a category.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.ColimitAlgorithm","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.ColimitAlgorithm","text":"Algorithm for computing colimits.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.ComposeCoproductCoequalizer","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.ComposeCoproductCoequalizer","text":"Compute pushout by composing a coproduct with a coequalizer.\n\nSee also: ComposeProductEqualizer.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.ComposeProductEqualizer","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.ComposeProductEqualizer","text":"Compute pullback by composing a product with an equalizer.\n\nSee also: ComposeCoproductCoequalizer.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.Limit","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.Limit","text":"Limit in a category.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.LimitAlgorithm","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.LimitAlgorithm","text":"Algorithm for computing limits.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.can_pushout_complement-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.can_pushout_complement","text":"Can a pushout complement be constructed for a composable pair?\n\nEven in nice categories, this is not generally possible.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.colimit","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.colimit","text":"Colimit of a diagram.\n\nTo define colimits in a category with objects Ob, override the method colimit(::FreeDiagram{Ob}) for general colimits or colimit(::D) with suitable type D <: FixedShapeFreeDiagram{Ob} for colimits of specific shape, such as coproducts or coequalizers.\n\nSee also: limit\n\n\n\n\n\n","category":"function"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.limit","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.limit","text":"Limit of a diagram.\n\nTo define limits in a category with objects Ob, override the method limit(::FreeDiagram{Ob}) for general limits or limit(::D) with suitable type D <: FixedShapeFreeDiagram{Ob} for limits of specific shape, such as products or equalizers.\n\nSee also: colimit\n\n\n\n\n\n","category":"function"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.pullback-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.pullback","text":"Pullback of a pair of morphisms with common codomain.\n\nTo implement for a type T, define the method limit(::Cospan{T}) and/or limit(::Multicospan{T}) or, if you have already implemented products and equalizers, rely on the default implementation.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.pushout-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.pushout","text":"Pushout of a pair of morphisms with common domain.\n\nTo implement for a type T, define the method colimit(::Span{T}) and/or colimit(::Multispan{T}) or, if you have already implemented coproducts and coequalizers, rely on the default implementation.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.pushout_complement-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.pushout_complement","text":"Pushout complement: extend composable pair to a pushout square.\n\nPushout complements are the essential ingredient for double pushout (DPO) rewriting.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.universal","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.universal","text":"Universal property of (co)limits.\n\nCompute the morphism whose existence and uniqueness is guaranteed by the universal property of (co)limits.\n\nSee also: limit, colimit.\n\n\n\n\n\n","category":"function"},{"location":"apis/categorical_algebra/#Catlab.Theories.coequalizer-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.Theories.coequalizer","text":"Coequalizer of morphisms with common domain and codomain.\n\nTo implement for a type T, define the method colimit(::ParallelPair{T}) or colimit(::ParallelMorphisms{T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.copair-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.Theories.copair","text":"Copairing of morphisms: universal property of coproducts/pushouts.\n\nTo implement for coproducts of type T, define the method universal(::BinaryCoproduct{T}, ::Cospan{T}) and/or universal(::Coproduct{T}, ::Multicospan{T}) and similarly for pushouts.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.coproduct-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.Theories.coproduct","text":"Coproduct of objects.\n\nTo implement for a type T, define the method colimit(::ObjectPair{T}) and/or colimit(::DiscreteDiagram{T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.create-Tuple{T} where T","page":"Categorical algebra","title":"Catlab.Theories.create","text":"Unique morphism out of an initial object.\n\nTo implement for a type T, define the method universal(::Initial{T}, ::SMulticospan{0,T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.delete-Tuple{T} where T","page":"Categorical algebra","title":"Catlab.Theories.delete","text":"Unique morphism into a terminal object.\n\nTo implement for a type T, define the method universal(::Terminal{T}, ::SMultispan{0,T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.equalizer-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.Theories.equalizer","text":"Equalizer of morphisms with common domain and codomain.\n\nTo implement for a type T, define the method limit(::ParallelPair{T}) and/or limit(::ParallelMorphisms{T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.factorize-Tuple{Equalizer{Ob, var\"#s126\"} where {Ob, var\"#s126\"<:ParallelMorphisms}, Any}","page":"Categorical algebra","title":"Catlab.Theories.factorize","text":"Factor morphism through (co)equalizer, via the universal property.\n\nTo implement for equalizers of type T, define the method universal(::Equalizer{T}, ::SMultispan{1,T}). For coequalizers of type T, define the method universal(::Coequalizer{T}, ::SMulticospan{1,T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.initial-Tuple{Type}","page":"Categorical algebra","title":"Catlab.Theories.initial","text":"Initial object.\n\nTo implement for a type T, define the method colimit(::EmptyDiagram{T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.pair-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.Theories.pair","text":"Pairing of morphisms: universal property of products/pullbacks.\n\nTo implement for products of type T, define the method universal(::BinaryProduct{T}, ::Span{T}) and/or universal(::Product{T}, ::Multispan{T}) and similarly for pullbacks.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.product-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.Theories.product","text":"Product of objects.\n\nTo implement for a type T, define the method limit(::ObjectPair{T}) and/or limit(::DiscreteDiagram{T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.Theories.terminal-Tuple{Type}","page":"Categorical algebra","title":"Catlab.Theories.terminal","text":"Terminal object.\n\nTo implement for a type T, define the method limit(::EmptyDiagram{T}).\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.@cartesian_monoidal_instance-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.@cartesian_monoidal_instance","text":"Define cartesian monoidal structure using limits.\n\nImplements an instance of CartesianCategory assuming that finite products have been implemented following the limits interface.\n\n\n\n\n\n","category":"macro"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.Limits.@cocartesian_monoidal_instance-Tuple{Any, Any}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.Limits.@cocartesian_monoidal_instance","text":"Define cocartesian monoidal structure using colimits.\n\nImplements an instance of CocartesianCategory assuming that finite coproducts have been implemented following the colimits interface.\n\n\n\n\n\n","category":"macro"},{"location":"apis/categorical_algebra/#Acsets","page":"Categorical algebra","title":"Acsets","text":"","category":"section"},{"location":"apis/categorical_algebra/#Overview-and-Theory","page":"Categorical algebra","title":"Overview and Theory","text":"","category":"section"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"For an in depth look into the theory behind acsets, we refer the reader to our paper on the subject, which also gives some sense as to how the implementation works. Here, we give a brief tutorial before the the API documentation.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"The most essential part of the acset machinery is the schema. The schema parameterizes the acset: each schema corresponds to a different type of acset. Schemas consist of four parts.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"Objects XY ((X,Y,Z)::Ob)\nHomomorphisms f colon X to Y (f :: Hom(X,Y)), which go from objects to objects\nData types mathttT (T :: Data)\nAttributes a colon X to mathttT (a :: Attr(X,T)), which go from objects to data types","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"For those with a categorical background, a schema is a presentation of a category S along with a functor S from S to the arrow category 0 to 1, such that S^-1(1) is discrete.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"An acset F on a schema consists of...","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"a set F(X) of \"primary keys\" for each object\na function F(f) colon F(X) to F(Y) for each morphism\na Julia data type F(mathttT) for each data type mathttT\na function F(a) colon F(X) to F(mathttT) for each attribute a.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"For those with a categorical background, an acset on a schema S consists of a functor from S to mathsfSet, such that objects in S^-1(0) map to finite sets, and objects in S^-1(1) map to sets that represent types. For any particular functor K colon S^-1(1) to mathsfSet, we can also take the category of acsets that restrict to this map on S^-1.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"We can also add relations to this presentation, but we currently do nothing with those relations in the implementation; they mostly serve as documentation.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"We will now give an example of how this all works in practice.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"using Catlab, Catlab.CategoricalAlgebra\n\n# Write down the schema for a weighted graph\n@present TheoryWeightedGraph(FreeSchema) begin\n V::Ob\n E::Ob\n src::Hom(E,V)\n tgt::Hom(E,V)\n T::AttrType\n weight::Attr(E,T)\nend\n\n# Construct the type used to store acsets on the previous schema\n# We *index* src and tgt, which means that we store not only\n# the forwards map, but also the backwards map.\n@acset_type WeightedGraph(TheoryWeightedGraph, index=[:src,:tgt])\n\n# Construct a weighted graph, with floats as edge weights\ng = @acset WeightedGraph{Float64} begin\n V = 4\n E = 5\n src = [1,1,1,2,3]\n tgt = [2,3,4,4,4]\n weight = [7.2, 9.3, 9.4, 0.1, 42.0]\nend","category":"page"},{"location":"apis/categorical_algebra/#API","page":"Categorical algebra","title":"API","text":"","category":"section"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"We first give an overview of the data types used in the acset machinery.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"FreeSchema A finite presentation of a category that will be used as the schema of a database in the algebraic databases conception of categorical database theory. Functors out of a schema into FinSet are combinatorial structures over the schema. Attributes in a schema allow you to encode numerical (any julia type) into the database. You can find several examples of schemas in Catlab.Graphs where they define categorical versions of graph theory.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"CSet/AttributedCSet is a struct/constructors whose values (tables, indices) are parameterized by a CatDesc/AttrDesc. These are in memory databases over the schema equiped with ACSetTranformations as natural transformations that encode relationships between database instances.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"CSetType/AttributedCSetTypeprovides a function to construct a julia type for ACSet instances, parameterized by CatDesc/AttrDesc. This function constructs the new type at runtime. In order to have the interactive nature of Julia, and to dynamically construct schemas based on runtime values, we need to define new Julia types at runtime. This function converts the schema spec to the corresponding Julia type.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"CatDesc/AttrDesc the encoding of a schema into a Julia type. These exist because Julia only allows certain kinds of data in the parameter of a dependent type. Thus, we have to serialize a schema into those primitive data types so that we can use them to parameterize the ACSet type over the schema. This is an implementation detail subject to complete overhaul.","category":"page"},{"location":"apis/categorical_algebra/","page":"Categorical algebra","title":"Categorical algebra","text":"Modules = [\n CategoricalAlgebra.CSets,\n CategoricalAlgebra.StructuredCospans,\n]\nPrivate = false","category":"page"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets","text":"Categories of C-sets and attributed C-sets.\n\n\n\n\n\n","category":"module"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.ACSetTransformation","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.ACSetTransformation","text":"Transformation between attributed C-sets.\n\nA homomorphism of C-sets is a natural transformation: a transformation between functors C → Set satisfying the naturality axiom for all morphisms in C. This struct records the data of a transformation; it does not enforce naturality, but see is_natural.\n\nA C-set transformation has a component for every object in C. When C-sets have attributes, the data types are assumed to be fixed. Thus, the naturality axiom for data attributes is a commutative triangle, rather than a commutative square.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.SubCSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.SubCSet","text":"Sub-C-set of a C-set.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.generate_json_acset-Tuple{T} where T<:ACSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.generate_json_acset","text":"Serialize an ACSet object to a JSON string\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.homomorphism-Tuple{StructACSet, StructACSet}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.homomorphism","text":"Find a homomorphism between two attributed C-sets.\n\nReturns nothing if no homomorphism exists. For many categories C, the C-set homomorphism problem is NP-complete and thus this procedure generally runs in exponential time. It works best when the domain object is small.\n\nThis procedure uses the classic backtracking search algorithm for a combinatorial constraint satisfaction problem (CSP). As is well known, the homomorphism problem for relational databases is reducible to CSP. Since the C-set homomorphism problem is \"the same\" as the database homomorphism problem (insofar as attributed C-sets are \"the same\" as relational databases), it is also reducible to CSP. Backtracking search for CSP is described in many computer science textbooks, such as (Russell & Norvig 2010, Artificial Intelligence, Third Ed., Chapter 6: Constraint satisfaction problems, esp. Algorithm 6.5). In our implementation, the search tree is ordered using the popular heuristic of \"minimum remaining values\" (MRV), also known as \"most constrained variable.\"\n\nTo restrict to monomorphisms, or homomorphisms whose components are all injective functions, set the keyword argument monic=true. To restrict only certain components to be injective or bijective, use monic=[...] or iso=[...]. For example, setting monic=[:V] for a graph homomorphism ensures that the vertex map is injective but imposes no constraints on the edge map.\n\nTo restrict the homomorphism to a given partial assignment, set the keyword argument initial. For example, to fix the first source vertex to the third target vertex in a graph homomorphism, set initial=(V=Dict(1 => 3),).\n\nSee also: homomorphisms, isomorphism.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.homomorphisms-Union{Tuple{S}, Tuple{StructACSet{S, Ts, Idxed, UniqueIdxed} where {Ts<:Tuple, Idxed, UniqueIdxed}, StructACSet{S, Ts, Idxed, UniqueIdxed} where {Ts<:Tuple, Idxed, UniqueIdxed}}} where S","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.homomorphisms","text":"Find all homomorphisms between two attributed C-sets.\n\nThis function is at least as expensive as homomorphism and when no homomorphisms exist, it is exactly as expensive.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.is_homomorphic-Tuple{StructACSet, StructACSet}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.is_homomorphic","text":"Is the first attributed C-set homomorphic to the second?\n\nA convenience function based on homomorphism.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.is_isomorphic-Tuple{StructACSet, StructACSet}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.is_isomorphic","text":"Are the two attributed C-sets isomorphic?\n\nA convenience function based on isomorphism.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.is_natural-Union{Tuple{ACSetTransformation{S, Comp, Dom, Codom} where {Comp<:NamedTuple, Dom<:(StructACSet{S, Ts, Idxed, UniqueIdxed} where {Ts<:Tuple, Idxed, UniqueIdxed}), Codom<:(StructACSet{S, Ts, Idxed, UniqueIdxed} where {Ts<:Tuple, Idxed, UniqueIdxed})}}, Tuple{S}} where S","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.is_natural","text":"Is the transformation between C-sets a natural transformation?\n\nUses the fact that to check whether a transformation is natural, it suffices to check the naturality equation on a generating set of morphisms.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.isomorphism-Tuple{StructACSet, StructACSet}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.isomorphism","text":"Find an isomorphism between two attributed C-sets, if one exists.\n\nSee homomorphism for more information about the algorithms involved.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.isomorphisms-Tuple{StructACSet, StructACSet}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.isomorphisms","text":"Find all isomorphisms between two attributed C-sets.\n\nThis function is at least as expensive as isomorphism and when no homomorphisms exist, it is exactly as expensive.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.parse_json_acset-Union{Tuple{T}, Tuple{Type{T}, Dict}} where T<:ACSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.parse_json_acset","text":"Deserialize a dictionary from a parsed JSON string to an object of the given ACSet type\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.parse_json_acset-Union{Tuple{T}, Tuple{Type{T}, String}} where T<:ACSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.parse_json_acset","text":"Deserialize a JSON string to an object of the given ACSet type\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.read_json_acset-Union{Tuple{T}, Tuple{Type{T}, String}} where T<:ACSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.read_json_acset","text":"Read a JSON file to an object of the given ACSet type\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.CSets.write_json_acset-Union{Tuple{T}, Tuple{T, AbstractString}} where T<:ACSet","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.CSets.write_json_acset","text":"Serialize an ACSet object to a JSON file\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans","text":"Structured cospans.\n\nThis module provides a generic interface for structured cospans with a concrete implementation for attributed C-sets.\n\n\n\n\n\n","category":"module"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan","text":"Structured cospan.\n\nThe first type parameter L encodes a functor L: A → X from the base category A, often FinSet, to a category X with \"extra structure.\" An L-structured cospan is then a cospan in X whose feet are images under L of objects in A. The category X is assumed to have pushouts.\n\nStructured cospans form a double category with no further assumptions on the functor L. To obtain a symmetric monoidal double category, L must preserve finite coproducts. In practice, L usually has a right adjoint R: X → A, which implies that L preserves all finite colimits. It also allows structured cospans to be constructed more conveniently from an object x in X plus a cospan in A with apex R(x).\n\nSee also: StructuredMulticospan.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan-Union{Tuple{L}, Tuple{Any, Multicospan{Ob, Hom, var\"#s126\"} where {Ob, Hom, var\"#s126\"<:StaticArrays.StaticVector{2, Hom}}}} where L","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan","text":"Construct structured cospan in R-form.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan-Union{Tuple{L}, Tuple{Multicospan{Ob, Hom, var\"#s126\"} where {Ob, Hom, var\"#s126\"<:StaticArrays.StaticVector{2, Hom}}, StaticArrays.StaticVector{2, T} where T}} where L","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospan","text":"Construct structured cospan in L-form.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospanOb","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.StructuredCospanOb","text":"Object in the category of L-structured cospans.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan","text":"Structured multicospan.\n\nA structured multicospan is like a structured cospan except that it may have a number of legs different than two.\n\nSee also: StructuredCospan.\n\n\n\n\n\n","category":"type"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan-Union{Tuple{L}, Tuple{Any, Multicospan}} where L","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.StructuredMulticospan","text":"Construct structured multicospan in R-form.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.OpenACSetTypes-Union{Tuple{X}, Tuple{S}, Tuple{Type{X}, Symbol}} where {S<:Catlab.Theories.SchemaDescType, X<:(StructACSet{S, Ts, Idxed, UniqueIdxed} where {Ts<:Tuple, Idxed, UniqueIdxed})}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.OpenACSetTypes","text":"Create types for open attributed C-sets from an attributed C-set type.\n\nNote: the type passed in should not be instantiated with concrete attribute types.\n\nThe resulting types, for objects and morphisms, each have the same type parameters for data types as the original type.\n\nSee also: OpenCSetTypes.\n\n\n\n\n\n","category":"method"},{"location":"apis/categorical_algebra/#Catlab.CategoricalAlgebra.StructuredCospans.OpenCSetTypes-Union{Tuple{X}, Tuple{S}, Tuple{Type{X}, Symbol}} where {S<:(Catlab.Theories.SchemaDescType{obs, homs, (), (), doms, codoms} where {obs, homs, doms, codoms}), X<:(StructCSet{S, Idxed, UniqueIdxed} where {Idxed, UniqueIdxed})}","page":"Categorical algebra","title":"Catlab.CategoricalAlgebra.StructuredCospans.OpenCSetTypes","text":"Create types for open C-sets from a C-set type.\n\nReturns two types, for objects, a subtype of StructuredCospanOb, and for morphisms, a subtype of StructuredMulticospan.\n\nSee also: OpenACSetTypes.\n\n\n\n\n\n","category":"method"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/sketches/preorders.jl\"","category":"page"},{"location":"generated/sketches/preorders/#Preorders","page":"Preorders","title":"Preorders","text":"","category":"section"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"(Image: )","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Many of the ideas in category theory can be viewed as generalizations of preorders or monoids. This sketch shows some features of Catlab through the lens of preorders. You will see examples of defining GATs, Presentations, Syntax, and Functors. These are illustrated with preorders or thin categories, which are particularly simple cases of categories.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"using Core: GeneratedFunctionStub\nusing Test\n\nusing Catlab, Catlab.Theories, Catlab.CategoricalAlgebra\nimport Catlab.Theories: compose","category":"page"},{"location":"generated/sketches/preorders/#Definition-of-a-Preorder-formalized-as-a-GAT","page":"Preorders","title":"Definition of a Preorder formalized as a GAT","text":"","category":"section"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"The following definitions can be found in the Catlab.Theories module.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"\"\"\" Theory of *preorders*\n\nPreorders encode the axioms of reflexivity and transitivity as term constructors.\n\"\"\"\n@theory Preorder{El,Leq} begin\n El::TYPE\n Leq(lhs::El, rhs::El)::TYPE\n @op (≤) := Leq\n\n # Preorder axioms are lifted to term constructors in the GAT.\n reflexive(A::El)::(A≤A) # ∀ A there is a term reflexive(A) which implies A≤A\n transitive(f::(A≤B), g::(B≤C))::(A≤C) ⊣ (A::El, B::El, C::El)\n\n # Axioms of the GAT are equivalences on terms or simplification rules in the logic\n f == g ⊣ (A::El, B::El, f::(A≤B), g::(A≤B))\n # Read as (f⟹ A≤B ∧ g⟹ A≤B) ⟹ f ≡ g\nend","category":"page"},{"location":"generated/sketches/preorders/#Preorders-are-Thin-Categories","page":"Preorders","title":"Preorders are Thin Categories","text":"","category":"section"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Definition of a thin category","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@theory ThinCategory{Ob,Hom} <: Category{Ob,Hom} begin\n f == g ⊣ (A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B))\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"of course this definition extends the GAT of categories","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@theory Category{Ob,Hom} begin\n # Unicode aliases.\n @op begin\n (→) := Hom\n (⋅) := compose\n end\n\n \"\"\" Object in a category \"\"\"\n Ob::TYPE\n\n \"\"\" Morphism in a category \"\"\"\n Hom(dom::Ob,codom::Ob)::TYPE\n\n id(A::Ob)::(A → A)\n compose(f::(A → B), g::(B → C))::(A → C) ⊣ (A::Ob, B::Ob, C::Ob)\n\n # Category axioms.\n ((f ⋅ g) ⋅ h == f ⋅ (g ⋅ h)\n ⊣ (A::Ob, B::Ob, C::Ob, D::Ob, f::(A → B), g::(B → C), h::(C → D)))\n f ⋅ id(B) == f ⊣ (A::Ob, B::Ob, f::(A → B))\n id(A) ⋅ f == f ⊣ (A::Ob, B::Ob, f::(A → B))\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Exercise: construct an isomorphism between the theory of thin categories and the theory of preorders. Show that they have the same models.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Once you have a GAT defined using the @theory macro, you can define presentations, which are logical syntax for giving examples of the theory. The GAT contains type and term constructors that you can use to write expressions. A presentation uses those expressions to create a specific example of the theory. We define P to be a preorder with 3 elements and 2 ≤ relationships.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@present P(FreeThinCategory) begin\n (X,Y,Z)::Ob\n f::Hom(X,Y)\n g::Hom(Y,Z)\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"another example","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@present Q(FreeThinCategory) begin\n (X,Y,Z)::Ob\n f::Hom(X,Y)\n g::Hom(Y,Z)\n Y′::Ob\n f′::Hom(X,Y′)\n g′::Hom(Y′,Z)\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Exercise: draw the Hasse diagrams for these preorders by hand.","category":"page"},{"location":"generated/sketches/preorders/#Composition-is-transitivity","page":"Preorders","title":"Composition is transitivity","text":"","category":"section"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"expressions in the presentation are paths in the Hasse Diagram","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"function compose(P::Presentation, vs::Vector{Symbol})\n compose(collect(generator(P, v) for v in vs))\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"expressions are represented at expression trees","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"ex = compose(P, [:f, :g])","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"the head of an expression is the root of the expression tree","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Catlab.head(ex)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"the julia type of the expression","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"typeof(ex)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"the GAT type of the expression","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"gat_typeof(ex)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"the parameters of the GAT Type","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"gat_type_args(ex)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"in any thin category there is at most one morphism between any pair of objects. In symbols: ex₁::Hom(X,Y) ∧ ex₂::Hom(X,Y) ⟹ ex₁ == ex₂","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"function thinequal(ex₁::FreeThinCategory.Hom, ex₂::FreeThinCategory.Hom)\n dom(ex₁) == dom(ex₂) && codom(ex₁) == codom(ex₂)\nend\n\n@test thinequal(ex, compose(P, [:f,:g])⋅id(generator(P,:Z)))","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Thinking in terms of preorders, the composite f⋅g::Hom(X,Z) is a proof that X ≤ Z in logical notation you would say f::Hom(X,Y) and g::Hom(Y,Z) ⊢ f⋅g::Hom(X,Z) given a proof that X≤Y and a proof of Y≤Z then ⋅ will create a proof of X≤Z by composing the proofs sequentially like chaining inequalities in math a key aspect of category theory is that you want to work constructively you don't want to know that there exists a composite, you want to hold onto that composite. in programming, the way that you hold onto things is putting data into data structures. While computers can access things by offset or addresses, programmers want to use names so when we prove in P that X≤Z, we name that proof by adding it as a generator","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@present P₂(FreeThinCategory) begin\n (X,Y,Z)::Ob\n f::Hom(X,Y)\n g::Hom(Y,Z)\n h::Hom(X,Z)\nend\n\nex = compose(P₂, [:f, :g])","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Now that we have a name for h, we can see that thinequal knows that f⋅g == h because according to the definition of a thin category, any two morphisms with the same domain and codomain are equal.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@test thinequal(ex, generator(P₂, :h))","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"There is an imperative interface to manipulating presentations by mutating them for this purpose","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"P₂′ = copy(P)\nadd_generator!(P₂′, Hom(:h, P[:X], P[:Z]))\ngenerators(P₂′)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"We could avoid this naming the homs situation by giving all the homs the same name however, then when you tried to write down a morphism, you wouldn't be able to refer to a specific one by name, because they are all named ≤.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@present R(FreeThinCategory) begin\n (x,y,z)::Ob\n (≤)::Hom(x,y)\nend\ngenerators(R)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Catlab won't let you make a presentation where the homs have the same exact name. So, this will error:","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@present Q(FreeThinCategory) begin\n (x,y,z)::Ob\n (≤)::Hom(x,y)\n (≤)::Hom(y,z)\n (≤)::Hom(x,z)\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"However, you can omit the names for homs with the following syntax, which is useful for thin categories.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"@present Q(FreeThinCategory) begin\n (x,y,z)::Ob\n ::Hom(x,y)\n ::Hom(y,z)\n ::Hom(x,z)\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"In a thin category, all the homs with the same domain and codomain are the same, so why don't we name them by their the domain and codomain and then use the property that any two homs with the same name are the same to encode the thinness. This is what the Hasse diagram representation does for us. The edges in the diagram are encoding the presentation data into a combinatorial object that we can visualize. There are many reasons to encode a logical structure into a combinatorial strucuture, one is that we generally have ways of drawing combinatorial objects that convey their saliant structure and enable visual reasoning. Another is algorithms, isomorphism between the combinatorial representations provide some of the isomorphisms between the logical structures. in this case, a graph homomorphism between Hasse Diagrams construct isomorphisms between the preorders they present. The converse is not true since there can be many Graphs that present the same preorder.","category":"page"},{"location":"generated/sketches/preorders/#Monotone-Maps","page":"Preorders","title":"Monotone Maps","text":"","category":"section"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"we can access the objects of a presentation by filtering on the gat_typeof","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"objects(P::Presentation) = filter(generators(P)) do x\n gat_typeof(x) == :Ob\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"we can access the homs of a presentation by filtering on the gat_typeof","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"homs(P::Presentation) = filter(generators(P)) do x\n gat_typeof(x) == :Hom\nend","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"a generator is in the set of homs if it is in the list of generators","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"in_homs(f::FreeThinCategory.Hom{:generator}, P::Presentation) =\n f in generators(P)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"a composite hom is in the list set of homs if all of its components are.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"in_homs(f::FreeThinCategory.Hom{:compose}, P::Presentation) =\n all(map(fᵢ->in_homs(fᵢ, P), args(f)))","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"we can check if a map is functorial, which is called monotone for preorders.","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"make sure all the objects in the domain are sent to objects in the codomain\nmake sure all the homs are sent to homs in the codomain\ncheck that the domains and codomainss of the homs match","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"function is_functorial(F::Functor)\n pₒ = map(objects(dom(F))) do X\n Ob(F)[X] in generators(codom(F))\n end |> all\n\n pₕ = map(homs(dom(F))) do f\n in_homs(Hom(F)[f], codom(F))\n end |> all\n\n pᵩ = map(homs(dom(F))) do f\n FX = Ob(F)[dom(f)]\n Ff = Hom(F)[f]\n FY = Ob(F)[codom(f)]\n dom(Ff) == FX && codom(Ff) == FY\n end |> all\n return pₒ && pₕ && pᵩ\nend\n\n@present Q(FreeThinCategory) begin\n (a,b,c,d)::Ob\n ab::Hom(a,b)\n bc::Hom(b,c)\n cd::Hom(c,d)\nend\ngenerators(Q)\n\nFₒ = Dict(:X=>:a, :Y=>:b, :Z=>:c)\nFₕ = Dict(:f=>:ab, :g=>:bc)\nF = Functor(Fₒ, Fₕ, P, Q)\n@test is_functorial(F)\n\nFₒ = Dict(:X=>:a, :Y=>:b, :Z=>:d)\nFₕ = Dict(:f=>:ab, :g=>[:bc, :cd])\nF = Functor(Fₒ, Fₕ, P, Q)\n@test is_functorial(F)\n\n\nFₒ = Dict(:X=>:a, :Y=>:b, :Z=>:c)\nFₕ = Dict(:f=>:ab, :g=>[:bc, :cd])\nF = Functor(Fₒ, Fₕ, P, Q)\n@test !is_functorial(F)","category":"page"},{"location":"generated/sketches/preorders/","page":"Preorders","title":"Preorders","text":"Monotone maps are functors for thin categories. One of the benefits of category theory is that we find abstractions that work in multiple domains. The abstraction of preserving the domains and codomains of morphisms is a key abstraction that we can use to define many notions in mathematics.","category":"page"},{"location":"apis/wiring_diagrams/#wiring_diagrams","page":"Wiring diagrams","title":"Wiring diagrams","text":"","category":"section"},{"location":"apis/wiring_diagrams/","page":"Wiring diagrams","title":"Wiring diagrams","text":"Modules = [\n WiringDiagrams.DirectedWiringDiagrams,\n WiringDiagrams.UndirectedWiringDiagrams,\n WiringDiagrams.MonoidalDirectedWiringDiagrams,\n WiringDiagrams.WiringDiagramAlgorithms,\n WiringDiagrams.WiringDiagramSerialization,\n WiringDiagrams.GraphMLWiringDiagrams,\n WiringDiagrams.JSONWiringDiagrams,\n]\nPrivate = false","category":"page"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams","text":"Data structure for (directed) wiring diagrams, aka string diagrams.\n\nA (directed) wiring diagram consists of a collection of boxes with input and output ports connected by wires. A box can be atomic (possessing no internal structure) or can itself be a wiring diagram. Thus, wiring diagrams can be nested recursively. Wiring diagrams are closely related to what the CS literature calls \"directed graphs with ports\" or more simply \"port graphs\". The main difference is that a wiring diagram has an \"outer box\": a wiring diagram has its own ports that can be connected to the ports of its boxes.\n\nThis module provides a generic data structure for wiring diagrams. Arbitrary data can be attached to the boxes, ports, and wires of a wiring diagram. The diagrams are \"abstract\" in the sense that they cannot be directly rendered as raster or vector graphics. However, they form a useful intermediate representation that can be serialized to and from GraphML or translated into Graphviz or other declarative diagram languages.\n\n\n\n\n\n","category":"module"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.AbstractBox","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.AbstractBox","text":"Base type for any box (node) in a wiring diagram.\n\nThis type represents an arbitrary black box with inputs and outputs.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.Box","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.Box","text":"An atomic box in a wiring diagram.\n\nThese boxes have no internal structure.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.Port","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.Port","text":"A port on a box to which wires can be connected.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.PortKind","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.PortKind","text":"Kind of port: input or output.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.Wire","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.Wire","text":"A wire connecting one port to another.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.encapsulate-Tuple{WiringDiagram, Vector{Int64}}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.encapsulate","text":"Encapsulate multiple boxes within a single sub-diagram.\n\nThis operation is a (one-sided) inverse to subsitution, see substitute.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.encapsulated_subdiagram-Union{Tuple{WD}, Tuple{WD, Vector{Int64}}} where WD<:WiringDiagram","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.encapsulated_subdiagram","text":"Create an encapsulating box for a set of boxes in a wiring diagram.\n\nTo a first approximation, the union of input ports of the given boxes will become the inputs ports of the encapsulating box and likewise for the output ports. However, when copies or merges occur, as in a cartesian or cocartesian category, a simplification procedure may reduce the number of ports on the encapsulating box.\n\nSpecifically:\n\nEach input port of an encapsulated box will have at most one incoming wire\n\nfrom the encapsulating outer box, and each output port of an encapsulated box will have at most one outgoing wire to the encapsulating outer box.\n\nA set of ports connected to the same outside (non-encapsulated) ports will be\n\nsimplified into a single port of the encapsulating box.\n\nSee also induced_subdiagram.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.graph-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.graph","text":"Grapn underlying wiring diagram, including parts for noin-internal wires.\n\nThe graph has two special vertices representing the input and output boundaries of the outer box.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.in_wires-Tuple{WiringDiagram, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.in_wires","text":"Get all wires coming into the box.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.in_wires-Tuple{WiringDiagram, Port}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.in_wires","text":"Get all wires coming into the port.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.induced_subdiagram-Union{Tuple{T}, Tuple{WiringDiagram{T, PortValue, WireValue, BoxValue} where {PortValue, WireValue, BoxValue}, Vector{Int64}}} where T","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.induced_subdiagram","text":"The wiring diagram induced by a subset of its boxes.\n\nSee also encapsulated_subdiagram.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.internal_graph-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.internal_graph","text":"Graph underlying wiring diagram, with edges for internal wires only.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.ocompose-Tuple{WiringDiagram, Vector{var\"#s125\"} where var\"#s125\"<:WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.ocompose","text":"Operadic composition of wiring diagrams.\n\nThis generic function has two different signatures, corresponding to the \"full\" and \"partial\" notions of operadic composition (Yau, 2018, Operads of Wiring Diagrams, Definitions 2.3 and 2.10).\n\nThis operation is a simple wrapper around substitute.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.out_wires-Tuple{WiringDiagram, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.out_wires","text":"Get all wires coming out of the box.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.out_wires-Tuple{WiringDiagram, Port}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.out_wires","text":"Get all wires coming out of the port.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.singleton_diagram-Tuple{Type, AbstractBox}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.singleton_diagram","text":"Wiring diagram with a single box connected to the outer ports.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.substitute-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.substitute","text":"Substitute wiring diagrams for boxes.\n\nPerforms one or more substitutions. When performing multiple substitutions, the substitutions are simultaneous.\n\nThis operation implements the operadic composition of wiring diagrams, see also ocompose.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.validate_ports-Tuple{Any, Any}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.validate_ports","text":"Check compatibility of source and target ports.\n\nThe default implementation is a no-op.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.wires-Tuple{WiringDiagram, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.wires","text":"Get all wires coming into or out of the box.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.UndirectedWiringDiagrams","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.UndirectedWiringDiagrams","text":"Data structure for undirected wiring diagrams.\n\n\n\n\n\n","category":"module"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.DirectedWiringDiagrams.add_wire!-Tuple{Catlab.WiringDiagrams.UndirectedWiringDiagrams.AbstractUWD, Tuple{Int64, Int64}, Tuple{Int64, Int64}}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.DirectedWiringDiagrams.add_wire!","text":"Wire together two ports in an undirected wiring diagram.\n\nA convenience method that creates and sets junctions as needed. Ports are only allowed to have one junction, so if both ports already have junctions, then the second port is assigned the junction of the first. The handling of the two arguments is otherwise symmetric.\n\nFIXME: When both ports already have junctions, the two junctions should be merged. To do this, we must implement merge_junctions! and thus also rem_part!.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.UndirectedWiringDiagrams.cospan_diagram-Union{Tuple{UWD}, Tuple{Type{UWD}, Catlab.CategoricalAlgebra.Sets.SetFunction{Dom, Codom} where {Dom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T), Codom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T)}, Catlab.CategoricalAlgebra.Sets.SetFunction{Dom, Codom} where {Dom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T), Codom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T)}}, Tuple{Type{UWD}, Catlab.CategoricalAlgebra.Sets.SetFunction{Dom, Codom} where {Dom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T), Codom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T)}, Catlab.CategoricalAlgebra.Sets.SetFunction{Dom, Codom} where {Dom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T), Codom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T)}, Any}} where UWD<:Catlab.WiringDiagrams.UndirectedWiringDiagrams.AbstractUWD","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.UndirectedWiringDiagrams.cospan_diagram","text":"Undirected wiring diagram defined by a cospan.\n\nThe wiring diagram has a single box. The ports of this box, the outer ports, the junctions, and the connections between them are defined by the cospan. Thus, this function generalizes singleton_diagram.\n\nSee also: junction_diagram.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.UndirectedWiringDiagrams.junction_diagram-Union{Tuple{UWD}, Tuple{Type{UWD}, Catlab.CategoricalAlgebra.Sets.SetFunction{Dom, Codom} where {Dom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T), Codom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T)}}, Tuple{Type{UWD}, Catlab.CategoricalAlgebra.Sets.SetFunction{Dom, Codom} where {Dom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T), Codom<:(Catlab.CategoricalAlgebra.FinSets.FinSet{Int64, T} where T)}, Any}} where UWD<:Catlab.WiringDiagrams.UndirectedWiringDiagrams.AbstractUWD","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.UndirectedWiringDiagrams.junction_diagram","text":"Undirected wiring diagram with no boxes, only junctions.\n\nSee also: singleton_diagram, cospan_diagram.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams","text":"Wiring diagrams as a symmetric monoidal category.\n\nThis module provides a high-level categorical interface to wiring diagrams, building on the low-level imperative interface and the operadic interface. It also defines data types and functions to represent diagonals, codiagonals, duals, caps, cups, daggers, and other gadgets in wiring diagrams.\n\n\n\n\n\n","category":"module"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.BoxOp","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.BoxOp","text":"Box wrapping another box.\n\nRepresents unary operations on boxes in wiring diagrams.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.Junction","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.Junction","text":"Junction node in a wiring diagram.\n\nJunction nodes are used to explicitly represent copies, merges, deletions, creations, caps, and cups.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.PortOp","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.PortOp","text":"Port value wrapping another value.\n\nRepresents unary operations on ports in wiring diagrams.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.Ports","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.Ports","text":"A list of ports.\n\nThe objects in categories of wiring diagrams.\n\n\n\n\n\n","category":"type"},{"location":"apis/wiring_diagrams/#Catlab.Syntax.functor-Tuple{WiringDiagram, Any, Any}","page":"Wiring diagrams","title":"Catlab.Syntax.functor","text":"Apply functor in a category of wiring diagrams.\n\nDefined by compatible mappings of ports and boxes.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.add_junctions-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.add_junctions","text":"Add junction nodes to wiring diagram.\n\nTransforms from the implicit to the explicit representation of diagonals and codiagonals. This operation is inverse to rem_junctions.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.implicit_mcopy-Tuple{Ports, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.implicit_mcopy","text":"Implicit copy in wiring diagram.\n\nCopies are represented by multiple outgoing wires from a single port and deletions by no outgoing wires.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.implicit_mmerge-Tuple{Ports, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.implicit_mmerge","text":"Implicit merge in wiring diagram.\n\nMerges are represented by multiple incoming wires into a single port and creations by no incoming wires.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junction_caps-Tuple{Ports}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junction_caps","text":"Wiring diagram of nested caps made out of junction nodes.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junction_cups-Tuple{Ports}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junction_cups","text":"Wiring diagram of nested cups made out of junction nodes.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junctioned_mcopy-Tuple{Ports, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junctioned_mcopy","text":"Explicit copy in wiring diagram.\n\nCopies and deletions are represented by junctions (boxes of type Junction).\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junctioned_mmerge-Tuple{Ports, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.junctioned_mmerge","text":"Explicit merge in wiring diagram.\n\nMerges and creations are represented by junctions (boxes of type Junction).\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.merge_junctions-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.merge_junctions","text":"Merge adjacent junction nodes into single junctions.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.rem_junctions-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.MonoidalDirectedWiringDiagrams.rem_junctions","text":"Remove junction nodes from wiring diagram.\n\nTransforms from the explicit to the implicit representation of diagonals and codiagonals. This operation is inverse to add_junctions.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.UndirectedWiringDiagrams.junction_diagram-Tuple{Ports, Int64, Int64}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.UndirectedWiringDiagrams.junction_diagram","text":"Wiring diagram with a junction node for each of the given ports.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.WiringDiagramAlgorithms","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.WiringDiagramAlgorithms","text":"Algorithms on wiring diagrams.\n\n\n\n\n\n","category":"module"},{"location":"apis/wiring_diagrams/#Catlab.Graphs.GraphAlgorithms.topological_sort-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.Graphs.GraphAlgorithms.topological_sort","text":"Topological sort of boxes in wiring diagram.\n\nReturns a list of box IDs, excluding the outer box's input and output IDs.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.WiringDiagramAlgorithms.crossing_minimization_by_sort-Tuple{WiringDiagram, AbstractVector{Int64}}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.WiringDiagramAlgorithms.crossing_minimization_by_sort","text":"Crossing minimization by sorting a univariate statistic.\n\nThe boxes in sources and/or targets are fixed and the boxes in vs are permuted. A permutation σ of the latter is returned, such that vs[σ] are the sorted box IDs. Both one-sided and two-sided crossing minimization are supported, depending on whether just one, or both, of sources and targets are given.\n\nIn this simple but popular heuristic algorithm, the boxes are permuted by sorting a univariate statistic of the positions of incoming and/or outgoing wires. Typical choices are:\n\nmean: the sample mean, yielding the \"barycenter method\"\nmedian: the sample median\n\nIn both cases, this algorithm has the property that if there is a permutation with no crossings, it will find it.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.WiringDiagramAlgorithms.normalize_cartesian!-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.WiringDiagramAlgorithms.normalize_cartesian!","text":"Put a wiring diagram for a cartesian category into normal form.\n\nThis function puts a wiring diagram representing a morphism in a free cartesian category into normal form. Copies and deletions are simplified as much as possible.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.WiringDiagramAlgorithms.normalize_copy!-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.WiringDiagramAlgorithms.normalize_copy!","text":"Normalize copies in a wiring diagram.\n\nThis function maximizes sharing of intermediate computations in a wiring diagram where copies are natural.\n\nThis algorithm is basically the same as the congruence closure algorithm on term graphs, in the special case of the empty relation R = ∅ (Baader & Nipkow, 1998, Term Rewriting and All That, Sec. 4.4). The main difference is the possibility of zero or many function outputs.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.WiringDiagramAlgorithms.normalize_delete!-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.WiringDiagramAlgorithms.normalize_delete!","text":"Normalize deletions in a wiring diagram.\n\nThis function removes all unused intermediate computations in a wiring diagram where deletion is natural.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.WiringDiagramSerialization","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.WiringDiagramSerialization","text":"Conventions for serialization of wiring diagrams.\n\nDefines a consistent set of names for boxes, ports, and wires to be used when serializing wiring diagrams, as well as conventions for serializing box, port, and wire attributes.\n\n\n\n\n\n","category":"module"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.GraphMLWiringDiagrams","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.GraphMLWiringDiagrams","text":"Serialize abstract wiring diagrams as GraphML.\n\nSerialization of box, port, and wire values can be overloaded by data type (see convert_to_graphml_data and convert_from_graphml_data).\n\nGraphML is the closest thing to a de jure and de facto standard in the space of graph data formats, supported by a variety of graph applications and libraries. We depart mildly from the GraphML spec by allowing JSON data attributes for GraphML nodes, ports, and edges.\n\nReferences:\n\nGraphML Primer: http://graphml.graphdrawing.org/primer/graphml-primer.html\nGraphML DTD: http://graphml.graphdrawing.org/specification/dtd.html\n\n\n\n\n\n","category":"module"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.GraphMLWiringDiagrams.generate_graphml-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.GraphMLWiringDiagrams.generate_graphml","text":"Generate GraphML representing a wiring diagram.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.GraphMLWiringDiagrams.parse_graphml-Tuple{Type, Type, Type, AbstractString}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.GraphMLWiringDiagrams.parse_graphml","text":"Parse a wiring diagram from a GraphML string or XML document.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.GraphMLWiringDiagrams.read_graphml-Tuple{Type, Type, Type, String}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.GraphMLWiringDiagrams.read_graphml","text":"Read a wiring diagram from a GraphML file.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.GraphMLWiringDiagrams.write_graphml-Tuple{WiringDiagram, String}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.GraphMLWiringDiagrams.write_graphml","text":"Write a wiring diagram to a file as GraphML.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.JSONWiringDiagrams","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.JSONWiringDiagrams","text":"Serialize abstract wiring diagrams as JSON.\n\nJSON data formats are convenient when programming for the web. Unfortunately, no standard for JSON graph formats has gained any kind of widespread adoption. We adopt a format compatible with that used by the KEILER project and its successor ELK (Eclipse Layout Kernel). This format is roughly feature compatible with GraphML, supporting nested graphs and ports. It also supports layout information like node position and size.\n\nReferences:\n\nKEILER's JSON graph format: https://rtsys.informatik.uni-kiel.de/confluence/display/KIELER/JSON+Graph+Format\nELK's JSON graph format: https://www.eclipse.org/elk/documentation/tooldevelopers/graphdatastructure/jsonformat.html\n\n\n\n\n\n","category":"module"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.JSONWiringDiagrams.generate_json_graph-Tuple{WiringDiagram}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.JSONWiringDiagrams.generate_json_graph","text":"Generate a JSON dict representing a wiring diagram.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.JSONWiringDiagrams.parse_json_graph-Tuple{Type, Type, Type, Union{AbstractString, IO}}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.JSONWiringDiagrams.parse_json_graph","text":"Parse a wiring diagram from a JSON string or dict.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.JSONWiringDiagrams.read_json_graph-Tuple{Type, Type, Type, String}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.JSONWiringDiagrams.read_json_graph","text":"Read a wiring diagram from a JSON file.\n\n\n\n\n\n","category":"method"},{"location":"apis/wiring_diagrams/#Catlab.WiringDiagrams.JSONWiringDiagrams.write_json_graph-Tuple{WiringDiagram, String}","page":"Wiring diagrams","title":"Catlab.WiringDiagrams.JSONWiringDiagrams.write_json_graph","text":"Write a wiring diagram to a file as JSON.\n\n\n\n\n\n","category":"method"},{"location":"generated/graphics/graphviz_schema_visualization/","page":"Visualizing Acset Schemas with Graphviz","title":"Visualizing Acset Schemas with Graphviz","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/graphics/graphviz_schema_visualization.jl\"","category":"page"},{"location":"generated/graphics/graphviz_schema_visualization/#Visualizing-Acset-Schemas-with-Graphviz","page":"Visualizing Acset Schemas with Graphviz","title":"Visualizing Acset Schemas with Graphviz","text":"","category":"section"},{"location":"generated/graphics/graphviz_schema_visualization/","page":"Visualizing Acset Schemas with Graphviz","title":"Visualizing Acset Schemas with Graphviz","text":"(Image: )","category":"page"},{"location":"generated/graphics/graphviz_schema_visualization/","page":"Visualizing Acset Schemas with Graphviz","title":"Visualizing Acset Schemas with Graphviz","text":"It is convenient to visualize schemas in a non-textual way; often schemas can have many objects, homs and attributes, and it is hard to keep these all in your head.","category":"page"},{"location":"generated/graphics/graphviz_schema_visualization/","page":"Visualizing Acset Schemas with Graphviz","title":"Visualizing Acset Schemas with Graphviz","text":"For this reason, we provide a function which takes a schema and produces a visual representation of it, using the Catlab Graphviz interface.","category":"page"},{"location":"generated/graphics/graphviz_schema_visualization/","page":"Visualizing Acset Schemas with Graphviz","title":"Visualizing Acset Schemas with Graphviz","text":"This is as simple as the following code. These figures are by no means publication-quality, but they can be useful for interactive development.","category":"page"},{"location":"generated/graphics/graphviz_schema_visualization/","page":"Visualizing Acset Schemas with Graphviz","title":"Visualizing Acset Schemas with Graphviz","text":"using Catlab.Present, Catlab.Graphics, Catlab.Graphs\n\nto_graphviz(Graphs.BasicGraphs.TheoryWeightedGraph)","category":"page"},{"location":"#Catlab.jl","page":"Catlab.jl","title":"Catlab.jl","text":"","category":"section"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Catlab.jl is a framework for applied and computational category theory, written in the Julia language. Catlab provides a programming library and interactive interface for applications of category theory to scientific and engineering fields. It emphasizes monoidal categories due to their wide applicability but can support any categorical structure that is formalizable as a generalized algebraic theory.","category":"page"},{"location":"#What-is-Catlab?","page":"Catlab.jl","title":"What is Catlab?","text":"","category":"section"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Catlab is, or will eventually be, the following things.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Programming library: First and foremost, Catlab provides data structures, algorithms, and serialization for applied category theory. Macros offer a convenient syntax for specifying categorical doctrines and type-safe symbolic manipulation systems. Wiring diagrams (aka string diagrams) are supported through specialized data structures and can be serialized to and from GraphML (an XML-based format) and JSON.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Interactive computing environment: Catlab can also be used interactively in Jupyter notebooks. Symbolic expressions are displayed using LaTeX and wiring diagrams are visualized using Compose.jl, Graphviz, or TikZ.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Computer algebra system: Catlab will serve as a computer algebra system for categorical algebra. Unlike most computer algebra systems, all expressions are typed using fragment of dependent type theory called generalized algebraic theories. We will implement core algorithms for solving word problems and reducing expressions to normal form with respect to several important doctrines, such as those of categories and of symmetric monoidal categories. For the computer algebra of classical abstract algebra, see AbstractAlgebra.jl and Nemo.jl.","category":"page"},{"location":"#What-is-Catlab-not?","page":"Catlab.jl","title":"What is Catlab not?","text":"","category":"section"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Catlab is not currently any of the following things, although we do not rule out that it could eventually evolve in these directions.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Automated theorem prover: Although there is some overlap between computer algebra and automated theorem proving, Catlab cannot be considered a theorem prover because it does not produce formal certificates of correctness (aka proofs).","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Proof assistant: Likewise, Catlab is not a proof assistant because it does not produce formally verifiable proofs. Formal verification is not within scope of the project.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Graphical user interface: Catlab does not provide a wiring diagram editor or other graphical user interface. It is primarily a programming library, not a user-facing application. However, there is another project in the AlgebraicJulia ecosystem, Semagrams.jl which does provide graphical user interfaces for interacting with wiring diagrams, Petri nets, and the like.","category":"page"},{"location":"#What-is-a-GAT?","page":"Catlab.jl","title":"What is a GAT?","text":"","category":"section"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Generalized Algebraic Theories (GATs) are the backbone of Catlab so let's expand a bit on GATs and how they fit into the bigger picture of algebra.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"An algebraic structure, like a group or category, is a mathematical object whose axioms all take the form of equations that are universally quantified (the equations have no exceptions). That’s not a formal definition but it’s a good heuristic. There are different ways to make this precise. The oldest, going back to universal algebra in the early 20th centrury, are algebraic theories.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Universal algebra (sometimes called general algebra) is the field of mathematics that studies algebraic structures themselves, not examples (\"models\") of algebraic structures. For instance, rather than take particular groups as the object of study, in universal algebra one takes the class of groups as an object of study. In an algebraic theory, you have a collection of (total) operations and they obey a set of equational axioms. Classically, there is only a single generating type, but there are also typed or multi-sorted versions of algebraic theories. Most of the classical structures of abstract algebra, such as groups, rings, and modules, can be defined as algebraic theories.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Importantly, the theory of categories is not algebraic. In other words, a category cannot be defined as a (multi-sorted) algebraic theory. The reason is that the operation of composition is partial, since you can only compose morphisms with compatible (co)domains. Now, categories sure feel like algebraic structures, so people have come up with generalizations of algebraic theories that accomodate categories and related structures.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"The first of these was Freyd’s essentially algebraic theories. In an essentially algebraic theory, you can have partially defined operations; however, to maintain the equational character of the system, the domains of operations must themselves be defined equationally. For example, the theory of categories would be defined as having two types, Ob and Hom, and the composition operation compose(f::Hom,g::Hom)::Hom would have domain given by the equation codom(f) == dom(g). As your theories get more elaborate, the sets of equations defining the domains get more complicated and reasoning about the structure is overwhelming.","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Later, Cartmell proposed generalized algebraic theories, which solves the same problem but in a different way. Rather than having partial operations, you have total operations but on dependent types (types that are parameterized by values). So now the composition operation has signature compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) where (A::Ob, B::Ob, C::Ob) exactly as appears in Catlab. This is closer to the way that mathematicians actually think and write about categories. For example, if you look at the definitions of category, functor, and natural transformation in Emily Riehl’s textbook, you will see that they are already essentially in the form of a GAT, whereas they require translation into an essentially algebraic theory. Nevertheless, GATs and essentially algebraic theories have the same expressive power, at least in their standard set-based semantics. GATs provide a version of the computer scientist's type theory that plays well with the mathematician's algebra, thus, providing a perfect opportunity for computer algebra systems.","category":"page"},{"location":"#Overview-of-Key-Components","page":"Catlab.jl","title":"Overview of Key Components","text":"","category":"section"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"There are several core parts to the Catlab design, we start with a brief overview of each one","category":"page"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Catlab.GAT provides @theory - defines a new Generalized Algebraic Theory. These are algebraic versions of what a logician would call a logical theory. They support equational reasoning and a limited version of dependent types. Namely the dependent types must also form an algebraic theory and you are only allowed to have equations between terms of the same type. Catlab ships with many predefined theories for important concepts like Categories and \"doctrines\" of categories like Symmetric Monoidal Categories. These predefined theories are defined in Catlab.Theories, but you can make your own with the @theory macro.\nCatlab.Syntax provides initial algebras for a GAT, which are declared with @syntax. These are represented as a typed version of Expr that allows you to customize the normalization procedure for example in a FreeCategory, the composition operation which is a unital and associative binary operation is normalized into lists. This allows you to write algorithms on Syntax trees that use different styles of simplification. The only styles available now are support for normalizing unital and associate operations like comoposition and a monoidal product.\n@instance associates Julia data structures as semantics for a GAT. This is known as functorial semantics, where you associate every type in the GAT with a type in Julia and every term constructor in the GAT to a julia function (possibly a struct constructor). These functions and types must satisfy the axioms that are encoded in the GAT. \n@present enumerates a finite set of generators for a model of the GAT just like you would write out a group (model of the theory of groups) as list of generators and relations, the presentation lets you enumerate the objects and morphisms that generate a category.","category":"page"},{"location":"#Table-of-Contents","page":"Catlab.jl","title":"Table of Contents","text":"","category":"section"},{"location":"","page":"Catlab.jl","title":"Catlab.jl","text":"Pages = [\n \"apis/core.md\",\n \"apis/theories.md\",\n \"apis/wiring_diagrams.md\",\n \"apis/graphics.md\",\n \"apis/programs.md\",\n ]\nDepth = 2","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"EditURL = \"https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/literate/graphics/composejl_wiring_diagrams.jl\"","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/#Drawing-wiring-diagrams-in-Compose.jl","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"(Image: )","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"Catlab can draw wiring diagrams using the Julia package Compose.jl.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"For best results, it is recommended to load the packages Convex.j and SCS.jl. When available they are used to optimize the layout of the outer ports.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"using Catlab.WiringDiagrams, Catlab.Graphics\n\nimport Convex, SCS","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/#Examples","page":"Drawing wiring diagrams in Compose.jl","title":"Examples","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/#Symmetric-monoidal-category","page":"Drawing wiring diagrams in Compose.jl","title":"Symmetric monoidal category","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"using Catlab.Theories\n\nA, B, C, D = Ob(FreeSymmetricMonoidalCategory, :A, :B, :C, :D)\nf, g = Hom(:f, A, B), Hom(:g, B, A);\nnothing #hide","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"To start, here are a few very simple examples.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(f)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(f⋅g)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(f⊗g)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"Here is a more complex example, involving generators with compound domains and codomains.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"h, k = Hom(:h, C, D), Hom(:k, D, C)\nm, n = Hom(:m, B⊗A, A⊗B), Hom(:n, D⊗C, C⊗D)\nq = Hom(:l, A⊗B⊗C⊗D, D⊗C⊗B⊗A)\n\nto_composejl((f⊗g⊗h⊗k)⋅(m⊗n)⋅q⋅(n⊗m)⋅(h⊗k⊗f⊗g))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"Identities and braidings appear as wires.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(id(A))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(braid(A,B))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(braid(A,B) ⋅ (g⊗f) ⋅ braid(A,B))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"The isomorphism A otimes B otimes C to C otimes B otimes A induced by the permutation (3 2 1) is a composite of braidings and identities.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"σ = (braid(A,B) ⊗ id(C)) ⋅ (id(B) ⊗ braid(A,C) ⋅ (braid(B,C) ⊗ id(A)))\n\nto_composejl(σ)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"By default, anchor points are added along identity and braiding wires to reproduce the expression structure in the layout. The anchors can be disabled to get a more \"unbiased\" layout.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(σ, anchor_wires=false)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/#Biproduct-category","page":"Drawing wiring diagrams in Compose.jl","title":"Biproduct category","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"A, B, C = Ob(FreeBiproductCategory, :A, :B, :C)\nf = Hom(:f, A, B)\n\nto_composejl(mcopy(A))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(delete(A))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(mcopy(A)⋅(f⊗f)⋅mmerge(B))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(mcopy(A⊗B), orientation=TopToBottom)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(mcopy(A⊗B⊗C), orientation=TopToBottom)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/#Compact-closed-category","page":"Drawing wiring diagrams in Compose.jl","title":"Compact closed category","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"The unit and co-unit of a compact closed category appear as caps and cups.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"A, B = Ob(FreeCompactClosedCategory, :A, :B)\n\nto_composejl(dunit(A))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(dcounit(A))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"In a self-dual compact closed category, such as a bicategory of relations, every morphism f A to B has a transpose f^dagger B to A given by bending wires:","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"A, B = Ob(FreeBicategoryRelations, :A, :B)\nf = Hom(:f, A, B)\n\nto_composejl((dunit(A) ⊗ id(B)) ⋅ (id(A) ⊗ f ⊗ id(B)) ⋅ (id(A) ⊗ dcounit(B)))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/#Abelian-bicategory-of-relations","page":"Drawing wiring diagrams in Compose.jl","title":"Abelian bicategory of relations","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"In an abelian bicategory of relations, such as the category of linear relations, the duplication morphisms Delta_X X to X oplus X and addition morphisms blacktriangledown_X X oplus X to X belong to a bimonoid. Among other things, this means that the following two morphisms are equal.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"X = Ob(FreeAbelianBicategoryRelations, :X)\n\nto_composejl(plus(X) ⋅ mcopy(X))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl((mcopy(X)⊕mcopy(X)) ⋅ (id(X)⊕swap(X,X)⊕id(X)) ⋅ (plus(X)⊕plus(X)))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/#Custom-styles","page":"Drawing wiring diagrams in Compose.jl","title":"Custom styles","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"The visual appearance of wiring diagrams can be customized by passing Compose properties.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"using Compose: fill, stroke\n\nA, B, = Ob(FreeSymmetricMonoidalCategory, :A, :B)\nf, g = Hom(:f, A, B), Hom(:g, B, A)\n\nto_composejl(f⋅g, props=Dict(\n :box => [fill(\"lavender\"), stroke(\"black\")],\n))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"X = Ob(FreeAbelianBicategoryRelations, :X)\n\nto_composejl(plus(X) ⋅ mcopy(X), props=Dict(\n :junction => [fill(\"red\"), stroke(\"black\")],\n :variant_junction => [fill(\"blue\"), stroke(\"black\")],\n))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"The background color can also be changed.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(f⋅g, background_color=\"lightgray\", props=Dict(\n :box => [fill(\"white\"), stroke(\"black\")],\n))","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"By default, the boxes are rectangular (:rectangle). Other available shapes include circles (:circle) and ellipses (:ellipse).","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"to_composejl(f⋅g, default_box_shape=:circle)","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/#Output-formats","page":"Drawing wiring diagrams in Compose.jl","title":"Output formats","text":"","category":"section"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"The function to_composejl returns a ComposePicture object, which contains a Compose.jl context as well as a recommended width and height. When displayed interactively, this object is rendered using Compose's SVG backend.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"Any backend can be used by calling Compose's draw function. The SVG and PGF (LaTeX) backends are always available. To use the PNG or PDF backends, the extra packages Cairo.jl and Fontconfig.jl must be installed.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"For example, here is how to use the PGF backend.","category":"page"},{"location":"generated/graphics/composejl_wiring_diagrams/","page":"Drawing wiring diagrams in Compose.jl","title":"Drawing wiring diagrams in Compose.jl","text":"using Compose: draw, PGF\n\npic = to_composejl(f⋅g, rounded_boxes=false)\npgf = sprint() do io\n pgf_backend = PGF(io, pic.width, pic.height,\n false, # emit_on_finish\n true, # only_tikz\n texfonts=true)\n draw(pgf_backend, pic.context)\nend\nprintln(pgf)","category":"page"}]
}