arXiv subjects

Tarmo Uustalu

Publications and source records attributed to Tarmo Uustalu.

At least 19 recordsLinked to original sources

arXiv2025

Monoid Structures on Indexed Containers

Containers represent a wide class of type constructions relevant for functional programming and (co)inductive reasoning. Indexed containers generalize this notion to better fit the scope of dependently typed programming. When interpreting types to be sets, a container describes an endofunctor on the category of sets while an I-indexed container describes an endofunctor on the category Set^I of I-indexed families of sets. We consider the monoidal structure on the category of I-indexed containers whose tensor product of containers describes the composition of the respective induced endofunctors. We then give a combinatorial characterization of monoids in this monoidal category, and we show how these monoids correspond precisely to monads on the induced endofunctors on Set^I. Lastly, we conclude by presenting some examples of monads on Set^I that fall under our characterization, including the product of two monads, indexed variants of the state and the writer monads and an example of a free monad. The technical results of this work are accompanied by a formalization in the proof assistant Cubical Agda.

cs.LO↗

arXiv2024

A Unifying Categorical View of Nondeterministic Iteration and Tests

We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We detach Kleene iteration from Kleene algebra and analyze it from the categorical perspective. The notion, we arrive at is that of Kleene-iteration category (with coproducts and tests), which we show to be general and robust in the sense of compatibility with programming language features, such as exceptions, store, concurrent behavior, etc. We attest the proposed notion w.r.t. various yardsticks, most importantly, by characterizing the free model as a certain category of (nondeterministic) rational trees.

cs.LO↗

arXiv2023

Canonical Gradings of Monads

We define a notion of grading of a monoid T in a monoidal category C, relative to a class of morphisms M (which provide a notion of M-subobject). We show that, under reasonable conditions (including that M forms a factorization system), there is a canonical grading of T. Our application is to graded monads and models of computational effects. We demonstrate our results by characterizing the canonical gradings of a number of monads, for which C is endofunctors with composition. We also show that we can obtain canonical grades for algebraic operations.

cs.LO↗

arXiv2022

What Makes a Strong Monad?

Strong monads are important for several applications, in particular, in the denotational semantics of effectful languages, where strength is needed to sequence computations that have free variables. Strength is non-trivial: it can be difficult to determine whether a monad has any strength at all, and monads can be strong in multiple ways. We therefore review some of the most important known facts about strength and prove some new ones. In particular, we present a number of equivalent characterizations of strong functor and strong monad, and give some conditions that guarantee existence or uniqueness of strengths. We look at strength from three different perspectives: actions of a monoidal category V, enrichment over V, and powering over V. We are primarily motivated by semantics of effects, but the results are also useful in other contexts.

cs.LO↗

arXiv2022

Proof Theory of Skew Non-Commutative MILL

Monoidal closed categories naturally model NMILL, non-commutative multiplicative intuitionistic linear logic: the monoidal unit and tensor interpret the multiplicative verum and conjunction; the internal hom interprets linear implication. In recent years, the weaker notion of (left) skew monoidal closed category has been proposed by Ross Street, where the three structural laws of left and right unitality and associativity are not required to be invertible, they are merely natural transformations with a specific orientation. A question arises: is it possible to find a logic which is naturally modelled by skew monoidal closed categories? We answer positively by introducing a cut-free sequent calculus for a skew version of NMILL that is a presentation of the free skew monoidal closed category. We study the proof-theoretic semantics of the sequent calculus by identifying a calculus of derivations in normal form, obtained from an adaptation of Andreoli's focusing technique to the skew setting. The resulting focused sequent calculus peculiarly employs a system of tags for keeping track of new formulae appearing in the antecedent and appropriately reducing non-deterministic choices in proof search. Focusing solves the coherence problem for skew monoidal closed categories by exhibiting an effective procedure for deciding equality of maps in the free such category.

cs.LO↗

arXiv2021

Proof Theory of Partially Normal Skew Monoidal Categories

The skew monoidal categories of Szlachányi are a weakening of monoidal categories where the three structural laws of left and right unitality and associativity are not required to be isomorphisms but merely transformations in a particular direction. In previous work, we showed that the free skew monoidal category on a set of generating objects can be concretely presented as a sequent calculus. This calculus enjoys cut elimination and admits focusing, i.e. a subsystem of canonical derivations, which solves the coherence problem for skew monoidal categories. In this paper, we develop sequent calculi for partially normal skew monoidal categories, which are skew monoidal categories with one or more structural laws invertible. Each normality condition leads to additional inference rules and equations on them. We prove cut elimination and we show that the calculi admit focusing. The result is a family of sequent calculi between those of skew monoidal categories and (fully normal) monoidal categories. On the level of derivability, these define 8 weakenings of the (unit,tensor) fragment of intuitionistic non-commutative linear logic.

cs.LO↗

arXiv2021

Deductive Systems and Coherence for Skew Prounital Closed Categories

In this paper, we develop the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew closed categories in turn are a weakening of the closed categories of Eilenberg and Kelly where no structural law is required to be invertible. The presence of a monoidal structure in these categories is not required. We construct several equivalent presentations of the free skew prounital closed category on a given set of generating objects: a categorical calculus (Hilbert-style system), a cut-free sequent calculus and a natural deduction system corresponding to a variant of planar (= non-commutative linear) typed lambda-calculus. We solve the coherence problem for skew prounital closed categories by showing that the sequent calculus admits focusing and presenting two reduction-free normalization procedures for the natural deduction calculus: normalization by evaluation and hereditary substitutions. Normal natural deduction derivations (beta-eta-long forms) are in one-to-one correspondence with derivations in the focused sequent calculus. Unexpectedly, the free skew prounital closed category on a set satisfies a left-normality condition which makes it lose its skew aspect. This pitfall can be avoided by considering the free skew prounital closed category on a skew multicategory instead. The latter has a presentation as a cut-free sequent calculus for which it is easy to see that the left-normality condition generally fails. The whole development has been fully formalized in the dependently typed programming language Agda.

cs.LO↗

arXiv2020

The Sequent Calculus of Skew Monoidal Categories

Szlachányi's skew monoidal categories are a well-motivated variation of monoidal categories in which the unitors and associator are not required to be natural isomorphisms, but merely natural transformations in a particular direction. We present a sequent calculus for skew monoidal categories, building on the recent formulation by one of the authors of a sequent calculus for the Tamari order (skew semigroup categories). In this calculus, antecedents consist of a stoup (an optional formula) followed by a context, and the connectives behave like in the standard monoidal sequent calculus except that the left rules may only be applied in stoup position. We prove that this calculus is sound and complete with respect to existence of maps in the free skew monoidal category, and moreover that it captures equality of maps once a suitable equivalence relation is imposed on derivations. We then identify a subsystem of focused derivations and establish that it contains exactly one canonical representative from each equivalence class. This coherence theorem leads directly to simple procedures for deciding equality of maps in the free skew monoidal category and for enumerating any homset without duplicates. Finally, and in the spirit of Lambek's work, we describe the close connection between this proof-theoretic analysis and Bourke and Lack's recent characterization of skew monoidal categories as left representable skew multicategories. We have formalized this development in the dependently typed programming language Agda.

cs.LO↗

arXiv2019

Interaction laws of monads and comonads

We introduce and study functor-functor and monad-comonad interaction laws as mathematical objects to describe interaction of effectful computations with behaviors of effect-performing machines. Monad-comonad interaction laws are monoid objects of the monoidal category of functor-functor interaction laws. We show that, for suitable generalizations of the concepts of dual and Sweedler dual, the greatest functor resp. monad interacting with a given functor or comonad is its dual while the greatest comonad interacting with a given monad is its Sweedler dual. We relate monad-comonad interaction laws to stateful runners. We show that functor-functor interaction laws are Chu spaces over the category of endofunctors taken with the Day convolution monoidal structure. Hasegawa's glueing endows the category of these Chu spaces with a monoidal structure whose monoid objects are monad-comonad interaction laws.

cs.LO↗

arXiv2019

Reordering Derivatives of Trace Closures of Regular Languages (Full Version)

We provide syntactic derivative-like operations, defined by recursion on regular expressions, in the styles of both Brzozowski and Antimirov, for trace closures of regular languages. Just as the Brzozowski and Antimirov derivative operations for regular languages, these syntactic reordering derivative operations yield deterministic and nondeterministic automata respectively. But trace closures of regular languages are in general not regular, hence these automata cannot generally be finite. Still, as we show, for star-connected expressions, the Antimirov and Brzozowski automata, suitably quotiented, are finite. We also define a refined version of the Antimirov reordering derivative operation where parts-of-derivatives (states of the automaton) are nonempty lists of regular expressions rather than single regular expressions. We define the uniform scattering rank of a language and show that, for a regexp whose language has finite uniform scattering rank, the truncation of the (generally infinite) refined Antimirov automaton, obtained by removing long states, is finite without any quotienting, but still accepts the trace closure. We also show that star-connected languages have finite uniform scattering rank.

cs.FL↗

arXiv2018

Codensity Lifting of Monads and its Dual

We introduce a method to lift monads on the base category of a fibration to its total category. This method, which we call codensity lifting, is applicable to various fibrations which were not supported by its precursor, categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended pseudometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We also introduce the dual method called density lifting of comonads. We next study the liftings of algebraic operations to the codensity liftings of monads. We also give a characterisation of the class of liftings of monads along posetal fibrations with fibred small meets as a limit of a certain large diagram.

cs.LO↗

arXiv2017

Generating Representative Executions [Extended Abstract]

Analyzing the behaviour of a concurrent program is made difficult by the number of possible executions. This problem can be alleviated by applying the theory of Mazurkiewicz traces to focus only on the canonical representatives of the equivalence classes of the possible executions of the program. This paper presents a generic framework that allows to specify the possible behaviours of the execution environment, and generate all Foata-normal executions of a program, for that environment, by discarding abnormal executions during the generation phase. The key ingredient of Mazurkiewicz trace theory, the dependency relation, is used in the framework in two roles: first, as part of the specification of which executions are allowed at all, and then as part of the normality checking algorithm, which is used to discard the abnormal executions. The framework is instantiated to the relaxed memory models of the SPARC hierarchy.

cs.PL↗

arXiv2016

Variations on Noetherianness

In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We want to say that a set is Noetherian, if, when we are shown elements from it one after another, we will sooner or later have seen some element twice. This idea can be made precise in a number of ways. We explore the properties and connections of some of the possible encodings. In particular, we show that certain implementations imply decidable equality while others do not, and we construct counterexamples in the latter case. Additionally, we explore the relation between Noetherianness and other notions of finiteness.

cs.LO↗

arXiv2016

Directed Containers as Categories

Directed containers make explicit the additional structure of those containers whose set functor interpretation carries a comonad structure. The data and laws of a directed container resemble those of a monoid, while the data and laws of a directed container morphism those of a monoid morphism in the reverse direction. With some reorganization, a directed container is the same as a small category, but a directed container morphism is opcleavage-like. We draw some conclusions for comonads from this observation, considering in particular basic constructions and concepts like the opposite category and a groupoid.

cs.LO↗

arXiv2015

Monads need not be endofunctors

We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. Under reasonable assumptions, relative monads are monoids in the functor category concerned and extend to monads, giving rise to a coreflection between relative monads and monads. Arrows are also an instance of relative monads.

cs.PL↗

arXiv2015

A Hoare logic for the coinductive trace-based big-step semantics of While

In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for While. In this semantics, both traces and evaluation (relating initial states of program runs to traces they produce) are defined coinductively. On terminating runs, this semantics agrees with the standard inductive state-based semantics. Here we present a Hoare logic counterpart of our coinductive trace-based semantics and prove it sound and complete. Our logic subsumes the standard partial-correctness state-based Hoare logic as well as the total-correctness variation: they are embeddable. In the converse direction, projections can be constructed: a derivation of a Hoare triple in our trace-based logic can be translated into a derivation in the state-based logic of a translated, weaker Hoare triple. Since we work with a constructive underlying logic, the range of program properties we can reason about has a fine structure; in particular, we can distinguish between termination and nondivergence, e.g., unbounded classically total search fails to be terminating, but is nonetheless nondivergent. Our meta-theory is entirely constructive as well, and we have formalized it in Coq.

cs.LO↗

arXiv2014

When is a container a comonad?

Abbott, Altenkirch, Ghani and others have taught us that many parameterized datatypes (set functors) can be usefully analyzed via container representations in terms of a set of shapes and a set of positions in each shape. This paper builds on the observation that datatypes often carry additional structure that containers alone do not account for. We introduce directed containers to capture the common situation where every position in a data-structure determines another data-structure, informally, the sub-data-structure rooted by that position. Some natural examples are non-empty lists and node-labelled trees, and data-structures with a designated position (zippers). While containers denote set functors via a fully-faithful functor, directed containers interpret fully-faithfully into comonads. But more is true: every comonad whose underlying functor is a container is represented by a directed container. In fact, directed containers are the same as containers that are comonads. We also describe some constructions of directed containers. We have formalized our development in the dependently typed programming language Agda.

cs.PL↗

arXiv2014

Coherence for Skew-Monoidal Categories

I motivate a variation (due to K. Szlachányi) of monoidal categories called skew-monoidal categories where the unital and associativity laws are not required to be isomorphisms, only natural transformations. Coherence has to be formulated differently than in the well-known monoidal case. In my (to my knowledge new) version, it becomes a statement of uniqueness of normalizing rewrites. I present a proof of this coherence theorem and also formalize it fully in the dependently typed programming language Agda.

cs.LO↗