Author name cluster

Richard Garner

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

I&C Journal 2023 Journal Article

Hypernormalisation in an abstract setting

Richard Garner

Jacobs' hypernormalisation is a construction on finitely supported discrete probability distributions, obtained by generalising certain patterns occurring in quantitative information theory. In this paper, we generalise Jacobs' notion in turn, by describing a notion of hypernormalisation in the abstract setting of a symmetric monoidal category endowed with a linear exponential monad—a structure arising in the categorical semantics of linear logic. We show that Jacobs' hypernormalisation arises in this fashion from the finitely supported probability measure monad on the category of sets, which can be seen as a linear exponential monad with respect to a non-standard monoidal structure on sets which we term the convex monoidal structure. We give the construction of this monoidal structure in terms of a quantum-algebraic notion known as a tricocycloid. Besides the motivating example, and its generalisations to the continuous context, we give a range of other instances of our abstract hypernormalisation, which swap out the side-effect of probabilistic choice for other important side-effects such as non-deterministic choice, ranked choice, and input from a stream of values.

Details DOI

TCS Journal 2014 Journal Article

Restriction categories as enriched categories

Robin Cockett
Richard Garner

Restriction categories were introduced as a simple equational axiomatisation for categories of partial maps such as those which arise in the foundations of computability theory. A restriction structure on a category is given by an operation obeying four simple axioms, that assigns to each morphism of the category an endomorphism of its domain to be thought of as the partial identity representing the degree of definition. In this paper, we show that restriction categories can be seen as a kind of enriched category; this allows their theory to be studied by way of the enrichment. Unlike most enrichments, ours is based not on a monoidal category, but rather a weak double category in the sense of Grandis–Paré, and provides—from a purely mathematical perspective—an example of such an enrichment arising in nature. Beyond exhibiting restriction categories as enriched categories, we show that varying the base of this enrichment also allows the important notions of join and range restriction category to be understood in the same manner.

Details DOI

TCS Journal 2014 Journal Article

Revisiting the categorical interpretation of dependent type theory

Pierre-Louis Curien
Richard Garner
Martin Hofmann

We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.

Details DOI

TCS Journal 2008 Journal Article

The identity type weak factorisation system

Nicola Gambino
Richard Garner

We show that the classifying category C ( T ) of a dependent type theory T with axioms for identity types admits a non-trivial weak factorisation system. We provide an explicit characterisation of the elements of both the left class and the right class of the weak factorisation system. This characterisation is applied to relate identity types and the homotopy theory of groupoids.

Details DOI