arXiv subjects

Andrea Laretto

Publications and source records attributed to Andrea Laretto.

6 recordsLinked to original sources

arXiv2026

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↗

arXiv2026

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öf 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öf type theory, with the notable exception of symmetry. We formalize our main theorems in Agda.

math.CT↗

arXiv2023

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án-Sabadini-Sobociński, 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 á la Guitart identify to certain Mealy machines á 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↗

arXiv2023

Specification and verification of a linear-time logic for graph transformation

We present a first-order linear-time temporal logic for reasoning about the evolution of directed graphs. Its semantics is based on the counterpart paradigm, thus allowing our logic to represent the creation, duplication, merging, and deletion of elements of a graph as well as how its topology changes over time. We then introduce a positive normal forms presentation, thus simplifying the actual process of verification. We provide the syntax and semantics of our logics with a computer-assisted formalisation using the proof assistant Agda, and we round up the paper by highlighting the crucial aspects of our formalisation and the practical use of quantified temporal logics in a constructive proof assistant.

cs.LO↗

arXiv2023

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↗

arXiv2023

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↗