SearcharxivSearch

arXiv subjects

Fosco Loregian

Publications and source records attributed to Fosco Loregian.

At least 19 recordsLinked to original sources

Two-dimensional transducers

We define a bicategory $\mathbf{2TDX}$ whose 1-cells provide a categorification of transducers, computational devices extending finite-state automata with output capabilities. This bicategory is a mathematically interesting object: its objects are categories $\mathcal{A},\mathcal{B},\dots$ and its 1-cells $(\mathcal{Q}, t) : \mathcal{A} \to \mathcal{B}$ consist of a category $\mathcal{Q}$ of `states', and a profunctor $$ t : \mathcal{A} \times \mathcal{Q}^\text{op}\times\mathcal{Q} \times (\mathcal{B}^*)^\text{op} \to \mathbf{Set} $$ where $\mathcal{B}^*$ denotes the free monoidal category over $\mathcal{B}$. Extending $t$ to $\mathcal{A}^*$ in a canonical way, to each `word' $\underline a$ in $\mathcal{A}^*$ one attaches an endoprofunctor over the category $\mathcal{Q}$ of states, enriched over presheaves on $\mathcal{B}^*$. We discuss a number of other characterizations of the hom-category $\mathbf{2TDX}(\mathcal{A},\mathcal{B})$; we establish a Kleisli-like universal property for $\mathbf{2TDX}(\mathcal{A},\mathcal{B})$ and explore the connection of $\mathbf{2TDX}$ to other bicategories of computational models, such as Bob Walters' bicategory of `circuits'; it is convenient to regard $\mathbf{2TDX}$ as the loose bicategory of a double category $\mathbb{D}\mathbf{TDX}$: the bicategory (resp., double category) of profunctors is naturally contained in the bicategory (resp., double category) $\mathbf{2TDX}$ (resp., $\mathbb{D}\mathbf{TDX}$); we study the completeness and cocompleteness properties of $\mathbb{D}\mathbf{TDX}$, the existence of companions and conjoints, and we sketch how monads, adjunctions, and other structures/properties that naturally arise from the definition work in $\mathbb{D}\mathbf{TDX}$.

math.CT

Doctrinal Semantics of Directed First-Order Logic

We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as rewrites between terms, allowing for types to be interpreted as preorders. The logic is equipped with a precise syntactic system of polarities, inspired by dinaturality, that keeps track of the occurrence of variables (positive/negative/both). We use this to give a characterization of directed equality as a relative left adjoint, generalizing the idea by Lawvere of equality as left adjoint; intuitively, the relativeness is used to capture the syntactic restriction that avoids symmetry of equality. The semantics of this logic and its system of variances is captured categorically using the notion of directed doctrine, which we prove sound and complete with respect to the syntax. Moreover, we prove that the classical fragment of our directed logic is complete with respect to a standard semantics in preorders.

cs.LO

Monads and limits in bicategories of circuits

We study monads in the (pseudo-)double category $\mathbf{KSW}(\mathcal{K})$ where loose arrows are Mealy automata valued in an ambient monoidal category $\mathcal{K}$, and the category of tight arrows is $\mathcal{K}$. Such monads turn out to be elegantly described through instances of semifree bicrossed products (bicrossed products of monoids, in the sense of Zappa-Sz\'ep-Takeuchi, where one factor is a free monoid). This result which gives an explicit description of the `free monad' double left adjoint to the forgetful functor. (Loose) monad maps are interesting as well, and relate to already known structures in automata theory. In parallel, we outline what double co/limits exist in $\mathbf{KSW}(\mathcal{K})$ and express in a synthetic language, based on double category theory, the bicategorical features of Katis-Sabadini-Walters `bicategory of circuits'.

math.CT

Di- is for Directed: First-Order Directed Type Theory via Dinaturality

We show how dinaturality plays a central role in the interpretation of directed type theory where types are interpreted as (1-)categories and directed equality is represented by $\hom$-functors. We present a general elimination principle based on dinaturality for directed equality which very closely resembles the $J$-rule used in Martin-L\"of type theory, and we highlight which syntactical restrictions are needed to interpret this rule in the context of directed equality. We then use these rules to characterize directed equality as a left relative adjoint to a functor between (para)categories of dinatural transformations which contracts together two variables appearing naturally with a single dinatural one, with the relative functor imposing the syntactic restrictions needed. We then argue that the quantifiers of such a directed type theory should be interpreted as ends and coends, which dinaturality allows us to present in adjoint-like correspondences to a weakening functor. Using these rules we give a formal interpretation to Yoneda reductions and (co)end calculus, and we use logical derivations to prove the Fubini rule for quantifier exchange, the adjointness property of Kan extensions via (co)ends, exponential objects of presheaves, and the (co)Yoneda lemma. We show transitivity (composition), congruence (functoriality), and transport (coYoneda) for directed equality by closely following the same approach of Martin-L\"of type theory, with the notable exception of symmetry. We formalize our main theorems in Agda.

math.CT

Fibrations of algebras

We study fibrations arising from indexed categories of the following form: fix two categories $\mathcal{A},\mathcal{X}$ and a functor $F : \mathcal{A} \times \mathcal{X} \longrightarrow\mathcal{X} $, so that to each $F_A=F(A,-)$ one can associate a category of algebras $\mathbf{Alg}_\mathcal{X}(F_A)$ (or an Eilenberg-Moore, or a Kleisli category if each $F_A$ is a monad). We call the functor $\int^{\mathcal{A}}\mathbf{Alg} \to \mathcal{A}$, whose typical fibre over $A$ is the category $\mathbf{Alg}_\mathcal{X}(F_A)$, the "fibration of algebras" obtained from $F$. Examples of such constructions arise in disparate areas of mathematics, and are unified by the intuition that $\int^\mathcal{A}\mathbf{Alg} $ is a form of semidirect product of the category $\mathcal{A}$, acting on $\mathcal{X}$, via the `representation' given by the functor $F : \mathcal{A} \times \mathcal{X} \longrightarrow\mathcal{X}$. After presenting a range of examples and motivating said intuition, the present work focuses on comparing a generic fibration with a fibration of algebras: we prove that if $\mathcal{A}$ has an initial object, under very mild assumptions on a fibration $p : \mathcal{E}\longrightarrow \mathcal{A}$, we can define a canonical action of $\mathcal{A}$ letting it act on the fibre $\mathcal{E}_\varnothing$ over the initial object. This result bears some resemblance to the well-known fact that the fundamental group $\pi_1(B)$ of a base space acts naturally on the fibers $F_b = p^{-1}b$ of a fibration $p : E \to B$.

math.CT

Automata and coalgebras in categories of species

We study generalized automata (in the sense of Ad\'amek-Trnkov\'a) in Joyal's category of (set-valued) combinatorial species, and as an important preliminary step, we study coalgebras for its derivative endofunctor $\partial$ and for the "Euler homogeneity operator" $L\circ\partial$ arising from the adjunction $L\dashv\partial\dashv R$. The theory is connected with, and in fact provides relatively nontrivial examples of, "differential 2-rigs", a notion recently introduced by the author putting combinatorial species on the same relation a generic (differential) semiring $(R,d)$ has with the (differential) semiring $\mathbb N[\![ X]\!]$ of power series with natural coefficients. The desire to study categories of "state machines" valued in an ambient monoidal category $(\mathcal K,\otimes)$ gives a pretext to further develop the abstract theory of differential 2-rigs, proving lifting theorems of a differential 2-rig structure from $(\mathcal R,\partial)$ to the category of $\partial$-algebras on objects of $\mathcal R$, and to categories of Mealy automata valued in $(\mathcal R,\otimes)$, as well as various constructions inspired by differential algebra such as jet spaces and modules of differential operators. These theorems adapt to various "species-like" categories such as coloured species, $k$-vector species (both used in operad theory), linear species (introduced by Leroux to study combinatorial differential equations), M\"obius species, and others.

math.CT

Adjoint functor theorems for lax-idempotent pseudomonads

For each pair of lax-idempotent pseudomonads $R$ and $I$, for which $I$ is locally fully faithful and $R$ distributes over $I$, we establish an adjoint functor theorem, relating $R$-cocontinuity to adjointness relative to $I$. This provides a new perspective on the nature of adjoint functor theorems, which may be seen as methods to decompose adjointness into cocontinuity and relative adjointness. As special cases, we recover variants of the adjoint functor theorem of Freyd, the multiadjoint functor theorem of Diers, and the pluriadjoint functor theorem of Solian--Viswanathan, as well as the adjoint functor theorems for locally presentable categories. More generally, we recover enriched $\Phi$-adjoint functor theorems for weakly sound classes of weight $\Phi$.

math.CT

The semibicategory of Moore automata

We study the semibicategory $\textsf{Mre}$ of "Moore automata": an arrangement of objects, 1- and 2-cells which is inherently and irredeemably nonunital in dimension one. Between the semibicategory of Moore automata and the better behaved bicategory $\textsf{Mly}$ of "Mealy automata" a plethora of adjunctions insist: the well-known essential equivalence between the two kinds of state machines that model the definitions of $\textsf{Mre}$ and $\textsf{Mly}$ is appreciated at the categorical level, as the equivalence induced between the fixpoints of an adjunction, in fact exhibiting $\textsf{Mre}(A,B)$ as a coreflective subcategory of $\textsf{Mly}(A,B)$; the comodality induced by this adjunction is but the $0$th step of a `level-like' filtration of the bicategory $\textsf{Mre}$ in a countable family of essential bi-localizations $\textsf{s}^n\textsf{Mre}\subseteq\textsf{Mre}$. We outline a way to generate intrinsically meaningful adjunctions of this form. We mechanize some of our main results using the proof assistant Agda.

math.CT

Bicategories of Automata, Automata in Bicategories

We study bicategories of (deterministic) automata, drawing from prior work of Katis-Sabadini-Walters, and Di Lavore-Gianola-Rom\'an-Sabadini-Soboci\'nski, and linking their bicategories of `processes' to a bicategory of Mealy machines constructed in 1974 by R. Guitart. We make clear the sense in which Guitart's bicategory retains information about automata, proving that Mealy machines \'a la Guitart identify to certain Mealy machines \'a la K-S-W that we call fugal automata; there is a biadjunction between fugal automata and the bicategory of K-S-W. Then, we take seriously the motto that a monoidal category is just a one-object bicategory. We define categories of Mealy and Moore machines inside a bicategory B; we specialise this to various choices of B, like categories, relations, and profunctors. Interestingly enough, this approach gives a way to interpret the universal property of reachability as a Kan extension and leads to a new notion of 1- and 2-cell between Mealy and Moore automata, that we call intertwiners, related to the universal property of K-S-W bicategory.

math.CT

Completeness for categories of generalized automata

We present a slick proof of completeness and cocompleteness for categories of $F$-automata, where the span of maps $E\leftarrow E\otimes I \to O$ that usually defines a deterministic automaton of input $I$ and output $O$ in a monoidal category $(\mathcal K,\otimes)$ is replaced by a span $E\leftarrow F E \to O$ for a generic endofunctor $F : \mathcal K\to \mathcal K$ of a generic category $\mathcal K$: these automata exist in their `Mealy' and `Moore' version and form categories $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$; such categories can be presented as strict 2-pullbacks in $\mathsf{Cat}$ and whenever $F$ is a left adjoint, both $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$ admit all limits and colimits that $\mathcal K$ admits. We mechanize some of of our main results using the proof assistant Agda and the library `agda-categories`.

math.CT

Fibrational Linguistics (FibLang): Language Acquisition

In this work we show how FibLang, a category-theoretic framework concerned with the interplay between language and meaning, can be used to describe vocabulary acquisition, that is the process with which a speaker acquires new vocabulary (through experience or interaction). We model two different kinds of vocabulary acquisition, which we call 'by example' and 'by paraphrasis'. The former captures the idea of acquiring the meaning of a word by being shown a witness representing that word, as in 'understanding what a cat is, by looking at a cat'. The latter captures the idea of acquiring meaning by listening to some other speaker rephrasing the word with others already known to the learner. We provide a category-theoretic model for vocabulary acquisition by paraphrasis based on the construction of free promonads. We draw parallels between our work and Wittgenstein's dynamical approach to language, commonly known as 'language games'.

math.CT

Fibrational linguistics: First concepts

We define a general mathematical framework for linguistics based on the theory of fibrations, called FibLang. We start by modelling the interaction between linguistics and cognition in the most general way possible, with a heavy focus on conceptually motivating any assumption we make. The advantage is that FibLang remains agnostic with respect to any particular axiomatization of grammar one may choose. As such, it is compatible with already existing categorical models of language (such as for example, DisCoCat), providing a formally sound framework to apply mathematical tools developed in the context of category theory, mainly categorical logic, to the study of language

math.CT

A Categorical Semantics for Hierarchical Petri Nets

We show how a particular variety of hierarchical nets, where the firing of a transition in the parent net must correspond to an execution in some child net, can be modelled utilizing a functorial semantics from a free category -- representing the parent net -- to the category of sets and spans between them. This semantics can be internalized via Grothendieck construction, resulting in the category of executions of a Petri net representing the semantics of the overall hierarchical net. We conclude the paper by giving an engineering-oriented overview of how our model of hierarchical nets can be implemented in a transaction-based smart contract environment.

math.CT

Rosen's no-go theorem for regular categories

The famous biologist Robert Rosen argued for an intrinsic difference between biological and artificial life, supporting the claim that `living systems are not mechanisms'. This result, understood as the claim that life-like mechanisms are non-computable, can be phrased as the non-existence of an equivalence between a category of `static'/analytic elements and a category of `variable'/synthetic elements. The property of a system of being synthetic, understood as being the gluing of `variable families' of analytica, must imply that the latter class of objects does not retain sufficient information in order to describe said variability; we contribute to this thesis with an argument rooted in elementary category theory. Seen as such, Rosen's `proof' that no living system can be a mechanism arises from a tension between two contrapuntal needs: on one side, the necessity to consider (synthetically) variable families of systems; on the other, the necessity to describe a syntheticum via an universally chosen analyticum.

math.CT

Escrows are optics

We provide a categorical interpretation for escrows, i.e. trading protocols in trustless environment, where the exchange between two agents is mediated by a third party where the buyer locks the money until they receive the goods they want from the seller. A simplified escrow system can be modeled as a certain kind of morphism in the category of optics on a monoidal category. When objects in the base category have monoid and comonoid structures, more involved kinds of escrows `with intermediaries' can be modelled as morphisms with action-like properties.

math.CT

Nets with Mana: A Framework for Chemical Reaction Modelling

We use categorical methods to define a new flavor of Petri nets where transitions can only fire a limited number of times, specified by a quantity that we call mana. We do so with chemistry in mind, looking at ways of modelling the behavior of chemical reactions that depend on enzymes to work. We prove that such nets can be either obtained as a result of a comonadic construction, or by enriching them with extra information encoded into a functor. We then use a well-established categorical result to prove that the two constructions are equivalent, and generalize them to the case where the firing of some transitions can "regenerate" the mana of others. This allows us to represent the action of catalysts and also of biochemical processes where the byproducts of some chemical reaction are exactly the enzymes that another reaction needs to work.

math.CT

Differential 2-rigs

We study the notion of a "differential 2-rig", a category R with coproducts and a monoidal structure distributing over them, also equipped with an endofunctor D : R -> R that satisfies a categorified analogue of the Leibniz rule. This is intended as a tool to unify various applications of such categories to computer science, algebraic topology, and enumerative combinatorics. The theory of differential 2-rigs has a geometric flavour but boils down to a specialization of the theory of tensorial strengths on endofunctors; this builds a surprising connection between apparently disconnected fields. We build "free 2-rigs" on a signature, and we prove various initiality results: for example, a certain category of colored species is the free differential 2-rig on a single generator.

math.CT

A Categorical Semantics for Bounded Petri Nets

We provide a categorical semantics for bounded Petri nets, both in the collective- and individual-token philosophy. In both cases, we describe the process of bounding a net internally, by just constructing new categories of executions of a net using comonads, and externally, using lax-monoidal-lax functors. Our external semantics is non-local, meaning that tokens are endowed with properties that say something about the global state of the net. We then prove, in both cases, that the internal and external constructions are equivalent, by using machinery built on top of the Grothendieck construction. The individual-token case is harder, as it requires a more explicit reliance on abstract methods.

math.CT