arXiv subjects

Owen Lynch

Publications and source records attributed to Owen Lynch.

11 recordsLinked to original sources

arXiv2026

Hippogriff: a semantic approach to uniting core and modules

In this paper we introduce Hippogriff, a language with a module system that unifies syntax between the core level and the module level. Hippogriff's type theory is dependent, with modularity features enabled via a universe of small types, but Hippogriff still supports general recursion without making typechecking nonterminating. This paper contains two halves. In the first half, we describe Hippogriff and its implementation. In the second half, we build categorical semantics for our use of dependent types that justify the use of general recursion at the value level. Specifically, we use an extension of the second-order generalized algebraic theory framework to include a synthetic phase distinction, and this allows us to make a mathematical connection between dependent type theories and split-context type theories (like System F). Included as supplements are a Haskell implementation of Hippogriff and an appendix describing the full type theory of Hippogriff using a second-order generalized algebraic theory with phase distinction.

cs.PL↗

arXiv2026

Clock systems for stochastic and non-deterministic categorical systems theories

One of the characteristic features of categorical systems theory is that the behavior of systems can be characterized by certain morphisms into them. In other words, behaviors form a representable covariant functor to Set. And more generally, in the compositional setting, behaviors form a representable double functor to Span. Clock systems are convenient because behavior functors represented by clock systems are automatically well-behaved. It was previously not known whether stochastic and non-deterministic systems theories have clock systems. In this paper, we show that indeed they do have clock systems. Moreover, the clock systems for non-deterministic systems point to generalized notions of behavior for non-linear time.

math.CT↗

arXiv2025

Directories: A Convenient and Well-Behaved Formalism for Hierarchical Organization in Categorical Systems Theory

This paper introduces an inherently strict presentation of categories with products, coproducts, or symmetric monoidal products that is inspired by file systems and directories. Rather than using nested binary tuples to combine objects or morphisms, the presentation uses named tuples. Specifically, we develop 2-monads whose strict 2-algebras are product categories, coproduct categories, or symmetric monoidal categories, in a similar vein to the classical Fam construction, but where the elements of the indexing set are period-separated identifiers like $\mathtt{cart.motor.momentum}$. Our development of directories is also intended to serve the secondary purpose of expositing certain aspects of polynomial monads, and is accompanied by Haskell code that shows how the mathematical ideas can be implemented.

math.CT↗

arXiv2025

Exergetic Port-Hamiltonian Systems Modeling Language

Mathematical modeling of real-world physical systems requires the consistent combination of a multitude of physical laws and phenomenological models. This challenging task can be greatly simplified by hierarchically decomposing systems into ultimately simple components. Moreover, the use of diagrams for expressing the decomposition helps make the process more intuitive and facilitates communication, even with non-experts. As an important requirement, models have to respect fundamental physical laws such as the first and the second law of thermodynamics. While some existing modeling frameworks make such guarantees based on structural properties of their models, they lack a formal graphical syntax. We present a compositional and thermodynamically consistent modeling language with a graphical syntax. In terms of its semantics, we essentially endow port-Hamiltonian systems with additional structural properties and a fixed physical interpretation, ensuring thermodynamic consistency in a manner closely related to the metriplectic or GENERIC formalism. While port-Hamiltonian systems are inspired by graphical modeling with bond graphs, neither the link between the two, nor bond graphs themselves, can be easily formalized. In contrast, our syntax is based on a refinement of the well-studied operad of undirected wiring diagrams. By combining a compositional, graphical syntax with an energy-based, thermodynamic approach, the presented modeling language simplifies the understanding, reuse, and modification of complex physical models.

eess.SY↗

arXiv2024

GATlab: Modeling and Programming with Generalized Algebraic Theories

Categories and categorical structures are increasingly recognized as useful abstractions for modeling in science and engineering. To uniformly implement category-theoretic mathematical models in software, we introduce GATlab, a domain-specific language for algebraic specification embedded in a technical programming language. GATlab is based on generalized algebraic theories (GATs), a logical system extending algebraic theories with dependent types so as to encompass category theory. Using GATlab, the programmer can specify generalized algebraic theories and their models, including both free models, based on symbolic expressions, and computational models, defined by arbitrary code in the host language. Moreover, the programmer can define maps between theories and use them to declaratively migrate models of one theory to models of another. In short, GATlab aims to provide a unified environment for both computer algebra and software interface design with generalized algebraic theories. In this paper, we describe the design, implementation, and applications of GATlab.

cs.LO↗

arXiv2024

All Concepts are $\mathbb{C}\mathbf{at}^\#$

We show that the double category $\mathbb{C}\mathbf{at}^\#$ of comonoids in the category of polynomial functors (previously shown by Ahman-Uustalu and Garner to be equivalent to the double category of categories, cofunctors, and prafunctors) contains several formal settings for basic category theory and has subcategories equivalent to both the double category $\mathbb{O}\mathbf{rg}$ of dynamic rewiring systems and the double category $\mathbb{P}\mathbf{oly}_{\mathcal{E}}$ of generalized polynomials in a finite limit category $\mathcal{E}$. Also serving as a natural setting for categorical database theory and generalized higher category theory, $\mathbb{C}\mathbf{at}^\#$ at once hosts models of a wide range of concepts from the theory and applications of polynomial functors and category theory.

math.CT↗

arXiv2024

Organizing Physics with Open Energy-Driven Systems

Organizing physics has been a long-standing preoccupation of applied category theory, going back at least to Lawvere. We contribute to this research thread by noticing that Hamiltonian mechanics and gradient descent depend crucially on a consistent choice of transformation -- which we call a reaction structure -- from the cotangent bundle to the tangent bundle. We then construct a compositional theory of reaction structures. Reaction-based systems offer a different perspective on composition in physics than port-Hamiltonian systems or open classical mechanics, in that reaction-based composition does not create any new constraints that must be solved for algebraically. The technical contributions of this paper are the development of symmetric monoidal categories of open energy-driven systems and open differential equations, and a functor between them, functioning as a "functorial semantics" for reaction structures. This approach echoes what has previously been done for open games and open gradient-based learners, and in fact subsumes the latter. We then illustrate our theory by constructing an n-fold pendulum as a composite of n-many pendula.

math.CT↗

arXiv2023

Relational Composition of Physical Systems: A Categorical Approach

In this master's thesis, we rigorously develop two frameworks of relational composition of systems using tools from category theory. The first framework addresses port-Hamiltonian systems, which are dynamical systems whose dynamics are connected to flows of energy across a boundary. The second framework addresses thermostatic systems, which are descriptions of equilibria in physical systems using entropy. We also review necessary subjects to develop these frameworks from a category-theoretic viewpoint, including inear algebra, differential geometry, and convex geometry.

math.CT↗

arXiv2023

Compositional Thermostatics

We define a thermostatic system to be a convex space of states together with a concave function sending each state to its entropy, which is an extended real number. This definition applies to classical thermodynamics, classical statistical mechanics, quantum statistical mechanics, and also generalized probabilistic theories of the sort studied in quantum foundations. It also allows us to treat a heat bath as a thermostatic system on an equal footing with any other. We construct an operad whose operations are convex relations from a product of convex spaces to a single convex space, and prove that thermostatic systems are algebras of this operad. This gives a general, rigorous formalism for combining thermostatic systems, which captures the fact that such systems maximize entropy subject to whatever constraints are imposed upon them.

math-ph↗

arXiv2022

Categorical Data Structures for Technical Computing

Many mathematical objects can be represented as functors from finitely-presented categories $\mathsf{C}$ to $\mathsf{Set}$. For instance, graphs are functors to $\mathsf{Set}$ from the category with two parallel arrows. Such functors are known informally as $\mathsf{C}$-sets. In this paper, we describe and implement an extension of $\mathsf{C}$-sets having data attributes with fixed types, such as graphs with labeled vertices or real-valued edge weights. We call such structures "acsets," short for "attributed $\mathsf{C}$-sets." Derived from previous work on algebraic databases, acsets are a joint generalization of graphs and data frames. They also encompass more elaborate graph-like objects such as wiring diagrams and Petri nets with rate constants. We develop the mathematical theory of acsets and then describe a generic implementation in the Julia programming language, which uses advanced language features to achieve performance comparable with specialized data structures.

math.CT↗

arXiv2018

The Inherent Instability of Disordered Systems

The Multiscale Law of Requisite Variety is a scientific law relating, at each scale, the variation in an environment to the variation in internal state that is necessary for effective response by a system. While this law has been used to describe the effectiveness of systems in self-regulation, the consequences for failure have not been formalized. Here we use this law to consider the internal dynamics of an unstructured system, and its response to a structured environment. We find that, due to its inability to respond, a completely unstructured system is inherently unstable to the formation of structure. And in general, any system without structure above a certain scale is unable to withstand structure arising above that scale. To describe complicated internal dynamics, we develop a characterization of multiscale changes in a system. This characterization is motivated by Shannon information theoretic ideas of noise, but considers structured information. We then relate our findings to political anarchism showing that society requires some organizing processes, even if there is no traditional government or hierarchies. We also formulate our findings as an inverse second law of thermodynamics; while closed systems collapse into disorder, systems open to a structured environment spontaneously generate order.

physics.soc-ph↗