跳到正文
研踪PaperTrail

论文库

检索计算机领域论文，按研究方向、作者或关键词筛选。

部分采集异常
正在读取账号与研究记录…

全站更新概况

+0新增论文
+0其中 AI 相关
+2已有论文修订
+100新增 AI 导读

arXiv 最近完成扫描：2026-11-15 00:32 · 全站最近入库：2026-11-14 15:09各信源进度 →

统计口径与数据新鲜度

统计 2026-11-14 01:04 — 2026-11-15 01:04（北京时间） · 点击数字查看对应简报；AI 相关包含在新增论文内。

最近完成检查：2026-11-15 00:32最近发现新增版本：2026-11-14 15:09库内论文最新更新时间：2026-11-13 02:59

每分钟刷新已保存的数据。空检查不代表采集异常；新收录可能包含历史论文。AI 导读按新增版本计数。

23,348 已收录论文19,580 AI 相关6,729 有修订112 HF 社区发现

浏览论文库

研究日报 / 周报 →按信源浏览 →

时间范围跟随排序：版本更新、本站收录或首次发表。最新收录可能包含历史论文。部分信源异常，查看状态 →

找到 25 篇论文 · 按版本更新时间排序上轮扫描起点 2026-11-15 00:30（北京时间）
新论文 · v1arXiv:2611.17106

对称编程与推理的数学基础

Mathematical foundations for symmetric programming and reasoning

Ohad Kammar, Matija Pretnar

AI 速读 基于摘要

该文基于数学中“不失一般性”（w.l.o.g.）的证明原则，提出一种统一利用对称性的数学抽象，用于编程与推理。

cs.PL · cs.LO · math.CT · math.GR · math.LO

arXiv ↗PDF ↗
查看原文摘要

We develop a mathematical abstraction for uniformly exploiting symmetries in programming and reasoning based on the mathematical proof principle `without-loss-of-generality' (w.l.o.g.). Given: group actions that describe symmetries of the input and the output; and a canoniser, which captures how arbitrary inputs get sent to canonical ones, our construction extends any function from the canonical inputs to the whole domain. We characterise the conditions on the canonisers which guarantee that the construction gives the unique equivariant (i.e. symmetry-preserving) extension. Furthermore, we adapt the construction to a dependently-typed setting, where it captures traditional symmetric w.l.o.g. arguments via the Curry-Howard correspondence. Finally, we extend the construction to algebraic data types, where the symmetries of the constructors both uniquely determine the symmetries of the data type and pave the way for efficient execution.

版本更新 · v3arXiv:2601.21843

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Tom de Jong, Nicolai Kraus, Axel Ljungström

原文摘要

Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We show that all higher coherences can be stated and derived if simplicial type theory is taken to be homotopy type theory with a postulated interval type. In technical terms, this means that if a type has unique fillers for $(2,1)$-horns, it has unique fillers for all inner $(n,k)$-horns. This generalizes a result of Riehl and Shulman for the case $n = 3, k \in \{1, 2\}$. Our main technical tool is the Leibniz adjunction: the pushout-product is left adjoint to the pullback-hom in the wild category of types. While this adjunction is well known for ordinary categories, it is much more involved for higher categories, and the fact that it can be proved for the wild category of types (a higher category without stated higher coherences) is non-trivial. We make profitable use of the equivalence between the wild category of maps and that of families. We have formalized the results in Cubical Agda.

math.CT · cs.LO · math.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2601.19426

For Generalised Algebraic Theories, Two Sorts Are Enough

Samy Avrillon, Ambrus Kaposi, Ambroise Lafont, Niyousha Najmaei, Johann Rosain

原文摘要

Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-Löf type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT involving only two sorts: a first one without dependencies, and another one indexed over the former. We show that a model of the reduced GAT is equivalently given by a pair consisting of a model of the original GAT, which we call the core model, and a "cartesian" morphism from the family of sets induced by this core model. In a type-theoretic metatheory, the initial model of a GAT is called a quotient inductive-inductive type (QIIT). The above characterisation justifies soundness of the reduction, in the sense that the QIIT of the original GAT can be simulated from the QIIT of the reduced GAT, by taking its core model. A particular case of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Other instances of this reduction can be found in the literature to simulate sophisticated QIITs in Cubical Agda. Indeed, the reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.

cs.PL · cs.LO · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.03472

Override and Update in Restriction Categories

Jean-Simon Pacaud Lemay, Chad Nester

原文摘要

We study the override and update operators on partial functions from the perspective of restriction categories. We propose a definition of override restriction categories, in which both of the operators in question exist. We prove a number of results concerning these operators and their relationship to the structure of the ambient restriction category, as well as relating them to the existing literature on the override and update operators. We provide various examples of override restriction categories and in particular show that every classical restriction category is an override restriction category.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v5arXiv:2501.18404

Graded String Diagrams with Applications in Probabilistic Reasoning

Ralph Sarkis, Fabio Zanasi

原文摘要

We introduce string diagrams for graded symmetric monoidal categories. Our approach includes a definition of graded monoidal theory and the corresponding freely generated syntactic category. The para construction on monoidal actegories is a motivating example for our framework, and we show how an axiomatic presentation of the resulting category $\mathbf{Para}(\mathbb{G},\mathbf{C})$ may be modularly obtained from presentations for $\mathbb{G}$ and $\mathbf{C}$. We demonstrate three different applications of our diagrammatic language under the same theme: probabilistic reasoning. First, we show how to axiomatise a variant of the graded category $\mathbf{ImP}$, recently introduced by Liell-Cock and Staton to model imprecise probability. This culminates in a representation, as string diagrams with grading wires, of programs with primitives for nondeterministic and probabilistic choices and conditioning. Second, we exploit our modular presentation result to provide a new proof for a presentation of $\mathbf{Gauss}$, the category of Gaussian stochastic maps. Third, we use grading wires to represent causal interventions on Bayesian networks.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2606.03369

A calculus of types in Isbell nuclei

Juan Luis Gastaldi, Samantha Jarvis, Thomas Seiller, John Terilla

原文摘要

We identify two constructions from different mathematical traditions. In linear logic and realisability, logical types are generated rather than fixed in advance: one begins with a universe of realisers equipped with execution, uses orthogonality to test their interactions, and takes types to be the biorthogonally closed subsets. In enriched Isbell duality, a quantitative relation induces an adjunction whose fixed points form a category, its nucleus. These constructions proceed by different means; we show that, in the present setting, they produce the same objects. The shared datum is minimal: an associative product, called execution, and a real-valued measurement, with no compatibility assumed between them. The failure of the measurement to be additive is at once the relation defining orthogonality and the quantitative relation whose Isbell nucleus we form, and the types cut out by orthogonality are exactly the fixed points of the associated adjunction. The identification pays off in both directions. The most natural product of types fails to be associative; repairing this failure forces a different notion of type, sensitive to both sides of a composite, on which the induced product is associative and, when execution has units, carries two residuals. What emerges is a noncommutative Lambek calculus, derived directly from execution and orthogonality rather than imposed. In the reverse direction, each such type, read on the categorical side, generates a quantitative relation of its own, and with it a derived adjunction and a further generation of types; these derived types are again types of the original situation, computed by the residuals of the Lambek calculus. We also prove a coherence theorem for the threefold arrangements of this construction and, in the finite-dimensional case, give explicit formulas for the product.

cs.LO · math.CT · math.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v4arXiv:2501.13229

The Yoneda embedding in simplicial type theory

Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz

原文摘要

Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category theory. While notoriously technical, manipulating $\infty$-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. defining the $(\infty,1)$-category of $\infty$-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen's Theorem A.

cs.LO · math.AT · math.CT

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.07207

A Complete Equational Theory for Quantum Circuits with Generalized Control

William Schober, Scott Wesley

原文摘要

Controlled subcircuits are commonplace in quantum algorithms as they represent the quantum analogue of branching statements (if then). We introduce a generalization of controlled subcircuits in the form of a binary operation which sends pairs of unitary quantum circuits to a generalized controlled operation, whose semantics are based on matrix exponentials and logarithms. The family of quantum circuits with generalized controlled operations and circuit exponentiation is denoted HQC for Hierarchical Quantum Circuits. We formalize HQC as a modified prop category using a novel category-theoretic construction, and provide a sound and complete equational theory for diagrammatic reasoning in HQC.

cs.LO · math.CT

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.05924

How to prove equations using diagrams: A categorical and operational semantics for e-graphs

Evan Patterson

原文摘要

E-graphs are a powerful algorithmic technique for automated equational reasoning but have resisted a conceptual understanding independent of issues of presentation and implementation. We propose an operational semantics for e-graphs based on the fundamental category-theoretic concepts of diagrams, limits, and initial functors. We illustrate the formalism through numerous example calculations and establish its soundness and completeness. Technical prerequisites are kept to a minimum in the main text; less standard elements of the mathematical theory are developed in two appendices.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2410.21889

Contextful Arrows via Wreath Products

Matteo Capucci, David Jaz Myers

原文摘要

We introduce contextads and the Ctx construction, unifying various structures and constructions in category theory dealing with context and contextful arrows---comonads and their Kleisli construction, actegories and their Para construction, adequate triples and their Span construction. Contextads are defined in terms of Lack--Street wreaths, suitably categorified for pseudomonads in a tricategory of spans in a 2-category with display maps. The associated wreath product provides the Ctx construction, and by its universal property we conclude trifunctoriality. This abstract approach lets us work up to structure, and thus swiftly prove that, under very mild assumptions, a contextad equipped colaxly with a 2-algebraic structure produces a similarly structured double category of contextful arrows. We also explore the role contextads might play qua dependently graded comonads in organizing contextful computation in functional programming. We show that many side-effects monads can be dually captured by dependently graded comonads, and gesture towards a general result on the `transposability' of parametric right adjoint monads to dependently graded comonads.

math.CT · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v5arXiv:2510.14716

Approaching the Continuous from the Discrete: an Infinite Tensor Product Construction

Antonio Lorenzin, Fabio Zanasi

原文摘要

Increasingly in recent years, probabilistic computation has been investigated through the lenses of categorical algebra, especially via string diagrammatic calculi. Whereas categories of discrete and Gaussian probabilistic processes have been thoroughly studied, with various axiomatisation results, more expressive classes of continuous probability are less understood, because of the intrinsic difficulty of describing infinite behaviour by algebraic means. In this work, we establish a universal construction that adjoins infinite tensor products, allowing continuous probability to be investigated from discrete settings. Our main result applies this construction to $\mathsf{FinStoch}$, the category of finite sets and stochastic matrices, obtaining a category of locally constant Markov kernels, where the objects are finite sets plus the Cantor space $2^{\mathbb{N}}$. Any probability measure on the reals can be reasoned about in this category. Furthermore, we show how to lift axiomatisation results through the infinite tensor product construction. This way we obtain an axiomatic presentation of continuous probability over countable powers of $2=\lbrace 0,1\rbrace$.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v5arXiv:2409.14591

Non-Cartesian Guarded Recursion with Daggers

Louis Lemonnier

原文摘要

Guarded recursion is a framework allowing for a formalisation of streams in classical (as opposed to concurrent, probabilistic, quantum) programming languages. The latter take their semantics in cartesian closed categories. However, some programming paradigms do not take their semantics in a cartesian setting; this is the case for concurrency, reversible and quantum programming for example. In this paper, we focus on reversible programming through its categorical model in dagger categories, which are categories that contain an involutive operator on morphisms. We show how to introduce the framework of guarded recursion into dagger categories with sufficient structure for data types, also called dagger rig categories. First, given an arbitrary category, we build another category shown to be suitable for guarded recursion in multiple ways, via enrichment and fixed point theorems. We then study the interaction between this construction and the structure of dagger rig categories, aiming for reversible programming. Finally, we show that our construction is suitable as a model of higher-order reversible programming languages, such as symmetric pattern matching, to which we add guarded recursion features.

cs.LO · cs.PL · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2508.20054

Between Markov and restriction. Two more monads on categories for relations

Cipriano Junior Cioffo, Fabio Gadducci, Davide Trotta

原文摘要

The study of categories abstracting the structural properties of relations has been extensively developed over the years, resulting in a rich and diverse body of work. In a previous paper we offered a survey providing a modern presentation of these ``categories for relations'' as instances of gs-monoidal categories, showing how they arise as Kleisli categories of suitable symmetric monoidal monads. The end result was a taxonomy that organised numerous related concepts in the literature, including in particular Markov and restriction categories. This paper further enriches the taxonomy: it proposes two categories that are once more instances of gs-monoidal categories, yet more abstract than Markov and restriction categories. They are characterised by an axiomatic notion of mass and domain of an arrow, the latter one of the key ingredients of restriction categories, which generalises the domain of partial functions. The paper then introduces mass and domain preserving monads, proving that the associated Kleisli categories in fact preserve the corresponding equations and that these monads arise naturally for the categories of semiring-weighted relations.

cs.LO · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2603.04530

Complete Diagrammatic Axiomatisations of Relative Entropy

Ralph Sarkis, Fabio Zanasi

原文摘要

Relative entropy is a fundamental class of distances between probability distributions, with widespread applications in probability theory, statistics, and machine learning. In this work, we study relative entropy from a categorical perspective, viewing it as a quantitative enrichment of categories of stochastic matrices. We consider two natural monoidal structures on stochastic matrices, given by the Kronecker product and the direct sum. Our main results are complete axiomatisations of Kullback-Leibler divergence and, more generally, of Rényi divergences of arbitrary order, for each such structure. Our axiomatic theories are formulated within the framework of quantitative monoidal algebra, using a graphical language of string diagrams enriched with quantitative equations.

cs.LO · cs.IT · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.22551

The category of nominal sets is locally monoidal closed

Fahimeh Bayeh, Peng Fu, Peter Selinger

原文摘要

The category Nom of nominal sets was proposed by Pitts and Gabbay as a setting for the semantics of abstract syntax with variable bindings. It is well-known that Nom is a topos, also known as the Schanuel topos, and in particular it follows that Nom is locally closed, i.e., every slice category Nom/X is cartesian-closed. In this paper, we show that Nom has a much stronger property: every monoidal (closed) structure on Nom induces a monoidal (closed) structure on all slice categories Nom/X. One monoidal closed structure of particular interest on Nom is the separated product A * B, whose right adjoint A -* B is called the separated function space. In particular, it follows that Nom is locally separatedly closed.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2603.18321

A Simple Categorical Calculus of Interacting Processes

Chad Nester, Niels Voorneveld

原文摘要

We present a calculus that models a simple sort of process interaction. Our calculus consists of a collection of terms together with a rewrite relation, parameterised by an arbitrary multicategory whose morphisms we understand as non-interactive processes. We show that our calculus is confluent and terminating, and that terms modulo the induced convertibility relation form a virtual double category. We relate our calculus to the free cornering of a monoidal category, which is a double-categorical model of process interaction that is similar in spirit to the calculus presented herein. Precisely, we construct a functor from the virtual double category given by our calculus into the underlying virtual double category of the free cornering of the free monoidal category on the multicategory of non-interacting processes. If we think of the terms of our calculus as programs and the rewriting system as an operational semantics for these programs, this functor gives a sound denotational semantics for our calculus in terms of the free cornering.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2603.16375

Monoidal categories graded by partial commutative monoids

Matthew Earnshaw, Chad Nester, Mario Román

原文摘要

Effectful categories have two classes of morphisms: pure morphisms, which form a monoidal category; and effectful morphisms, which can only be combined monoidally with central morphisms (such as the pure ones), forming a premonoidal category. This suggests seeing morphisms of an effectful category as carrying a grade that combines under the monoidal product in a partially defined manner. We axiomatize this idea with the notion of monoidal category graded by a partial commutative monoid (PCM). Monoidal categories arise as the special case of grading by the singleton PCM, and effectful categories arise from grading by a two-element PCM. Further examples include grading by powerset PCMs, modelling non-interfering parallelism for programs accessing shared resources, and grading by intervals, modelling bounded resource usage. We show that effectful categories form a coreflective subcategory of PCM-graded monoidal categories; introduce cartesian structure, recovering Freyd categories; and describe PCM-graded monoidal categories as monoids by viewing a PCM as a thin promonoidal category.

cs.LO · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2605.21337

Multicategorical Semantics for Untyped Effects

Ariel Grunfeld, Liron Cohen

原文摘要

Completeness proofs in categorical semantics usually proceed by building a syntactic category whose composition is given by substitution. For untyped effectful Call-by-Value languages, this runs into a basic obstacle: there is no canonical notion of simultaneous substitution of computations, since evaluation order is semantically meaningful. We address this by taking single computation substitutions, that is, binding steps, as primitive, and representing computation substitution by finite sequential lists composed by concatenation. We formalize this idea in a one-object Freyd-multicategorical setting. We introduce Freyd operads, separating a cartesian operad of values from a symmetric Ren-cartesian preoperad of computations, connected by a Freyd functor, and from any Freyd operad we construct a corresponding Freyd PROP of substitutions. We prove that this construction is representable and, in the strict one-object setting, left adjoint to restriction to codomain 1. Using the induced term model, we interpret untyped computational lambda-calculus with procedures and higher-order functions in weakly closed Freyd operads, and prove soundness, initiality, and completeness. This yields a categorical semantics tailored to untyped effectful computation and broad enough to encompass realizability-oriented models such as monadic combinatory algebras.

cs.PL · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.37815

Concurrent Strategies as Street Fibrations

Hugo Paquet, Glynn Winskel

原文摘要

Concurrent games and strategies based on event structures are an established and expressive model of interactive computation. In this paper we revisit the problem of equipping this model with symmetry. Symmetry is essential for many applications, but it is also a source of mathematical complexity, not least because strategies with symmetry can be compared up to several distinct notions of equivalence. Our first contribution is a complete characterization of two classes of strategies for which composition admits an identity. For these two classes the identity laws hold, respectively, up to a "weak" and a "strong" notion of equivalence. The main result is that the weak class of strategies corresponds precisely to those inducing Street fibrations over the game. We also show how the established "thin" approach to symmetry also fits in this general framework. A second contribution is a formal connection between games and setoid-valued profunctors. This follows a long tradition of relating games and relational models, but here additionally includes a very general model of symmetries. Our characterization of strategies as Street fibrations makes the connection to profunctors significantly easier to establish.

cs.LO · math.CT

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.03174

Final coalgebras over R-modules

Oisín Flynn-Connolly, Henning Basold, Chase Ford

原文摘要

Final coalgebras and the coinduction principle for coalgebras over $R$-modules, where $R$ is a commutative ring, are essential in determining the denotational behaviour of various types of linear weighted automata. The goal of this paper is to provide lower and upper bounds on the ordinals that are needed to construct final coalgebras over $R$-modules as the limit of a transfinite sequence of functor iterations. We give an example of a binary intersection preserving finitary functor on the category of abelian groups, which is the category of modules over integers, that fails to converge in $ω\cdot 2$ steps, thus settling an open problem of Adámek, Milius, and Moss. Then we relate this to the failure of the Artinian property of the integers and show that all finitary functors on $R$-modules for a Noetherian ring $R$ with Krull dimension $n$, which preserve countable directed intersections and a generalised notion of monomorphism, converge in $ω\cdot (n + 2)$ steps. We also establish how the connection between Aczel-Mendler bisimulation and behavioural equivalence is mediated by the functor $\operatorname{Ext}^1$. These results show that homological algebra tools can play an important role in coalgebra.

cs.LO · math.AC · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v4arXiv:2603.25710

Stone Duality for Monads

Richard Garner, Alyssa Renata, Nicolas Wu

原文摘要

We introduce a contravariant idempotent adjunction between (i) the category of ranked monads on $\mathsf{Set}$; and (ii) the category of internal categories and internal retrofunctors in the category of locales. The left adjoint takes a monad $T$-viewed as a notion of computation, following Moggi-to its localic behaviour category $\mathsf{LB}T$. This behaviour category is understood as "the universal transition system" for interacting with $T$: its "objects" are states and the "morphisms" are transitions. On the other hand, the right adjoint takes a localic category $\mathsf{LC}$-similarly understood as a transition system-to the monad $Γ\mathsf{LC}$ where $(Γ\mathsf{LC})A$ is the set of $A$-indexed families of local sections to the source map which jointly partition the locale of objects. The fixed points of this adjunction consist of (i) hyperaffine-unary monads, i.e., those monads where term $t$ admits a read-only operation $\bar{t}$ predicting the output of $t$; and (ii) ample localic categories, i.e., whose source maps are local homeomorphisms and whose locale of objects are strongly zero-dimensional. The hyperaffine-unary monads arise in earlier works by Johnstone and Garner as a syntactic characterization of those monads with Cartesian closed Eilenberg-Moore categories. This equivalence is the Stone duality for monads; so-called because it further restricts to the classical Stone duality by viewing a Boolean algebra $B$ as a monad of $B$-partitions and the corresponding Stone space as a localic category with only identity morphisms.

cs.LO · cs.PL · math.CT

查看论文
arXiv ↗PDF ↗
版本更新 · v4arXiv:2510.03953

Uniqueness and non-uniqueness of deriving transformations

Jean-Baptiste Vienney

原文摘要

A differential category is an additive symmetric monoidal category with an algebra modality, axiomatizing smooth functions, and a deriving transformation, axiomatizing the differentiation of these smooth functions. An algebra modality may or may not have both the nullary and the binary Seely isomorphisms. Lemay proved that if an algebra modality has both Seely isomorphisms, then it has at most one deriving transformation. It was then an open problem whether every algebra modality has at most one deriving transformation. We answer this question in the negative by constructing algebra modalities with infinite sets of deriving transformations. We also clarify the relations between the nullary Seely isomorphism, the binary Seely isomorphism, and uniqueness of deriving transformations (that is, the property for an algebra modality to have at most one deriving transformation). First, we refine Lemay's theorem by removing the assumption of the nullary Seely isomorphism. Then, we show by means of various examples that the six combinations of absence or presence of nullary Seely isomorphism, binary Seely isomorphism, and uniqueness of deriving transformations, which are not already ruled out by the refined uniqueness theorem, can be realized.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v5arXiv:2502.03477

Partial Markov Categories

Elena Di Lavore, Mario Román, Paweł Sobociński

原文摘要

We introduce partial Markov categories as a synthetic framework for synthetic probabilistic inference, blending the work of Cho and Jacobs, Fritz, and Golubtsov on Markov categories with the work of Cockett and Lack on cartesian restriction categories. We describe observations, Bayes' theorem, normalisation, and both Pearl's and Jeffrey's updates in purely categorical terms.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2610.37944

Symmetric List Objects

Fiona Blackett, Vikraman Choudhury, Rin Liu

原文摘要

Cons-lists are fundamental to functional programming, and are well-understood as initial algebras, and as a concrete construction of free monoids. In category theory, such list objects can be axiomatised internal to any monoidal category, with nil and cons maps, and a recursion mechanism. When strengthened to support parametrised recursion, they can be shown to give the free monoid construction. We study a small variant on parametrised list objects called parametrised symmetric list objects, in a symmetric monoidal category, where the two frontmost elements are allowed to be permuted. We show that this gives a construction of free commutative monoids, and develop some related theory.

math.CT · cs.LO

查看论文
arXiv ↗PDF ↗
版本更新 · v4arXiv:2403.17961

A categorical formulation of Kraus' paradox

Andrew W. Swan

原文摘要

We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.

math.CT · cs.LO · math.LO

查看论文
arXiv ↗PDF ↗