Enriched Lawvere Theories for Operational Semantics

TL;DR

This paper introduces enriched Lawvere theories as a flexible framework for modeling operational semantics of formal systems, enabling translation between different semantic forms and unifying models through the Grothendieck construction.

Contribution

It extends Lawvere theories to enriched settings, allowing detailed descriptions of operational semantics and providing a categorical approach to relate various semantic models.

Findings

Enriched Lawvere theories effectively model operational semantics.

The Grothendieck construction unifies models across contexts.

Application to SKI-combinator calculus demonstrates practical utility.

Abstract

Enriched Lawvere theories are a generalization of Lawvere theories that allow us to describe the operational semantics of formal systems. For example, a graph enriched Lawvere theory describes structures that have a graph of operations of each arity, where the vertices are operations and the edges are rewrites between operations. Enriched theories can be used to equip systems with operational semantics, and maps between enriching categories can serve to translate between different forms of operational and denotational semantics. The Grothendieck construction lets us study all models of all enriched theories in all contexts in a single category. We illustrate these ideas with the SKI-combinator calculus, a variable-free version of the lambda calculus.

Equations

$$\begin{array}[]{rl}\text{types: }&\text{objects of }\mathsf{T}\\ \text{terms: }&\text{morphisms of }\mathsf{T}\\ \text{equations between terms: }&\text{commuting diagrams}\\ \text{rewrites between terms: }&\text{``edges'' in hom in }\mathsf{V}\\ \end{array}$$

$$\begin{array}[]{lll}\textbf{Simplicial Sets}&\mathsf{sSet}\text{-theories represent ``small-step'' operational semantics:}\\ &\text{--- an edge is a {single} term rewrite.}\\ \textbf{Categories}&\mathsf{Cat}\text{-theories represent ``big-step'' operational semantics:}\\ &\text{(Often this means a rewrite to a normal form. We use the term more generally.)}\\ &\text{--- a morphism is a {finite sequence} of rewrites.}\\ \textbf{Posets}&\mathsf{Pos}\text{-theories represent ``full-step'' operational semantics:}\\ &\text{--- a boolean is the {existence} of a big-step rewrite.}\\ \textbf{Sets}&\mathsf{Set}\text{-theories represent denotational semantics:}\\ &\text{--- an element is a {connected component} of the rewrite relation.}\end{array}$$

$$\mathsf{sSet}$$

$$\begin{array}[]{rl}\text{an object}&M\\ \text{an identity element}&e\colon 1\to M\\ \text{and multiplication}&m\colon M^{2}\to M\\ \text{obeying the associative law}&m\circ(m\times M)=m\circ(M\times m)\\ \text{and the right and left unit laws}&m\circ(e\times\mathrm{id}_{\_}M)=\mathrm{id}_{\_}M=m\circ(\mathrm{id}_{\_}M\times e).\\ \end{array}$$

$$\mathsf{Set}$$

$$U:\mathsf{Mod}(\mathsf{T},\mathsf{Set})\to \mathsf{Set}$$

$$F:\mathsf{Set}\to \mathsf{Mod}(\mathsf{T},\mathsf{Set}),$$

$$\mathsf{Mod}(F(n),\mu )=\mathsf{Mod}(\mathsf{T}(\tau (n),-),\mu )\cong \mu (\tau (n))\cong \mu (\tau (1){)}^n=\mathsf{Set}(n,U(\mu ))$$

$$T(X)={\int }^{n\in \mathsf{N}}{X}^n\times \mathsf{T}(n,1).$$

$$k^{\mathrm{op}}:{\mathsf{Set}}^{\mathrm{op}}\to \mathsf{Kl}(T{)}^{\mathrm{op}}$$

$$\mathsf{Kl}(T{)}^{\mathrm{op}}(n,m)=\mathsf{Kl}(T)(m,n)=\mathsf{Set}(m,T(n))$$

$$\begin{array}[]{rl}\text{a collection of objects}&\mathrm{Ob}(\mathsf{C})\\ \text{a hom-object function}&\mathsf{C}(-,-)\colon\mathrm{Ob}(\mathsf{C})\times\mathrm{Ob}(\mathsf{C})\to\mathrm{Ob}(\mathsf{V})\\ \text{composition morphisms}&\circ_{\_}{a,b,c}\colon\mathsf{C}(b,c)\times\mathsf{C}(a,b)\to\mathsf{C}(a,c)\quad\forall a,b,c\in\mathrm{Ob}(\mathsf{C})\\ \text{identity-assigning morphisms}&id_{\_}a\colon 1_{\_}\mathsf{V}\to\mathsf{C}(a,a)\quad\forall a\in\mathrm{Ob}(\mathsf{C})\\ \end{array}$$

$$\begin{array}[]{rl}\text{a function}&F\colon\mathrm{Ob}(\mathsf{C})\to\mathrm{Ob}(\mathsf{D})\\ \text{a collection of morphisms}&F_{\_}{ab}\colon\mathsf{C}(a,b)\to\mathsf{D}(F(a),F(b))\quad\forall a,b\in\mathsf{C}\\ \end{array}$$

$$\begin{array}[]{rl}\text{a family}&\alpha_{\_}a\colon 1_{\_}\mathsf{V}\to\mathsf{D}(F(a),G(a))\quad\forall a\in\mathrm{Ob}(\mathsf{C})\\ \end{array}$$

$$\underline{\mathsf{V}}(v,w)=w^v\forall v,w\in \mathsf{V}.$$

$$\underline{\mathsf{V}}(u\times v,w)\cong \underline{\mathsf{V}}(u,w^v)$$

$$C(b,-)\cong \prod _{\_}{i=1}^{n}C(b_{\_}i,-).$$

$$u^{v+w}\cong u^v\times u^w\text{ and }{w}^0\cong 1_{\_}\mathsf{V}$$

$$\mathsf{C}(-,b)\cong \prod _{\_}{i=1}^n\mathsf{C}(-,b_{\_}i).$$

$$(u\times v{)}^w\cong u^w\times v^w\text{ and }{1}_{\_}{\mathsf{V}}^w\cong 1_{\_}\mathsf{V}$$

$$p_{\_}i:1_{\_}\mathsf{V}\to \mathsf{C}(b,b_{\_}i)$$

$$1_{\_}\mathsf{V}\stackrel{i{d}_{\_}b}{⟶}\mathsf{C}(b,b)\stackrel{\sim }{⟶}\prod _{\_}{i=1}^n\mathsf{C}(b,b_{\_}i)\to \mathsf{C}(b,b_{\_}i)$$

$$p:1_{\_}\mathsf{V}\to \prod _{\_}{i=1}^n\mathsf{C}(b,b_{\_}i)$$

$$\mathsf{C}(-,b)\stackrel{\sim }{⟶}{1}_{\_}\mathsf{V}\times \mathsf{C}(-,b)\stackrel{p\times 1}{\to }\prod _{\_}{i=1}^n\mathsf{C}(b,b_{\_}i)\times \mathsf{C}(-,b)⟶\prod _{\_}{i=1}^n\mathsf{C}(-,b_{\_}i)$$

$$1_{\_}\mathsf{V}\stackrel{p}{⟶}\prod _{\_}{i=1}^n\mathsf{C}(b,b_{\_}i)\stackrel{{\prod }_{\_}iF}{\to }\mathsf{D}(F(b),F(b_{\_}i))$$

$$\mathsf{C}(-,c^v)\cong \mathsf{C}(-,c{)}^v.$$

$$q:1_{\_}\mathsf{V}\to \mathsf{C}(c^v,c{)}^v,$$

$$1_{\_}\mathsf{V}\stackrel{i{d}_{\_}{c}^v}{⟶}\mathsf{C}(c^v,c^v)\stackrel{\sim }{⟶}\mathsf{C}(c^v,c{)}^v.$$

$$\tau :{\underline{\mathsf{V}}}_{\_}{f}^{\mathrm{op}}\to \mathsf{T}$$

$$n_{\_}\mathsf{V}=\sum _{\_}i\in n{1}_{\_}\mathsf{V}.$$

Full text

1 Introduction

Formal systems are not always explicitly connected to how they operate in practice. Lawvere theories [21] are an excellent formalism for describing algebraic structures obeying equational laws, but they do not specify how to compute in such a structure, for example taking a complex expression and simplifying it using rewrite rules. Recall that a Lawvere theory is a category with finite products $\mathsf{T}$ generated by a single object $t$, for “type”, and morphisms $t^{n}\to t$ representing $n$-ary operations, with commutative diagrams specifying equations. There is a theory for groups, a theory for rings, and so on. We can specify algebraic structures of a given kind in some category $\mathsf{C}$ with finite products by a product-preserving functor $\mu\colon\mathsf{T}\to\mathsf{C}$. This is a simple and elegant form of denotational semantics. However, Lawvere theories know nothing of operational semantics. Our goal here is to address this using “enriched” Lawvere theories.

In a Lawvere theory, the objects are types and the morphisms are terms; however, there are no relations between terms, only equations. The process of computing one term into another should be given by hom-objects with more structure. In operational semantics, program behavior is often specified by labelled transition systems, or labelled directed multigraphs [27]. The edges of such a graph represent rewrites:

{(\lambda x.x+x\;\;2)}$${2+2}$${4}$$\scriptstyle{\beta}$$\scriptstyle{+}

We can use an enhanced Lawvere theory in which, rather than merely sets of morphisms, there are graphs or perhaps categories. Enriched Lawvere theories are exactly for this purpose.

In a theory $\mathsf{T}$ enriched in a category $\mathsf{V}$ of some kind of “directed object”, including graphs, categories, and posets, the theory has the following interpretation:

[TABLE]

To be clear, this is not a new idea. Using enriched Lawvere theories for operational semantics has been explored in the past. For example, category-enriched theories have been studied by Seely [30] for the $\lambda$-calculus, and poset-enriched ones by Ghani and Lüth [24] for understanding “modularity” in term rewriting systems. They have been utilized extensively by Power, enriching in $\omega$-complete partial orders to study recursion [14] – in fact, there the simplified “natural number” enriched theories which we explore were implicitly considered.

The goal of this paper is to give a simple unified explanation of enriched Lawvere theories and some of their applications to operational semantics. We aim our explanations at readers familiar with category theory but not yet enriched categories. To reduce the technical overhead we only consider enrichment over cartesian closed categories.

In general for a cartesian closed category $\mathsf{V}$, a $\mathsf{V}$-theory is a $\mathsf{V}$-enriched Lawvere theory with natural number arities. We consider $\mathsf{V}$ as a choice of “method of computation” for algebraic theories. The main idea of this paper is that product-preserving functors between enriching categories allow for the translation between different kinds of semantics. This translation could be called “change of computation”—or, following standard mathematical terminology, change of base.

Because operational semantics uses graphs to represent terms and rewrites, one might expect some category like $\mathsf{Gph}$, the category of directed multigraphs, to be our main example of enriching category: that is, the “thing” of $n$-ary operations, or $n$-variable terms in a theory, is a directed graph whose edges are rewrites. This is known as small-step operational semantics, meaning each edge represents a single instance of a rewrite rule.

When studying formal languages, one wants to pass from this local view to a global view: given a term, one cares about its possible evolutions after not only one rewrite but any finite sequence of rewrites. We study how programs operate in finite time. In computer science, this corresponds to defining a rewrite relation and forming its transitive closure, called big-step operational semantics. This is the classic example which change of base aims to generalize.

However, there is a subtlety. We may try to model the translation from small-step to big-step operational semantics using the “free category” functor, which for any directed multigraph forms the category whose objects are vertices and morphisms are finite paths of edges. However, this functor does not preserve products. One might hope to cure this using a better-behaved variant of directed multigraphs, such as reflexive graphs. One advantage of reflexive graphs is that that each vertex has a distinguished edge from it to itself; these describe rewrites that “do nothing”. Thus, in a product of reflexive graphs there are edges describing the process of rewriting one factor while doing nothing in the other. This lets us handle parallelism. Unfortunately, as we shall explain, the free category functor from reflexive graphs to categories still fails to preserve products.

To obtain a product-preserving change of base taking us from small-step to big-step operational semantics, it seems the cleanest solution is to generalize graphs to simplicial sets. A simplicial set is a contravariant functor from the category $\Delta$ of finite linear orders and monotone maps to the category of sets and functions. It can be visualized as a space built from “simplices”, which generalize triangles to any dimension: point, line, triangle, tetrahedron, etc. For an introduction to simplicial sets, see Friedman [13]. We use $\mathsf{sSet}$ to denote the category of simplicial sets, namely $\mathsf{Set}^{\Delta^{\mathrm{op}}}$.

Simplicial sets allow one to generalize rewriting to higher-dimensional rewriting, but this is not our focus here. Indeed, we only need two facts about simplicial sets in this paper:

• •

There is a full and faithful embedding of $\mathsf{RGph}$, the category of reflexive graphs, in $\mathsf{sSet}$, so we can think of a reflexive graph as a special kind of simplicial set (namely one whose $n$-simplices for $n>1$ are all degenerate).

• •

The free category functor $\mathrm{FC}\colon\mathsf{sSet}\to\mathsf{Cat}$, often called “realization”, preserves products.

We thus obtain a spectrum of cartesian closed categories $\mathsf{V}$ to enrich over, each connected to the next by a product-preserving functor, which allow us to examine the computation of term calculi in various ways:

[TABLE]

In Section 2 we review Lawvere theories as a more explicit, but equivalent, presentation of finitary monads. In Section 3, we recall the basics of enrichment over cartesian closed categories. In Section 4 we give the central definition of $\mathsf{V}$-theory, adapted from the work of Lucyshyn-Wright [23]. Using his work we show that a $\mathsf{V}$-theory $\mathsf{T}$ gives a monadic adjunction between $\mathsf{V}$ and the $\mathsf{V}$-category of models of $\mathsf{T}$ in $\mathsf{V}$. This generalizes a fundamental result for Lawvere theories.

In Section 5 we discuss how suitable functors between enriching categories induce change of base: they transform theories, and their models, from one method of rewriting to another. Our main examples arise from this chain of adjunctions:

[TABLE]

The right adjoints here automatically preserve finite products, but the left adjoints do as well, and these are what we really need:

• •

The functor $\mathrm{FC}\colon\mathsf{sSet}\to\mathsf{Cat}$ maps a simplicial set (for example a reflexive graph) to the category it freely generates. Change of base along $\mathrm{FC}$ maps small-step operational semantics to big-step operational semantics.

• •

The functor $\mathrm{FP}\colon\mathsf{Cat}\to\mathsf{Pos}$ maps a category $C$ to the poset whose elements are objects of $C$, with $c\leq c^{\prime}$ iff $C$ has a morphism from $c$ to $c^{\prime}$. Change of base along $\mathrm{FP}$ maps big-step operational semantics to full-step operational semantics.

• •

The functor $\mathrm{FS}\colon\mathsf{Pos}\to\mathsf{Set}$ maps a poset $P$ to the set of “components” of $P$, where $p,p^{\prime}\in P$ are in the same component if $p\leq p^{\prime}$. Change of base along $\mathrm{FS}$ maps full-step operational semantics to denotational semantics.

In Section 6 we show that models of all $\mathsf{V}$-theories for all enriching $\mathsf{V}$ can be assimilated into one category using the Grothendieck construction. In Section 7 we bring all the strands together and demonstrate these concepts in applications. First we consider the $SKI$-combinator calculus, and then we show how theories enriched over the category of labelled graphs can be used to study bisimulation.

Acknowledgements

This paper builds upon the ideas of Mike Stay and Greg Meredith presented in “Representing operational semantics with enriched Lawvere theories” [31]. We appreciate their offer to let us develop this work further for use in the innovative distributed computing system RChain, and gratefully acknowledge the support of Pyrofex Corporation. We also thank Richard Garner, Todd Trimble and others at the $n$-Category Café for classifying cartesian closed categories where every object is a finite coproduct of copies of the terminal object [3].

2 Lawvere Theories

Algebraic structures are traditionally treated as sets equipped with operations obeying equations, but we can generalize such structures to live in any category with finite products. For example, given any category $\mathsf{C}$ with finite products, we can define a monoid internal to $\mathsf{C}$ to consist of:

[TABLE]

Lawvere theories formalize this idea. For example, there is a Lawvere theory $\mathsf{Th}(\mathsf{Mon})$, the category with finite products freely generated by an object $t$ equipped with an identity element $e\colon 1\to t$ and multiplication $m\colon t^{2}\to t$ obeying the associative law and unit laws listed above. This captures the “Platonic idea” of a monoid internal to a category with finite products. A monoid internal to $\mathsf{C}$ then corresponds to a functor $\mu\colon\mathsf{T}\to\mathsf{C}$ that preserves finite products.

In more detail, let $\mathsf{N}$ be any skeleton of the category of finite sets $\mathsf{FinSet}$. Because $\mathsf{N}$ is the free category with finite coproducts on $1$, $\mathsf{N}^{\mathrm{op}}$ is the free category with finite products on $1$. A Lawvere theory is a category with finite products $\mathsf{T}$ equipped with a functor $\tau\colon\mathsf{N}^{\mathrm{op}}\to\mathsf{T}$ that is the identity on objects and preserves finite products. Thus, a Lawvere theory is essentially a category generated by one object $\tau(1)=t$ and $n$-ary operations $t^{n}\to t$, as well as the projection and diagonal morphisms of finite products.

For efficiency let us call a functor that preserves finite products cartesian. Lawvere theories are the objects of a category $\mathsf{Law}$ whose morphisms are cartesian functors $f\colon\mathsf{T}\to\mathsf{T}^{\prime}$ that obey $f\tau=\tau^{\prime}$. More generally, for any category with finite products $\mathsf{C}$, a model of the Lawvere theory $\mathsf{T}$ in $\mathsf{C}$ is a cartesian functor $\mu\colon\mathsf{T}\to\mathsf{C}$. The models of $\mathsf{T}$ in $\mathsf{C}$ are the objects of a category $\mathsf{Mod}(\mathsf{T},\mathsf{C})$, in which the morphisms are natural transformations.

A theory can thus have models in many different contexts. For example, there is a Lawvere theory $\mathsf{Th}(\mathsf{Mon})$, the theory of monoids, described as above. Ordinary monoids are models of this theory in $\mathsf{Set}$, while topological monoids are models of this theory in $\mathsf{Top}$.

For completeness, it is worthwhile to mention the presentation of a Lawvere theory: how exactly does the above “sketch” of $\mathsf{Th}(\mathsf{Mon})$ produce a category with finite products? It is precisely analogous to the presentation of an algebra by generators and relations: we form the free category with finite products on the data given, and impose the required equations. The result is a category whose objects are powers of $t$, and whose morphisms are composites of products of the morphisms in $\mathsf{Th}(\mathsf{Mon})$, projections, deletions, symmetries and diagonals. A detailed account was given by Barr and Wells [5, Chap. 4].

In 1965, Linton [22] proved that Lawvere theories correspond to “finitary monads” on the category of sets. For every Lawvere theory $\mathsf{T}$, there is an adjunction:

[TABLE]

The functor

[TABLE]

sends each model $\mu$ to its underlying set, $X=\mu(\tau(1))$. Its left adjoint, the free model functor

[TABLE]

sends each finite set $n\in\mathsf{N}$ to the representable functor $\mathsf{T}(\tau(n),-)\colon\mathsf{T}\to\mathsf{Set}$, and in general any set $X$ to the colimit of all such representables as $n$ ranges over the poset of finite subsets of $X$. In rough terms, $F(X)$ is the model of all $n$-ary operations from $\mathsf{T}$ on the set $X$.

If we momentarily abbreviate $\mathsf{Mod}(\mathsf{T},\mathsf{Set})$ as $\mathsf{Mod}$, we obtain an adjunction

[TABLE]

where the left isomorphism arises from the Yoneda lemma, and the right isomorphism from the product preservation of $\mu$.

This adjunction induces a monad $T$ on $\mathsf{Set}$:

[TABLE]

The integral here is a coend, essentially a coproduct quotiented by the equations of the theory and the equations induced by the cartesian structure of the category. This forms the set of all terms that can be constructed from applying the operations to the elements, subject to the equations of the theory. The monad constructed this way is always finitary: that is, it preserves filtered colimits [2], or its action on sets is determined by its action on finite sets.

Conversely, for a monad $T$ on $\mathsf{Set}$, its Kleisli category $\mathsf{Kl}(T)$ is the category of all free algebras of the monad, which has all coproducts. There is a functor $k\colon\mathsf{Set}\to\mathsf{Kl}(T)$ that is the identity on objects and preserves coproducts. Thus,

[TABLE]

is a cartesian functor, and restricting its domain to $\mathsf{N}^{\mathrm{op}}$ is a Lawvere theory $k_{\_}T$. To see what this is doing, note that:

[TABLE]

where the latter is considered as $m$ $n$-ary operations in the Lawvere theory $k_{\_}T$. When $T$ is finitary, the monad arising from this Lawvere theory is naturally isomorphic to $T$ itself.

This correspondence sets up an equivalence between the category $\mathsf{Law}$ of Lawvere theories and the category of finitary monads on $\mathsf{Set}$. There is also an equivalence between the category $\mathsf{Mod}(\mathsf{T},\mathsf{Set})$ of models of a Lawvere theory $\mathsf{T}$ and the category of algebras of the corresponding finitary monad $T$. Furthermore, all this generalizes with $\mathsf{Set}$ replaced by any “locally finitely presentable” category [2]. For more details see [5, 21, 25].

One final point, provided to us by Mike Stay: while monads are often associated with functional programming languages such as Haskell, Lawvere theories correspond to interfaces or abstract classes in object-oriented programming. In these one declares various constants, types, and abstract functions satisfying tests, and then one implements the interface by assigning these elements, sets, functions, and equations—precisely a model in $\mathsf{Set}$. While people think of monads as the main example of “categories in programming”, in fact Lawvere theories are ubiquitous.

3 Enrichment

To incorporate the aspect of computation, we now turn to Lawvere theories that have hom-objects rather than mere hom-sets. To do this we use enriched category theory [19] and replace sets with objects of a cartesian closed category $\mathsf{V}$, called the “enriching” category or “base”. A $\mathsf{V}$-enriched category or $\mathsf{V}$-category $\mathsf{C}$ is:

[TABLE]

such that composition is associative and unital. A $\mathsf{V}$-functor $F\colon\mathsf{C}\to\mathsf{D}$ is:

[TABLE]

such that $F$ preserves composition and identity. A $\mathsf{V}$-natural transformation $\alpha\colon F\Rightarrow G$ is:

[TABLE]

such that $\alpha$ is “natural” in $a$: an evident square commutes. There is a 2-category $\mathsf{V}\mathsf{Cat}$ of $\mathsf{V}$-categories, $\mathsf{V}$-functors, and $\mathsf{V}$-natural transformations.

We can construct new $\mathsf{V}$-categories from old ones by taking products or opposites, in obvious ways. There is also a $\mathsf{V}$-category denoted $\underline{\mathsf{V}}$ with the same objects as $\mathsf{V}$ and with hom-objects given by the internal hom:

[TABLE]

The concepts of adjunction and monad generalize straightforwardly to $\mathsf{V}$-categories, and when we speak of an adjunction or monad in the enriched context this generalization is what we mean [19]. For example, there is an adjunction

[TABLE]

called “currying”.

We can generalize products and coproducts to the enriched context. Given a $\mathsf{V}$-category $\mathsf{C}$, the $\mathsf{V}$-coproduct of an $n$-tuple of objects $b_{\_}1,\dots,b_{\_}n\in\mathrm{Ob}(C)$ is an object $b$ equipped with a $\mathsf{V}$-natural isomorphism

[TABLE]

If such an object exists, we denote it by $\sum_{\_}{i=1}^{n}b_{\_}i$. This makes sense even when $n=0$: a 0-ary $\mathsf{V}$-coproduct in $\mathsf{C}$ is called a $\mathsf{V}$-initial object and denoted as $0_{\_}\mathsf{C}$. When $\mathsf{V}$ is cartesian closed, any finite coproduct that exists in $\mathsf{V}$ is also a $\mathsf{V}$-coproduct in $\underline{\mathsf{V}}$. In particular,

[TABLE]

whenever [math] is an initial object of $\mathsf{V}$. Conversely, any finite $\mathsf{V}$-coproduct that exists in $\mathsf{V}$ is also a coproduct in the usual sense.

Similarly, a $\mathsf{V}$-product of objects $b_{\_}1,\dots,b_{\_}n\in\mathrm{Ob}(C)$ is an object $b$ equipped with a $\mathsf{V}$-natural isomorphism

[TABLE]

If such an object $b$ exists, we denote it by $\prod_{\_}{i=1}^{n}b_{\_}i$. A 0-ary product in $\mathsf{C}$ is called a $\mathsf{V}$-terminal object and denoted as $1_{\_}\mathsf{C}$. Whenever $\mathsf{V}$ is cartesian closed, the finite products in $\mathsf{V}$ are also $\mathsf{V}$-products in $\underline{\mathsf{V}}$. In particular,

[TABLE]

where our chosen terminal object $1_{\_}\mathsf{V}$ is also $\mathsf{V}$-terminal. Conversely, any finite $\mathsf{V}$-product in $\mathsf{V}$ is also a product in the usual sense.

A general $\mathsf{V}$-category $\mathsf{C}$ does not exactly have projections from a $\mathsf{V}$-product to its factors, since given two objects $c,c^{\prime}\in\mathrm{Ob}(\mathsf{C})$ there is not, fundamentally, a set of morphisms from $c$ to $c^{\prime}$. Instead there is the hom-object $\mathsf{C}(c,c^{\prime})$, which is an object of $\mathsf{V}$. However, any object $v$ of $\mathsf{V}$ has a set of elements, namely morphisms $f\colon 1_{\_}\mathsf{V}\to v$. Elements of $\mathsf{C}(c,c^{\prime})$ act like morphisms from $c$ to $c^{\prime}$.

In particular, any $\mathsf{V}$-product $b=\prod_{\_}{i=1}^{n}b_{\_}i$ gives rise to elements

[TABLE]

which serve as substitutes for the projections in a usual product. These elements are defined as composites

[TABLE]

where the isomorphism comes from Eq. (2) and the last arrow is a projection in $\mathsf{V}$.

Even better, we can bundle up all these elements $p_{\_}i$ into a single element

[TABLE]

which serves as a substitute for the universal cone in a usual product. Starting from $p$ we can recover the $\mathsf{V}$-natural isomorphism in Eq. (2) as follows:

[TABLE]

where the last arrow is given by composition. Thus, we say a universal cone exhibiting $b$ as the $\mathsf{V}$-product of objects $b_{\_}1,\dots,b_{\_}n$ is an element $p\colon 1_{\_}\mathsf{V}\to\prod_{\_}{i=1}^{n}\mathsf{C}(b,b_{\_}i)$ such that the $\mathsf{V}$-natural transformation $\mathsf{C}(-,b)\to\prod_{\_}{i=1}^{n}\mathsf{C}(-,b_{\_}i)$ given by Eq. (3) is an isomorphism.

The advantage of this reformulation is that we can say a $\mathsf{V}$-functor $F\colon\mathsf{C}\to\mathsf{D}$ preserves finite $\mathsf{V}$-products if for every universal cone $p\colon 1_{\_}\mathsf{V}\to\prod_{\_}{i=1}^{n}\mathsf{C}(b,b_{\_}i)$ exhibiting $b$ as the $\mathsf{V}$-product of the objects $b_{\_}i$, the composite

[TABLE]

is universal cone exhibiting $F(b)$ as the $\mathsf{V}$-product of the objects $F(b_{\_}i)$.

A bit more subtly, generalizing the exponentials in $\mathsf{V}$, a $\mathsf{V}$-category $\mathsf{C}$ can have “powers”. Given $v\in\mathrm{Ob}(\mathsf{V})$, we say an object $c^{v}\in\mathrm{Ob}(\mathsf{C})$ is a $v$-power of $c\in\mathrm{Ob}(\mathsf{C})$ if it is equipped with a $\mathsf{V}$-natural isomorphism

[TABLE]

In the special case $\mathsf{V}=\mathsf{Set}$ this forces $c^{v}$ to be the $v$-fold product of copies of $c$. As with $\mathsf{V}$-products, it is useful to repackage the isomorphism of Eq. (4) so we can say what it means for a $\mathsf{V}$-functor to preserve $v$-powers. First, note that this isomorphism gives rise to an element

[TABLE]

namely the composite

[TABLE]

Conversely, any element $q\colon 1_{\_}\mathsf{V}\to\mathsf{C}(c^{v},c)^{v}$ determines a $\mathsf{V}$-natural transformation $e\colon C(-,c^{v})\to C(-,c)^{v}$, and we say $e$ is a universal cone if this $\mathsf{V}$-natural transformation is an isomorphism. Next, suppose $\mathsf{C}$ and $\mathsf{D}$ are $\mathsf{V}$-categories with $v$-powers. We say a $\mathsf{V}$-functor $F\colon\mathsf{C}\to\mathsf{D}$ preserves $v$-powers if it maps universal cones to universal cones.

There are just a few more technicalities. A category is locally finitely presentable if it is the category of models for a finite limits theory, and an object is finite if its representable functor is finitary: that is, it preserves filtered colimits [2]. A $\mathsf{V}$-category $\mathsf{C}$ is locally finitely presentable if its underlying category $\mathsf{C}_{\_}0$ is locally finitely presentable, $\mathsf{C}$ has finite powers, and $(-)^{x}\colon\mathsf{C}_{\_}0\to\mathsf{C}_{\_}0$ is finitary for all finitely presentable $x$. The details are not crucial here: all categories to be considered are locally finitely presentable. We will use $\mathsf{V}_{\_}f$ to denote the full subcategory of $\mathsf{V}$ of finite objects: in $\mathsf{sSet}$, these are simplicial sets with finitely many $n$-simplices for each $n$.

4 Enriched Lawvere Theories

Power introduced the notion of enriched Lawvere theory about twenty years ago, “in seeking a general account of what have been called notions of computation” [28]. The original definition is as follows: for a symmetric monoidal closed category $(\mathsf{V},\otimes,1)$, a “$\mathsf{V}$-enriched Lawvere theory” is a $\mathsf{V}$-category $\mathsf{T}$ that has powers by objects in $\mathsf{V}_{\_}f$, equipped with an identity-on-objects $\mathsf{V}$-functor

[TABLE]

that preserves these powers. A “model” of a $\mathsf{V}$-theory is a $\mathsf{V}$-functor $\mu\colon\mathsf{T}\to\mathsf{V}$ that preserves powers by finite objects of $\mathsf{V}$. There is a category $\mathsf{Mod}(\mathsf{T},\mathsf{V})$ whose objects are models and whose morphisms are $\mathsf{V}$-natural transformations. The monadic adjunction and equivalence of Section 2 generalize to the enriched setting.

In this paper, however, we only consider natural number arities, while still retaining enrichment. To do this we use the work of Lucyshyn-Wright [23], who along with Power [26] has generalized Power’s original ideas to allow a more flexible choice of arities. We also limit ourselves to the case where the tensor product of $\mathsf{V}$ is cartesian. This has a significant simplifying effect, yet it suffices for many cases of interest in computer science.

Thus, in all that follows, we let $(\mathsf{V},\times,1_{\_}\mathsf{V})$ be a cartesian closed category equipped with chosen finite coproducts of the terminal object $1_{\_}\mathsf{V}$, say

[TABLE]

Define $\mathsf{N}_{\_}\mathsf{V}$ to be the full subcategory of $\mathsf{V}$ containing just these objects $n_{\_}\mathsf{V}$. There is also a $\mathsf{V}$-category $\underline{\mathsf{N}}_{\_}\mathsf{V}$ whose objects are those of $\mathsf{N}_{\_}\mathsf{V}$ and whose hom-objects are given as in $\mathsf{V}$. We define the $\mathsf{V}$-category of arities for $\mathsf{V}$ to be

[TABLE]

We shall soon see that $\mathsf{A}_{\_}\mathsf{V}$ has finite $\mathsf{V}$-products.

Definition 1**.**

We define a $\mathsf{V}$-theory $(\mathsf{T},\tau)$ to be a $\mathsf{V}$-category $\mathsf{T}$ equipped with a $\mathsf{V}$-functor

[TABLE]

that is the identity on objects and preserves finite $\mathsf{V}$-products.

Definition 2**.**

A model of $\mathsf{T}$ in a $\mathsf{V}$-category $\mathsf{C}$ is a $\mathsf{V}$-functor

[TABLE]

that preserves finite $\mathsf{V}$-products.

Just as all the objects of a Lawvere theory are finite products of a single object, we shall see that all the objects of $\mathsf{T}$ are finite $\mathsf{V}$-products of the object

[TABLE]

Definition 3**.**

We define $\mathsf{V}\mathsf{Law}$, the category of $\mathsf{V}$-theories, to be the category for which an object is a $\mathsf{V}$-theory and a morphism from $(\mathsf{T},\tau)$ to $(\mathsf{T}^{\prime},\tau^{\prime})$ is a $\mathsf{V}$-functor $f\colon\mathsf{T}\to\mathsf{T}^{\prime}$ that preserves finite $\mathsf{V}$-products and has $f\tau=\tau^{\prime}$.

Definition 4**.**

For every $\mathsf{V}$-theory $(T,\tau)$ and every $\mathsf{V}$-category $\mathsf{C}$ with finite $\mathsf{V}$-products, we define $\mathsf{Mod}(\mathsf{T},\mathsf{C})$, the category of models of $(\mathsf{T},\tau)$ in $\mathsf{C}$, to be the category for which an object is a $\mathsf{V}$-functor $\mu\colon\mathsf{T}\to\mathsf{C}$ that preserves finite $\mathsf{V}$-products and a morphism is a $\mathsf{V}$-natural transformation.

The basic monadicity results for Lawvere theories generalize to $\mathsf{V}$-theories when $\mathsf{V}$ is complete and cocomplete, as in the main examples we consider: $\mathsf{V}=\mathsf{sSet},\mathsf{Cat},\mathsf{Pos},$ and $\mathsf{Set}$. Under this extra assumption $\mathsf{V}\mathsf{Law}$ and $\mathsf{Mod}(\mathsf{T},\mathsf{C})$ can be promoted to $\mathsf{V}$-categories, which we call $\underline{\mathsf{V}\mathsf{Law}}$ and $\underline{\mathsf{Mod}}(\mathsf{T},\mathsf{C})$. Furthermore, there is a $\mathsf{V}$-functor

[TABLE]

sending any model $\mu\colon\mathsf{T}\to\mathsf{V}$ to its underlying object $\mu(t)\in\mathsf{V}$. Recall that monads and adjunctions make sense in $\mathsf{V}\mathsf{Cat}$, just as they do in $\mathsf{Cat}$. The $\mathsf{V}$-functor $U$ has a left adjoint

[TABLE]

and $\underline{\mathsf{Mod}}(\mathsf{T},\mathsf{V})$ is equivalent to the $\mathsf{V}$-category of algebras of the resulting monad $T=UF$. More precisely:

Theorem 5**.**

Suppose $\mathsf{V}$ is cartesian closed, complete and cocomplete, and has chosen finite coproducts of the terminal object. Let $(\mathsf{T},\tau)$ be a $\mathsf{V}$-theory. Then there is a monadic adjunction

[TABLE]

Proof.

This follows from Lucyshyn-Wright’s general theory [23], so our task is simply to explain how. He allows $\mathsf{V}$ to be a symmetric monoidal category, and uses a more general concept of algebraic theory with a system of arities given by any fully faithful symmetric monoidal $\mathsf{V}$-functor $j\colon\mathsf{J}\to\underline{\mathsf{V}}$. For us $\mathsf{J}=\underline{\mathsf{N}}_{\_}\mathsf{V}$ and $j\colon\underline{\mathsf{N}}_{\_}\mathsf{V}\to\underline{\mathsf{V}}$ is the obvious inclusion; this is his Example 3.7.

Lucyshyn-Wright defines a $\mathsf{J}$-theory to be a $\mathsf{V}$-functor $\tau\colon\mathsf{J}^{\mathrm{op}}\to\mathsf{T}$ that is the identity on objects and preserves powers by objects in $\mathsf{J}$ (or more precisely, their images under $j$). For us $\mathsf{J}^{\mathrm{op}}=\mathsf{A}_{\_}\mathsf{V}$. So, to apply his theory, we need to show that a $\mathsf{V}$-functor $\tau\colon\mathsf{A}_{\_}\mathsf{V}\to\mathsf{T}$ preserves powers by objects in $\mathsf{N}_{\_}\mathsf{V}$ if and only if it preserves finite $\mathsf{V}$-products. This is Lemma 16 below.

He defines a model (or “algebra”) of a $\mathsf{J}$-theory to be a $\mathsf{V}$-functor $\tau\colon\mathsf{T}\to\underline{\mathsf{V}}$ that preserves powers by objects in $\mathsf{J}$. He defines a morphism of models to be a $\mathsf{V}$-natural transformation between such $\mathsf{V}$-functors. So, to apply his theory, we also need to show that when $\mathsf{J}=\underline{\mathsf{N}}_{\_}\mathsf{V}$, a $\mathsf{V}$-functor $\mu\colon\mathsf{T}\to\underline{\mathsf{V}}$ preserves powers by objects of $\mathsf{J}$ if and only if it preserves finite $\mathsf{V}$-products. This is Lemma 17 below.

A technical concept fundamental to Lucyshyn-Wright’s theory is that of an eleutheric system of arities $j\colon\mathsf{J}\to\underline{\mathsf{V}}$. This is one where the left Kan extension of any $\mathsf{V}$-functor $f\colon\mathsf{J}\to\underline{\mathsf{V}}$ along $j$ exists and is preserved by each $\mathsf{V}$-functor $\underline{\mathsf{V}}(x,-)\colon\underline{\mathsf{V}}\to\underline{\mathsf{V}}$. In Example 7.5.5 he shows that $j\colon\underline{\mathsf{N}}_{\_}\mathsf{V}\to\underline{\mathsf{V}}$ is eleutheric when $\mathsf{V}$ is countably cocomplete. In Thm. 8.9 shows that when $j\colon\mathsf{J}\to\underline{\mathsf{V}}$ is eleutheric, and has equalizers, we may form the $\mathsf{V}$-category $\underline{\mathsf{Mod}}(\mathsf{T},\mathsf{V})$, and that the forgetful $\mathsf{V}$-functor

[TABLE]

is monadic. This is the result we need. So, our theorem actually holds whenever $\mathsf{V}$ is cartesian closed, with equalizers and countable colimits, and has chosen finite coproducts of the initial object. ∎

Before turning to examples, a word about Lucyshyn-Wright’s construction of the left adjoint $F$ and the monad $T$ is in order. These rely on the “free model” on an object $n_{\_}\mathsf{V}\in\mathsf{V}$. This is the enriched generalization of the free model described in Section 2: it is the composite of $\tau^{\mathrm{op}}\colon\mathsf{A}_{\_}\mathsf{V}^{\mathrm{op}}\to\mathsf{T}^{\mathrm{op}}$ with the enriched Yoneda embedding $y\colon\mathsf{T}^{\mathrm{op}}\to[\mathsf{T},\mathsf{V}]$:

[TABLE]

Since an object of $\mathsf{V}$ does not necessarily have a “poset of finite subobjects” over which to take a filtered colimit (as in $\mathsf{Set}$), the extension of this “free model” functor $y\tau^{\mathrm{op}}$ to all of $\mathsf{V}$ is specified by a somewhat higher-powered generalization: it is the left Kan extension of $y\tau^{\mathrm{op}}$ along $j$.

[TABLE]

This is the universal “best solution” to the problem of making the triangle commute up to a $\mathsf{V}$-natural transformation. That is, for any functor $G\colon\mathsf{V}\to[\mathsf{T},\mathsf{V}]$ and $\mathsf{V}$-natural transformation $\theta\colon y\tau^{\mathrm{op}}\Rightarrow Gj$, the latter factors uniquely through $\eta$. From the adjunction between $\mathsf{V}$ and the category of models $\mathsf{Mod}(\mathsf{T},\mathsf{V})$ we obtain a $\mathsf{V}$-enriched monad

[TABLE]

and this has a more concrete formula as an enriched coend:

[TABLE]

We next give two examples of a rather abstract nature, where we show how $\mathsf{Cat}$-enriched Lawvere theories can describe categories with extra structure. In Section 7 we study examples more directly connected to operational semantics.

Example 6**.**

When $\mathsf{V}=\mathsf{Cat}$, a $\mathsf{V}$-category is a 2-category, so a $\mathsf{V}$-theory deserves to be called a 2-theory. For example, let $\mathsf{T}=\mathsf{Th}(\mathrm{PsMon})$ be the 2-theory of pseudomonoids. A pseudomonoid [10] is a weakened version of a monoid: rather than associativity and unitality equations, it has 2-isomorphisms called the associator and unitors, which we can treat as rewrite rules. To equate various possible rewrite sequences, these 2-isomorphisms must obey equations called “coherence laws”. Power [20] has introduced “enriched sketches” as a way of presenting enriched Lawvere theories. Informally, here is a presentation of the 2-theory for pseudomonoids:

[TABLE]

[TABLE]

[TABLE]

[TABLE]

We write the equations as commutative diagrams merely for convenience; they could also be written as equations in a more traditional style. The top diagram expresses the pentagon identity for the associator, while the bottom one expresses the usual coherence law involving the left and right unitors.

Models of $\mathsf{T}=\mathsf{Th}(\mathrm{PsMon})$ in $\mathsf{Cat}$ are monoidal categories: let us explore this example in more detail. A model of $\mathsf{T}$ is a finite-product-preserving 2-functor $\mu\colon\mathsf{T}\to\mathsf{Cat}$, which sends

[TABLE]

such that the coherence laws of the rewrites are preserved. Thus, a model is a category equipped with a tensor product $\otimes$ and unit object $I$ such that these operations are associative and unital up to natural isomorphism; so these models are precisely monoidal categories.

Given two models $\mu,\nu\colon\mathsf{T}\to\mathsf{Cat}$, a morphism of models is a 2-natural transformation $\varphi\colon\mu\Rightarrow\nu$; this amounts to a strict monoidal functor $\varphi\colon(\mathsf{C},\otimes_{\_}C,I_{\_}C)\to(\mathsf{D},\otimes_{\_}D,I_{\_}D)$. The strictness arises because morphisms between models are 2-natural transformations rather than pseudonatural transformations. There is a substantial amount of theory on pseudomonads and pseudoalgebras [7, 11], but to the authors’ knowledge the theory-monad correspondence has not yet been extended to include the case of weak naturality.

Finally, because $\mathsf{Cat}$ is complete and cocomplete, the category of models $\mathsf{Mod}(\mathsf{T},\mathsf{Cat})$ can be promoted to a 2-category $\underline{\mathsf{Mod}}(\mathsf{T},\mathsf{Cat})$. This is the 2-category of monoidal categories, strict monoidal functors, and monoidal natural transformations.

We can accomplish the same thing on the monad side: a $\mathsf{Cat}$-enriched monad is called a 2-monad, and $\mathsf{T}$ gives rise to the “free monoidal category” 2-monad $T$ on $\mathsf{Cat}$ [7]. To apply this 2-monad to $C\in\mathsf{Cat}$ we first form the free model on $\mathsf{C}$ by taking a left Kan extension as above, and then evaluate this model at the generating object. In the same way that the (underlying set of the) free monoid on a set $X$ consists of all finite strings of elements of $X$, $T(\mathsf{C})$ is the monoidal category consisting of all finite tensor products of objects of $\mathsf{C}$ and all morphisms built from those of $\mathsf{C}$ by composition and tensoring together with associators and unitors obeying the necessary coherence laws. Morphisms of these algebras are strict monoidal functors, while 2-morphisms are natural transformation. We thus have a 2-equivalence between $\underline{\mathsf{Mod}}(\mathsf{T},\mathsf{Cat})$ and the 2-category of algebras of $T$.

In this way, 2-theories generalize equipping set-like objects with operations obeying equations to equipping category-like objects with operations obeying equations up to transformations that obey equations of their own. In particular, this gives us a way to present graphical calculi such as string diagrams – the language of monoidal categories.

Example 7**.**

Enrichment generalizes operations in more ways than by weakening equations to coherent isomorphisms. We can also use 2-theories to describe other structures that make sense inside 2-categories, such as adjunctions.

For example, we may define a cartesian category $\mathsf{X}$ to be one equipped with right adjoints to the diagonal $\Delta_{\_}\mathsf{X}\colon\mathsf{X}\to\mathsf{X}\times\mathsf{X}$ and the unique functor $!_{\_}\mathsf{X}\colon\mathsf{X}\to 1_{\_}\mathsf{Cat}$. These right adjoints are a functor $m\colon\mathsf{X}^{2}\to\mathsf{X}$ describing binary products in $\mathsf{X}$ and a functor $e\colon 1\to\mathsf{X}$ picking out the terminal object in $\mathsf{X}$. We can capture the fact that they are right adjoints by providing them with units and counits and imposing the triangle equations. There is thus a 2-theory $\mathsf{Th}(\mathsf{Cart})$ whose models in $\mathsf{Cat}$ are categories with chosen finite products. More generally a model of this 2-theory in any 2-category $\mathsf{C}$ with finite products is called a cartesian object in $\mathsf{C}$.

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Again we write the equations as commutative diagrams, but this time commutative triangles of 2-morphisms in $\mathsf{Th}(\mathsf{Cart})$. These are the triangle equations that force $m$ to be the right adjoint of $\Delta_{\_}\mathsf{X}$ and $e$ to be the right adjoint of $!_{\_}\mathsf{X}$. A model of $\mathsf{Th}(\mathsf{Cart})$ is a category with chosen binary products and a chosen terminal object; morphisms in $\mathsf{Mod}(\mathsf{Th}(\mathsf{Cart}),\mathsf{Cat})$ are functors that strictly preserve this extra structure.

The subtle interplay between the cartesian structure of $\mathsf{Th}(\mathsf{Cart})$ and the cartesian structure of the object $\mathsf{X}\in\mathsf{Th}(\mathsf{Cart})$ is an example of the “microcosm principle”: objects with a given structure are most generally defined in a context that has the same sort of structure. As seen in the previous example, we can also define pseudomonoids in any 2-category with finite products, but this is excess to requirements: one can in fact define them more generally in any monoidal 2-category [10].

In fact, if we let arities be finite categories, we would have $\mathsf{Cat}$-theories of categories with finite limits and colimits. However, for the purposes of this paper we are using only natural number arities. This suffices for constructing $\mathsf{Th}(\mathsf{Cart})$ and also $\mathsf{Th}(\mathsf{CoCart})$, the theory of categories with chosen binary coproducts and a chosen initial object. Various other kinds of categories—distributive categories, rig categories, etc.—can also be expressed using $\mathsf{Cat}$-theories with natural number arities. This gives a systematic formalization of these categories, internalizes them to new contexts, and allows for the generation of 2-monads that describe them.

5 Change of Base

We now have the tools to formulate the main idea: a choice of enrichment for Lawvere theories corresponds to a choice of computation, and changing enrichments corresponds to a change of computation. We propose a general framework in which one can translate between different forms of computation: small-step, big-step, full-step operational semantics, and denotational semantics.

5.1 General results

Suppose that $\mathsf{V}$ and $\mathsf{W}$ are enriching categories of the sort we are considering: cartesian closed categories equipped with chosen finite coproducts of the terminal object. Suppose $F\colon\mathsf{V}\to W$ preserves finite products. This induces a change of base functor $F_{\_}*\colon\mathsf{V}\mathsf{Cat}\to\mathsf{W}\mathsf{Cat}$ [8] which takes any $\mathsf{V}$-category $\mathsf{C}$ and produces a $\mathsf{W}$-category $F_{\_}*(\mathsf{C})$ with the same objects but with

[TABLE]

for all objects $a,b$. Composition in $F_{\_}*(\mathsf{C})$ is defined by

[TABLE]

The identity-assigning morphisms are given by

[TABLE]

Moreover, if $f\colon\mathsf{C}\to\mathsf{D}\in\mathsf{V}\mathsf{Cat}$ is a $\mathsf{V}$-functor, there is a $\mathsf{W}$-functor $F_{\_}*(f)\colon F_{\_}*(C)\to F_{\_}*(D)$ that on objects equals $f$ and on hom-objects equals $F(f)$. If $\alpha\colon f\Rightarrow g$ is a $\mathsf{V}$-natural transformation and $c\in\mathrm{Ob}(\mathsf{C})$, then we define

[TABLE]

Thus, change of base actually gives a 2-functor from the 2-category of $\mathsf{V}$-categories, $\mathsf{V}$-functors and $\mathsf{V}$-natural transformations to the corresponding 2-category for $\mathsf{W}$.

In fact, the change of base operation gives a 2-functor

[TABLE]

where $\mathsf{Cart}\mathsf{Cat}$ is the 2-category of cartesian closed categories equipped with chosen finite coproducts of the terminal object, finite product preserving functors preserving these chosen finite coproducts, and natural transformations. In particular, if $\mathsf{V}$ has not just finite coproducts of the terminal object but all coproducts of this object, there is a map of adjunctions

[TABLE]

Each set $X$ is mapped to the $X$-indexed coproduct of the terminal object in $\mathsf{V}$ and conversely each object $v$ of $\mathsf{V}$ is represented in $\mathsf{Set}$ by the hom-set from the unit to $v$. The latter induces the “underlying category” change of base, which forgets the enrichment. The former induces the “free $\mathsf{V}$-enrichment” change of base, whereby ordinary $\mathsf{Set}$-categories are converted to $\mathsf{V}$-categories, denoted $\mathsf{C}\mapsto\underline{\mathsf{C}}$. These form an adjunction, because 2-functors preserve adjunctions.

We now study how change of base affects theories and their models. We start by asking when a functor $F\colon\mathsf{V}\to\mathsf{W}$ induces a change of base $F_{\_}*\colon\mathsf{V}\mathsf{Cat}\to\mathsf{W}\mathsf{Cat}$ that “preserves enriched theories”. That is, given a $\mathsf{V}$-theory

[TABLE]

we want to determine conditions for the base-changed functor

[TABLE]

to induce a $\mathsf{W}$-theory in a canonical way. Recall that we require $\mathsf{V}$ and $\mathsf{W}$ to be cartesian closed, equipped with chosen finite coproducts of their terminal objects. We thus expect the following conditions to be sufficient: $F$ should be cartesian, and it should preserve the chosen finite coproducts of the terminal object:

[TABLE]

for all $n$.

Given these conditions there is a $\mathsf{W}$-functor, in fact an isomorphism

[TABLE]

On objects this maps $n_{\_}\mathsf{W}$ to $n_{\_}\mathsf{V}$, and on hom-objects it is simply the identity from

[TABLE]

to

[TABLE]

where we use Lemma 13 in these computations.

Using this we obtain a composite $\mathsf{W}$-functor

[TABLE]

This is the identity on objects and preserves finite $\mathsf{V}$-products because each of the factors has these properties. It is thus a $\mathsf{W}$-theory.

Theorem 8**.**

Let $\mathsf{V}$, $\mathsf{W}$ be cartesian closed categories with chosen finite coproducts of their terminal objects, and let $F\colon\mathsf{V}\to\mathsf{W}$ be a cartesian functor that preserves these chosen coproducts. Then $F_{\_}*$ preserves enriched theories: that is, for every $\mathsf{V}$-theory $\tau_{\_}\mathsf{V}\colon\mathsf{A}_{\_}\mathsf{V}\to\mathsf{T}$, the $\mathsf{W}$-functor

[TABLE]

is a $\mathsf{W}$-theory. Moreover, $F_{\_}*$ preserves models: for every model $\mu\colon\mathsf{T}\to\mathsf{C}$ of $(\mathsf{T},\tau_{\_}\mathsf{V})$, the $\mathsf{W}$-functor $F_{\_}*(\mu)\colon F_{\_}*(\mathsf{T})\to F_{\_}*(\mathsf{C})$ is a model of $(F_{\_}*(\mathsf{T}),\tau_{\_}\mathsf{W})$.

Proof.

We have shown the first part. For the second, by Lemma 17 it suffices to assume that $\mu$ preserves finite $\mathsf{N}_{\_}V$-powers and check that $F_{\_}*(\mu)$ preserves $\mathsf{N}_{\_}\mathsf{W}$-powers. We leave this as an exercise to the reader. ∎

Hence, any cartesian functor that preserves chosen finite coproducts of the terminal object gives a change of base. It thus provides for a method of translating formal languages between various “modes of operation”. Moreover, this reasoning generalizes to multisorted $\mathsf{V}$-theories, enriched theories which have multiple sorts: given any $n\in\mathbb{N}$, the monoidal subcategory $(\mathsf{N}_{\_}\mathsf{V})^{n}$ is also an eleutheric system of arities, so Lucyshyn-Wright’s monadicity theorem still applies.

5.2 Examples

Now let us look at some examples. The most important changes of base are the left adjoints in this diagram from Sec. 1:

[TABLE]

The first step describes the translation from small-step to big-step operational semantics. As already mentioned, we need to use simplicial sets rather than graphs; let us now say more about why.

A first attempt might use directed multigraphs. Such graphs have directed edges and allow multiple edges between any pair of vertices. The category $\mathsf{Gph}$ of directed multigraphs is $\mathsf{Set}^{\mathsf{G}}$ where $\mathsf{G}$ is the category with two objects $v$ and $e$ and two morphisms $s,t\colon e\to v$. The “free category” functor $\mathrm{F}\colon\mathsf{Gph}\to\mathsf{Cat}$ gives for every graph $G$ a category $\mathrm{F}(G)$ as follows:

[TABLE]

The morphisms in $\mathrm{F}(G)$ are called edge paths. Just as an edge describes a single rewrite in small-step operational sematics, an edge path describes a sequence of rewrites in big-step operational semantics. The edge paths with $n=0$ serve as identity morphisms.

Unfortunately, $\mathrm{F}\colon\mathsf{Gph}\to\mathsf{Cat}$ does not preserve products, so it is not a valid base change. To see this, let $G_{\_}1$ be $\{0\xrightarrow{e}1\}$, the graph with two vertices and one edge. The product $G_{\_}1\times G_{\_}1$ looks like this:

[TABLE]

Thus the free category $\mathrm{F}(G_{\_}1\times G_{\_}1)$ has just one non-identity morphism. On the other hand $\mathrm{F}(G_{\_}1)\times\mathrm{F}(G_{\_}1)$ has five non-identity morphisms, shown here:

[TABLE]

where we write $\mathrm{id}$ for identity morphisms and $e$ for the edge path consisting of the single edge $e$. Note that the triangles in this diagram commute. In terms of rewriting, the category $\mathrm{F}(G_{\_}1\times G_{\_}1)$ only allows the rewrite $e\colon 0\to 1$ to occur simultaneously in both factors, while $\mathrm{F}(G_{\_}1)\times\mathrm{F}(G_{\_}1)$ allows it to occur independently in either factor, in a commuting way.

To solve this problem one, might try to use reflexive graphs. Such graphs have directed edges and allows multiple edges between any pair of vertices; further, each vertex $v$ is equipped with a distinguished identity edge $i(v)$ from $v$ to itself. The category $\mathsf{RGph}$ of reflexive graphs is $\mathsf{Set}^{\mathsf{R}}$, where $\mathsf{R}$ is the category with two objects $v$ and $e$, two morphisms $s,t\colon e\to v$, and a morphism $i\colon v\to e$ obeying $si=ti=1_{\_}v$. There is a free category functor $\mathrm{F}^{\prime}\colon\mathsf{RGph}\to\mathsf{Cat}$, which is like the free category functor for $\mathsf{Gph}$ except that we identify an edge path $(e_{\_}1,\dots,e_{\_}n)$ with the same path having $e_{\_}i$ omitted when $e_{\_}i$ is an identity edge. Thus, the identity edges of a reflexive graph $R$ become identity morphisms in $\mathrm{F}^{\prime}(R)$.

The advantage of reflexive graphs is that they allow rewrites in a product to occur independently in either factor. For example, let $R_{\_}1$ be the reflexive graph with two vertices and one non-identity edge, $\{0\xrightarrow{e}1\}$ (where we do not draw identity edges). The product $R_{\_}1\times R_{\_}1$ has five non-identity edges:

[TABLE]

Thus, the free category $\mathrm{F}^{\prime}(R_{\_}1\times R_{\_}1)$ has two noncommuting triangles. On the other hand, $\mathrm{F}^{\prime}(R_{\_}1)\times\mathrm{F}^{\prime}(R_{\_}1)$ is the product of the category with a single non-identity morphism $e\colon 0\to 1$ with itself, so it is this category:

[TABLE]

with two commuting triangles. Thus $\mathrm{F}^{\prime}\colon\mathsf{RGph}\to\mathsf{Cat}$ again fails to preserve products, though in some sense it comes closer. Simply put, while $\mathrm{F}^{\prime}(R_{\_}1\times R_{\_}1)$ allows rewrites to be done independently in either factor, these rewrites fail to commute.

To solve this problem we shall consider $\mathsf{RGph}$ as a full subcategory of the category of simplicial sets, $\mathsf{sSet}$. To do this, we treat a reflexive graph as a simplicial set with only degenerate simplices for $n>1$. There is a left adjoint $\mathrm{FC}\colon\mathsf{sSet}\to\mathsf{Cat}$, usually called realization, and this functor preserves products [17, Prop. B.0.15]. For example, if we treat $R_{\_}1$ above as a simplicial set and take the product $R_{\_}1\times R_{\_}1$ in $\mathsf{sSet}$, this contains triangles that force the triangles in $\mathrm{FC}(R_{\_}1\times R_{\_}1)$ to commute. Thus, realization provides a useful base change to translate from small-step operational semantics to big-step operational semantics.

The other functors in our chain of left adjoints are simpler. The “free poset” functor $\mathrm{FP}\colon\mathsf{Cat}\to\mathsf{Pos}$ maps any category $C$ to the poset whose elements are objects of $C$, with $c\leq c^{\prime}$ iff $C$ contains a morphism from $c$ to $c^{\prime}$. This is a valid change of base—i.e., it preserves finite products—because the product of posets is defined in the same way as the product of categories. If we apply this change of base to a model of a $\mathsf{Cat}$-enriched theory, we obtain a model of a $\mathsf{Pos}$-enriched theory that says for any pair of terms the presence or absence of a rewrite sequence from one to the other, without distinguishing between different sequences. We call this full-step operational semantics.

Finally, we can pass to the purely abstract realm where all computation is already complete. For this we take the left adjoint $\mathrm{FS}\colon\mathsf{Pos}\to\mathsf{Set}$ to the functor $\mathrm{UP}\colon\mathsf{Set}\to\mathsf{Pos}$ sending any set to the discrete poset on that set. The functor $\mathrm{FS}$ collapses each connected component of the poset to a point; this too preserves finite products. If we apply this change of base to a model of a $\mathsf{Pos}$-enriched theory, we obtain a model of a $\mathsf{Set}$-enriched theory that extracts its denotational semantics by identifying all terms related by rewrites. If the rewrites are terminating and confluent, we can choose a representative term for each equivalence class: the unique term that admits no nontrivial rewrites.

6 The Category of All Models

In addition to base change, there are two other natural and useful ways to go between models of enriched theories. Suppose $\mathsf{V}$ is any cartesian closed category with chosen finite coproducts of the terminal object. Let $\mathsf{V}\mathsf{Mod}(\mathsf{T},\mathsf{C})$ be the category of models of a $\mathsf{V}$-theory $\mathsf{T}$ in a $\mathsf{V}$-category $\mathsf{C}$ with finite $\mathsf{V}$-products, as in Defn. 4. A morphism of $\mathsf{V}$-theories $f\colon\mathsf{T}\to\mathsf{T}^{\prime}$ induces a change of theory functor between the respective categories of models

[TABLE]

defined as pre-composition with $f$. Similarly, a $\mathsf{V}$-product-preserving $\mathsf{V}$-functor $g\colon\mathsf{C}\to\mathsf{C}^{\prime}$ induces a change of context functor

[TABLE]

defined as post-composition with $g$.

These translations, as well as change of base, can all be packed up nicely using the Grothendieck construction: given any functor $F\colon\mathsf{D}\to\mathsf{Cat}$, there is a category $\int F$ that encapsulates all of the categories in the image of $F$, defined as follows:

[TABLE]

Moreover there is a functor $p_{\_}F\colon\int F\to\mathsf{D}$ given as follows:

[TABLE]

For more details see [8, 16]. We noted in Section 4 that $\mathsf{V}\mathsf{Law}$ and $\mathsf{Mod}(\mathsf{T},\mathsf{C})$ can be promoted to $\mathsf{V}$-categories when $\mathsf{V}$ is complete and cocomplete: this and further conditions imply that we can use the enriched Grothendieck construction [6], but we focus on the ordinary Grothendieck construction for simplicity.

First, this construction lets us bring together all models of all different $\mathsf{V}$-theories in all different contexts into one category. All the $\mathsf{V}$-theories are objects of $\mathsf{V}\mathsf{Law}$, as in Defn. 3. We can also create a category of all “$\mathsf{V}$-contexts”.

Definition 9**.**

Let $\mathsf{V}\mathsf{Con}$, the category of $\mathsf{V}$-contexts be the category for which an object is a $\mathsf{V}$-category with finite $\mathsf{V}$-products and a morphism is a functor that preserves finite $\mathsf{V}$-products.

There is a functor

[TABLE]

that sends any object $(\mathsf{T},\mathsf{C})$ to $\mathsf{V}\mathsf{Mod}(\mathsf{T},\mathsf{C})$ and any morphism $(f,g)$ to $f^{*}g_{\_}*=g_{\_}*f^{*}$. The functoriality of $\mathsf{V}\mathsf{Mod}$ summarizes the contravariant change-of-theory and the covariant change-of-context above. Applying the Grothedieck construction we obtain a category $\int\mathsf{V}\mathsf{Mod}$. Technically an object of $\int\mathsf{V}\mathsf{Mod}$ is a triple $(T,\mathsf{C},\mu)$, but more intuitively it is a model $\mu\colon\mathsf{T}\to\mathsf{C}$ of any $\mathsf{V}$-theory $\mathsf{T}$ in any $\mathsf{V}$-context $\mathsf{C}$. Similarly, a morphism

[TABLE]

in $\mathsf{V}\mathsf{Mod}$ consists of:

• •

a morphism of $\mathsf{V}$-theories $f\colon\mathsf{T}^{\prime}\to\mathsf{T}$,

• •

a $\mathsf{V}$-functor $g\colon\mathsf{C}\to\mathsf{C}^{\prime}$ that preserves finite $\mathsf{V}$-products, and

• •

a $\mathsf{V}$-natural transformation $\alpha\colon g\circ\mu\circ f\Rightarrow\mu^{\prime}$.

This is a natural way to map between different models of different theories in different contexts.

We can go further by creating a category that even contains all choices of enriching categories $\mathsf{V}$:

Definition 10**.**

Let $\mathsf{Enr}$ be the category for which an object is a cartesian closed category $\mathsf{V}$ with chosen finite coproducts of the terminal object, and a morphism is a cartesian functor $F\colon\mathsf{V}\to\mathsf{W}$ preserving the chosen finite coproducts of the initial object.

There is a functor

[TABLE]

that maps any object $\mathsf{V}$ to $\int\mathsf{V}\mathsf{Mod}$ and any morphism $F\colon\mathsf{V}\to\mathsf{W}$ to a functor

[TABLE]

that has the following effect:

• •

$\mathrm{Mod}(F)$ maps any object $(\mathsf{T},\mathsf{C},\mu)$ to the object $(F_{\_}*(\mathsf{T}),F_{\_}*(\mathsf{C}),F_{\_}*(\mu))$.

• •

$\mathrm{Mod}(F)$ maps any morphism $(f,g,\alpha)$ to the morphism $(F_{\_}*(f),F_{\_}*(g),F_{\_}*(\alpha))$.

Thus, we can use the Grothendieck construction once more to pack up all choices of enrichment into one big category:

Theorem 11**.**

There is a category $\int\mathrm{Mod}$ in which:

• •

An object is a choice of cartesian closed category $\mathsf{V}$ with chosen finite coproducts of the terminal object, a $\mathsf{V}$-theory $\mathsf{T}$, a $\mathsf{V}$-category $\mathsf{C}$ with finite $\mathsf{V}$-products, and a model $\mu\colon\mathsf{T}\to\mathsf{C}$.

• •

A morphism is a cartesian functor $F\colon\mathsf{V}\to\mathsf{W}$ preserving the chosen finite coproducts of the terminal object and a morphism $(f,g,\alpha)\colon(F_{\_}*(\mathsf{T}),F_{\_}*(\mathsf{C}),F_{\_}*(\mu))\to(\mathsf{T},\mathsf{C},\mu)$ in $\mathsf{W}\mathsf{Mod}$.

This category allows us to formally treat morphisms between objects of “different kinds”, something we often use informally, for example when speaking of a map from a set to a ring, or a group to a topological group. There are many unexplored questions about the large, heterogeneous categories which arise from the Grothendieck construction, regarding what unusual structure may be gained, such as limits and colimits with objects of different types, or identifying “processes” in which the kinds of objects change in an essential way. However, for our purposes we need only recognize that enriched Lawvere theories can be assimilated into one category, providing a single place in which to study change of base, change of theory, and change of context.

7 Applications

In computer science literature, enriched algebraic theories have primarily been studied in the context of “computational effects” [14]. Stay and Meredith have proposed that enriched Lawvere theories can be utilized for the design of programming languages [32]. To circumvent the question of variable binding, there is another approach which instead uses an enriched theory as a “compiler” which translates a language with binding to one without. This idea comes from the subject of combinatory logic.

7.1 The $SKI$-combinator calculus

The $\lambda$-calculus is an elegant formal language which is the foundation of functional computation, the model of intuitionistic logic, and the internal logic of cartesian closed categories: this is the Curry–Howard–Lambek correspondence [4].

Terms are constructed recursively by variables, application, and abstraction, and the basic rewrite is beta reduction, which substitutes the applied term for the bound variable:

[TABLE]

Despite the apparent simplicity, there are complications regarding substitution. Consider the term $M=\lambda x.(\lambda y.(xy))$: if this is applied to the variable $y$, then $(M\;y)\Rightarrow\lambda y.(y\;y)$ — but this is not intended, because the $y$ in $M$ is just a placeholder, it is “bound” by whatever will be plugged in, while the $y$ being substituted is “free”, meaning it can refer to some other value or function in the program. Hence whenever a free variable is to be substituted for a bound variable, we need to rename the bound variable to prevent “variable capture” (e.g. $(My)\Rightarrow\lambda z.(y\;z)$).

This problem was noticed early in the history of mathematical foundations, even before the $\lambda$-calculus, and so Moses Schönfinkel invented combinatory logic [29], a basic form of logic without the red tape of variable binding, hence without functions in the usual sense. The $SKI$-calculus is the “variable-free” representation of the $\lambda$-calculus; $\lambda$-terms are translated via “abstraction elimination” into strings of combinators and applications. This is a technique for programming languages to minimize the subtleties of variables.

The insight of Stay and Meredith [31] is that even though enriched Lawvere theories have no variables, they can be used to study some programming languages through abstraction elimination. When representing such a language as a $\mathsf{sSet}$-theory, vertices—i.e., 0-simplices—in the simplicial set $\hom(1,t)$ serve as closed terms. More generally, vertices in $\hom(t^{n},t)$ serve as terms with $n$ free variables. Rewrite rules going between such terms are edges—i.e., 1-simplices—in $\hom(t^{n},t)$.

To illustrate this, here is the theory of the $SKI$-calculus:

[TABLE]

[TABLE]

These rewrites are implicitly universally quantified; i.e., they apply to arbitrary subterms $-,=,\equiv$ without any variable binding involved, by using the cartesian structure of the category. They are edges with vertices as follows:

[TABLE]

Here $l,r$ denote the unitors and $s$ the symmetry of the product.

These abstract rules are evaluated on concrete terms by “plugging in” via precomposition. For example:

[TABLE]

A model of this theory is a $\mathsf{sSet}$-functor $\mu\colon\mathsf{Th}(\mathsf{SKI})\to\mathsf{sSet}$ that preserves finite $\mathsf{sSet}$-products. This gives a simplicial set $\mu(t)$. The images of the nullary operations $S,K,I$ under $\mu$ are distinguished vertices of $\mu(t)$, because $\mu$ preserves the terminal object, which “points out” vertices. The image of the binary operation $(-\;-)$ gives for every pair of vertices $(u,v)\in\mu(t)^{2}$ a vertex $(u\;v)$ in $\mu(t)$ which stands for their application. In this way all possible terms built from $S$, $K$, $I$ and application give vertices in $\mu(t)$. Similarly, rewrites going between these terms give edges in $\mu(t)$. Thus, $\mu$ gives a map of simplicial sets

[TABLE]

that maps the “syntactic” graph of all closed terms and rewrites to the “semantic” graph: each rewrite between terms in the theory is sent to a rewrite between the images of these terms in the model.

The fact that $\mu((-\;-)):\mu(t)^{2}\to\mu(t)$ is not just a function but a map of simplicial sets means that pairs of edges $(a\to b,c\to d)$ in $\mathsf{Th}(\mathsf{SKI})(1,t)$ are sent to edges $(a\;b)\to(c\;d)$ in $\mathsf{sSet}(1,\mu(t))$. This gives the full complexity of the theory: given a large term (program), there are many different ways it can be computed—and some take fewer steps than others:

[TABLE]

More generally, the image $\mu(t)^{n}$ is a simplicial set whose vertices are $SKI$-terms with $n$ free variables and whose edges are $n$-tuples of rewrites between such terms. This is because the enriched functor $\mu$ gives maps of simplicial sets

[TABLE]

As the $n$-ary operations and rewrites thereof are built up from application and the three rewrites, everything works the same way as in the case $n=0$.

This process is intuitive, but how do we actually define the model, as a functor, to pick out a specific graph? There are many models of $\mathsf{Th}(\mathsf{SKI})$, but in particular we care about the canonical free model, which means that $\mu(t)$ is simply the graph of all closed terms and rewrites in the $SKI$-calculus. This utilizes the enriched adjunction of Thm. 5:

[TABLE]

Then the canonical model of closed terms and rewrites is simply the free model on the empty graph, $f_{\_}\mathsf{sSet}(\emptyset)$, i.e. the $\mathsf{V}$-functor $\mathsf{T}(1,-)\colon\mathsf{T}\to\mathsf{V}$. Hence for us, the syntax and semantics of the $SKI$ combinator calculus are unified in the model

[TABLE]

Here we reap the benefits of the abstract construction: the graph $\mu_{\_}{SKI}^{\mathsf{sSet}}(t)$ represents the small-step operational semantics of the $SKI$-calculus:

[TABLE]

We can now consider the base changes in Sec. 5.2, to translate between several important kinds of computation for the $SKI$-calculus. Given the above description of $\mathsf{Th}(\mathsf{SKI})$ as enriched in $\mathsf{sSet}$, we can apply the “free category” realization functor to the hom-objects, turning these reflexive graphs into categories.

Here we enjoy the fact that this functor indeed preserves products, which is essential for considering tuples of programs running in parallel: for example if we designate $G_{\_}n:=\mathsf{Th}(\mathsf{SKI})(t^{n},t)$, then the fact that $\mathrm{FC}(G_{\_}m\times G_{\_}n)\cong\mathrm{FC}(G_{\_}m)\times\mathrm{FC}(G_{\_}n)$ ensures that the execution of an $m$-term program and an $n$-term program simultaneously (but independently) is the same as executing one, then the other.

Thus $\mathrm{FC}$ translates the theory of $SKI$ from “small-step” to “big-step” operational semantics:

$\mathrm{FC}_{\_}*(\mathsf{Th}(\mathsf{SKI}))$ is the theory of the $SKI$ calculus, but now with hom-categories whose morphisms represent finite sequences of rewrite edges in the original theory.

We can continue these base-changes to “full-step” and denotational semantics, by applying the “free poset” and “free set” (connected components) functors to the hom-objects of this theory. This process demonstrates the idea of having a “spectrum” of detail with which to analyze the semantics of a programming language, or general algebraic theory.

For example, consider the following computation:

[TABLE]

The solid arrows are the one-step rewrites of the initial $\mathsf{sSet}$-theory; applying $\mathrm{FC}_{\_}*$ gives the dotted composites, and $\mathrm{FP}_{\_}*$ asserts that all composites between any two objects are equal. Finally, $\mathrm{FS}_{\_}*$ collapses the whole diagram to $S$. This is a simple demonstration of the basic stages of computation: small-step, big-step, full-step, and denotational semantics.

7.2 Change of theory

We can equip term calculi with reduction contexts, which determine when rewrites are valid, thus giving the language a certain evaluation strategy. For example, the “weak head normal form” is given by only allowing rewrites on the left-hand side of the term.

We can do this for $\mathsf{Th}(\mathsf{SKI})$ by adding a reduction context marker as a unary operation, and a structural congruence rule which pushes the marker to the left-hand side of an application; lastly we modify the rewrite rules to be valid only when the marker is present:

[TABLE]

[TABLE]

The $SKI$-calculus is thereby equipped with “lazy evaluation”, an essential paradigm in modern programming. This represents a broad potential application of equipping theories with computational methods, such as evaluation strategies.

Moreover, these equipments can be added or removed as needed: using change-of-theory, we can utilize a “free reduction” $\mathsf{sSet}$-functor $f_{\_}R\colon\mathsf{Th}(\mathsf{SKI})\to\mathsf{Th}(\mathsf{SKI}+\mathsf{R})$:

[TABLE]

This essentially interprets ordinary $SKI$ as having every subterm be a reduction context. This is a $\mathsf{sSet}$-functor because its hom component consists of graph-homomorphisms

[TABLE]

which simply send each application to its postcomposition with $R$, and each rewrite to its “marked” correspondent.

So, by precomposition this induces the change of theory on categories of models:

[TABLE]

for all semantic categories $\mathsf{C}$, which forgets the reduction contexts.

Similarly, there is a $\mathsf{sSet}$-functor $u_{\_}R\colon\mathsf{Th}(SKI+R)\to\mathsf{Th}(SKI)$ which forgets reduction contexts, by sending $\sigma_{\_}r,\kappa_{\_}r,\iota_{\_}r\mapsto\sigma,\kappa,\iota$ and $R\mapsto id_{\_}t$; this latter is the only way that the marked reductions can be mapped coherently to the unmarked. However, this means that $u_{\_}R^{*}$ does not give the desired change-of-theory of “freely adjoining contexts”, because collapsing $R$ to the identity eliminates the significance of the marker.

This illustrates a key aspect of categorical universal algebra: because change-of-theory is given by precomposition and is thus contravariant, properties (equations) and structure (operations) can only be removed. This is a necessary limitation, at least in the present setup, but there are ways to make do. These abstract theories are not floating in isolation but are implemented in code: one can simply use a “maximal theory” with all pertinent structure, then selectively forget as needed.

8 Conclusion

We have shown how enriched Lawvere theories provide a framework for unifying the structure and behavior of formal languages. Enriching theories in category-like structures reifies operational semantics by incorporating rewrites between terms, and appropriate functors between enriching categories induce change-of-base functors between categories of enriched theories and models—this simplified condition is obtained by using only natural number arities. This idea is motivated by an example sequence of such functors, which provide a spectrum of detail in which to study the rewriting properties of a theory.

Change of base, along with change of theory and change of context, can be used to create a single category $\mathrm{Mod}$, which consists of all models of all enriched Lawvere theories in all contexts. We have demonstrated these concepts with the theory of combinatory logic, $\mathsf{Th}(\mathsf{SKI})$, describing a change of base from small-step operational semantics to big-step to full-step to denotational semantics.

Finally, we suggest that there are many interesting change-of-base functors, by considering an endofunctor on the category of labelled transition systems, which quotients by the bisimulation relation and is indeed a change of base.

Appendix A Natural Number Arities

In this appendix we prove the lemmas required for Theorem 5 and our study of base change in Section 5. Throughout we assume $\mathsf{V}$ is cartesian closed with chosen $n$-fold coproducts $n_{\_}\mathsf{V}$ of its terminal object.

We begin with a study of $\mathsf{N}_{\_}\mathsf{V}$, the full subcategory of $\mathsf{V}$ on the objects $n_{\_}\mathsf{V}$. First we must resolve a potential ambiguity. On the one hand, for any object $b$ of $\mathsf{V}$ we can form the exponential $b^{n_{\_}\mathsf{V}}$. On the other hand, we can take the product of $n$ copies of $b$, which we call $b^{n}$. Luckily these are the same, or at least naturally isomorphic:

Lemma 12**.**

The functors $(-)^{n_{\_}\mathsf{V}}\colon\mathsf{V}\to\mathsf{V}$ and $(-)^{n}\colon\mathsf{V}\to\mathsf{V}$ are naturally isomorphic.

Proof.

If $a,b\in\mathsf{V}$, then

[TABLE]

Each of these isomorphisms is natural in $a$ and $b$, so by the Yoneda lemma $(-)^{n_{\_}\mathsf{V}}\cong(-)^{n}$. ∎

We can now understand coproducts, products and exponentials in $\mathsf{N}_{\_}\mathsf{V}$:

Lemma 13**.**

If $\mathsf{V}$ is any cartesian closed category with chosen coproducts of the initial object then $\mathsf{N}_{\_}\mathsf{V}$ is cartesian closed, with finite coproducts. The unique initial object of $\mathsf{N}_{\_}V$ is $0_{\_}\mathsf{V}$. The binary coproducts in $\mathsf{N}_{\_}\mathsf{V}$ are unique, given by

[TABLE]

The unique terminal object of $\mathsf{N}_{\_}\mathsf{V}$ is $1_{\_}\mathsf{V}$, and the binary products are unique, given by

[TABLE]

Exponentials in $\mathsf{N}_{\_}\mathsf{V}$ are also unique, given by

[TABLE]

Proof.

In $\mathsf{V}$ we know that $0_{\_}\mathsf{V}$ is an initial object and $1_{\_}\mathsf{V}$ is a terminal object, by definition. Since the subcategory $\mathsf{N}_{\_}\mathsf{V}$ is skeletal $0_{\_}\mathsf{V}$ is the unique initial object and $1_{\_}\mathsf{V}$ is the unique terminal object in $\mathsf{N}_{\_}\mathsf{V}$. Similarly, in $\mathsf{V}$ we have defined $(m+n)_{\_}\mathsf{V}$ to be a coproduct of $m_{\_}\mathsf{V}$ and $n_{\_}\mathsf{V}$, so in $\mathsf{N}_{\_}\mathsf{V}$ it is the unique such, and we can unambiguously write

[TABLE]

Products distribute over coproducts in any cartesian closed category, so in $\mathsf{V}$ we have

[TABLE]

where in the second step we use the distributive law twice. It follows that $\mathsf{N}_{\_}\mathsf{V}$ has finite products, and since this subcategory is skeletal they are unique, given by

[TABLE]

Finally, by Lemma 12 we have

[TABLE]

It follows that $\mathsf{N}_{\_}\mathsf{V}$ has exponentials, and since this subcategory is skeletal they are unique, given by

[TABLE]

We warn the reader that $\hom(m_{\_}\mathsf{V},n_{\_}\mathsf{V})$ may not have $n^{m}$ elements. It does in $\mathsf{sSet},\mathsf{Cat},\mathsf{Pos}$ and of course $\mathsf{Set}$, but not in $\mathsf{V}=\mathsf{Set}^{k}$, where $|\hom(m_{\_}\mathsf{V},n_{\_}\mathsf{V})|=n^{km}$. In fact, whenever $\mathsf{N}_{\_}\mathsf{V}$ has finite hom-sets it is equivalent to $\mathsf{FinSet}^{k}$ for some $k$. The reason is that $2_{\_}\mathsf{V}$ is an internal Boolean algebra in $\mathsf{V}$, so its set of elements $\hom(1_{\_}\mathsf{V},2_{\_}\mathsf{V})$ must be some Boolean algebra $B$ in $\mathsf{Set}$. A further argument due to Garner and Trimble shows that $\mathsf{N}_{\_}\mathsf{V}$ is completely characterized, up to equivalence, by this Boolean algebra, and any Boolean algebra can occur [3]. If this Boolean algebra is finite it must be isomorphic to $\{0,1\}^{k}$ for some $k\geq 0$. In this case, $\mathsf{N}_{\_}\mathsf{V}$ is equivalent to $\mathsf{FinSet}^{k}$.

Now suppose $\mathsf{C}$ is a $\mathsf{V}$-category. The question arises whether the power of an object $c\in\mathsf{C}$ by $n_{\_}\mathsf{V}$ must also be the $\mathsf{V}$-product of $n$ copies of $c$. The answer is yes:

Lemma 14**.**

Let $\mathsf{C}$ be a $\mathsf{V}$-category and $c\in\mathrm{Ob}(\mathsf{C})$. Then the power $c^{n_{\_}\mathsf{V}}$ exists if and only if the $n$-fold $\mathsf{V}$-product $c^{n}$ exists, in which case they are isomorphic.

Proof.

In Section 3 we saw that an object $b\in\mathrm{Ob}(\mathsf{C})$ is an $n$-fold $\mathsf{V}$-product of copies of $c$ precisely when it is equipped with a universal cone

[TABLE]

Similarly, $b$ is an $n_{\_}\mathsf{V}$-power of $c$ when it is equipped with a universal cone

[TABLE]

The universality properties have the same form, and by Lemma 12 the functors $(-)^{n}\colon\mathsf{V}\to\mathsf{V}$ and $(-)^{n_{\_}\mathsf{V}}\colon\mathsf{V}\to\mathsf{V}$ are naturally isomorphic. Thus, given either sort of universal cone we get the other, so an object is an $n$-fold product of copies of $c$ if and only if it is the $n_{\_}\mathsf{V}$-power of $c$. ∎

Lemma 15**.**

Suppose $\mathsf{C}$ is a $\mathsf{V}$-category such that every object is the $n$-fold $\mathsf{V}$-product $c^{n}$ of some object $c$. Then a $\mathsf{V}$-functor $F\colon\mathsf{C}\to\mathsf{D}$ preserves finite $\mathsf{V}$-products if and only if it preserves powers by all objects of $\mathsf{N}_{\_}\mathsf{V}$.

Proof.

Define a “finite $\mathsf{V}$-power” to be a finite $\mathsf{V}$-product of $n$ copies of the same object. The $\mathsf{V}$-functor $F$ preserves finite $\mathsf{V}$-powers if and only if it maps any universal cone

[TABLE]

in $\mathsf{C}$ to a universal cone in $\mathsf{D}$. Similarly, $F$ preserves powers by all objects of $\mathsf{N}_{\_}\mathsf{V}$ if and only if it maps any universal cone

[TABLE]

in $\mathsf{C}$ to a universal cone in $\mathsf{D}$. Two kinds of universality are involved here, but since they have the same form, and since Lemma 12 says the functors $(-)^{n}\colon\mathsf{V}\to\mathsf{V}$ and $(-)^{n_{\_}\mathsf{V}}\colon\mathsf{V}\to\mathsf{V}$ are naturally isomorphic, it follows that $F$ preserves finite $\mathsf{V}$-powers if and only if it preserves powers by all objects of $\mathsf{N}_{\_}\mathsf{V}$.

It thus suffices to show that $F$ preserves finite $\mathsf{V}$-products if and only if it preserves finite $\mathsf{V}$-powers. This follows from the assumption that every object is the $n$-fold $\mathsf{V}$-product $c^{n}$ of some object $c$. ∎

Lemma 16**.**

Let $\mathsf{V}$ be cartesian closed with chosen finite coproducts of the terminal object and let $\mathsf{T}$ be a $\mathsf{V}$-category. These conditions for a $\mathsf{V}$-functor $\tau\colon\mathsf{A}_{\_}\mathsf{V}\to\mathsf{T}$ are equivalent:

$(T,\tau)$ is a $\mathsf{V}$-theory, 2. 2.

$\tau$ preserves finite $\mathsf{V}$-products, 3. 3.

$\tau$ preserves powers by objects of $\mathsf{N}_{\_}\mathsf{V}$.

Proof.

Conditions 1 and 2 are equivalent by definition. Since $\mathsf{A}_{\_}\mathsf{V}=\underline{\mathsf{N}}_{\_}\mathsf{V}^{\mathrm{op}}$, finite $\mathsf{V}$-products in $\mathsf{A}_{\_}\mathsf{V}$ are the same as finite $\mathsf{V}$-coproducts in $\underline{\mathsf{N}}_{\_}\mathsf{V}$, which are the same as finite coproducts in $\mathsf{N}_{\_}\mathsf{V}$. Since every object in $\underline{\mathsf{N}}_{\_}\mathsf{V}$ is a finite coproduct of copies of $1_{\_}\mathsf{V}$, Lemma 15 implies that conditions 2 and 3 are equivalent. ∎

Lemma 17**.**

Given a $\mathsf{V}$-theory $(\mathsf{T},\tau)$ and a $\mathsf{V}$-functor $\mu\colon\mathsf{T}\to\mathsf{C}$, the following conditions are equivalent:

• •

$\mu$ is a model of $(\mathsf{T},\tau)$,

• •

$\mu$ preserves finite $\mathsf{V}$-products,

• •

$\mu$ preserves powers by objects of $\mathsf{N}_{\_}\mathsf{V}$.

Proof.

Conditions 1 and 2 are equivalent by definition. Since $\tau$ is the identity on objects and preserves $\mathsf{V}$-products each object of $\mathsf{T}$ is of the form $t^{n}$ where $t=\tau(1_{\_}\mathsf{V})$. Thus, Lemma 15 implies that conditions 2 and 3 are equivalent. ∎