lawvere.tex

\documentclass[a4paper,UKenglish]{article}
\usepackage[letterpaper, margin=1.2in]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{authblk}
\usepackage{pict2e}
\usepackage[mathscr]{euscript}
\usepackage{tikz-cd}
\tikzstyle{none}=[inner sep=0pt]
\tikzstyle{circ}=[circle,fill=black,draw,inner sep=3pt]
\usepackage{fancybox}
\usepackage[all,2cell]{xy} \UseAllTwocells
\usetikzlibrary{arrows, positioning, intersections}
\input{coya-tikz.tex}
\tikzset{%
	symbol/.style={%
		draw=none,
		every to/.append style={%
			edge node={node [sloped, allow upside down, auto=false]{$#1$}}}
	}
}
\theoremstyle{definition}
\newtheorem{definition}{Definition}[section]
\newtheorem{theorem}{Theorem}
\newtheorem*{theorem*}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}{Corollary}[theorem]

\def\rd{\rotatebox[origin=c]{90}{$\dashv$}} %rotate dash right
\def\ld{\rotatebox[origin=c]{-90}{$\dashv$}} %rotate dash left

\newcommand{\Th}{\mathrm{Th}}
\newcommand{\Gph}{\mathrm{Gph}}
\newcommand{\Set}{\mathrm{Set}}
\newcommand{\Grp}{\mathrm{Grp}}
\newcommand{\Cat}{\mathrm{Cat}}
\newcommand{\Law}{\mathrm{Law}}
\newcommand{\Mnd}{\mathrm{Mnd}}
\newcommand{\Top}{\mathrm{Top}}
\newcommand{\Mon}{\mathrm{Mon}}
\newcommand{\Alg}{\mathrm{Alg}}
\newcommand{\CCC}{\mathrm{CCC}}
\newcommand{\Pos}{\mathrm{Pos}}
\newcommand{\Mod}{\mathrm{Mod}}
\newcommand{\FinSet}{\mathrm{FinSet}}

\newcommand{\FC}{\mathrm{FC}}
\newcommand{\FP}{\mathrm{FP}}
\newcommand{\US}{\mathrm{US}}

\newcommand{\op}{\mathrm{op}}
\newcommand{\NN}{\mathrm{N}}
\newcommand{\pic}{$\pi$-calculus}
\newcommand{\V}{\mathscr{V}}
\newcommand{\W}{\mathscr{W}}
\newcommand{\D}{\mathscr{D}}
\newcommand{\C}{\mathscr{C}}
\newcommand{\K}{\mathscr{K}}
\newcommand{\J}{\mathscr{J}}
\newcommand{\T}{\mathscr{T}}
\newcommand{\pfk}{\pitchfork}

\begin{document}

\title{Operation through Enrichment}
\author{John C. Baez and Christian Williams\\University of California, Riverside}

\maketitle

\section{Introduction}

Formal systems are often defined without intrinsic connection to how they actually \textit{operate} in practice. In everyday computation, the \textit{structure} of the program is separate from the \textit{dynamics} - but their disparity is the primary source of error. If these are unified in one mathematical object, the system can be proven \textit{correct by construction}. \textbf{Operational semantics} \cite{sos} is an essential tool in language design and verification, which formally specifies program behavior by \textit{labelled transition systems}, or labelled directed graphs:
\begin{center}\begin{tikzcd}(\lambda x.x+x \; , \; 2) \ar{r}{\beta} & 2+2 \ar{r}{+} & 4\end{tikzcd}\end{center}

The idea is to \textit{reify} operational semantics via \textbf{enrichment} \cite{enrich}. In the categorical representation of an algebraic theory, the objects are \textit{types}, and the morphisms are \textit{terms}; hence to represent the actual \textit{process} of computation, we need the higher-level notion of \textit{rewriting} one term into another - the hom-object or ``thing of morphisms" between two terms should be not a set but a \textit{category}-like structure, where these 2-morphisms represent \textit{rewrites}. For instance, the $SK$-combinator calculus is the ``abstraction-free'' $\lambda$-calculus, generated by two basic rewrite rules (see $\S$8):

\[\begin{minipage}{.2 \textwidth}
		\begin{tikzcd}
		t^3 \ar[bend right,swap,""name=1]{d}{(((Sx)y)z)} \ar[bend left,""name=2]{d}{((xz)(yz))}\\
		t \ar[Rightarrow, from=1, to=2]
		\end{tikzcd}
	\end{minipage}\qquad \qquad
	\begin{minipage}{.2 \textwidth}
		\begin{tikzcd}
		t^2 \ar[bend right,swap,""name=1]{d}{((Kx)y)} \ar[bend left,""name=2]{d}{x}\\
		t \ar[Rightarrow, from=1, to=2]
		\end{tikzcd}
\end{minipage}\]

A \textbf{Lawvere theory} \cite{lawvere} defines an algebraic structure abstractly, as a category $\T$ generated by powers of a single object $t$, for ``term'', and morphisms $t^n \to t$ representing $n$-ary operations, satisfying equations. This presents the \textit{theory} of a kind of algebra, which can be modelled in a category $\C$ by a power-preserving functor $\mu:\T \to \C$. This is a very general notion of ``algebra'' - computational formalisms are also presented by generators and relations: in particular, a \textbf{term calculus} represents a \textit{formal language} by sorts, term constructors, and congruence rules.

Using enriched Lawvere theories for operational semantics has been explored in the past. This was studied in the case of categories by Seely \cite{seely}, posets by Ghani and L\"uth \cite{ghani}, and others, for various related purposes. Here we allow quite general enrichments, to incorporate these approaches in a common framework - but we focus attention on graph-enriched Lawvere theories, which have a clear connection to the original idea of operational semantics:

\[\begin{array}{rl}
\text{sorts} & \text{: generating object } t\\
\text{term constructors} & \text{: generating morphisms } t^n \to t\\
\text{structural congruence} & \text{: commuting diagrams}\\
\text{\textasteriskcentered \quad rewrite rules} & \text{: generating hom-edges\quad\textasteriskcentered}\\
\end{array}\]

There are many other useful enriching categories. Better yet, there are functors between them that allow the seamless \textit{transition} between different kinds of operational semantics. There is a \textit{spectrum} of enriching categories which forms a gradient of resolution for the semantics of term calculi. For an enriching category $\V$, a \textbf{$\V$-theory} is a $\V$-enriched Lawvere theory with natural number arities (see $\S$4):\\\\
\textbf{Graphs}: $\Gph$-theories represent ``small-step" operational semantics * \\ - a hom-graph edge represents a \textit{single} term rewrite.\\
\textbf{Categories}: $\Cat$-theories represent ``big-step" operational semantics:\\ - identity and composition represent the \textit{reflexive-transitive} closure of the rewrite relation.\\
\textbf{Posets}: $\Pos$-theories represent ``full-step" operational semantics:\\ - a hom-poset boolean represents the \textit{existence} of a big-step rewrite.\\
\textbf{Sets}: $\Set$-theories represent denotational semantics (provided the calculus is \textit{confluent}, see \cite{lam}):\\ - a hom-set element represents an \textit{equivalence class} of the symmetric closure of the big-step relation.\\\\
(We will use \textit{reflexive} graphs, meaning every vertex has a distinguished self-loop; this is not the convention, but it is needed for the ``free category'' functor to be a change-of-semantics ($\S$6).)\\

Operational semantics is unified by enriched Lawvere theories and canonical functors between enriching categories. This provides a more systematic categorical representation of computation.

A motivating example is ``logic as a distributive law" \cite{ladl}, an algorithm for deriving a spatial-behavioral type system from a formal presentation of a computational calculus. Essential properties such as soundness be proven, a powerful query language is generated, and modalities can be ``built in" to express principles of the system.

This idea impacts more than computation, and even though these concepts have been well-known for decades, the practical significance has not been fully realized. With the modern paradigm of ``programs $\simeq$ proofs'', this method applies to many subjects throughout mathematics. We demonstrate this idea with several examples, and consider future potential.\\

We gratefully acknowledge the support of Pyrofex Incorporated.

\section{Lawvere Theories}
Computer science loves monads, but they are widely regarded as somewhat mysterious. They are almost too elegant; it is difficult to ``grok'' how they work before working with them significantly. This is fairly ironic, because most are actually equivalent to something much more straightforward: Lawvere theories.

The ``theory of monoids'' can be defined without any reference to sets:
\[\begin{array}{rl}
\text{an object} & M\\
\text{an identity element} & e:1 \to M\\
\text{and multiplication} & m: M^2 \to M\\
\text{with associativity} & m \circ (m \times M) = m \circ (M \times m)\\
\text{and unitality} & e \circ M = M = M \circ e\\
\end{array}\]

\textit{Lawvere theories} formalize this idea. They were originally called \textit{finite product} theories: a skeleton $\NN$ of the category of finite sets $\FinSet$ is the free category with finite coproducts on $1$ - every finite set is equal to the disjoint union of copies of $\{*\}$; conversely, $\NN^\op$ is the free category with finite \textit{products} on $1$. So, a category with finite products $\T$ equipped with a strictly product-preserving bijective-on-objects functor $\tau:\NN^\op \to \T$ is essentially a category generated by one object $\tau(1) = M$ and $n$-ary operations $M^n \to M$, as well as the projection and diagonal morphisms of finite products. Lawvere theories form a category $\Law$, with finite-product functors $f: \T\to \T'$ such that $f\tau = \tau'$.

The abstraction of this definition is powerful: the syntax encapsulates the algebraic theory, \textit{independent} of semantics, and then one is free to realize $M$ as almost any formal object. For another category with finite products $\C$, a \textbf{model} of the Lawvere theory in $\C$ is a product-preserving functor $\mu: \T \to \C$. By the ``free'' property above, this functor is determined by $\mu(\tau(1)) = \mu(M) = X \in \C$. The models of $\T$ in $\C$ form a category $[\T,\C]_{fp}$, in which the morphisms are natural transformations. The general theory can be thereby modelled in many useful ways. For example, ordinary groups are models $\T_\Grp \to \Set$, while functors $\T_\Grp \to \Top$ are topological groups.

Lawvere theories and \textit{finitary monads} provide complementary representations of algebraic structures and computation, as discussed by Hyland and Power in \cite{ltam}, and they were proven to be equivalent by Linton in \cite{linton}. For every Lawvere theory $\T$, there is an adjunction:

\[\begin{tikzcd}
	\Set \arrow[bend left=10,below]{rr}{F}
	& \ld &
	\arrow[bend left=10,above]{ll}{U} \left[\T,\Set\right]_{fp}
\end{tikzcd}\]

There is the \textit{underlying set} functor $U:[\T,\Set]_{fp} \to \Set$ which sends each model $\mu$ to the image of the generating object, $\mu(\tau(1)) = X$ in $\Set$. There is the \textit{free model} functor $F:\Set \to [\T,\Set]_{fp}$ which sends each finite set $n$ to the representable functor $\T(|n|,-):\T \to \Set$, and in general a set $X$ to the functor which sends $t^n \in \T$ to the set of all $n$-ary operations on $X$: $\{f(x_1,...,x_n)|f\in \T(n,1), x_i\in X\}$ - this is the \textit{filtered colimit} of representables indexed by the poset of finite subsets of $X$ \cite{nlab}, which pertains to conditions of finitude (see $\S$3). These form the adjunction: $$\Mod(F(n),\mu) \cong \mu(n) \cong \Set(n,U(\mu))$$ The left isomorphism is by the Yoneda lemma, and the right isomorphism is by the universal property of $(-)^n$ in $\Set$. Essentially, these are opposite ways of representing the $n$-ary operations of a model.

This adjunction induces a monad $T$ on $\Set$, which sends each set $X$ to the set of all terms in the theory on $X$ up to equality - the integral symbol is a \textit{coend}, essentially a coproduct quotiented by the equations of the theory: $$T(X) = \int^{n\in \NN} \T(n,1) \times X^n$$

Conversely, for a monad $T$ on $\Set$, its \textit{Kleisli category} is the category of all \textit{free algebras} of the monad. There is a ``comparison'' functor $k: \Set \to Kl(T)$ which is the identity on objects and preserves products, so restricting the domain of $k$ to $\NN$ forms the canonical Lawvere theory corresponding to the monad. This restriction is what limits the equivalence to \textit{finitary} monads ($\S$3). There is a good explanation of all this in Milewski's categorical computation blog \cite{milew}.

The correspondence of Lawvere theories and finitary monads forms an equivalence between the category of Lawvere theories and the category of finitary monads on $\Set$, as well as the categories of models and algebras for every corresponding pair $(\T, T)$: $$\mathrm{Law} \cong \mathrm{Mnd}_f$$ $$\Mod(\T) \cong \Alg(T)$$ This generalizes to arbitrary \textit{locally finitely presentable} modelling categories $\C$ ($\S$3). The previous references suffice; we do not need further details. 

\section{Enrichment}
We generalize \textit{sets} of morphisms to \textit{objects} of morphisms, to endow formal systems with operational information. Let $(\V,\otimes,I)$ be a monoidal category \cite{maclane}, the ``enriching'' category.

A \textbf{$\V$-category} or $\V$-enriched category $\C$ is:
\[\begin{array}{rl}
\text{a collection of objects} & Obj(\C)\\
\text{a hom-object function} & \C(-,-):Obj(\C) \times Obj(\C) \to Obj(\V)\\
\text{composition morphisms} & \circ_{a,b,c}:\C(b,c) \otimes \C(a,b) \to \C(a,c) \quad \forall a,b,c \in Obj(\C)\\
\text{identity elements} & i_a:I\to\C(a,a) \quad \forall a \in Obj(\C)\\
\end{array}\]
such that composition is associative and unital.

A \textbf{$\V$-functor} $F:\C \to \D$ is:
\[\begin{array}{rl}
\text{a function} & F_0: Obj(\C) \to Obj(\D)\\
\text{hom-morphisms} & F_{ab}: \C(a,b) \to \D(Fa,Fb) \quad \forall a,b \in \C\\
\end{array}\]
such that $F$ is compatible with composition and identity.

A \textbf{$\V$-natural transformation} $\alpha: F \Rightarrow G$ is:
\[\begin{array}{rl}
\text{a family} & \alpha_a: I \to \D(Fa,Ga) \quad \forall a \in Obj(\C)\\
\end{array}\]
such that $\alpha$ is ``natural'' in $a$. Hence there is a \textit{2-category} \textbf{$\V\Cat$} of $\V$-categories, $\V$-functors, and $\V$-natural transformations. See \cite{enrich} for reference.

Let $\V$ be a \textbf{closed symmetric monoidal category}, providing
\[\begin{array}{rl}
\text{internal hom} & [-,-]:\V^\op\otimes \V \to \V\\
\text{symmetry braiding} & \tau_{a,b}:a\otimes b\cong b\otimes a \quad \forall a,b \in Obj(\C)\\
\text{tensor-hom adjunction} & \V(a\otimes b,c) \cong \V(a,[b,c]) \quad \forall a,b,c \in Obj(\V)\\
\end{array}\]
Then $\V$ is \textit{itself} a $\V$-category, denoted $\tilde{\V}$, with internal hom as the hom-object function. The tensor-hom adjunction is the all-important \textit{currying}; the counit is \textit{evaluation}, in the fundamental sense. This generalizes to an \textit{action} of $\V$ on any $\V$-category $\C$: for $x \in Obj(\V)$ and $a,b \in Obj(\C)$, the \textbf{power} of $b$ by $x$ and the \textbf{copower} of $a$ by $x$ are objects of $\C$ which represent the adjunction:
\begin{equation}\label{eq:co-power}
	\C(a\odot x,b) \cong \left[x, \C(a,b)\right] \cong \C(a,x\pfk b)
\end{equation}
and $\C$ is $\V$-powered or copowered if all powers or copowers exist.

These are the two basic forms of \textit{enriched limit} and \textit{colimit}, which are not especially intuitive; but they are a direct generalization of a familiar idea in the category of sets. In $\Set$, the power is the ``exponential'' function set and the copower is the product. To generalize this to an action on other $\Set$-categories, note that:
\[\begin{array}{lcr}
	X \pfk Y = & Y^X & \cong \prod_{x\in X}Y\\
	\\
	X \odot Y = & X \times Y & \cong \coprod_{y\in Y}X
\end{array}\]
So, categories are canonically $\Set$-powered or copowered by indexed products or coproducts of copies of an object, provided that these exist. Even though the definition of Lawvere theory seems to be all about products, it is actually about \textit{powers}, because these constitute the \textit{arities} of the operations. This is precisely what is generalized in the enriched form.

(We will use exponential notation $x\pfk b = b^x$, and denote the unit $I$ by 1, because the enriching categories under consideration are cartesian.)

There are just a few more technicalities. Given a $\V$-category $\C$, one often considers the \textit{Yoneda embedding} into the $\V$-presheaf category $[\C^\op, \V]$, and it is important if certain subcategories are representable; generally, some properties of $\C$ depend on a condition of ``finitude'' \cite{finite}. A category is \textbf{locally finitely presentable} if it is the category of models for a \textit{sketch}, a theory with not only products but general \textit{limits}, and an object is finitely presentable or \textit{finite} if its representable functor is \textbf{finitary}, or preserves filtered colimits. A $\V$-category $\C$ is locally finitely presentable if the underlying category $\C_0$ is LFP, $\C$ has finite powers, and $(-)^x: \C_0 \to \C_0$ is finitary for all finitely presentable $x$.

The details are not crucial - all categories to be considered are locally finitely presentable. Denote by $\V_f$ the subcategory of $\V$ of finite objects - in $\Gph$, these are simply graphs with finitely many vertices and edges.

\section{Enriched Lawvere theories}
All of these abstract definitions culminate in the central concept: for a symmetric monoidal closed category $(\V,\otimes,I)$, a \textit{$\V$-enriched Lawvere theory} \`a la Power \cite{power} is a finitely-powered $\V$-category $\T$ equipped with a strictly power-preserving bijective-on-objects $\V$-functor $\tau:\V_f^\op \to \T$. A \textit{model} of a $\V$-theory is a finite-power $\V$-functor $\mu:\T \to \V$, and $\V$-natural transformations between them form the $\V$-category of models $[\T,\V]_{fp}$. The monadic adjunction and equivalence of $\S$2 generalize to $\V$-theories, as originally formulated by Power.

However, this requires $\T$ to have \textit{all} powers of $\V_f$, i.e. the theory must have arities for every finite object of $\V$. It is potentially very useful to include these generalized arities, but this introduces the question of how to \textit{present} such a theory; this is much more subtle and abstract than $n$-ary operations. However, this is not needed for our purposes - we only need \textit{natural number} arities, while still retaining enrichment.

A very general and useful definition of enriched algebraic theory was introduced by Lucyshyn-Wright \cite{rbb}, which allows for theories to be parameterized by a \textbf{system of arities}, a full subcategory inclusion $j: \J \xhookrightarrow{} \V$ containing the monoidal unit and closed under tensor.

A $\V$-enriched algebraic theory with $j$-arities or \textbf{$\J$-$\V$ theory} $(\T,\tau)$ is a $\V$-category $\T$ equipped with a $\J$-power preserving bijective-on-objects $\V$-functor $\tau:\tilde{\J}^\op \to \T$. A \textbf{model} of this theory in a $\V$-category $\C$ is a finite-power preserving $\V$-functor $\T \to \C$.

A $\J$-$\V$ theory is essentially a $\V$-category with objects being $\J$-powers $t^J$ of a generating object $t$, for $J \in \J$ - note that $t$ itself is $t^I$. In the same way that every $n\in \NN^\op$ is a power of $1 \in \Set$, every $J\in \tilde{\J}$ is a power of the monoidal unit $I\in \V$ (using equation \ref{eq:co-power}): $$\tilde{\J}(J\odot I,J) \cong [I, \tilde{\J}(J,J)] \cong \tilde{\J}(J,J^I)$$ This is just the direct generalization of the usual isomorphisms $J \times I \simeq J \simeq J^I$. Since a $\tau$ preserves $\J$-powers, this implies that every object of $\T$ is a power of $t = \tau(I)$.

Of course, these form categories: $\J$-$\V$ theories and $\J$-power preserving $\V$-functors $f: \T \to \T'$ such that $f\tau = \tau'$ give the category $\V\Law$; and for every theory $\T$ and every $\V$-category $\C$ with $\J$-powers, there is the category $\Mod(\T,\C)$ of $\V$-functors and $\V$-natural transformations between them. (Note: if $\V$ is a \textit{cosmos}, i.e. complete and cocomplete, then $\V\Cat$ has \textit{enriched functor categories} - hence $\V\Law$ and $\Mod(\T,\C)$ are actually $\V$-categories. This is potentially useful, and the ``operational'' $\V$'s of this paper are indeed cosmoi.)

Here is an overview of the concepts: 

\[\begin{array}{ccccl}
j: & \J & \hookrightarrow & \V & \text{arities}\\
& & & \frown & \text{enrichment}\\
\tau: & \tilde{\J}^\op & \to & \T & \text{theory}\\
& & & (\downarrow) & \text{models}\\
& & & \C & \text{semantics}\\
\end{array}\]

This parameterization is quite general; for example, Power's definition is the case $\J = \V_f$. A system of arities is \textbf{eleutheric} if left Kan extensions along $j$ exist and are preserved by $\V(K,-)$ for all $K \in Ob(\J)$. This is what is needed to have the essential \textit{monadicity} theorems: Lucyshyn-Wright proved that any $\J$-$\V$ theory for an eleutheric system of arities has a category of models for $\C = \V$ which is \textit{monadic} over $\V$, and the induced $\V$-monad is ``j-ary'' in that it ``conditionally preserves $\J$-flat colimits'', i.e. can be thought of as a monad with $\J$ arities.

The usual kinds of arities are eleutheric: in particular, finite cardinals. Hence, $\NN$-$\V$ theories have all of the nice relations with monads as ordinary Lawvere theories, and the same arities - but they now have the rich ``operational'' information of $\V$, and this $\V$ is adaptable.

\section{Change of Base}

We propose a general framework in which one can \textit{transition} seamlessly between different forms of operational semantics: small-step, big-step, full-step, denotational:
\[\begin{tikzcd}[column sep=small]
\Gph \arrow[bend left,below]{rr}{F_C}
& \ld &
\arrow[bend left,above]{ll}{U_G} \Cat \arrow[bend left,below]{rr}{F_P}
& \ld &
\arrow[bend left,above]{ll}{U_C} \Pos \arrow[bend left,below]{rr}{U_S}
& \rd &
\Set \arrow[bend left,above]{ll}{F_P}
\end{tikzcd}\]
This is effected by a \textbf{monoidal functor} - a functor $$(F,\lambda,\upsilon): (\V,\otimes_\V,I_\V) \to (\W,\otimes_\W,I_\W)$$ which transfers the tensor and unit via the \textit{laxor} and \textit{unitor}
\[\begin{array}{rl}
\lambda: & F(a) \otimes_\W F(b) \to F(a\otimes_\V b)\\
\upsilon: & I_\W \to F(I_\V)
\end{array}\]
such that $\lambda$ is natural in $a,b$ and associative, and unital relative to $\upsilon$.

This induces a \textbf{change of base} functor $F_*:\V\Cat \to \W\Cat$ \cite{borceux}. This is the strange but elegant operation on enriched categories whereby the objects remain unchanged, but the hom-objects are transformed by the functor between enriching categories. If $f: \C \to \D \in \V\Cat$ is a $\V$-functor, then $F_*(f)_{obj} = f_{obj}$ and $F_*(f)_{hom} = F\circ f_{hom}$, and $F_*(\C)$ is defined:

\[\begin{array}{rl}
\text{objects} & Obj(\C)\\
\text{hom-function} & F \circ \C(-,-)\\
\text{composition} & F(\circ_{a,b,c}) \circ \lambda\\
\text{identity} & F(i_a) \circ \upsilon\\
\end{array}\]
The change of base operation forms a 2-functor (or ``$\Cat$-functor''):
\[\begin{array}{ccc}
\Mon\Cat & \xrightarrow{(-)_*} & 2\Cat\\
(F: \V\to\W) & \mapsto & (F_*: \V\Cat\to\W\Cat)
\end{array}\]
In particular, there is an important correspondence of adjunctions:
\[\begin{tikzcd}
	\Set \arrow[bend left,below]{rr}{-\odot I}
	& \ld &
	\arrow[bend left,above]{ll}{\V(I,-)} \V
	\arrow[maps to]{r}
	& \Cat \arrow[bend left,below]{rr}{(-\odot I)_*}
	& \ld &
	\arrow[bend left,above]{ll}{(\V(I,-))_*} \V\Cat
\end{tikzcd}\]

Each set $X$ is represented in $\V$ as the $X$-indexed coproduct of the unit object, and conversely, each object $a$ of $\V$ is represented in $\Set$ by the hom-set from the unit to $a$. This process induces the change of base whereby ordinary $\Set$-categories are converted to $\V$-categories, denoted $\C \mapsto \tilde{\C}$.

This is precisely what is needed: the ``arity'' category $\NN$ sits inside many enriching categories under various guises: as \textit{finite discrete graphs}, \textit{categories}, \textit{posets}, etc. For each $\V$ we can define the arity subcategory $\NN_\V$ to be the full subcategory of finite coproducts (copowers) of the unit object, and this remains essentially unchanged by the change-of-base above to the $\V$-category $\tilde{\NN}_\V$.

We only need to show that everything is simplified by restricting to this particular $\J$.

\section{Simplify with $\NN$-arities}

Most of the enriched algebraic theory literature deals with generalized arities; these will be important in time, but for present applications, we would like the benefits of enrichment with the simplicity of natural number arities. Here we provide some lemmas for this simplification.

Let $(\V,\times,I_\V)$ be a cartesian closed category with finite coproducts. Define $\NN_\V$ to be the full subcategory of finite coproducts of the unit object: $$n_\V = \coprod_{n \in \NN} I_\V$$ which is the \textit{copower} of $I_\V$ by a finite set $n \in \NN$, characterized by the universal property $$\V(n_\V,a) = \V(I_\V \odot n,a) \simeq \Set(n,\V(I_\V,a))$$ This is our ``system of arities'', the full monoidal subcategory $\J \hookrightarrow \V$.

We will call $\NN$-$\V$ theories \textbf{$\V$-theories} for simplicity. The point is that instead of thinking about fancy enriched powers, we just want to think about good old products:

\begin{lemma}
	Let $\V$ and $\NN_\V$ be as above. Then $n_\V$-powers in $\tilde{\V}$ are isomorphic to $n$-powers, i.e. $n$-fold products, in $\V$.
\end{lemma}
\begin{proof}
	\[\begin{array}{rcll}
	\V(a,[n_\V,b]) & \simeq & \V(a\times n_\V,b) & \text{hom-tensor adjunction}\\
	& = & \V(a\times (\coprod_n I_\V),b) & \text{definition of } n_\V\\
	& \simeq & \V(\coprod_n(a\times I_\V),b) & \text{distributivity}\\
	& \simeq & \V(\coprod_n a,b) & \text{unitality}\\
	& \simeq & V(a,\prod_n b) & \text{co/continuity of hom}\\
	\end{array}\]

Each of these isomorphisms is \textit{natural} in $a$; so by the Yoneda lemma, this implies $[n_\V,b] \simeq \prod_n b$.
\end{proof}

So, the \textit{full} sub-$\V$-category $\tilde{\NN}_\V$ has hom-objects which are essentially sets:
\[\begin{tikzcd}
\left[n_\V,m_\V\right] \simeq \prod_n (\coprod_m I_\V) \;\; (`` \; \simeq m^n \;")
\end{tikzcd}\]

In $\V\Cat$, the objects of the theory $\T$ are $n_\V$-powers of a generating object $s$. Alas, we cannot simply say that ``$s^{n_\V} \simeq \prod_n s$'', because the latter does not make sense in the $\V$-category $\T$; products are characterized by a $\Set$-enriched universal property. However, we only need:

\begin{lemma}
	Let $\T$ be a $\V$-category with $\NN_\V$-powers. Then homs into $s^{n_\V}$ are isomorphic to $n$ homs into $s$, because \[\begin{tikzcd} \T(a,s^{n_\V}) \simeq [n_\V,\T(a,s)] \simeq \prod_n \T(a,s) \end{tikzcd}\] by definition of power, and Lemma 1.
\end{lemma}

If the functor $F:\V \to \W$ induces a change of base $F_*:\V\Cat \to \W\Cat$ which preserves $\V$-theories - i.e. every $\V$-theory $\tau_\V$ corresponds to a $\W$-theory $\tau_\W$ - then $F$ is a \textit{change of semantics}. Since the powers $s^{n_\V}$ are the only objects of $\T$, it suffices to determine when the above universal property is preserved. Because the homs of base change are defined $$F_*(\T)(a,s^{n_\V}) = F(\T(a,s^{n_\V}))$$ we only need $F$ to preserve finite products:

\begin{lemma}
	Let $F: \V \to \W$ preserve finite products, and let $\NN_\V$, $\NN_\W$ be defined as above. If $f: \C \to \D$ is a $\V$-functor which preserves $\NN_\V$-powers, then $F_*(f):F_*(\C)\to F_*(\D)$ is a $\W$-functor which preserves $\NN_\W$-powers.
\end{lemma}
\begin{proof}
	\[\begin{array}{rcll}
	F_*(\D)(F_*(f)(a),F_*(f)(s^{n_\V})) & = & F(\D(f(a),f(s^{n_\V})) & \text{definition of base change}\\
	& \simeq & F(\D(f(a),f(s)^{n_\V}) & f \text{ preserves } \NN_\V \text{-powers}\\
	& \simeq & F(\prod_n \D(f(a),f(s))) & \text{Lemma 2 for } \V\\
	& \simeq & \prod_n F(\D(f(a),f(s))) & F \text{ preserves finite products}\\
	& = & \prod_n F_*(\D)(f(a),f(s)) & \text{definition of base change}\\
	& \simeq & F_*(\D)(f(a),f(s)^{n_\W}) & \text{Lemma 2 for } \W\\
	\end{array}\]
\end{proof}

Finally, we use $F_*(\tau)$ and the isomorphism $N: \NN_\V \simeq \NN_\W$ - denote by $\tilde{N}: \tilde{\NN}_\W^\op \to F_*(\tilde{\NN}_\V^\op)$ the isomorphism which sends $n_\W \mapsto n_\V$ and is the identity on morphisms - to construct a $\W$-functor which precisely fits the definition of an $\W$-theory:

\begin{theorem}
	Let $\V$, $\W$ be cartesian closed categories with finite coproducts, and let $F: \V \to \W$ preserve finite products. Then $F$ is a \textbf{change of semantics}; i.e. for every $\V$-theory $\tau_\V: \NN_\V^\op \to \T$, the $\W$-functor $$\tau_\W := F_*(\tau_\V) \circ \tilde{N}: \NN_\W^\op \to F_*(\T)$$ is a $\W$-theory. Moreover, $F$ preserves \textit{models}, i.e. for every $\NN_\V$-power preserving $\mu:\T \to \C$, the $\W$-functor $F_*(\mu)$ preserves $\NN_\W$-powers.
\end{theorem}
\begin{proof}
	The $\W$-functor $\tau_\W$ is bijective-on-objects because $\tau_\V$ and $\tilde{N}$ are; and it preserves $\NN_\W$-powers because $\tilde{N}$ does and $F_*(\tau_\V)$ does by the previous lemma. This preservation is \textit{strict} because $F_*(\T)$ has the same objects as $\T$, so the isomorphism implies that $\tau_\W(I_\W^{n_\W}) = \tau_\W(I_\W)^{n_\W}$. The preservation of models follows from the previous lemma.
\end{proof}

Hence, any functor between cartesian closed categories which preserves finite products constitutes a ``change of semantics'' - this is a simple, ubiquitous condition, which provides for a method of transitioning formal systems between various \textit{modus operandi}. Before exploring applications, we introduce two more useful kinds of transitions, and demonstrate how this can all be encapsulated in one elegant categorical idea.

\section{Putting It All Together}

In addition to change-of-base, there are two other natural and useful transitions for these theories. Let $\V\mathrm{Law}$ be the category of $\V$-theories, and let $f:\T\to \T'$ be a morphism of theories; this induces a ``change-of-theory'' functor between the respective categories of models $$f^*:\V\Mod(\T',\C)\to \V\Mod(\T,\C)$$ defined as precomposition by $f$. Similarly, given a finite-product functor $g: \C \to \C'$, this induces a ``change-of-model'' functor $$g_*:\V\Mod(\T,\C) \to \V\Mod(\T,\C')$$ defined as postcomposition by $g$.

All of this can be packed up nicely using the \textbf{Grothendieck construction}: given a (pseudo)functor $F: \D \to \Cat$, there is a \textit{fibration} $\bar{F}: \int F \to \D$ which encapsulates all of the categories in the image of $F$ - the category $\int F$ consists of
\[\begin{array}{rl}
\text{objects} & (d,x) : d\in \D, \; x\in F(d)\\
\text{morphisms} & (f:d\to d',a:F(f)(x)\to x')\\
\text{composition} & (f,a) \circ (f',a') = (f \circ f', a \circ F(f)(a'))\\
\end{array}\]

(Although we noted after Definition 4.1 that $\V\Law$ and $\Mod(\T,\C)$ are $\V$-categories when $\V$ is a cosmos, we will focus on the nonenriched case for simplicity and generality.)

This idea allows us to bring together \textit{all} of the different enrichments, theories, and models into \textit{one} big category. For every enriching category $\V$, let $\V\Cat_{fp}$ be the subcategory of $\V\Cat$ of $\V$-categories with finite powers and finite-power preserving functors; then there is a functor $$\V\Mod: \V\Law^\op \times \V\Cat_{fp} \to \Cat$$ which sends $(\T,\C) \mapsto \V\Mod(\T,\C)$. Functoriality characterizes the contravariant change-of-theory and the covariant change-of-model above.

Utilizing the construction, there is a category \textbf{$\int \V\Mod$} with objects and morphisms $$((f,g),\alpha): ((\T,\C),\mu) \to ((\T',\C'),\mu')$$ being $\V$-functors $f:\T\to \T'$, $g:\C\to \C'$, and $\V$-natural transformation $\alpha:\V\Mod(f,g)(\mu)\to \mu'$.

\begin{lemma}
	There is a functor $\mathrm{thy}: \CCC_{fp} \to \Cat$ which assigns $\V \mapsto \int \V\Mod$ and change-of-semantics $(F: \V \to \W) \mapsto (F_*^*: \int \V\Mod \to \int \W\Mod)$.
\end{lemma}
\begin{proof}
	Given $F:\V\to \W$, base change $F_*: \V\Cat \to \W\Cat$ is a 2-functor, thereby inducing the functor $F_*^*:\V\Mod\to \W\Mod$ which sends a morphism $((f,g),\alpha)$ to $((F_*(f),F_*(g)),F_*(\alpha))$. Checking functoriality is left to the reader.
\end{proof}

Thus, we can use the construction \textit{again} to encapsulate even the enrichment:
\begin{theorem}
	There is a category $\mathrm{Thy} := \int \mathrm{thy}$ with objects and morphisms $$(F,((f,g),\alpha)): (\V,((\T,\C),\mu)) \to (\W,((\T',\C'),\mu'))$$ being a change-of-semantics $F$ and a morphism $(f,g,\alpha): F_*^*(((\T,\C),\mu)) \to ((\T',\C'),\mu')$ in $\W\Mod$.
\end{theorem}

This category assimilates a whole lot of useful information. Most importantly, there are morphisms between objects of ``different kinds'', something which we consider often but is normally not possible in category theory. For example, let $\V$ be $\Set$, let $\mathbb{Z}$ be the ring of integers and let $\mathbb{R}$ be the topological group of real numbers. These are the objects $((\T_{\mathrm{Ring}},\Set),\mathbb{Z})$ and $((\T_\Grp,\Top),\mathbb{R})$.

\section{Applications}

In theoretical computer science literature, enriched algebraic theories have primarily been studied in the context of \textit{computational effects}. It is an original insight of Mike Stay and Greg Meredith \cite{ladl} that Lawvere theories can actually be utilized for the design of \textbf{programming languages}. This idea comes from caring about a relatively old and neglected subject - \textit{combinatory logic}.

\subsection{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 \cite{rosetta}.

Terms are constructed recursively by \textit{variables}, \textit{application}, and \textit{abstraction}, and the basic rewrite is \textit{beta reduction}: $$M,N := x \;\; | \;\; (M\; N) \;\; | \;\; \lambda x.M$$ $$(\lambda x.M\; N) \Rightarrow M[N/x]$$

Despite its simplicity, there are subtle complications regarding \textit{substitution}, or evaluation of functions. 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 \textit{rename} the bound to prevent ``variable capture'' (e.g. $(M y) \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\"onfinkel invented \textbf{combinatory logic} \cite{combs} - a basic form of logic without the red tape of variable binding, hence without functions in the usual sense. The $SKI$-calculus is the \textit{variable-free} representation of the $\lambda$-calculus; $\lambda$-terms are translated via \textit{abstraction elimination} into strings of combinators and applications. This is an important method for programming languages to minimize the subtleties of variables.

The key insight here is that Lawvere theories are \textit{by definition} free of variables, and it is precisely through abstraction elimination a programming language can be made an algebraic object. When representing a computational calculus as an $\NN$-$\Gph$ theory, the general rewrite rules are simply edges in the hom-graphs $t^n \to t$, with the object $t$ serving in place of the variable. Below is the theory of the $SKI$-combinator calculus:

\[\begin{array}{rcl}
& \ovalbox{Th(\textit{SKI})} &\\\\
\text{Sorts} & t &\\\\
\text{Term Constructors} & S & :1 \to t\\
& K & :1 \to t\\
& I & :1 \to t\\
& (-\; -) & : t^2 \to t\\\\
\text{Structural Congruence} & \text{n/a} &\\\\
\mathrm{Rewrites} & \sigma & :(((S\; x)\; y)\; z) \Rightarrow ((x\; z)\; (y\; z))\\
& \kappa & :((K\; y)\; z) \Rightarrow y\\
& \iota & :(I\; z) \Rightarrow z\\
\end{array}\]
These denote rewrites for arbitrary subterms $x, y, z$ without any variable binding involved, by using the \textit{cartesian structure} of the category. They are simply edges with vertices:
\[\begin{array}{rl}
(((S\; x)\; y)\; z)&: t^3 \xrightarrow{l^{-1} \times t^3} 1\times t^3 \xrightarrow{S \times t^3} t^4 \xrightarrow{(-\;-)\times t^2} t^3 \xrightarrow{(-\;-) \times t} t^2 \xrightarrow{(-\;-)} t\\
((x\; z)\; (y\; z))&: t^3 \xrightarrow{t^2 \times \Delta} t^4 \xrightarrow{t \times \tau \times t} t^4 \xrightarrow{(-\;-) \times (-\;-)} t^2 \xrightarrow{(-\;-)} t\\\\
((K\; y)\; z)&: t^2 \xrightarrow{l^{-1} \times t^2} 1\times t^2 \xrightarrow{K \times t^2} t^3 \xrightarrow{(-\;-)\times t} t^2 \xrightarrow{(-\;-)} t\\
y&: t^2 \xrightarrow{t \times !} t \times 1 \xrightarrow{r} t\\\\
(I\; z)&: t \xrightarrow{l^{-1}} 1\times t \xrightarrow{I \times t} t^2 \xrightarrow{(-\;-)} t\\
z&: t \xrightarrow{t} t
\end{array}\]

These implicitly universally quantified rules are applied by \textit{precomposing} with the terms to be ``plugged in'': using that a morphism $1 \to t^n$ is equivalent to $n$ morphisms $1 \to t$, terms are constructed from constants, then the abstract rewrite rules evaluate on concrete terms (morphisms $1\to t$ are the \textit{closed} terms, meaning they have no free variables; in general morphisms $t^n\to t$ are terms with $n$ free variables, and the same reasoning applies):
\[\begin{tikzcd}
	((KS)I): \arrow[Rightarrow,d,swap,"\kappa \circ (S\times I)"] & 1 \arrow[r,"S\times I"] & t^2 \arrow[r,"((K\; y)\; z)"] & t\\
	S: & 1 \arrow[r,"S\times I"] & t^2 \arrow[r,"y"] & t
\end{tikzcd}\]\\

A model of this theory is a power-preserving $\Gph$-functor $\mu: \Th(SKI) \to \Gph$. This gives a graph $\mu(t)$ of all terms and rewrites in the $SKI$-calculus, which is generated as follows:
\[\begin{tikzcd}
1 \simeq \mu(1) \arrow[r,"\mu(S)"] & \mu(t) & \mu(t^2) \arrow[l,swap,"\mu(\left(-\;-\right))"] \simeq \mu(t)^2
\end{tikzcd}\]
The images of the nullary operations $S,K,I$ are distinguished vertices of the graph $\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$, through the isomorphism $\mu(t)^2 \simeq \mu(t^2)$, a vertex $(u\; v)$ in $\mu(t)$ which is their application.

In this way all possible terms are generated (writing $\mu(S),\mu(K),\mu(I)$ as $S,K,I$ for sanity): $$((((S\; (K\; (I\; I)))\; S) \dots$$

The rewrites are transferred by the \textit{enrichment} of the functor: rather than functions between hom-sets, the morphism component of $\mu$ consists of graph homomorphisms between hom-graphs. So, $$\mu_{1,t}: \Th(SKI)(1,t)\to \Gph(1,\mu(t))$$ maps the ``syntactic'' graph of all closed terms and rewrites coherently into the ``semantic'' graph - meaning a rewrite in the theory $a\Rightarrow b$ is sent to a rewrite in the model $\mu(a) \Rightarrow \mu(b)$, like a functor without composition.

These rewrites in the image of $\mu$ are \textit{graph transformations}, like natural transformation without naturality, and this is how the model realizes the $\Gph$-theory as an actual graph of terms and rewrites: in the same way that a transformation between two constant functors $a\Rightarrow b: 1\to \C$ is just a morphism $a(1)\to b(1)$ in $\C$, a rewrite of closed terms $a\Rightarrow b: 1\to \mu(t)$ corresponds to an edge in $\mu(t)$:
\[\begin{tikzcd}
	\mu((I\; S)) \;\; \bullet \arrow[r,"\mu(\iota)"] & \bullet \;\; \mu(S)
\end{tikzcd}\]

Finally, the fact that $\mu((-\;-))$ is not just a function but a graph homomorphism means that pairs of edges (rewrites) $(a\to b, c\to d)$ are sent to rewrites $(a\; b) \to (c\; d)$. This gives the full complexity of the theory: given a large term (program), there are many different ways it can be computed - and some are better than others:
\[\begin{tikzcd}
	((K\; S)\; (((S\; K)\; I)\; (I\; K))) \arrow[r,"\sigma"] \arrow[dddd,swap,"\kappa"] & ((K\; S)\; ((K\;(I\; K))\; (I\; (I\; K)))) \arrow[d,"\iota"]\\
	& ((K\; S)\; ((K\; K)\; (I\; (I\; K)))) \arrow[d,"\iota"]\\
	& ((K\; S)\; ((K\; K)\; (I\; K))) \arrow[d,"\iota"]\\
	& ((K\; S)\; ((K\; K)\; K)) \arrow[d,"\kappa"]\\
	S & ((K\; S)\; K)\arrow[l,"\kappa"]\\
\end{tikzcd}\]\\

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 $\Th(SKI)$, but in particular we care about the canonical \textit{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 version of the adjunction in $\S2$:
\[\begin{tikzcd}
\Gph \arrow[bend left=10,below]{rr}{F}
& \ld &
\arrow[bend left=10,above]{ll}{U} \left[\Th(SKI),\Gph\right]_{fp}
\end{tikzcd}\]

As described in our source for $\J$-$\V$ theory \cite{rbb}, section 8, the \textbf{free model} on a generating object is given similarly to the $\Set$-enriched case: postcompose the theory $\V$-functor $\tau: \NN^\op \to \T$ with the covariant enriched Yoneda embedding $y_\V: \T \to [\T,\V]$, sending each $n \in \NN$ to its representable $\V$-functor, i.e. the $n$-ary operations of $\T$:
\[\begin{array}{rllll}
	\NN^\op & \xrightarrow{\tau} & \T & \xrightarrow{y_\V} & \left[\T,\V\right]\\
	n & \mapsto & t^n & \mapsto & \T(t^n,-)
\end{array}\]

So the canonical model of closed terms and rewrites is simply the $\V$-functor $\T(1,-):\T\to \V$. Hence for us, the syntax and semantics of the $SKI$ combinator calculus, and thus the $\lambda$ calculus, are unified in the model $$\mu_{SKI}^\Gph: \Th(SKI)(1,-): \Th(SKI) \to \Gph$$
Here we reap the benefits of the abstract construction - the graph $\mu_{SKI}^\Gph(t)$ is the \textit{transition system} which represents the \textbf{small-step operational semantics} of the $SKI$-calculus: $$(\mu(a) \to \mu(b) \in \mu_{SKI}^\Gph(t)) \iff (a \Rightarrow b \in \Th(SKI)(1,t))$$

\subsection{Change-of-base}
Now we can succinctly characterize the transformation from small-step to \textbf{big step}, which is found throughout the operational semantics literature. The \textit{free category} functor $\FC: \Gph \to \Cat$ gives for every graph $G$ the category $\FC(G)$ whose objects are the vertices of $G$, and whose morphisms are freely generated by the edges of $G$, i.e. sequences 
\[\begin{array}{rl}
\text{objects} & \text{vertices of } G\\
\text{morphisms} & \text{finite sequences of vertices and edges } (v_1,e_1,v_2,e_2,...,v_n)\\
\text{composition} & (v_1,e_1,v_2,e_2,...,v_n) \circ (v'_1,e'_1,v'_2,e'_2,...,v'_n) = (v_1,e_1,...,v_n=v'_1,e'_1,...,v'_n)\\
\end{array}\]

This functor preserves products, because the definition of graphical product and categorical product are identical except for composition: vertices/objects are pairs of vertices/objects from each component, and same for edges/morphisms; hence the above operation fulfills the preservation isomorphism: $$\FC(G\times H) \simeq \FC(G)\times \FC(H)$$ because they have the same objects, and a morphism of the former is a sequence of pairs, while that of the latter is the corresponding pair of sequences.

Thus $\FC$ is the change-of-semantics which induces the \textit{transitive closure} of the rewrite relation, hence $$\mu_{SKI}^\Cat := \FC_*(\mu_{SKI}^\Gph)$$ is the \textit{category} which represents the big-step operational semantics of the $SKI$-calculus.

The same reasoning applies to the \textit{free poset} functor $\FP: \Cat \to \Pos$; it is a change-of-semantics because the product of posets is defined in the same way. This induces the lesser-known \textbf{full-step semantics}, which collapses hom-sets to subsingletons, simply asserting the existence of a rewrite sequence between terms, without distinguishing between different paths.

Finally, we can pass to the purely abstract realm where all computation is already completed - the \textit{underlying set} functor $\US: \Pos \to \Set$ collapses every connected component of the full-step poset to a point, equating every formal expression to its final value. Assuming that the language is \textit{terminating}, meaning every term has a finite sequence of possible rewrites, and \textit{confluent}, meaning every pair of paths which branch from a term eventually rejoin, then this functor gives the \textbf{denotational semantics} of the language.

Thus from this simple sequence of functors, we can compute the spectrum of semantics for the $SKI$-calculus. For example,


\subsection{Change-of-theory: reduction contexts}
We can equip term calculi with \textit{reduction contexts}, which determine when rewrites are valid, thus giving the language a certain \textbf{evaluation strategy}. For example, the \textit{weak head normal form} is given by only allowing rewrites on the left-hand side of the term. We can do this for $\Th(SKI)$ by adding a reduction context \textit{marker}, an endomorphism $$R: t \to t$$ and a structural congruence rule which pushes the marker to the left-hand side of an application, $$R(x\; y) = (Rx\; y)$$ and modify the rewrite rules to be valid only when the marker is present: 
\[\begin{array}{rl}
\sigma & :(((RS\; x)\; y)\; z) \Rightarrow ((Rx\; z)\; (y\; z))\\
\kappa & :((RK\; y)\; z) \Rightarrow Ry\\
\iota & :(RI\; z) \Rightarrow Rz\\
\end{array}
\]

The $SKI$-calculus is thereby equipped with ``lazy evaluation'', an essential paradigm in modern programming. (include proofs from ROSwELT about weak head normal form?) This represents a broad potential application of equipping theories with computational methods, such as evaluation strategies. Moreover, these equipments can be modified as needed: using \textit{change-of-theory}, we can utilize a $\Gph$-functor $$f: \Th(SKI) \to \Th(SKI+R)$$ which sends $S,K,I$ to $RS,RK,RI$, and $\sigma, \kappa, \iota$ to the corresponding rewrites. This essentially interprets ordinary $SKI$ as having every subterm be a reduction context; we then need only to add a structural congruence rule to $\Th(SKI+R)$ to eliminate redundant markers in the right-hand side of applications: $$(x\; Ry) = (x\; y)$$ Then $f$ is a $\Gph$-functor which sends rewrites to rewrites correctly, thus inducing the change of theory $$f^*: \Mod(\Th(SKI+R),\C) \to \Mod(\Th(SKI),\C)$$ for all semantic categories $\C$, which forgets the reduction contexts.

\newpage

\bibliographystyle{amsplain}
\bibliography{lawvere}

\end{document}