Algebraic Model Management: A Survey
We survey the field of model management and describe a new model management approach based on algebraic specification.
Source author record
David I. Spivak
David I. Spivak appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.
ResearcherUnclaimed source record
Catalog footprint
What is connected
29works
15topics
4close collaborators
Research graph
See the researcher in context
Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Published work
29 published item(s)
preprint2022arXiv
Collectives: Compositional protocols for contributions and returns
We introduce a concept called a collective: an interface with a protocol for aggregating contributions and distributing returns. Through such a protocol, many members may participate in a mutual endeavor. We present a variety of real-world examples of collectives to explore the many kinds of things that members can contribute (such as time, work, ideas, or resources) as well as the many ways these contributions can be aggregated and returns distributed. In addition, we illustrate several ways in which new collectives can be constructed from old, alluding to the fact that all these constructions have a natural mathematical description within the category of polynomial functors equipped with a certain monoidal structure.
0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv
Fast Left Kan Extensions Using The Chase
We show how computation of left Kan extensions can be reduced to computation of free models of cartesian (finite-limit) theories. We discuss how the standard and parallel chase compute weakly free models of regular theories and free models of cartesian theories, and compare the concept of "free model" with a similar concept from database theory known as "universal model". We prove that, as algorithms for computing finite free models of cartesian theories, the standard and parallel chase are complete under fairness assumptions. Finally, we describe an optimized implementation of the parallel chase specialized to left Kan extensions that achieves an order of magnitude improvement in our performance benchmarks compared to the next fastest left Kan extension algorithm we are aware of.
0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv
Generalized Lens Categories via functors $\mathcal{C}^{\rm op}\to\mathsf{Cat}$
Lenses have a rich history and have recently received a great deal of attention from applied category theorists. We generalize the notion of lens by defining a category $\mathsf{Lens}_F$ for any category $\mathcal{C}$ and functor $F\colon \mathcal{C}^{\rm op}\to\mathsf{Cat}$, using a variant of the Grothendieck construction. All of the mathematics in this note is straightforward; the purpose is simply to see lenses in a broader context where some closely-related examples, such as ringed spaces and open continuous dynamical systems, can be included.
0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv
Behavioral Mereology: A Modal Logic for Passing Constraints
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may assume a completely elementary set-theoretic discussion. We consider the relationship between various parts of a whole in terms of how behavioral constraints are passed between them, and give an inter-modal logic that generalizes the usual alethic modalities in the setting of symmetric accessibility.
0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv
Proceedings of the 3rd Annual International Applied Category Theory Conference 2020
The third annual International Applied Category Theory Conference (ACT2020) was planned to take place at MIT in Cambridge, Massachusetts USA. However, the global COVID-19 pandemic made the prospect of holding a large in-person meeting impossible, and the event was thus held completely online. Holding the talks online had the new benefits of reducing carbon footprint, being inclusive of people from more parts of the world, and producing higher-quality video talks, which have been posted online for posterity. The ACT2020 contributions spanned a broad spectrum of application areas, including databases, dynamical systems, functional programming, game theory, lenses, neuroscience, probabilistic programming, natural language processing, quantum mechanics, and cyberphysical systems. Papers featured a broad range of categorical techniques. Papers in this Proceedings volume represents about half of the talks presented at ACT2020. Being included in the proceedings vs. not is not an indication of talk quality, but instead almost exclusively the choice of the authors, e.g. to present work already published elsewhere.
0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv
Wiring diagrams as normal forms for computing in symmetric monoidal categories
Applications of category theory often involve symmetric monoidal categories (SMCs), in which abstract processes or operations can be composed in series and parallel. However, in 2020 there remains a dearth of computational tools for working with SMCs. We present an "unbiased" approach to implementing symmetric monoidal categories, based on an operad of directed, acyclic wiring diagrams. Because the interchange law and other laws of a SMC hold identically in a wiring diagram, no rewrite rules are needed to compare diagrams. We discuss the mathematics of the operad of wiring diagrams, as well as its implementation in the software package Catlab.
0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv
A Compositional Sheaf-Theoretic Framework for Event-Based Systems (Extended Version)
A compositional sheaf-theoretic framework for the modeling of complex event-based systems is presented. We show that event-based systems are machines, with inputs and outputs, and that they can be composed with machines of different types, all within a unified, sheaf-theoretic formalism. We take robotic systems as an exemplar of complex systems and rigorously describe actuators, sensors, and algorithms using this framework.
0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv
Behavioral Mereology (Proofs and Properties)
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may assume a completely elementary set-theoretic discussion. We consider the relationship between various parts of a whole in terms of how behavioral constraints are passed between them, and give an inter-modal logic that generalizes the usual alethic modalities in the setting of symmetric accessibility.
0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv
Dirichlet Functors are Contravariant Polynomial Functors
Polynomial functors are sums of covariant representable functors from the category of sets to itself. They have a robust theory with many applications -- from operads and opetopes to combinatorial species. In this paper, we define a contravariant analogue of polynomial functors: Dirichlet functors. We develop the basic theory of Dirichlet functors, and relate them to their covariant analogues.
0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv
Poly: An abundant categorical setting for mode-dependent dynamics
Dynamical systems---by which we mean machines that take time-varying input, change their state, and produce output---can be wired together to form more complex systems. Previous work has shown how to allow collections of machines to reconfigure their wiring diagram dynamically, based on their collective state. This notion was called "mode dependence", and while the framework was compositional (forming an operad of re-wiring diagrams and algebra of mode-dependent dynamical systems on it), the formulation itself was more "creative" than it was natural. In this paper we show that the theory of mode-dependent dynamical systems can be more naturally recast within the category Poly of polynomial functors. This category is almost superlatively abundant in its structure: for example, it has \emph{four} interacting monoidal structures $(+,\times,\otimes,\circ)$, two of which ($\times,\otimes$) are monoidal closed, and the comonoids for $\circ$ are precisely categories in the usual sense. We discuss how the various structures in Poly show up in the theory of dynamical systems. We also show that the usual coalgebraic formalism for dynamical systems takes place within Poly. Indeed one can see coalgebras as special dynamical systems---ones that do not record their history---formally analogous to contractible groupoids as special categories.
0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv
The steady states of coupled dynamical systems compose according to matrix arithmetic
Open dynamical systems are mathematical models of machines that take input, change their internal state, and produce output. For example, one may model anything from neurons to robots in this way. Several open dynamical systems can be arranged in series, in parallel, and with feedback to form a new dynamical system---this is called compositionality---and the process can be repeated in a fractal-like manner to form more complex systems of systems. One issue is that as larger systems are created, their state space grows exponentially. In this paper a technique for calculating the steady states of an interconnected system of systems, in terms of the steady states of its component dynamical systems, is provided. These are organized into "steady state matrices" which generalize bifurcation diagrams. It is shown that the compositionality structure of dynamical systems fits with the familiar monoidal structure for the steady state matrices, where serial, parallel, and feedback composition of matrices correspond to multiplication, Kronecker product, and partial trace operations. The steady state matrices of dynamical systems respect this compositionality structure, exponentially reducing the complexity involved in studying the steady states of composite dynamical systems.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
Algebras of Open Dynamical Systems on the Operad of Wiring Diagrams
In this paper, we use the language of operads to study open dynamical systems. More specifically, we study the algebraic nature of assembling complex dynamical systems from an interconnection of simpler ones. The syntactic architecture of such interconnections is encoded using the visual language of wiring diagrams. We define the symmetric monoidal category W, from which we may construct an operad O(W), whose objects are black boxes with input and output ports, and whose morphisms are wiring diagrams, thus prescribing the algebraic rules for interconnection. We then define two W-algebras, G and L, which associate semantic content to the structures in W. Respectively, they correspond to general and to linear systems of differential equations, in which an internal state is controlled by inputs and produces outputs. As an example, we use these algebras to formalize the classical problem of systems of tanks interconnected by pipes, and hence make explicit the algebraic relationships among systems at different levels of granularity.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
Categories as mathematical models
Written to be contributed as the "mathematical modeling" chapter of a book, edited by Elaine Landry, to be titled "Categories for the Working Philosopher". In this chapter, category theory is presented as a mathematical modeling framework that highlights the relationships between objects, rather than the objects in themselves. A working definition of model is given, and several examples of mathematical objects, such as vector spaces, groups, and dynamical systems, are considered as categorical models.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
Functorial Data Migration: From Theory to Practice
In this paper we describe a functorial data migration scenario about the manufacturing service capability of a distributed supply chain. The scenario is a category-theoretic analog of an OWL ontology-based semantic enrichment scenario developed at the National Institute of Standards and Technology (NIST). The scenario is presented using, and is included with, the open-source FQL tool, available for download at categoricaldata.net/fql.html.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
Nesting of dynamic systems and mode-dependent networks
For many networks, the connection pattern (often called the topology) can vary in time, depending on the changing state, or mode, of the modules within the network. For example, "airplane mode" is the name for one communicative mode of a modern cellphone, in which it will not connect with any cellphone towers; thus the topology of the cellular network is dependent on the modes of its modules. This paper addresses the issue of nesting such mode-dependent networks, in which a local network can be abstracted as a single module in a larger network. Each module in the network represents a dynamic system, whose behavior includes repeatedly updating its communicative mode. It is in this way that the dynamics of the modules controls the topology of the networks at all levels. This paper provides a formal semantics, using the category-theoretic framework of operads and their algebras, to capture the nesting property and dynamics of mode-dependent networks. We provide a detailed running example to ground the mathematics.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
QINL: Query-integrated Languages
We describe an alternative solution to the impedance-mismatch problem between programming and query languages: rather than embed queries in a programming language, as done in LINQ systems, we embed programs in a query language, and dub the result QINL.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
Relational Foundations For Functorial Data Migration
We study the data transformation capabilities associated with schemas that are presented by directed multi-graphs and path equations. Unlike most approaches which treat graph-based schemas as abbreviations for relational schemas, we treat graph-based schemas as categories. A schema $S$ is a finitely-presented category, and the collection of all $S$-instances forms a category, $S$-inst. A functor $F$ between schemas $S$ and $T$, which can be generated from a visual mapping between graphs, induces three adjoint data migration functors, $Σ_F:S$-inst$\to T$-inst, $Π_F: S$-inst $\to T$-inst, and $Δ_F:T$-inst $\to S$-inst. We present an algebraic query language FQL based on these functors, prove that FQL is closed under composition, prove that FQL can be implemented with the select-project-product-union relational algebra (SPCU) extended with a key-generation operation, and prove that SPCU can be implemented with FQL.
0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv
Toward formalizing ologs: Linguistic structures, instantiations, and mappings
We define the notion of linguistic structure on a small category, in order to provide a more formal description of ontology logs, also known as ologs, introduced by R. E. Kent and D. I. Spivak in their paper "Ologs: A categorical framework for knowledge representation." In particular, we construct a bicategory $\mathsf{Eng}$, of English noun phrases and verb phrases, endorsed as functional by varying sets of authors. An olog is then defined as a lax functor to $\mathsf{Eng}$. We then present a new notion of linguistic functor, which extends Spivak's notion of meaningful functors. Finally, we discuss the relationship between ologs and databases in this context.
0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv
Type theoretical databases
We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. The point of interest for computer science is that this category can be seen to represent tables in a natural way. Thus the category is a model for databases, a single mathematical structure in which all database schemas and instances (of a suitable, but sufficiently general form) are represented. The type theory then allows for the specification of database schemas and instances, the manipulation of the same with the usual type-theoretic operations, and the posing of queries.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
Category theory for scientists (Old version)
There are many books designed to introduce category theory to either a mathematical audience or a computer science audience. In this book, our audience is the broader scientific community. We attempt to show that category theory can be applied throughout the sciences as a framework for modeling phenomena and communicating results. In order to target the scientific audience, this book is example-based rather than proof-based. For example, monoids are framed in terms of agents acting on objects, sheaves are introduced with primary examples coming from geography, and colored operads are discussed in terms of their ability to model self-similarity. A new version with solutions to exercises will be available through MIT Press.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
Functorial Data Migration
In this paper we present a simple database definition language: that of categories and functors. A database schema is a small category and an instance is a set-valued functor on it. We show that morphisms of schemas induce three "data migration functors", which translate instances from one schema to the other in canonical ways. These functors parameterize projections, unions, and joins over all tables simultaneously and can be used in place of conjunctive and disjunctive queries. We also show how to connect a database and a functional programming language by introducing a functorial connection between the schema and the category of types for that language. We begin the paper with a multitude of examples to motivate the definitions, and near the end we provide a dictionary whereby one can translate database concepts into category-theoretic concepts and vice-versa.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
The operad of temporal wiring diagrams: formalizing a graphical language for discrete-time processes
We investigate the hierarchical structure of processes using the mathematical theory of operads. Information or material enters a given process as a stream of inputs, and the process converts it to a stream of outputs. Output streams can then be supplied to other processes in an organized manner, and the resulting system of interconnected processes can itself be considered a macro process. To model the inherent structure in this kind of system, we define an operad $\mathcal{W}$ of black boxes and directed wiring diagrams, and we define a $\mathcal{W}$-algebra $\mathcal{P}$ of processes (which we call propagators, after Radul and Sussman). Previous operadic models of wiring diagrams use undirected wires without length, useful for modeling static systems of constraints, whereas we use directed wires with length, useful for modeling dynamic flows of information. We give multiple examples throughout to ground the ideas.
0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv
The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits
Wiring diagrams, as seen in digital circuits, can be nested hierarchically and thus have an aspect of self-similarity. We show that wiring diagrams form the morphisms of an operad $\mcT$, capturing this self-similarity. We discuss the algebra $\Rel$ of mathematical relations on $\mcT$, and in so doing use wiring diagrams as a graphical language with which to structure queries on relational databases. We give the example of circuit diagrams as a special case. We move on to show how plug-and-play devices and also recursion can be formulated in the operadic framework as well. Throughout we include many examples and figures.
0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv
Kleisli Database Instances
We use monads to relax the atomicity requirement for data in a database. Depending on the choice of monad, the database fields may contain generalized values such as lists or sets of values, or they may contain exceptions such as various types of nulls. The return operation for monads ensures that any ordinary database instance will count as one of these generalized instances, and the bind operation ensures that generalized values behave well under joins of foreign key sequences. Different monads allow for vastly different types of information to be stored in the database. For example, we show that classical concepts like Markov chains, graphs, and finite state automata are each perfectly captured by a different monad on the same schema.
0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv
Ologs: a categorical framework for knowledge representation
In this paper we introduce the olog, or ontology log, a category-theoretic model for knowledge representation (KR). Grounded in formal mathematics, ologs can be rigorously formulated and cross-compared in ways that other KR models (such as semantic networks) cannot. An olog is similar to a relational database schema; in fact an olog can serve as a data repository if desired. Unlike database schemas, which are generally difficult to create or modify, ologs are designed to be user-friendly enough that authoring or reconfiguring an olog is a matter of course rather than a difficult chore. It is hoped that learning to author ologs is much simpler than learning a database definition language, despite their similarity. We describe ologs carefully and illustrate with many examples. As an application we show that any primitive recursive function can be described by an olog. We also show that ologs can be aligned or connected together into a larger network using functors. The various methods of information flow and institutions can then be used to integrate local and global world-views. We finish by providing several different avenues for future research.
0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv
Table manipulation in simplicial databases
In \cite{Spi}, we developed a category of databases in which the schema of a database is represented as a simplicial set. Each simplex corresponds to a table in the database. There, our main concern was to find a categorical formulation of databases; the simplicial nature of the schemas was to some degree unexpected and unexploited. In the present note, we show how to use this geometric formulation effectively on a computer. If we think of each simplex as a polygonal tile, we can imagine assembling custom databases by mixing and matching tiles. Queries on this database can be performed by drawing paths through the resulting tile formations, selecting records at the start-point of this path and retrieving corresponding records at its end-point.
0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv
Mapping spaces in Quasi-categories
We apply the Dwyer-Kan theory of homotopy function complexes in model categories to the study of mapping spaces in quasi-categories. Using this, together with our work on rigidification from [DS1], we give a streamlined proof of the Quillen equivalence between quasi-categories and simplicial categories. Some useful material about relative mapping spaces in quasi-categories is developed along the way.
0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv
Rigidification of quasi-categories
We give a new construction for rigidifying a quasi-category into a simplicial category, and prove that it is weakly equivalent to the rigidification given by Lurie. Our construction comes from the use of necklaces, which are simplicial sets obtained by stringing simplices together. As an application of these methods, we use our model to reprove some basic facts from Lurie's "Higher Topos Theory" regarding the rigidification process.
0 citations0 reviewsNo code linkedOpen access