arXiv subjects

Paul Blain Levy

Publications and source records attributed to Paul Blain Levy.

10 recordsLinked to original sources

arXiv2025

What is a monoid?

In many situations one encounters an entity that resembles a monoid. It consists of a carrier and two operations that resemble a unit and a multiplication, subject to three equations that resemble associativity and left and right unital laws. The question then arises whether this entity is, in fact, a monoid in a suitable sense. Category theorists have answered this question by providing a notion of monoid in a monoidal category, or more generally in a multicategory. While these encompass many examples, there remain cases which do not fit into these frameworks, such as the notion of relative monad and the modelling of call-by-push-value sequencing. In each of these examples, the leftmost and/or the rightmost factor of a multiplication or associativity law seems to be distinguished. To include such examples, we generalize the multicategorical framework in two stages. Firstly, we move to the framework of a left-skew multicategory (due to Bourke and Lack), which generalizes both multicategory and left-skew monoidal category. The notion of monoid in this framework encompasses examples where only the leftmost factor is distinguished, such as the notion of relative monad. Secondly, we consider monoids in the novel framework of a bi-skew multicategory. This encompasses examples where both the leftmost and the rightmost factor are distinguished, such as the notion of a category on a span, and the modelling of call-by-push-value sequencing. In the bi-skew framework (which is the most general), we give a coherence result saying that a monoid corresponds to an unbiased monoid, i.e. a map from the terminal bi-skew multicategory.

math.CT↗

arXiv2025

Probabilistic Strategies: Definability and the Tensor Completeness Problem

Programs that combine I/O and countable probabilistic choice, modulo either bisimilarity or trace equivalence, can be seen as describing a probabilistic strategy. For well-founded programs, we might expect to axiomatize bisimilarity via a sum of equational theories and trace equivalence via a tensor of such theories. This is by analogy with similar results for nondeterminism, established previously. While bisimilarity is indeed axiomatized via a sum of theories, and the tensor is indeed at least sound for trace equivalence, completeness in general, remains an open problem. Nevertheless, we show completeness in the case that either the probabilistic choice or the I/O operations used are finitary. We also show completeness up to impersonation, i.e. that the tensor theory regards trace equivalent programs as solving the same system of equations. This entails completeness up to the cancellation law of the probabilistic choice operator. Furthermore, we show that a probabilistic trace strategy arises as the semantics of a well-founded program iff it is victorious. This means that, when the strategy is played against any partial counterstrategy, the probability of play continuing forever is zero. We link our results (and open problem) to particular monads that can be used to model computational effects.

cs.LO↗

arXiv2025

Broad Infinity and Generation Principles

We introduce Broad Infinity, a new set-theoretic axiom scheme based on the slogan "Every time we construct a new element, we gain a new arity." It says that three-dimensional trees whose growth is controlled by a specified class function form a set. Such trees are called "broad numbers". Assuming AC (the axiom of choice), or at least the weak version known as WISC (Weakly Initial Set of Covers), we show that Broad Infinity is equivalent to Mahlo's principle, which says that the class of all regular limit ordinals is stationary. Assuming AC or WISC, Broad Infinity also yields a convenient principle for generating a subset of a class using a "rubric" (family of rules). This directly gives the existence of Grothendieck universes, without requiring a detour via ordinals. In the absence of choice, Broad Infinity implies that the derivations of elements from a rubric form a set. This yields the existence of Tarski-style universes. Additionally, we reveal a pattern of resemblance between "Wide" principles, that are provable in ZFC, and "Broad" principles, that go beyond ZFC. Note: this paper uses a base theory that is weaker than ZF but includes classical first-order logic and Replacement.

math.LO↗

arXiv2022

The Price of Mathematical Scepticism

This paper argues that, insofar as we doubt the bivalence of the Continuum Hypothesis or the truth of the Axiom of Choice, we should also doubt the consistency of third-order arithmetic, both the classical and intuitionistic versions. Underlying this argument is the following philosophical view. Mathematical belief springs from certain intuitions, each of which can be either accepted or doubted in its entirety, but not half-accepted. Therefore, our beliefs about reality, bivalence, choice and consistency should all be aligned.

math.HO↗

arXiv2019

A Theory of Particular Sets

ZFC has sentences that quantify over all sets or all ordinals, without restriction. Some have argued that sentences of this kind lack a determinate meaning. We propose a set theory called TOPS, using Natural Deduction, that avoids this problem by speaking only about particular sets.

math.LO↗

arXiv2018

Formulating Categorical Concepts using Classes

We examine the use of classes to formulate several categorical notions. This leads to two proposals: an explicit structure for working with subobjects, and a hierarchy of $k$-classes. We apply the latter to both ordinary and higher categories.

math.CT↗

arXiv2018

A Ghost at $ω_1$

In the final chain of the countable powerset functor, we show that the set at index $ω_1$, regarded as a transition system, is not strongly extensional because it contains a "ghost" element that has no successor even though its component at each successor index is inhabited. The method, adapted from a construction of Forti and Honsell, also gives ghosts at larger ordinals in the final chain of other subfunctors of the powerset functor. This leads to a precise description of which sets in these final chains are strongly extensional.

cs.LO↗

arXiv2017

Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version)

We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $λ$-calculi with algebraic effects. We first of all endow a computational $λ$-calculus with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract.

cs.LO↗

arXiv2013

Exploring the Boundaries of Monad Tensorability on Set

We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We present two main results: we show that the tensor of two monads need not in general exist by presenting two counterexamples, one of them involving finite powerset (i.e. the theory of join semilattices); this solves a somewhat long-standing open problem, and contrasts with recent results that had ruled out previously expected counterexamples. On the other hand, we show that tensors with bounded powerset monads do exist from countable powerset upwards.

cs.LO↗

arXiv2012

Proceedings Fourth Workshop on Mathematically Structured Functional Programming

This volume contains the proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012), taking place on 25 March, 2012 in Tallinn, Estonia, as a satellite event of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. MSFP is devoted to the derivation of functionality from structure. It highlights concepts from algebra, semantics and type theory as they are increasingly reflected in programming practice, especially functional programming. The workshop consists of two invited presentations and eight contributed papers on a range of topics at that interface.

cs.LO↗