/
index.html
2 lines (2 loc) · 18.8 KB
/
index.html
1
2
<!DOCTYPE html>
<html lang="en"><head><meta charset="UTF-8"/><meta name="viewport" content="width=device-width, initial-scale=1.0"/><title>Catlab.jl · Catlab.jl</title><script data-outdated-warner src="assets/warner.js"></script><link href="https://cdnjs.cloudflare.com/ajax/libs/lato-font/3.0.0/css/lato-font.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/juliamono/0.045/juliamono.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/5.15.4/css/fontawesome.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/5.15.4/css/solid.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/5.15.4/css/brands.min.css" rel="stylesheet" type="text/css"/><link href="https://cdnjs.cloudflare.com/ajax/libs/KaTeX/0.13.24/katex.min.css" rel="stylesheet" type="text/css"/><script>documenterBaseURL="."</script><script src="https://cdnjs.cloudflare.com/ajax/libs/require.js/2.3.6/require.min.js" data-main="assets/documenter.js"></script><script src="siteinfo.js"></script><script src="../versions.js"></script><link class="docs-theme-link" rel="stylesheet" type="text/css" href="assets/themes/documenter-dark.css" data-theme-name="documenter-dark" data-theme-primary-dark/><link class="docs-theme-link" rel="stylesheet" type="text/css" href="assets/themes/documenter-light.css" data-theme-name="documenter-light" data-theme-primary/><script src="assets/themeswap.js"></script><script src="assets/analytics.js"></script></head><body><div id="documenter"><nav class="docs-sidebar"><a class="docs-logo" href><img src="assets/logo.svg" alt="Catlab.jl logo"/></a><div class="docs-package-name"><span class="docs-autofit"><a href>Catlab.jl</a></span></div><form class="docs-search" action="search/"><input class="docs-search-query" id="documenter-search-query" name="q" type="text" placeholder="Search docs"/></form><ul class="docs-menu"><li class="is-active"><a class="tocitem" href>Catlab.jl</a><ul class="internal"><li><a class="tocitem" href="#What-is-Catlab?"><span>What is Catlab?</span></a></li><li><a class="tocitem" href="#Overview-of-Key-Components"><span>Overview of Key Components</span></a></li><li><a class="tocitem" href="#Table-of-Contents"><span>Table of Contents</span></a></li></ul></li><li><span class="tocitem">Vignettes</span><ul><li><input class="collapse-toggle" id="menuitem-2-1" type="checkbox"/><label class="tocitem" for="menuitem-2-1"><span class="docs-label">Seven Sketches in Compositionality</span><i class="docs-chevron"></i></label><ul class="collapsed"><li><a class="tocitem" href="generated/sketches/partitions/">Partitions</a></li><li><a class="tocitem" href="generated/sketches/preorders/">Preorders</a></li><li><a class="tocitem" href="generated/sketches/meets/">Meets in Preorders</a></li><li><a class="tocitem" href="generated/sketches/smc/">Symmetric Monoidal Categories</a></li><li><a class="tocitem" href="generated/sketches/cat_elements/">The Category of Elements</a></li></ul></li><li><input class="collapse-toggle" id="menuitem-2-2" type="checkbox"/><label class="tocitem" for="menuitem-2-2"><span class="docs-label">Graphs</span><i class="docs-chevron"></i></label><ul class="collapsed"><li><a class="tocitem" href="generated/graphs/graphs/">The Category of Graphs</a></li><li><a class="tocitem" href="generated/graphs/graphs_label/">Labeled Graphs</a></li><li><a class="tocitem" href="generated/graphs/subgraphs/">Algebra of subgraphs</a></li></ul></li><li><input class="collapse-toggle" id="menuitem-2-3" type="checkbox"/><label class="tocitem" for="menuitem-2-3"><span class="docs-label">Categorical Algebra</span><i class="docs-chevron"></i></label><ul class="collapsed"><li><a class="tocitem" href="generated/categorical_algebra/diagrams/">Diagrams</a></li><li><a class="tocitem" href="generated/categorical_algebra/acset_serialization/">Serializing acsets</a></li></ul></li><li><input class="collapse-toggle" id="menuitem-2-4" type="checkbox"/><label class="tocitem" for="menuitem-2-4"><span class="docs-label">Wiring Diagrams</span><i class="docs-chevron"></i></label><ul class="collapsed"><li><a class="tocitem" href="generated/wiring_diagrams/wiring_diagram_basics/">Basics of wiring diagrams</a></li><li><a class="tocitem" href="generated/wiring_diagrams/diagrams_and_expressions/">Wiring diagrams and syntactic expressions</a></li><li><a class="tocitem" href="generated/wiring_diagrams/wd_cset/">Wiring Diagrams as Attributed C-Sets</a></li></ul></li><li><input class="collapse-toggle" id="menuitem-2-5" type="checkbox"/><label class="tocitem" for="menuitem-2-5"><span class="docs-label">Graphics</span><i class="docs-chevron"></i></label><ul class="collapsed"><li><a class="tocitem" href="generated/graphics/graphviz_graphs/">Drawing graphs in Graphviz</a></li><li><a class="tocitem" href="generated/graphics/graphviz_wiring_diagrams/">Drawing wiring diagrams in Graphviz</a></li><li><a class="tocitem" href="generated/graphics/composejl_wiring_diagrams/">Drawing wiring diagrams in Compose.jl</a></li><li><a class="tocitem" href="generated/graphics/tikz_wiring_diagrams/">Drawing wiring diagrams in TikZ</a></li><li><a class="tocitem" href="generated/graphics/layouts_vs_drawings/">Layouts versus drawings of wiring diagrams</a></li></ul></li></ul></li><li><span class="tocitem">Modules</span><ul><li><a class="tocitem" href="apis/core/">Theories, instances, and expressions</a></li><li><a class="tocitem" href="apis/theories/">Standard library of theories</a></li><li><a class="tocitem" href="apis/categorical_algebra/">Categorical algebra</a></li><li><a class="tocitem" href="apis/graphs/">Graphs</a></li><li><a class="tocitem" href="apis/wiring_diagrams/">Wiring diagrams</a></li><li><a class="tocitem" href="apis/graphics/">Graphics</a></li><li><a class="tocitem" href="apis/programs/">Programs</a></li></ul></li></ul><div class="docs-version-selector field has-addons"><div class="control"><span class="docs-label button is-static is-size-7">Version</span></div><div class="docs-selector control is-expanded"><div class="select is-fullwidth is-size-7"><select id="documenter-version-selector"></select></div></div></div></nav><div class="docs-main"><header class="docs-navbar"><nav class="breadcrumb"><ul class="is-hidden-mobile"><li class="is-active"><a href>Catlab.jl</a></li></ul><ul class="is-hidden-tablet"><li class="is-active"><a href>Catlab.jl</a></li></ul></nav><div class="docs-right"><a class="docs-edit-link" href="https://github.com/AlgebraicJulia/Catlab.jl/blob/master/docs/src/index.md" title="Edit on GitHub"><span class="docs-icon fab"></span><span class="docs-label is-hidden-touch">Edit on GitHub</span></a><a class="docs-settings-button fas fa-cog" id="documenter-settings-button" href="#" title="Settings"></a><a class="docs-sidebar-button fa fa-bars is-hidden-desktop" id="documenter-sidebar-button" href="#"></a></div></header><article class="content" id="documenter-page"><h1 id="Catlab.jl"><a class="docs-heading-anchor" href="#Catlab.jl">Catlab.jl</a><a id="Catlab.jl-1"></a><a class="docs-heading-anchor-permalink" href="#Catlab.jl" title="Permalink"></a></h1><p>Catlab.jl is a framework for applied and computational category theory, written in the <a href="https://julialang.org">Julia</a> 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.</p><h2 id="What-is-Catlab?"><a class="docs-heading-anchor" href="#What-is-Catlab?">What is Catlab?</a><a id="What-is-Catlab?-1"></a><a class="docs-heading-anchor-permalink" href="#What-is-Catlab?" title="Permalink"></a></h2><p>Catlab is, or will eventually be, the following things.</p><p><strong>Programming library</strong>: 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.</p><p><strong>Interactive computing environment</strong>: Catlab can also be used interactively in <a href="http://jupyter.org">Jupyter notebooks</a>. Symbolic expressions are displayed using LaTeX and wiring diagrams are visualized using <a href="https://github.com/GiovineItalia/Compose.jl">Compose.jl</a>, <a href="http://www.graphviz.org">Graphviz</a>, or <a href="https://github.com/pgf-tikz/pgf">TikZ</a>.</p><p><strong>Computer algebra system</strong>: 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 <a href="https://ncatlab.org/nlab/show/generalized+algebraic+theory">generalized algebraic theories</a>. 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 <a href="https://github.com/wbhart/AbstractAlgebra.jl">AbstractAlgebra.jl</a> and <a href="https://github.com/wbhart/Nemo.jl">Nemo.jl</a>.</p><h3 id="What-is-Catlab-not?"><a class="docs-heading-anchor" href="#What-is-Catlab-not?">What is Catlab not?</a><a id="What-is-Catlab-not?-1"></a><a class="docs-heading-anchor-permalink" href="#What-is-Catlab-not?" title="Permalink"></a></h3><p>Catlab is <em>not</em> currently any of the following things, although we do not rule out that it could eventually evolve in these directions.</p><p><strong>Automated theorem prover</strong>: 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).</p><p><strong>Proof assistant</strong>: Likewise, Catlab is not a proof assistant because it does not produce formally verifiable proofs. Formal verification is not within scope of the project.</p><p><strong>Graphical user interface</strong>: 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, <a href="https://github.com/AlgebraicJulia/Semagrams.jl">Semagrams.jl</a> which does provide graphical user interfaces for interacting with wiring diagrams, Petri nets, and the like.</p><h3 id="What-is-a-GAT?"><a class="docs-heading-anchor" href="#What-is-a-GAT?">What is a GAT?</a><a id="What-is-a-GAT?-1"></a><a class="docs-heading-anchor-permalink" href="#What-is-a-GAT?" title="Permalink"></a></h3><p>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.</p><p>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.</p><p><a href="https://en.wikipedia.org/wiki/Universal_algebra">Universal algebra</a> (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.</p><p>Importantly, the theory of categories is <a href="https://mathoverflow.net/q/354920">not algebraic</a>. 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.</p><p>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 <code>compose(f::Hom,g::Hom)::Hom</code> would have domain given by the equation <code>codom(f) == dom(g)</code>. As your theories get more elaborate, the sets of equations defining the domains get more complicated and reasoning about the structure is overwhelming.</p><p>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 <code>compose(f::Hom(A,B), g::Hom(B,C))::Hom(A,C) where (A::Ob, B::Ob, C::Ob)</code> 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 <a href="http://www.math.jhu.edu/~eriehl/context/">Emily Riehl’s textbook</a>, 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.</p><h2 id="Overview-of-Key-Components"><a class="docs-heading-anchor" href="#Overview-of-Key-Components">Overview of Key Components</a><a id="Overview-of-Key-Components-1"></a><a class="docs-heading-anchor-permalink" href="#Overview-of-Key-Components" title="Permalink"></a></h2><p>There are several core parts to the Catlab design, we start with a brief overview of each one</p><ol><li><p><a href="apis/core/#gats">Catlab.GAT</a> provides <code>@theory</code> - 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 <code>@theory</code> macro.</p></li><li><p><a href="apis/core/#syntax-systems">Catlab.Syntax</a> provides initial algebras for a GAT, which are declared with <code>@syntax</code>. 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.</p></li><li><p><a href="apis/core/#Catlab.GAT.@instance-Tuple{Any, Any}"><code>@instance</code></a> 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. </p></li><li><p><a href="apis/core/#Catlab.Present.@present-Tuple{Any, Any}"><code>@present</code></a> 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.</p></li></ol><h2 id="Table-of-Contents"><a class="docs-heading-anchor" href="#Table-of-Contents">Table of Contents</a><a id="Table-of-Contents-1"></a><a class="docs-heading-anchor-permalink" href="#Table-of-Contents" title="Permalink"></a></h2><ul><li><a href="apis/core/#Theories,-instances,-and-expressions">Theories, instances, and expressions</a></li><li class="no-marker"><ul><li><a href="apis/core/#gats">Theories</a></li><li><a href="apis/core/#instances">Instances</a></li><li><a href="apis/core/#syntax-systems">Syntax systems</a></li><li><a href="apis/core/#API">API</a></li></ul></li><li><a href="apis/theories/#Standard-library-of-theories">Standard library of theories</a></li><li><a href="apis/wiring_diagrams/#wiring_diagrams">Wiring diagrams</a></li><li><a href="apis/graphics/#graphics">Graphics</a></li><li><a href="apis/programs/#programs">Programs</a></li><li class="no-marker"><ul><li><a href="apis/programs/#API">API</a></li></ul></li></ul></article><nav class="docs-footer"><a class="docs-footer-nextpage" href="generated/sketches/partitions/">Partitions »</a><div class="flexbox-break"></div><p class="footer-message">Powered by <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> and the <a href="https://julialang.org/">Julia Programming Language</a>.</p></nav></div><div class="modal" id="documenter-settings"><div class="modal-background"></div><div class="modal-card"><header class="modal-card-head"><p class="modal-card-title">Settings</p><button class="delete"></button></header><section class="modal-card-body"><p><label class="label">Theme</label><div class="select"><select id="documenter-themepicker"><option value="documenter-light">documenter-light</option><option value="documenter-dark">documenter-dark</option></select></div></p><hr/><p>This document was generated with <a href="https://github.com/JuliaDocs/Documenter.jl">Documenter.jl</a> version 0.27.23 on <span class="colophon-date" title="Friday 7 October 2022 21:32">Friday 7 October 2022</span>. Using Julia version 1.8.2.</p></section><footer class="modal-card-foot"></footer></div></div></div></body></html>