section subsection subsubsection part partnumber partentrypagenumber title
descriptionlabel

# Initial Semantics for Reduction Rules

Benedikt Ahrens

###### Abstract

We give an algebraic characterization of the syntax and operational semantics
of a class of simply–typed languages, such as the language $\mathsf{PCF}$: we
characterize simply–typed syntax with variable binding and equipped with
reduction rules via a universal property, namely as the initial object of some
category of models. For this purpose, we employ techniques developed in two
previous works: [2] models syntactic translations between languages _over
different sets of types_ as initial morphisms in a category of models. [1]
characterizes untyped syntax _with reduction rules_ as initial object in a
category of models. In the present work, we show that those techniques are
modular enough to be combined: we thus characterize simply–typed syntax with
reduction rules as initial object in a category. The universal property yields
an operator which allows to specify translations — that are semantically
faithful by construction — between languages over possibly different sets of
types.

We specify a language by a _2–signature_ , that is, a signature on two levels:
the _syntactic_ level specifies the types and terms of the language, and
associates a type to each term. The _semantic_ level specifies, through
_inequations_ , reduction rules on the terms of the language. To any given
2–signature we associate a category of models. We prove that this category has
an initial object, which integrates the types and terms freely generated by
the 2–signature, and the reduction relation on those terms generated by its
inequations. We call this object the _(programming) language generated by the
2–signature_.

This paper is an extended version of an article published in the proceedings
of WoLLIC 2012.

##  1 Introduction

We give an algebraic characterization, via a universal property, of the
programming language generated by a _signature_. More precisely, we define a
notion of _2–signature_ which allows the specification of the _types and
terms_ of a programming language — via a 1–signature, say, $\Sigma$ — as well
as its _semantics_ in form of reduction rules, specified through a set $A$ of
inequations over $\Sigma$. To any 1–signature $\Sigma$ we associate a category
of _models of $\Sigma$_. Given a 2–signature $(\Sigma,A)$, the inequations of
$A$ give rise to a _satisfaction_ predicate on the models of $\Sigma$, and
thus specify a full subcategory of models of $\Sigma$ which satisfy the
inequations of $A$. We call this subcategory the _category of models of
$(\Sigma,A)$_. Our main theorem states that this category has an initial
object — the programming language associated to $(\Sigma,A)$ —, which
integrates the types and terms generated by $\Sigma$, equipped with the
reduction relation generated by the inequations of $A$.

As an example, we specify a translation from $\mathsf{PCF}$ to the untyped
lambda calculus $\operatorname{\mathsf{ULC}}$ using the category–theoretic
iteration operator. This translation is by construction faithful with respect
to reduction in $\mathsf{PCF}$ and $\operatorname{\mathsf{ULC}}$. This example
is verified formally in the proof assistant Coq [9]. The Coq files as well as
documentation are available online at

http://math.unice.fr/laboratoire/logiciels.

The present work is an extended version of another work by the author [3]. In
that previous work, the main theorem [3, Thm. 44] is stated, but no proof is
given. In the present work, we review the definitions given in the earlier
work and present a proof of the main theorem. Afterwards, we explain in detail
the formal verification in the proof assistant Coq [9] of an instance of this
theorem, for the simply–typed programming language $\mathsf{PCF}$. Finally, we
illustrate the iteration operator coming from initiality by specifying an
executable certified translation in Coq from $\mathsf{PCF}$ to the untyped
lambda calculus.

###  1.1 Summary

We define a notion of 2–signature in order to specify the types and terms and
reduction rules of functional programming languages. Given any 2–signature, we
characterize its associated programming language as initial object in some
category. This characterization of syntax with reduction rules is given in two
steps:

  1. 1.

At first _pure syntax_ is characterized as initial object in some category.
Here we use the term “pure” to express the fact that no semantic aspects such
as reductions on terms are considered. As will be explained in subsubsection
1.1.1, this characterization is actually a consequence of an earlier result
[2].

  2. 2.

Afterwards we consider _inequations_ specifying _reduction rules_. Given a set
of reduction rules for terms, we build up on the preceding result to give an
algebraic characterization of syntax _with reduction_. Inequations for
_untyped_ syntax are considered in earlier work [1]; in the present work, the
main result of that earlier work is carried over to _simply–typed_ syntax.

In summary, the merit of this work is to give an algebraic characterization of
simply–typed syntax _with reduction rules_ , building up on such a
characterization for _pure_ syntax given earlier [2]. Our approach is based on
relative monads as defined by [5] from the category $\mathsf{Set}$ of sets to
the category $\mathsf{Pre}$ of preorders. Compared to traditional monads,
relative monads allow for different categories as domain and codomain.

We now explain the above two points in more detail:

####  1.1.1 Pure Syntax

A 1–signature $(S,\Sigma)$ is a pair which specifies the types and terms of a
language, respectively. Furthermore, it associates a type to any term. To any
1–signature $(S,\Sigma)$ we associate a category
$\operatorname{Rep}^{\Delta}(S,\Sigma)$ of _representations_ , or “models”, of
$\Sigma$, where a model of $(S,\Sigma)$ is built from a model $T$ of the types
specified by $S$ and a relative monad on the functor
${\Delta}^{T}:{\mathsf{Set}}^{T}\to{\mathsf{Pre}}^{T}$.

This category has an initial object (cf. Sect. 3.2), which integrates the
types and terms freely generated by $(S,\Sigma)$. We call this object the
_(pure) syntax associated to $(S,\Sigma)$_. As mentioned above, we use the
term “pure” to distinguish this initial object from the initial object
associated to a _2–signature_ , which gives an analogous characterization of
syntax _with reduction rules_ (cf. below).

Initiality for pure syntax is actually a consequence of a related initiality
theorem proved in another work [2]: in that work, we associate, to any
signature $(S,\Sigma)$, a category $\operatorname{Rep}(S,\Sigma)$ of models of
$(S,\Sigma)$, where a model is built from a (traditional) monad over
${\mathsf{Set}}^{T}$ instead of a relative monad as above. We connect the
corresponding categories by exhibiting a pair of adjoint functors (cf. Sect.
3.2) between our category $\operatorname{Rep}^{\Delta}(S,\Sigma)$ of
representations of $(S,\Sigma)$ and that of [2],

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
40.95831pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\operatorname{Rep}(S,\Sigma)\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
42.72917pt\raise 17.5pt\hbox{\hbox{\kern
3.0pt\raise-1.92639pt\hbox{$\textstyle{\scriptstyle\Delta_{*}}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
90.67401pt\raise 3.96297pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
42.87454pt\raise-17.5pt\hbox{\hbox{\kern
3.0pt\raise-1.92639pt\hbox{$\textstyle{\scriptstyle
U_{*}}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
7.99963pt\raise-3.7038pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
43.9236pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise-2.43056pt\hbox{$\textstyle{\scriptstyle\bot}$}}}}}\ignorespaces{\hbox{\kern
90.66833pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\operatorname{Rep}^{\Delta}(S,\Sigma)}$}}}}}}}\ignorespaces\ignorespaces}}}}\enspace.$

We thus obtain an initial object in our category
$\operatorname{Rep}^{\Delta}(S,\Sigma)$ using the fact that left adjoints are
cocontinuous: the image under the functor
$\Delta_{*}:\operatorname{Rep}(S,\Sigma)\to\operatorname{Rep}^{\Delta}(S,\Sigma)$
of the initial object in the category $\operatorname{Rep}(S,\Sigma)$ is
initial in $\operatorname{Rep}^{\Delta}(S,\Sigma)$.

####  1.1.2 Syntax with Reduction Rules

Given a 1–signature $(S,\Sigma)$, an _$(S,\Sigma)$ –inequation_
$E=(\alpha,\gamma)$ associates a pair $(\alpha^{R},\gamma^{R})$ of _parallel_
morphisms in a suitable category to any representation $R$ of $(S,\Sigma)$. In
a sense made precise later, we can ask whether

$\alpha^{R}\enspace\leq\enspace\gamma^{R}\enspace,$

due to our use of relative monads towards families of _preordered_ sets. If
this is the case, we say that $R$ _satisfies_ the inequation $E$. A
_2–signature_ is a pair $((S,\Sigma),A)$ consisting of a 1–signature
$(S,\Sigma)$, which specifies the types and terms of a language, together with
a set $A$ of _$(S,\Sigma)$ –inequations_, which specifies reduction rules on
those terms. Given a 2–signature $((S,\Sigma),A)$, we call _representation of
$((S,\Sigma),A)$_ any representation of $(S,\Sigma)$ that satisfies each
inequation of $A$. The _category of representations of $((S,\Sigma),A)$_ is
defined to be the full subcategory of representations of $(S,\Sigma)$ whose
objects are representations of $((S,\Sigma),A)$.

We would like to exhibit an initial object in the category of representations
of $((S,\Sigma),A)$, and thus must rule out inequations which are never
satisfied. We call _classic_ $(S,\Sigma)$–inequation any
$(S,\Sigma)$–inequation whose codomain is of a particular form. Our main
result states that for any set $A$ of classic $(S,\Sigma)$–inequations the
category of representations of $((S,\Sigma),A)$ has an initial object. The
class of classic inequations is large enough to account for the fundamental
reduction rules; in particular, beta and eta reductions are given by classic
inequations.

Our definitions ensure that any reduction rule between terms that is expressed
by an inequation $E\in A$ is automatically propagated into subterms. The set
$A$ of inequations hence only needs to contain some “generating” inequations,
a fact that is well illustrated by the example 2–signature $\Lambda\beta$ of
the untyped lambda calculus with beta reduction [1]: This signature has only
one inequation $\beta$ which expresses beta reduction at the root of a term,

$\lambda x.M(N)\enspace\leadsto\enspace M[x:=N]\enspace.$

The initial representation of $\Lambda\beta$ is given by the untyped lambda
calculus, equipped with the reflexive and transitive beta reduction relation
$\twoheadrightarrow_{\beta}$ as presented by [6].

###  1.2 Related Work

Initial Semantics results for syntax with variable binding were first
presented on the LICS’99 conference. Those results are concerned only with the
_syntactic aspect_ of languages: they characterize the _set of terms_ of a
language as an initial object in some category, while not taking into account
reductions on terms. In lack of a better name, we refer to this kind of
initiality results as _purely syntactic_.

Some of these initiality theorems have been extended to also incorporate
semantic aspects, e.g., in form of equivalence relations between terms. These
extensions are reviewed in the second paragraph.

##### Purely syntactic results

Initial Semantics for “pure” syntax — i.e. without considering semantic
aspects — with variable binding were presented by several people
independently, differing in the modelling of variable binding:

The _nominal approach_ by [16] (see also [15, 27]) uses a set theory enriched
with _atoms_ to establish an initiality result. Their approach models lambda
abstraction as a constructor which takes a pair of a variable name and a term
as arguments. In contrast to the other techniques mentioned in this list, in
the nominal approach syntactic equality is different from
$\alpha$–equivalence. [22] proves an initiality result modelling variable
binding in a Higher–Order Abstract Syntax (HOAS) style. [13] (also [11, 12])
model variable binding through nested datatypes as introduced by [7]. [13]’s
approach [13] is extended to _simply–typed syntax_ by [26]. [30] generalize
and subsume those three approaches to a general category of contexts. An
overview of this work and references to more technical papers is given by
[29]. [18] prove an initiality result for untyped syntax based on the notion
of _module over a monad_. Their work has been extended to simply–typed syntax
by [31].

##### Incorporating Semantics

Rewriting in nominal settings has been examined by [10]. [17] present
rewriting for algebraic theories without variable binding; they characterize
equational theories (with a _symmetry_ rule) resp. rewrite systems (with
_reflexivity_ and _transitivity_ rule, but without _symmetry_) as
_coequalizers_ resp.  _coinserters_ in a category of monads on the categories
$\mathsf{Set}$ resp. $\mathsf{Pre}$. [14] have extended Fiore’s work to
integrate semantic aspects into initiality results. In particular, Hur’s
thesis [23] is dedicated to _equational_ systems for syntax with variable
binding. In a “Further research” section [23, Chap. 9.3], Hur suggests the use
of preorders, or more generally, arbitrary relations to model _in_ equational
systems. [18] prove initiality of the set of lambda terms modulo beta and eta
conversion in a category of _exponential monads_. In an unpublished paper,
[19] define a notion of _half–equation_ and _equation_ to express congruence
between terms. We adopt their definition in this paper, but interpret a pair
of half–equations as _in_ equation rather than equation. This emphasizes the
_dynamic_ viewpoint of reductions as _directed_ equalities rather than the
_static_ , mathematical viewpoint one obtains by considering symmetric
relations. In a “Future Work” section, [20, Sect. 8] mention the idea of using
preorders as an approach to model semantics, and they suggest interpreting the
untyped lambda calculus with beta and eta reduction rule as a monad over the
category $\mathsf{Pre}$ of preordered sets. The present work gives an
alternative viewpoint to their suggestion by considering the lambda calculus
with beta reduction — and a class of programming languages in general — as a
preorder–valued _relative_ monad on the functor
$\Delta:\mathsf{Set}\to\mathsf{Pre}$. The rationale underlying our use of
relative monads from sets to preorders is that we consider _contexts_ to be
given by unstructured sets, whereas _terms_ of a language carry structure in
form of a reduction relation. In this view it is reasonable to suppose
variables and terms to live in _different_ categories, which is possible
through the use of relative monads on the functor
$\Delta:\mathsf{Set}\to\mathsf{Pre}$ (cf. Def. 2.6) instead of traditional
monads (cf. also [1]). Relative monads were introduced by [5]. In that work,
the authors characterize the untyped lambda calculus as a relative monad over
the inclusion functor from finite sets to sets. Their point of view can be
combined with ours, leading to considering monads on the functor
${\Delta}\circ{i}:\mathsf{Fin}\to\mathsf{Pre}$, cf. Sect. 2.1. [21] , taking
the viewpoint of Categorical Semantics, defines a category Sig of 2–signatures
for _simply–typed_ syntax with reduction rules, and constructs an adjunction
between Sig and the category $\mathsf{2CCCat}$ of small cartesian closed
2–categories. He thus associates to any signature a 2–category of types, terms
and reductions satisfying a universal property. More precisely, terms are
given by morphisms in this category, and reductions are expressed by the
existence of 2–cells between terms. His approach differs from ours in the way
in which variable binding is modelled: Hirschowitz encodes binding in a
Higher–Order Abstract Syntax (HOAS) style through exponentials.

###  1.3 Synopsis

In the second section we review the definition of relative monads and modules
over such monads as well as their morphisms. Some constructions on monads and
modules are given, which will be of importance in what follows.

In the third section we define arities, half–equations and inequations, as
well as their representations. Afterwards we prove our main result.

In the fourth section we describe the formalization in the proof assistant Coq
of an instance of our main result, for the particular case of the language
$\mathsf{PCF}$.

##  2 Relative Monads and Modules

The functor underlying a monad is necessarily endo — this is enforced by the
type of monadic multiplication. _Relative monads_ were introduced by [5] to
overcome this restriction. One of their motivations was to consider the
untyped lambda calculus over _finite_ contexts as a monad–like structure —
similar to the monad structure on the lambda calculus over arbitrary contexts
exhibited by [4].

We review the definition of relative monads and define suitable _colax
morphisms of relative monads_. Afterwards we define _modules over relative
monads_ and port the constructions on modules over monads defined by [18] to
modules over _relative_ monads.

###  2.1 Definitions

We review the definition of relative monad as given by [5] and define suitable
morphisms for them. As an example we consider the lambda calculus with beta
reduction as a relative monad from sets to preorders, on the functor
$\Delta:\mathsf{Set}\to\mathsf{Pre}$ (cf. Def. 2.6). Afterwards we define
_modules over relative monads_ and carry over the constructions on modules
over regular monads of [18] to modules over relative monads.

The definition of relative monads is analogous to that of monads _in Kleisli
form_ , except that the underlying map of objects is between _different_
categories. Thus, for the operations to remain well–typed, one needs an
additional “mediating” functor, in the following usually called $F$, which is
inserted wherever necessary:

######  2.1 Definition (Relative Monad, [5]):

Given categories ${\mathcal{C}}$ and $\mathcal{D}$ and a functor
$F:{\mathcal{C}}\to\mathcal{D}$, a _relative monad
$P:{\mathcal{C}}\stackrel{{\scriptstyle F}}{{\to}}\mathcal{D}$ on $F$_ is
given by the following data:

  * •

a map $P\colon{\mathcal{C}}\to\mathcal{D}$ on the objects of ${\mathcal{C}}$,

  * •

for each object $c$ of ${\mathcal{C}}$, a morphism
$\eta_{c}\in\mathcal{D}(Fc,Pc)$ and

  * •

for each two objects $c,d$ of ${\mathcal{C}}$, a _substitution_ map (whose
subscripts we usually omit)

$\sigma_{c,d}\colon\mathcal{D}(Fc,Pd)\to\mathcal{D}(Pc,Pd)$

such that the following diagrams commute for all suitable morphisms $f$ and
$g$:

$\textstyle{Fc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{c}}$$\scriptstyle{f}$$\textstyle{Pc\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma\left({f}\right)}$$\textstyle{Pc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma\left({\eta_{c}}\right)}$$\scriptstyle{\operatorname{id}}$$\textstyle{Pc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma\left({f}\right)}$$\scriptstyle{\sigma\left({{\sigma\left({g}\right)}\circ{f}}\right)}$$\textstyle{Pd\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma\left({g}\right)}$$\textstyle{Pd\enspace,}$$\textstyle{Pc\enspace,}$$\textstyle{Pe\enspace.}$

######  2.2 Remark __:

Relative monads on the identity functor
$\operatorname{Id}:{\mathcal{C}}\to{\mathcal{C}}$ precisely correspond to
monads.

Various examples of relative monads are given by [5]. They give one example
related to syntax and substitution:

######  2.3 Example (Lambda Calculus over Finite Contexts):

[5] consider the untyped lambda calculus as a relative monad on the functor
$J:\mathsf{Fin}_{\mathrm{skel}}\to\mathsf{Set}$. Here the category
$\mathsf{Fin}_{\mathrm{skel}}$ is the category of finite cardinals, i.e. the
skeleton of the category $\mathsf{Fin}$ of _finite_ sets and maps between
finite sets. The category $\mathsf{Set}$ is the category of sets, cf. Def.
2.4.

We will give another example (cf. Sect. 2.1) of how to view syntax _with
reduction rules_ as a relative monad. For this, we first fix some definitions.

######  2.4 Definition:

The category $\mathsf{Set}$ is the category of sets and total maps between
them, together with the usual composition of maps.

######  2.5 Definition:

The category $\mathsf{Pre}$ of preorders has, as objects, sets equipped with a
preorder, and, as morphisms between any two preordered sets $A$ and $B$, the
monotone functions from $A$ to $B$. We consider $\mathsf{Pre}$ as a category
enriched over itself as follows: given $f,g\in\mathsf{Pre}(A,B)$, we say that
$f\leq g$ iff for any $a\in A$, $f(a)\leq g(a)$ in $B$.

######  2.6 Definition (Functor $\Delta:\mathsf{Set}\to\mathsf{Pre}$ and
Forgetful Functor):

We call $\Delta:\mathsf{Set}\to\mathsf{Pre}$ the left adjoint of the forgetful
functor $U:\mathsf{Pre}\to\mathsf{Set}$,

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
13.47226pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\mathsf{Set}\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
28.34724pt\raise 17.5pt\hbox{\hbox{\kern
3.0pt\raise-2.39166pt\hbox{$\textstyle{\scriptstyle\Delta}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
62.11176pt\raise 4.2431pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
28.49261pt\raise-17.5pt\hbox{\hbox{\kern
3.0pt\raise-2.39166pt\hbox{$\textstyle{\scriptstyle
U}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
4.40012pt\raise-3.00433pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
28.54167pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise-2.43056pt\hbox{$\textstyle{\scriptstyle\bot}$}}}}}\ignorespaces{\hbox{\kern
62.11115pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\mathsf{Pre}}$}}}}}}}\ignorespaces\ignorespaces}}}}\enspace.$

The functor $\Delta$ associates, to each set $X$, the set itself together with
the smallest preorder, i.e. the diagonal of $X$,

$\Delta(X):=(X,\delta_{X})\enspace.$

In other words, for any $x,y\in X$ we have $x\delta_{X}y$ if and only if
$x=y$. The functor $\Delta:\mathsf{Set}\to\mathsf{Pre}$ is a _full embedding_
, i.e. it is fully faithful and injective on objects. We have
${U}\circ{\Delta}=\operatorname{Id}_{\mathsf{Set}}$. Altogether, the embedding
$\Delta:\mathsf{Set}\to\mathsf{Pre}$ is a coreflection. We denote by $\varphi$
the family of isomorphisms

$\varphi_{X,Y}:\mathsf{Pre}(\Delta X,Y)\cong\mathsf{Set}(X,UY)\enspace.$

We omit the indices of $\varphi$ whenever they can be deduced from the
context.

######  2.7 Definition (Category of Families):

Let ${\mathcal{C}}$ be a category and $T$ be a set, i.e. a discrete category.
We denote by ${{\mathcal{C}}}^{T}$ the functor category, an object of which is
a $T$–indexed family of objects of ${\mathcal{C}}$. Given two families $V$ and
$W$, a morphism $f:V\to W$ is a family of morphisms in ${\mathcal{C}}$,

$f:t\mapsto f(t):V(t)\to W(t)\enspace.$

We write $V_{t}:=V(t)$ for objects and morphisms. Given another category
$\mathcal{D}$ and a functor $F:{\mathcal{C}}\to\mathcal{D}$, we denote by
${F}^{T}$ the functor defined on objects and morphisms as

${F}^{T}:{{\mathcal{C}}}^{T}\to{\mathcal{D}}^{T},\quad
f\mapsto\bigl{(}t\mapsto F(f_{t})\bigr{)}\enspace.$

######  2.8 Remark __:

Given a set $T$, the adjunction of Def. 2.6 induces an adjunction

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.56586pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathsf{Set}}^{T}\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
28.92584pt\raise 17.5pt\hbox{\hbox{\kern
3.0pt\raise-3.075pt\hbox{$\textstyle{\scriptstyle{\Delta}^{T}}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
65.20688pt\raise 4.56238pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
29.0712pt\raise-17.5pt\hbox{\hbox{\kern
3.0pt\raise-3.075pt\hbox{$\textstyle{\scriptstyle{U}^{T}}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
4.66019pt\raise-3.00433pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
30.5668pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise-2.43056pt\hbox{$\textstyle{\scriptstyle\bot}$}}}}}\ignorespaces{\hbox{\kern
65.20474pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathsf{Pre}}^{T}}$}}}}}}}\ignorespaces\ignorespaces}}}}\enspace.$

######  2.9 Example (Simply–Typed Lambda Calculus as Relative Monad on
$\Delta^{T}$):

Let

$T:=T_{\operatorname{\mathsf{TLC}}}::=\leavevmode\nobreak\
*\leavevmode\nobreak\ \mid\leavevmode\nobreak\
T_{\operatorname{\mathsf{TLC}}}\leadsto T_{\operatorname{\mathsf{TLC}}}$

be the set of types of the simply–typed lambda calculus. Consider the set
family of simply–typed lambda terms over $T_{\operatorname{\mathsf{TLC}}}$,
indexed by typed contexts:

⬇

Inductive TLC (V : T -> Type) : T -> Type :=

| Var : forall t, V t -> TLC V t

| Abs : forall s t TLC (V + s) t -> TLC V (s $\sim$> t)

| App : forall s t, TLC V (s $\sim$> t) -> TLC V s -> TLC V t.

Here the context V + s is the context V extended by a fresh variable of type s
— the variable that is bound by the constructor Abs (cf. also Sect. 2.3). We
leave the object type arguments implicit and write $\lambda M$ and $M(N)$ for
$\operatorname{Abs}M$ and $\operatorname{App}MN$, respectively. We equip each
set $\operatorname{\mathsf{TLC}}(V)(t)$ of lambda terms over context $V$ of
object type $t$ with a preorder taken as the reflexive–transitive closure of
the relation generated by the rule

$\quad\lambda M(N)\leavevmode\nobreak\ \leq\leavevmode\nobreak\ M[*:=N]$

and its propagation into subterms. This defines a monad
$\operatorname{\mathsf{TLC}}_{\beta}$ from families of sets to families of
preorders over the functor $\Delta^{T}$,

$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}:{\mathsf{Set}}^{T}\stackrel{{\scriptstyle\Delta^{T}}}{{\longrightarrow}}{\mathsf{Pre}}^{T}.$

The family $\eta^{\operatorname{\mathsf{TLC}}}$ is given by the constructor
$\operatorname{Var}$, and the substitution map

$\sigma_{X,Y}:{\mathsf{Pre}}^{T}\bigl{(}\Delta^{T}(X),\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(Y)\bigr{)}\to{\mathsf{Pre}}^{T}\bigl{(}\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(X),\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(Y)\bigr{)}$
((1))

is given by capture–avoiding simultaneous substitution. Via the adjunction of
Sect. 2.1 the substitution can also be read as

$\sigma_{X,Y}:{\mathsf{Set}}^{T}\bigl{(}X,\operatorname{\mathsf{TLC}}(Y)\bigr{)}\to{\mathsf{Pre}}^{T}\bigl{(}\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(X),\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(Y)\bigr{)}\enspace.$

In the previous example, the substitution of the lambda calculus satisfies an
additional monotonicity property: the map $\sigma_{X,Y}$ in Disp. (1) is
monotone for the preorders on hom–sets defined in Def. 2.5 and its propagation
in products. This motivates the following definition:

######  2.10 Definition:

Given a monad $P$ on $\Delta^{T}$ for some set $T$. We say that $P$ is _a
reduction monad_ if for any $X$ and $Y$ the substition $\sigma_{X,Y}$ is
_monotone_ for the preorders on ${\mathsf{Pre}}^{T}(\Delta^{T}X,PY)$ and
${\mathsf{Pre}}^{T}(PX,PY)$.

The monad $\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$ is thus a reduction
monad. It will be clear from Def. 2.40 why we are interested in reduction
monads.

######  2.11 Remark _Relative Monads are functorial_ :

Given a monad $P$ over $F:{\mathcal{C}}\to\mathcal{D}$, a functorial action
(rlift) for $P$ is defined by setting, for any morphism $f:c\to d$ in
${\mathcal{C}}$,

$P(f):=\operatorname{lift}_{P}(f):=\sigma\left({{\eta}\circ{Ff}}\right)\enspace.$

The functor axioms are easily proved from the monadic axioms.

The substitution $\sigma=(\sigma_{c,d})_{c,d\in|{\mathcal{C}}|}$ of a relative
monad $P$ is binatural:

######  2.12 Remark _Naturality of Substitution_ :

Given a relative monad $P$ over $F:{\mathcal{C}}\to\mathcal{D}$, then its
substitution $\sigma$ is natural in $c$ and $d$. We write
$f^{*}(h):={h}\circ{f}$. For naturality in $c$ we check that the diagram

$\textstyle{c\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{\mathcal{D}(Fc,Pd)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{c,d}}$$\textstyle{\mathcal{D}(Pc,Pd)}$$\textstyle{c^{\prime}}$$\textstyle{\mathcal{D}(Fc^{\prime},Pd)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{c^{\prime},d}}$$\scriptstyle{(Ff)^{*}}$$\textstyle{\mathcal{D}(Pc^{\prime},Pd)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Pf)^{*}}$

commutes. Given $g\in\mathcal{D}(Fc^{\prime},Pd)$, we have

$\displaystyle{\sigma(g)}\circ{Pf}$
$\displaystyle={\sigma(g)}\circ{\sigma({\eta_{c^{\prime}}}\circ{Ff})}$
$\displaystyle\stackrel{{\scriptstyle
3}}{{=}}\sigma({\sigma(g)}\circ{{\eta_{c^{\prime}}}\circ{Ff}})$
$\displaystyle\stackrel{{\scriptstyle 1}}{{=}}\sigma({g}\circ{Ff})\enspace,$

where the numbers correspond to the diagrams of Def. 2.1 used to rewrite in
the respective step. Similarly we check naturality in $d$. Writing
$h_{*}(g):={h}\circ{g}$, the diagram

$\textstyle{d\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h}$$\textstyle{\mathcal{D}(Fc,Pd)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{c,d}}$$\scriptstyle{(Ph)_{*}}$$\textstyle{\mathcal{D}(Pc,Pd)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(Ph)_{*}}$$\textstyle{d^{\prime}}$$\textstyle{\mathcal{D}(Fc^{\prime},Pd)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{c^{\prime},d}}$$\textstyle{\mathcal{D}(Pc^{\prime},Pd)}$

commutes: given $g\in\mathcal{D}(Fc,Pd)$, we have

$\displaystyle{Ph}\circ{\sigma(g)}$
$\displaystyle={\sigma({\eta_{d^{\prime}}}\circ{Fh})}\circ{\sigma(g)}$
$\displaystyle\stackrel{{\scriptstyle
3}}{{=}}\sigma({\sigma({\eta_{d^{\prime}}}\circ{Fh})}\circ{g})$
$\displaystyle=\sigma({Ph}\circ{g})\enspace.$

If $(T_{i})_{i\in I}$ is a family of sets and $f:I\to J$ a map of sets, then
we obtain a family of sets $(T^{\prime}_{j})_{j\in J}$ by setting
$T^{\prime}_{j}:=\coprod_{\\{i|f(i)=j\\}}T_{i}$. The following construction
generalizes this reparametrization:

######  2.13 Definition (Retyping Functor):

Let $T$ and $T^{\prime}$ be sets and $g:T\to T^{\prime}$ be a map. Let
${\mathcal{C}}$ be a cocomplete category. The map $g$ induces a functor

$g^{*}:{{\mathcal{C}}}^{T^{\prime}}\to{{\mathcal{C}}}^{T}\enspace,\quad
W\mapsto{W}\circ{g}\enspace.$

The _retyping functor associated to $g:T\to T^{\prime}$_,

$\vec{g}:{{\mathcal{C}}}^{T}\to{{\mathcal{C}}}^{T^{\prime}}\enspace,$

is defined as the left Kan extension operation along $g$, that is, we have an
adjunction

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
9.89917pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{{\mathcal{C}}}^{T}\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
26.58716pt\raise 17.5pt\hbox{\hbox{\kern
3.0pt\raise-3.57222pt\hbox{$\textstyle{\scriptstyle\vec{g}}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
58.12418pt\raise 5.10718pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{{}{{}{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}{}{{{}{}{}{{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}}}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}{}{}{{}{}}\ignorespaces\ignorespaces{\hbox{\kern
27.06131pt\raise-17.5pt\hbox{\hbox{\kern
3.0pt\raise-1.29167pt\hbox{$\textstyle{\scriptstyle
g^{*}}$}}}}}\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern
4.21939pt\raise-3.00433pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
27.13402pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise-2.43056pt\hbox{$\textstyle{\scriptstyle\bot}$}}}}}\ignorespaces{\hbox{\kern
58.11697pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{{{\mathcal{C}}}^{T^{\prime}}}$}}}}}}}\ignorespaces\ignorespaces}}}}\enspace.$
((2))

Put differently, the map $g:T\to T^{\prime}$ induces an endofunctor $\bar{g}$
on ${{\mathcal{C}}}^{T}$ with object map

$\bar{g}(V):={\vec{g}(V)}\circ{g}$

and we have a natural transformation ctype — the unit of the adjunction of
Disp. (2),

${\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{ctype}}}}}}:\operatorname{Id}\Rightarrow\bar{g}:{{\mathcal{C}}}^{T}\to{{\mathcal{C}}}^{T}\enspace.$

######  2.14 Definition (Pointed index sets):

Given a category ${\mathcal{C}}$, a set $T$ and a natural number $n$, we
denote by ${{\mathcal{C}}}^{T}_{n}$ the category with, as objects, diagrams of
the form

$n\stackrel{{\scriptstyle\mathbf{t}}}{{\to}}T\stackrel{{\scriptstyle
V}}{{\to}}{\mathcal{C}}\enspace,$

written $(V,t_{1},\ldots,t_{n})$ with $t_{i}:=\mathbf{t}(i)$. A morphism $h$
to another such $(W,\mathbf{t})$ with the same pointing map $\mathbf{t}$ is
given by a morphism $h:V\to W$ in ${{\mathcal{C}}}^{T}$. Any functor
$F:{{\mathcal{C}}}^{T}\to{\mathcal{D}}^{T}$ extends to
$F_{n}:{{\mathcal{C}}}^{T}_{n}\to{\mathcal{D}}^{T}_{n}$ via

$F_{n}(V,t_{1},\ldots,t_{n}):=(FV,t_{1},\ldots,t_{n})\enspace.$

######  2.15 Remark __:

The category ${{\mathcal{C}}}^{T}_{n}$ consists of $T^{n}$ copies of
${{\mathcal{C}}}^{T}$, which do not interact. Due to the “markers”
$(t_{1},\ldots,t_{n})$ we can act differently on each copy, cf., e.g., Def.
2.35 and 2.36.

Retyping functors generalize to categories with pointed indexing sets; when
changing types according to a map of types $g:T\to T^{\prime}$, the markers
must be adapted as well:

######  2.16 Definition:

Given a map of sets $g:T\to T^{\prime}$, by postcomposing the pointing map
with $g$, the retyping functor generalizes to the functor

$\vec{g}(n):{{\mathcal{C}}}^{T}_{n}\to{{\mathcal{C}}}^{T^{\prime}}_{n}\enspace,\quad(V,\mathbf{t})\mapsto\bigl{(}\vec{g}V,g_{*}(\mathbf{t})\bigr{)}\enspace,$

where $g_{*}(\mathbf{t}):={g}\circ{\mathbf{t}}:n\to T^{\prime}$.

We are interested in monads on the category ${\mathsf{Set}}^{T}$ of families
of sets indexed by $T$ and relative monads on
$\Delta^{T}:{\mathsf{Set}}^{T}\to{\mathsf{Pre}}^{T}$ as well as their
relationship:

######  2.17 Lemma (Relative Monads on $\Delta^{T}$ and Monads on
${\mathsf{Set}}^{T}$):

Let $P$ be a relative monad on
$\Delta^{:}{\mathsf{Set}}^{T}\to{\mathsf{Pre}}^{T}$. By postcomposing with the
forgetful functor ${U}^{T}:{\mathsf{Pre}}^{T}\to{\mathsf{Set}}^{T}$ we obtain
a monad

$UP:{\mathsf{Set}}^{T}\to{\mathsf{Set}}^{T}\enspace.$

The substitution is defined, for $m:X\to UPY$ by setting

$U\sigma:m\mapsto U\left(\sigma\left({\varphi^{-1}m}\right)\right)\enspace,$

making use of the adjunction $\varphi$ of Sect. 2.1. Conversely, to any monad
$P$ over ${\mathsf{Set}}^{T}$, we associate a relative monad $\Delta P$ over
$\Delta^{T}$ by postcomposing with $\Delta^{T}$.

We generalize the definition of colax monad morphisms [25] to relative monads:

######  2.18 Definition (Colax Morphism of Relative Monads):

Suppose given two relative monads $P:{\mathcal{C}}\stackrel{{\scriptstyle
F}}{{\to}}\mathcal{D}$ and $Q:{\mathcal{C}}^{\prime}\stackrel{{\scriptstyle
F^{\prime}}}{{\to}}\mathcal{D}^{\prime}$. A _colax morphism of relative
monads_ from $P$ to $Q$ is a quadruple $h=(G,G^{\prime},N,\tau)$ of a functor
$G\colon{\mathcal{C}}\to{\mathcal{C}}^{\prime}$, a functor
$G^{\prime}:\mathcal{D}\to\mathcal{D}^{\prime}$ as well as a natural
transformation $N:F^{\prime}G\to G^{\prime}F$ and a natural transformation
$\tau:PG^{\prime}\to GQ$ such that the following diagrams commute for any
objects $c,d$ and any suitable morphism $f$:

$\textstyle{G^{\prime}Pc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G^{\prime}\sigma^{P}\left({f}\right)}$$\scriptstyle{\tau_{c}}$$\textstyle{G^{\prime}Pd\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau_{d}}$$\textstyle{QGc\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma^{Q}\left({{{\tau_{d}}\circ{G^{\prime}f}}\circ{Nc}}\right)}$$\textstyle{QGd}$
$\textstyle{F^{\prime}Gc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Nc}$$\scriptstyle{\eta^{Q}_{Gc}}$$\textstyle{G^{\prime}Fc\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{G^{\prime}\eta^{P}_{c}}$$\textstyle{G^{\prime}Pc\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\tau_{c}}$$\textstyle{QGc.}$

Naturality of $\tau$ in the preceding definition is actually a consequence of
the commutative diagrams of Def. 2.18, cf. Lemma colax_RMonad_Hom_NatTrans in
the Coq library.

######  2.19 Remark __:

In Sect. 3 we are going to use the following instance of the preceding
definition: the categories ${\mathcal{C}}$ and ${\mathcal{C}}^{\prime}$ are
instantiated by ${\mathsf{Set}}^{T}$ and ${\mathsf{Set}}^{T^{\prime}}$,
respectively, for sets $T$ and $T^{\prime}$. The functor $G$ is the retyping
functor (cf. Def. 2.13) associated to some translation of types $g:T\to
T^{\prime}$. Similarly, the categories $\mathcal{D}$ and
$\mathcal{D}^{\prime}$ are instantiated by ${\mathsf{Pre}}^{T}$ and
${\mathsf{Pre}}^{T^{\prime}}$, and the functor $F$ by

$F:=\Delta^{T}:{\mathsf{Set}}^{T}\to{\mathsf{Pre}}^{T}\enspace,$

and similar for $F^{\prime}$:

$\textstyle{{\mathsf{Set}}^{T}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Delta^{T}}$$\scriptstyle{\vec{g}}$$\textstyle{{\mathsf{Pre}}^{T}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\vec{g}}$$\textstyle{{\mathsf{Set}}^{T^{\prime}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Delta^{T^{\prime}}}$$\textstyle{{\mathsf{Pre}}^{T^{\prime}}.\ignorespaces\ignorespaces}$$\textstyle{\scriptstyle\operatorname{Id}}$

Given a monad $P$ on $F:{\mathcal{C}}\to\mathcal{D}$, the notion of _module
over $P$_ generalizes the notion of monadic substitution:

######  2.20 Definition (Module over a Relative Monad):

Let $P\colon{\mathcal{C}}\stackrel{{\scriptstyle F}}{{\to}}\mathcal{D}$ be a
relative monad and let $\mathcal{E}$ be a category. A _module $M$ over $P$
with codomain $\mathcal{E}$_ is given by

  * •

a map $M:{\mathcal{C}}\to\mathcal{E}$ on the objects of the categories
involved and

  * •

for all objects $c,d$ of ${\mathcal{C}}$, a map

$\varsigma_{c,d}:\mathcal{D}(Fc,Pd)\to\mathcal{E}(Mc,Md)$

such that the following diagrams commute for all suitable morphisms $f$ and
$g$:

$\textstyle{Mc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varsigma({f})}$$\scriptstyle{\varsigma({{\sigma\left({g}\right)}\circ{f}})}$$\textstyle{Md\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varsigma({g})}$$\textstyle{Mc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varsigma({\eta_{c}})}$$\scriptstyle{\operatorname{id}}$$\textstyle{Me}$$\textstyle{Mc.}$

A functoriality (rmlift) for such a module $M$ is then defined similarly to
that for relative monads: for any morphism $f:c\to d$ in ${\mathcal{C}}$ we
set

$M(f):=\operatorname{rmlift}_{M}(f):=\varsigma({{\eta}\circ{Ff}})\enspace.$

The following examples of modules are instances of constructions explained in
the next section:

######  2.21 Example (Sect. 2.1 cont.):

The map
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}:V\mapsto\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(V)$
yields a module over the relative monad
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$, the _tautological
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$–module_
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$.

######  2.22 Example:

Given $V\in{\mathsf{Set}}^{T}$ and $s\in T$, we denote by $V+s$ the context
$V$ enriched by an additional variable of type $s$. The map
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}^{s}:V\mapsto\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(V^{s})$
inherits the structure of a
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$–module from the tautological
module $\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$ (cf. Sect. 2.1). We call
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}^{s}$ the _derived module with
respect to $s\in T$_ of the module
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$; cf. also Sect. 2.2.

######  2.23 Example:

Given $t\in T$, the map
$V\mapsto\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(V)(t):{\mathsf{Set}}^{T}\to\mathsf{Pre}$
inherits a structure of a
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$–module, the _fibre module
$[{\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}}]_{t}$ with respect to $t\in
T$_.

######  2.24 Example:

Given $s,t\in T$, the map
$V\mapsto\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(V)(s\leadsto
t)\times\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}(V)(s)$ inherits a
structure of an $\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$–module.

A _module morphism_ is a family of morphisms that is compatible with module
substitution in the source and target modules:

######  2.25 Definition (Morphism of Relative Modules):

Let $M$ and $N$ be two relative modules over
$P\colon{\mathcal{C}}\stackrel{{\scriptstyle F}}{{\to}}\mathcal{D}$ with
codomain $\mathcal{E}$. A _morphism of relative $P$–modules_ from $M$ to $N$
is given by a collection of morphisms $\rho_{c}\in\mathcal{E}(Mc,Nc)$ such
that for all morphisms $f\in\mathcal{D}(Fc,Pd)$ the following diagram
commutes:

$\textstyle{Mc\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varsigma^{M}({f})}$$\scriptstyle{\rho_{c}}$$\textstyle{Md\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\rho_{d}}$$\textstyle{Nc\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varsigma^{N}({f})}$$\textstyle{Nd.}$

The modules over $P$ with codomain $\mathcal{E}$ and morphisms between them
form a category called $\operatorname{\mathsf{RMod}}({P},{\mathcal{E}})$ (in
the digital library: RMOD P E). Composition and identity morphisms of modules
are defined by pointwise composition and identity, similarly to the category
of monads.

######  2.26 Example (Sect. 2.1, 2.1, Sect. 2.1 cont.):

Abstraction and application are morphisms of
$\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}$–modules:

$\displaystyle\operatorname{Abs}_{s,t}$
$\displaystyle:[{\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}^{s}}]_{t}\to[{\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}}]_{s\leadsto
t}\enspace,$ $\displaystyle\operatorname{App}_{s,t}$
$\displaystyle:[{\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}}]_{s\leadsto
t}\times[{\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}}]_{s}\to[{\operatorname{\mathsf{TLC}}_{\mathsf{\beta}}}]_{t}\enspace.$

###  2.2 Constructions on Relative Monads and Modules

The following constructions are analogous to those used by [18].

Any relative monad $P$ comes with the _tautological_ module over $P$ itself:

######  2.27 Definition (Tautological Module):

Every relative monad $P$ on $F:{\mathcal{C}}\to\mathcal{D}$ yields a module
$(P,\sigma^{P})$ — also denoted by $P$ — over itself, i.e. an object in the
category $\operatorname{\mathsf{RMod}}({P},{\mathcal{D}})$.

######  2.28 Definition (Constant and Terminal Module):

Let $P$ be a relative monad on $F:{\mathcal{C}}\to\mathcal{D}$. For any object
$e\in\mathcal{E}$ the constant map $T_{e}\colon{\mathcal{C}}\to\mathcal{E}$,
$c\mapsto e$ for all $c\in{\mathcal{C}}$, is equipped with the structure of a
$P$–module by setting $\varsigma_{c,d}(f)=\operatorname{id}_{e}$. In
particular, if $\mathcal{E}$ has a terminal object $1_{\mathcal{E}}$, then the
constant module $T_{1_{\mathcal{E}}}:c\mapsto 1_{\mathcal{E}}$ is terminal in
$\operatorname{\mathsf{RMod}}({P},{\mathcal{E}})$.

######  2.29 Definition (Postcomposition with a functor):

Let $P$ be a relative monad on $F:{\mathcal{C}}\to\mathcal{D}$, and let $M$ be
a $P$–module with codomain $\mathcal{E}$. Let $G:\mathcal{E}\to\mathcal{X}$ be
a functor. Then the object map ${G}\circ{M}:{\mathcal{C}}\to\mathcal{X}$
defined by $c\mapsto G(M(c))$ is equipped with a $P$–module structure by
setting, for $c,d\in{\mathcal{C}}$ and $f\in\mathcal{D}(Fc,Pd)$,

$\varsigma^{{G}\circ{M}}(f):=G(\varsigma^{M}(f))\enspace.$

For $M:=P$ (considered as tautological module over itself) and $G$ a constant
functor mapping to an object $x\in\mathcal{X}$ and its identity morphism
$\operatorname{id}_{x}$, we obtain the constant module
$(T_{x},\operatorname{id})$ as in the preceding definition.

Given a module $N$ over a relative monad $Q$ and a monad morphism $\tau:P\to
Q$ into $Q$, we can rebase or “pull back” the module $N$ along $\tau$:

######  2.30 Definition (Pullback Module):

Suppose given two relative monads $P$ and $Q$ and a morphism $\tau:P\to Q$ as
in Def. 2.18. Let $N$ a $Q$-module with codomain $\mathcal{E}$. We define a
$P$-module $h^{*}M$ to $\mathcal{E}$ with object map

$c\mapsto M(Gc)$

by defining the substitution map, for $f:Fc\to Pd$, as

$\varsigma^{h^{*}M}({f}):=\varsigma^{M}({{{h_{d}}\circ{G^{\prime}f}}\circ{N_{c}}})\enspace.$

The module thus defined is called the _pullback module of $N$ along $h$_. The
pullback extends to module morphisms and is functorial.

######  2.31 Definition (Induced Module Morphism):

With the same notation as before, the monad morphism $h$ induces a morphism of
$P$–modules $h:G^{\prime}P\to h^{*}Q$. Note that the domain module is the
module obtained by postcomposing (the tautological module of) $P$ with
$G^{\prime}$, whereas for (traditional) monads the domain module was just the
tautological module of the domain monad [18].

One big difference between monads — both traditional and relative ones — and
modules over them is that for the latter we know how to take _products_ :

######  2.32 Definition (Product):

Suppose the category $\mathcal{E}$ has products. Let $M$ and $N$ be
$P$–modules with codomain $\mathcal{E}$. Then the map

$M\times N:{\mathcal{C}}\to\mathcal{E},\quad c\mapsto Mc\times Nc$

is canonically equipped with a substitution and thus constitutes a module
called the _product of $M$ and $N$_. This construction extends to a product on
$\operatorname{\mathsf{RMod}}({P},{\mathcal{E}})$.

###  2.3 Derivation & Fibre

We are particularly interested in relative monads on the functor
$\Delta^{T}:{\mathsf{Set}}^{T}\to{\mathsf{Pre}}^{T}$ for some set $T$, and
modules over such monads. _Derivation_ and _fibre_ , two important
constructions of [20] on modules over monads on families of sets, carry over
to modules over relative monads on ${\Delta}^{T}$.

Given $u\in T$, we denote by $D(u)\in{\mathsf{Set}}^{T}$ the context with
$D(u)(u)=\\{*\\}$ and $D(u)(t)=\emptyset$ for $u\neq t$. For a context
$V\in{\mathsf{Set}}^{T}$ we set $V^{*u}:=V+D(u)$.

######  2.33 Definition:

Given a monad $P$ over $\Delta^{T}$ and a $P$–module $M$ with codomain
$\mathcal{E}$, we define the derived module of $M$ with respect to $u\in T$ by
setting

$M^{u}(V):=M(V^{*u})\enspace.$

The module substitution is defined, for
$f\in{\mathsf{Pre}}^{T}(\Delta^{T}V,PW)$, by

$\varsigma^{M^{u}}({f}):=\varsigma^{M}({{}_{u}{f}})\enspace.$

Here the “shifted” map

${}_{u}{f}\in{\mathsf{Pre}}^{T}\bigl{(}\Delta^{T}(V^{*u}),P(W^{*u})\bigr{)}$

is the adjunct under the adjunction of Sect. 2.1 of the coproduct map

$\varphi({}_{u}{f}):=[{P(\mathrm{inl})}\circ{f},\eta(\mathrm{inr}(*))]:V^{*u}\to
UP(W^{*u})\enspace,$

where $[\mathrm{inl},\mathrm{inr}]=\operatorname{id}:W^{*u}\to W^{*u}$.
Derivation is an endofunctor on the category of $P$–modules with codomain
$\mathcal{E}$.

######  2.34 Notation __:

In case the set $T$ of types is $T=\\{*\\}$ the singleton set of types, i.e.
when talking about untyped syntax, we denote by $M^{\prime}$ the derived
module of $M$. Given a natural number $n$, we denote by $M^{n}$ the module
obtained by deriving $n$ times the module $M$.

Analogously to [2], we derive more generally with respect to a natural
transformation $\tau:1\to\mathcal{T}U_{n}$:

######  2.35 Definition (Derived Module):

Let $\tau:1\to\mathcal{T}U_{n}$ be a natural transformation. Let $T$ be a set
and $P$ be a relative monad on $\Delta^{T}_{n}$. Given any $P$–module $M$, we
call _derivation of $M$ with respect to $\tau$_ the module with object map
$M^{\tau}(V):=M\left(V^{\tau(V)}\right)$.

######  2.36 Definition:

Let $P$ be a relative monad over $F$, and $M$ a $P$–module with codomain
$\mathcal{E}^{T}$ for some category $\mathcal{E}$. The _fibre module
$[{M}]_{t}$ of $M$ with respect to $t\in T$_ has object map

$c\mapsto M(c)(t)=M(c)_{t}$

and substitution map

$\varsigma^{[{M}]_{t}}({f}):=\bigl{(}\varsigma^{M}({f})\bigr{)}_{t}\enspace.$

This definition generalizes to fibres with respect to a natural transformation
as in Def. 2.35.

The pullback operation commutes with products, derivations and fibres :

######  2.37 Lemma:

Let ${\mathcal{C}}$ and $\mathcal{D}$ be categories and $\mathcal{E}$ be a
category with products. Let $P\colon{\mathcal{C}}\to\mathcal{D}$ and
$Q\colon{\mathcal{C}}\to D$ be monads over $F:{\mathcal{C}}\to\mathcal{D}$ and
$F^{\prime}:{\mathcal{C}}^{\prime}\to\mathcal{D}^{\prime}$, resp., and
$\rho:P\to Q$ a monad morphism. Let $M$ and $N$ be $P$–modules with codomain
$\mathcal{E}$. The pullback functor is cartesian:

$\rho^{*}(M\times N)\cong\rho^{*}M\times\rho^{*}N\enspace.$

######  2.38 Lemma:

Consider the setting as in the preceding lemma, with $F=\Delta^{T}$, and $t\in
T$. Then we have

$\rho^{*}(M^{t})\cong(\rho^{*}M)^{t}\enspace.$

######  2.39 Lemma:

Suppose $N$ is a $Q$–module with codomain ${\mathcal{E}}^{T}$, and $t\in T$.
Then

$\rho^{*}[{M}]_{t}\cong[{\rho^{*}M}]_{t}\enspace.$

######  2.40 Definition (Substitution of _one_ Variable):

Let $T$ be a (nonempty) set and let $P$ be a _reduction monad_ (cf. Def. 2.10)
over ${\Delta}^{T}$. For any $s,t\in T$ and $X\in{\mathsf{Set}}^{T}$ we define
a binary substitution operation

$\displaystyle\operatorname{subst}_{s,t}(X):P(X^{*s})_{t}\times P(X)_{s}$
$\displaystyle\to P(X)_{t},$ $\displaystyle(y,z)$ $\displaystyle\mapsto
y[*:=z]:=\sigma\left({[\eta_{X},\lambda x.z]}\right)(y)\enspace.$

For any pair $(s,t)\in T^{2}$, we thus obtain a morphism of $P$–modules

$\operatorname{subst}^{P}_{s,t}:[{{P}^{s}}]_{t}\times[{{P}}]_{s}\to[{{P}}]_{t}\enspace.$

Observe that this substitution operation is monotone in both arguments:
monotonicity in the first argument is a consequence of the monadic axioms.
Monotonicity in the second argument is enforced by considering reduction
monads (Def. 2.10).

##  3 Signatures, Representations, Initiality

We combine the techniques of [2] and [1] in order to obtain an initiality
result for simple type systems with reductions on the term level. As an
example, we specify, via the iteration principle coming from the universal
property, a semantically faithful translation from $\mathsf{PCF}$ with its
usual reduction relation to the untyped lambda calculus with beta reduction.

More precisely, in this section we define a notion of _signature_ and suitable
_representations_ for such signatures, such that the types and terms generated
by the signature, equipped with reductions according to the inequations
specified by the signature, form the _initial representation_. Analogously to
[1], we define a notion of _2–signature_ with two levels: a _syntactic_ level
specifying types and terms of a language, and, on top of that, a _semantic_
level specifying reduction rules on the terms.

###  3.1 1–Signatures

A _1–signature_ specifies types and terms over these types. We give two
presentations of 1–signatures, a _syntactic_ one (cf. Def. 3.7) and a
_semantic_ one (cf. Def. 3.18). The syntactic presentation is the same as in
[2]. However, the semantic presentation is here adapted to our use of
_relative_ monads or, to be more precise, _reduction monads_.

####  3.1.1 Signatures for Types

We present _algebraic signatures_ , which later are used to specify the
_object types_ of the languages we consider. Algebraic signatures and their
models were first considered by [8].

######  3.1 Definition (Algebraic Signature):

An _algebraic signature $S$_ is a family of natural numbers, i.e. a set
$J_{S}$ and a map (carrying the same name as the signature)
$S:J_{S}\to\mathbb{N}$. For $j\in J_{S}$ and $n\in\mathbb{N}$, we also write
$j:n$ instead of $j\mapsto n$. An element of $J$ resp. its image under $S$ is
called an _arity_ of $S$.

######  3.2 Example (Algebraic Signature of $T_{\operatorname{\mathsf{TLC}}}$,
Sect. 2.1):

The algebraic signature of the types of the simply–typed lambda calculus is
given by

$S_{\operatorname{\mathsf{TLC}}}:=\\{*:0\enspace,\quad(\leadsto):2\\}\enspace.$

To any algebraic signature we associate a category of _representations_. We
call _representation of $S$_ any set $U$ equipped with operations according to
the signature $S$. A _morphism of representations_ is a map between the
underlying sets that is compatible with the operations on either side in a
suitable sense. Representations and their morphisms form a category. We give
the formal definitions:

######  3.3 Definition (Representation of an Algebraic Signature):

A representation $R$ of an algebraic signature $S$ is given by

  * •

a set $X$ and

  * •

for each $j\in J_{S}$, an operation $j^{R}:X^{S(j)}\to X$.

In the following, given a representation $R$, we write $R$ also for its
underlying set.

######  3.4 Definition (Morphisms of Representations):

Given two representations $T$ and $U$ of the algebraic signature $S$, a
_morphism_ from $T$ to $U$ is a map $f:T\to U$ such that, for any arity
$n=S(j)$ of $S$, we have

${f}\circ{j^{T}}={j^{U}}\circ{(\underbrace{f\times\ldots\times f}_{n\text{
times}})}\enspace.$

######  3.5 Example:

The language $\mathsf{PCF}$ [28, 24] is a simply–typed lambda calculus with a
fixed point operator and arithmetic constants. Let
$J:=\\{\iota,o,(\Rightarrow)\\}$. The signature of the types of $\mathsf{PCF}$
is given by the arities

$S_{\mathsf{PCF}}:=\\{\iota:0\enspace,\quad
o:0\enspace,\quad(\Rightarrow):2\\}\enspace.$

A representation $T$ of $S_{\mathsf{PCF}}$ is given by a set $T$ and three
operations,

$\iota^{T}:T\enspace,\quad o^{T}:T\enspace,\quad(\Rightarrow)^{T}:T\times T\to
T\enspace.$

Given two representations $T$ and $U$ of $S_{\mathsf{PCF}}$, a morphism from
$T$ to $U$ is a map $f:T\to U$ between the underlying sets such that, for any
$s,t\in T$,

$\displaystyle f(\iota^{T})$ $\displaystyle=\iota^{U}\enspace,$ $\displaystyle
f(o^{T})$ $\displaystyle=o^{U}\quad\text{ and}$ $\displaystyle
f(s\Rightarrow^{T}t)$ $\displaystyle=f(s)\Rightarrow^{U}f(t)\enspace.$

####  3.1.2 Signatures for Terms

Consider the example of the simply–typed lambda calculus over a set
$T_{\operatorname{\mathsf{TLC}}}$ of types. Its signature for terms may be
given as follows:

$\\{\operatorname{abs}_{s,t}:=\bigl{[}([s],t)\bigr{]}\to(s\leadsto
t)\enspace,\quad\operatorname{app}_{s,t}:=\bigl{[}([],s\leadsto
t),([],s)\bigr{]}\to t\\}_{s,t\in T_{\operatorname{\mathsf{TLC}}}}\enspace.$
((3))

The parameters $s$ and $t$ range over the set
$T_{\operatorname{\mathsf{TLC}}}$ of types, the initial representation of the
signature for types from Sect. 3.1.1. Our goal is to consider representations
of the simply–typed lambda calculus in monads over categories of the form
${\mathsf{Set}}^{T}$ for _any_ set $T$ — provided that $T$ is equipped with a
representation of the signature $S_{\operatorname{\mathsf{TLC}}}$. It thus is
more suitable to specify the signature of the simply–typed lambda calculus as
follows:

$\\{\operatorname{abs}:=\bigl{[}([1],2)\bigr{]}\to(1\leadsto
2)\enspace,\quad\operatorname{app}:=\bigl{[}([],1\leadsto 2),([],1)\bigr{]}\to
2\\}\enspace.$ ((4))

For any representation $T$ of $S_{\operatorname{\mathsf{TLC}}}$, the variables
$1$ and $2$ range over elements of $T$. In this way the number of abstractions
and applications depends on the representation $T$ of
$S_{\operatorname{\mathsf{TLC}}}$: intuitively, a representation of the above
signature of Disp. (4) over a representation $T$ of
$T_{\operatorname{\mathsf{TLC}}}$ has $T^{2}$ abstractions and $T^{2}$
applications — one for each pair of elements of $T$.

######  3.6 Definition (Type of Degree $n$):

For $n\geq 1$, we call _types of $S$ of degree $n$_ the elements of the set
$S(n)$ of types associated to the signature $S$ with free variables in the set
$\\{1,\ldots,n\\}$. We set $S(0):=\hat{S}$. Formally, the set $S(n)$ may be
obtained as the initial representation of the signature $S$ enriched by $n$
nullary arities.

Types of degree $n$ are used to form classic arities of degree $n$:

######  3.7 Definition (Classic Arity of Degree $n$):

A classic arity for terms over the signature $S$ for types of degree $n$ is of
the form

$\bigl{[}([t_{1,1},\ldots,t_{1,m_{1}}],t_{1}),\ldots,([t_{k,1},\ldots,t_{k,m_{k}}],t_{k})\bigr{]}\to
t_{0}\enspace,$ ((5))

where $t_{i,j},t_{i}\in S(n)$. More formally, a classic arity of degree $n$
over $S$ is a pair consisting of an element $t_{0}\in S(n)$ and a list of
pairs. where each pair itself consists of a list
$[t_{i,1},\ldots,t_{i,m_{i}}]$ of elements of $S(n)$ and an element $t_{i}$ of
$S(n)$.

A classic arity of the form given in Disp. (5) denotes a constructor — or a
family of constructors, for $n\geq 1$ — whose output type is $t_{0}$, and
whose $k$ inputs are terms of type $t_{i}$, respectively, in each of which
variables of type according to the list $[t_{i,1},\ldots,t_{i,m_{i}}]$ are
bound by the constructor.

We have to adapt the _semantic_ definition of signatures for terms, however,
since we now work with reduction monads on $\Delta^{T}$ for some set $T$
instead of monads over families of sets. The following definition is the
analogue of earlier work [2], adapted to the use of _relative_ monads:

######  3.8 Definition (Relative $S$–Monad):

Given an algebraic signature $S$, the _category ${S}\text{-}\mathsf{RMnd}$ of
relative $S$–monads_ is defined as the category whose objects are pairs
$(T,P)$ of a representation $T$ of $S$ and a reduction monad

$P:{\mathsf{Set}}^{T}\stackrel{{\scriptstyle\Delta^{T}}}{{\longrightarrow}}{\mathsf{Pre}}^{T}\enspace.$

A morphism from $(T,P)$ to $(T^{\prime},P^{\prime})$ is a pair $(g,f)$ of a
morphism of $S$–representations $g:T\to T^{\prime}$ and a morphism of relative
monads $f:P\to P^{\prime}$ over the retyping functor $\vec{g}$ as in Sect.
2.1.

Given $n\in\mathbb{N}$, we write ${S}\text{-}\mathsf{RMnd}_{n}$ for the
category whose objects are pairs $(T,P)$ of a representation $T$ of $S$ and a
reduction monad $P$ over $\Delta^{T}_{n}$. A morphism from $(T,P)$ to
$(T^{\prime},P^{\prime})$ is a pair $(g,f)$ of a morphism of
$S$–representations $g:T\to T^{\prime}$ and a monad morphism $f:P\to
P^{\prime}$ over the retyping functor $\vec{g}_{n}$ defined in Def. 2.16.

Similarly, we have a large category of modules over relative monads:

######  3.9 Definition (Large Category
$\operatorname{\mathsf{LRMod}}_{n}({S},{\mathcal{D}})$ of Modules):

Given a natural number $n\in\mathbb{N}$, an algebraic signature $S$ and a
category $\mathcal{D}$, we call
$\operatorname{\mathsf{LRMod}}_{n}({S},{\mathcal{D}})$ the category an object
of which is a pair $(P,M)$ of a relative $S$–monad
$P\in{S}\text{-}\mathsf{RMnd}_{n}$ and a $P$–module with codomain
$\mathcal{D}$. A morphism to another such $(Q,N)$ is a pair $(f,h)$ of a
morphism of relative $S$–monads $f:P\to Q$ in ${S}\text{-}\mathsf{RMnd}_{n}$
and a morphism of relative modules $h:M\to f^{*}N$.

As before, we sometimes just write the module — i.e. the second — component of
an object or morphism of the large category of modules. Given
$M\in\operatorname{\mathsf{LRMod}}_{n}({S},{\mathcal{D}})$, we thus write
$M(V)$ or $M_{V}$ for the value of the module on the object $V$.

A _half–arity over $S$ of degree $n$_ is a functor from relative $S$–monads to
the category of large modules of degree $n$:

######  3.10 Definition (Half–Arity over $S$ (of degree $n$)):

Given an algebraic signature $S$ and $n\in\mathbb{N}$, we call _half–arity
over $S$ of degree $n$_ a functor

$\alpha:{S}\text{-}\mathsf{RMnd}\to\operatorname{\mathsf{LRMod}}_{n}({S},{\mathsf{Pre}})\enspace.$

which is pre–inverse to the forgetful functor.

As before we restrict ourselves to a class of such functors. Again, we start
with the _tautological_ module:

######  3.11 Definition (Tautological Module of Degree $n$):

Given $n\in\mathbb{N}$, any relative monad $R$ over $\Delta^{T}$ induces a
monad $R_{n}$ over $\Delta^{T}_{n}$ with object map
$(V,t_{1},\ldots,t_{n})\mapsto(RV,t_{1},\ldots,t_{n})$. To any relative
$S$–monad $R$ we associate the tautological module of $R_{n}$,

$\Theta_{n}(R):=(R_{n},R_{n})\in\operatorname{\mathsf{LRMod}}_{n}({S},{{\mathsf{Pre}}^{T}_{n}})\enspace.$

Furthermore, we use _canonical natural transformations_ (cf. Def. 3.13) to
build _classic_ half–arities; these transformations specify context extension
(derivation) and selection of specific object types (fibre):

######  3.12 Definition ($S{\mathcal{C}}_{n}$):

Given a category ${\mathcal{C}}$ — think of it as the category $\mathsf{Set}$
of sets — we define the category $S{\mathcal{C}}_{n}$ to be the category an
object of which is a triple $(T,V,\mathbf{t})$ where $T$ is a representation
of $S$, the object $V\in{{\mathcal{C}}}^{T}$ is a $T$–indexed family of
objects of ${\mathcal{C}}$ and $\mathbf{t}$ is a vector of elements of $T$ of
length $n$. We denote by $SU_{n}:S{\mathcal{C}}_{n}\to\mathsf{Set}$ the
functor mapping an object $(T,V,\mathbf{t})$ to the underlying set $T$.

We have a forgetful functor
$S{\mathcal{C}}_{n}\to\mathcal{T}{\mathcal{C}}_{n}$ which forgets the
representation structure. On the other hand, any representation $T$ of $S$ in
a set $T$ gives rise to a functor ${{\mathcal{C}}}^{T}_{n}\to
S{\mathcal{C}}_{n}$, which “attaches” the representation structure.

The meaning of a term $s\in S(n)$ as a natural transformation

$s:1\Rightarrow SU_{n}:S{\mathcal{C}}_{n}\to\mathsf{Set}$

is now given by recursion on the structure of $s$:

######  3.13 Definition (Canonical Natural Transformation):

Let $s\in S(n)$ be a type of degree $n$. Then $s$ denotes a natural
transformation

$s:1\Rightarrow SU_{n}:S{\mathcal{C}}_{n}\to\mathsf{Set}\enspace$

defined recursively on the structure of $s$ as follows: for
$s=\alpha(a_{1},\ldots,a_{k})$ the image of a constructor $\alpha\in S$ we set

$s(T,V,\mathbf{t})=\alpha(a_{1}(T,V,\mathbf{t}),\ldots,a_{k}(T,V,\mathbf{t}))$

and for $s=m$ with $1\leq m\leq n$ we define

$s(T,V,\mathbf{t})=\mathbf{t}(m)\enspace.$

We call a natural transformation of the form $s\in S(n)$ _canonical_.

######  3.14 Definition (Classic Half–Arity):

As with monads (cf. [2]), we restrict our attention to _classic_ half–arities,
which we define analogously to [2] as constructed using derivations and
products, starting from the fibres of the tautological module and the constant
singleton module. We omit the precise statement of this definition.

The following clauses define an inductive set of _classic_ half–arities, to
which we restrict our attention:

  * •

The constant functor $*:R\mapsto 1$ is a classic half–arity.

  * •

Given any canonical natural transformation $\tau:1\to SU_{n}$ (cf. Def. 3.13),
the point-wise fibre module with respect to $\tau$ (cf. Def. 2.36) of the
tautological module $\Theta_{n}:R\mapsto(R_{n},R_{n})$ (cf. Def. 3.11) is a
classic half–arity of degree $n$,

$[{\Theta_{n}}]_{\tau}:{S}\text{-}\mathsf{RMnd}\to\operatorname{\mathsf{LRMod}}_{n}({S},{\mathsf{Set}})\enspace,\quad
R\mapsto[{R_{n}}]_{\tau}\enspace.$

  * •

Given any (classic) half–arity
$M:{S}\text{-}\mathsf{Mnd}\to\operatorname{\mathsf{LMod}}_{n}({S},{\mathsf{Set}})$
of degree $n$ and a canonical natural transformation $\tau:1\to SU_{n}$, the
point-wise derivation of $M$ with respect to $\tau$ is a (classic) half–arity
of degree $n$,

$M^{\tau}:{S}\text{-}\mathsf{RMnd}\to\operatorname{\mathsf{LRMod}}_{n}({S},{\mathsf{Set}})\enspace,\quad
R\mapsto\bigl{(}M(R)\bigr{)}^{\tau}\enspace.$

Here $\bigl{(}M(R)\bigr{)}^{\tau}$ really means derivation of the module, i.e.
derivation in the second component of $M(R)$.

  * •

For a half–arity $M$, let $M_{i}:R\mapsto\pi_{i}M(R)$ denote the $i$–th
projection. Given two (polynomial) half–arities $M$ and $N$ of degree $n$,
which coincide pointwise on the first component, i.e. such that $M_{1}=N_{1}$.
Then their product $M\times N$ is again a (polynomial) half–arity of degree
$n$. Here the product is really the pointwise product in the second component,
i.e.

$M\times N:R\mapsto\bigl{(}M_{1}(R),M_{2}(R)\times N_{2}(R)\bigr{)}\enspace.$

A half–arity of degree $n$ thus associates, to any relative $S$–monad $P$ over
a set of types $T$, a _family of $P$–modules_ indexed by $T^{n}$:

######  3.15 Remark _Module of Higher Degree corresponds to a Family of
Modules_ :

Let $T$ be a set and let $R$ be a monad on the functor ${\Delta}^{T}$. Then a
module $M$ over the monad $R_{n}$ corresponds precisely to a family of
$R$–modules $(M_{\mathbf{t}})_{\mathbf{t}\in T^{n}}$ by (un)currying.
Similarly, a morphism $\alpha:M\to N$ of modules of degree $n$ is equivalent
to a family $(\alpha_{\mathbf{t}})_{\mathbf{t}\in T^{n}}$ of morphisms of
modules of degree zero with $\alpha_{\mathbf{t}}:M_{\mathbf{t}}\to
N_{\mathbf{t}}$.

An arity of degree $n\in\mathbb{N}$ for terms over an algebraic signature $S$
is defined to be a pair of functors from relative $S$–monads to modules in
$\operatorname{\mathsf{LRMod}}_{n}({S},{\mathsf{Pre}})$. The degree $n$
corresponds to the number of object type indices of its associated
constructor. As an example, the arities of $\operatorname{Abs}$ and
$\operatorname{App}$ of Disp. (4) are of degree $2$.

######  3.16 Definition (Weighted Set):

A weighted set is a set $J$ together with a map $d:J\to\mathbb{N}$.

######  3.17 Definition (Term–Arity, Signature over $S$):

A _classic arity $\alpha$ over $S$ of degree $n$_ is a pair

$s=\bigl{(}\operatorname{dom}(\alpha),\operatorname{cod}(\alpha)\bigr{)}$

of half–arities over $S$ of degree $n$ such that

  * •

$\operatorname{dom}(\alpha)$ is classic and

  * •

$\operatorname{cod}(\alpha)$ is of the form $[{\Theta_{n}}]_{\tau}$ for some
canonical natural transformation $\tau$ as in Def. 3.13.

Any classic arity is thus _syntactically_ of the form given in Def. 3.7. We
write $\operatorname{dom}(\alpha)\to\operatorname{cod}(\alpha)$ for the arity
$\alpha$, and $\operatorname{dom}(\alpha,R):=\operatorname{dom}(\alpha)(R)$
and similar for the codomain and morphisms of relative $S$–monads. Given a
weighted set $(J,d)$ as in Def. 3.16, a _term–signature_ $\Sigma$ over $S$
indexed by $(J,d)$ is a $J$-family $\Sigma$ of algebraic arities over $S$, the
arity $\Sigma(j)$ being of degree $d(j)$ for any $j\in J$.

######  3.18 Definition (Typed Signature):

A _typed signature_ is a pair $(S,\Sigma)$ consisting of an algebraic
signature $S$ for sorts and a term–signature $\Sigma$ (indexed by some
weighted set) over $S$.

######  3.19 Example:

The terms of the simply typed lambda calculus over the type signature of Sect.
3.1.1 are given by the arities

$\displaystyle\operatorname{abs}$
$\displaystyle:[{\Theta^{1}}]_{2}\to[{\Theta}]_{1\leadsto 2}\enspace,$
$\displaystyle\operatorname{app}$ $\displaystyle:[{\Theta}]_{1\leadsto
2}\times[{\Theta}]_{1}\to[{\Theta}]_{2}\quad,$

both of which are of degree $2$ — we leave the degree implicit. The outer
lower index and the exponent are to be interpreted as de Bruijn variables,
ranging over types. They indicate the fibre (cf. Def. 2.36) and derivation
(cf. Def. 2.35), respectively, in the special case where the corresponding
natural transformation is given by a natural number as in Def. 3.13. In
particular, contrast that to the signature for the simply–typed lambda
calculus we gave in Disp. (3). The difference is that now “similar” arities
which differ only in an object type parameter, are grouped together, whereas
this is not the case in Disp. (3).

Those two arities, $\operatorname{abs}$ and $\operatorname{app}$, can in fact
be considered over any algebraic signature $S$ with an arrow constructor, in
particular over the signature $S_{\mathsf{PCF}}$ (cf. Sect. 3.1.2).

######  3.20 Example (Sect. 3.1.1 continued):

We continue considering $\mathsf{PCF}$. The signature $S_{\mathsf{PCF}}$ for
its types is given in Sect. 3.1.1. The term–signature of $\mathsf{PCF}$ is
given in Fig. 1: it consists of an arity for abstraction and an arity for
application, each of degree 2, an arity (of degree 1) for the fixed point
operator, and one arity of degree 0 for each logic and arithmetic constant —
some of which we omit:

$\displaystyle\operatorname{abs}$
$\displaystyle:[{\Theta^{1}}]_{2}\to[{\Theta}]_{1\Rightarrow 2}\enspace,$
$\displaystyle\operatorname{app}$ $\displaystyle:[{\Theta}]_{1\Rightarrow
2}\times[{\Theta}]_{1}\to[{\Theta}]_{2}\enspace,$ $\displaystyle\mathbf{Fix}$
$\displaystyle:[{\Theta}]_{1\Rightarrow 1}\to[{\Theta}]_{1}\enspace,$
$\displaystyle\mathbf{n}$ $\displaystyle:*\to[{\Theta}]_{\iota}\qquad\text{for
$n\in\mathbb{N}$}$ $\displaystyle\mathbf{Succ}$
$\displaystyle:*\to[{\Theta}]_{\iota\Rightarrow\iota}$
$\displaystyle\mathbf{Pred}$
$\displaystyle:*\to[{\Theta}]_{\iota\Rightarrow\iota}$
$\displaystyle\mathbf{Zero?}$ $\displaystyle:*\to[{\Theta}]_{\iota\Rightarrow
o}$ $\displaystyle\mathbf{cond_{\iota}}$
$\displaystyle:*\to[{\Theta}]_{o\Rightarrow\iota\Rightarrow\iota\Rightarrow\iota}$
$\displaystyle\mathbf{T},\mathbf{F}$ $\displaystyle:*\to[{\Theta}]_{o}$
$\displaystyle\vdots$

Figure 1: Term Signature of $\mathsf{PCF}$

Our presentation of $\mathsf{PCF}$ is inspired by [24], who — similarly to
[28] — consider, e.g., the successor as a constant of arrow type. As an
alternative, one might consider the successor as a constructor expecting a
term of type $\iota$ as argument, yielding a term of type $\iota$. For our
purpose, those two points of view are equivalent.

###  3.2 Representations of 1–Signatures

######  3.21 Definition (Representation of an Arity, a Signature over $S$):

A representation of an arity $\alpha$ over $S$ in an $S$–monad $R$ is a
morphism of relative modules

$\operatorname{dom}(\alpha,R)\to\operatorname{cod}(\alpha,R)\enspace.$

A representation $R$ of a signature over $S$ is a given by a relative
$S$–monad — called $R$ as well — and a representation $\alpha^{R}$ of each
arity $\alpha$ of $S$ in $R$.

Representations of $(S,\Sigma)$ are the objects of a category
$\operatorname{Rep}^{\Delta}(S,\Sigma)$, whose morphisms are defined as
follows:

######  3.22 Definition (Morphism of Representations):

Given representations $P$ and $R$ of a typed signature $(S,\Sigma)$, a
morphism of representations $f:P\to R$ is given by a morphism of relative
$S$–monads $f:P\to R$, such that for any arity $\alpha$ of $S$ the following
diagram of module morphisms commutes:

$\textstyle{\operatorname{dom}(\alpha,P)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\operatorname{dom}(\alpha,f)}$$\scriptstyle{\alpha^{P}}$$\textstyle{\operatorname{cod}(\alpha,P)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\operatorname{cod}(\alpha,f)}$$\textstyle{\operatorname{dom}(\alpha,R)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha^{R}}$$\textstyle{\operatorname{cod}(\alpha,R).}$

######  3.23 Lemma:

For any typed signature $(S,\Sigma)$, the category of representations of
$(S,\Sigma)$ has an initial object.

###### Proof.

The initial object is obtained, analogously to the untyped case (cf. [1]), via
an adjunction $\Delta_{*}\dashv U_{*}$ between the categories of
representations of $(S,\Sigma)$ in relative monads and those in monads as in
[2].

In more detail, to any relative $S$–monad $(T,P)\in{S}\text{-}\mathsf{RMnd}$
we associate the $S$–monad $U(T,P):=(T,UP)$ where $U_{*}P$ is the monad
obtained by postcomposing with the forgetful functor
${U}^{T}:{\mathsf{Pre}}^{T}\to{\mathsf{Set}}^{T}$. Substitution for $U_{*}P$
is defined, in each fibre, as in Sect. 2.1. For any arity $s\in\Sigma$ we have
that

$U_{*}\operatorname{dom}(s,P)\cong\operatorname{dom}(s,U_{*}P)\enspace,$

and similar for the codomain. The postcomposed representation morphism
$U_{*}s(P)$ hence represents $s$ in $U_{*}P$ in the sense of [2]. This defines
the functor
$U_{*}:\operatorname{Rep}^{\Delta}(S,\Sigma)\to\operatorname{Rep}(S,\Sigma)$.
Conversely, to any $S$–monad we can associate a relative $S$–monad by
postcomposing with ${\Delta}^{T}:{\mathsf{Set}}^{T}\to{\mathsf{Pre}}^{T}$,
analogous to the untyped case in [1], yielding
$\Delta_{*}:\operatorname{Rep}(S,\Sigma)\to\operatorname{Rep}^{\Delta}(S,\Sigma)$.
In summary, the natural isomorphism

$\varphi_{R,P}:\bigl{(}\operatorname{Rep}^{\Delta}(S,\Sigma)\bigr{)}(\Delta_{*}R,P)\cong\bigl{(}\operatorname{Rep}(S,\Sigma)\bigr{)}(R,U_{*}P)$

is given by postcomposition with the forgetful functor (from left to right)
resp. the functor $\Delta$ (from right to left).

∎

###  3.3 Inequations

Analogously to the untyped case (cf. [1]), an inequation associates, to any
representation of $(S,\Sigma)$ in a relative monad $P$, two parallel morphisms
of $P$–modules. However, similarly to arities, an inequation may now be, more
precisely, a _family of inequations_ , indexed by object types. Consider the
simply–typed lambda calculus, which was defined with _typed_ abstraction and
application. Similarly, we have a _typed substitution_ operation for
$\operatorname{\mathsf{TLC}}$, which substitutes a term of type $s\in
T_{\operatorname{\mathsf{TLC}}}$ for a free variable of type $s$ in a term of
type $t\in T_{\operatorname{\mathsf{TLC}}}$, yielding again a term of type
$t$. For $s,t\in T_{\operatorname{\mathsf{TLC}}}$ and
$M\in\operatorname{\mathsf{TLC}}(V^{*s})_{t}$ and
$N\in\operatorname{\mathsf{TLC}}(V)_{s}$, beta reduction is specified by

$\lambda_{s,t}M(N)\leadsto M[*:=N]\enspace,$

where our notation hides the fact that not only abstraction, but also
application and substitution are typed operations. More formally, such a
reduction rule might read as a family of inequations between morphisms of
modules

${\operatorname{app}_{s,t}}\circ{(\operatorname{abs}_{s,t}\times\operatorname{id})}\enspace\leq\enspace\\_[*^{s}:=_{t}\\_]\enspace,$

where $s,t\in T_{\operatorname{\mathsf{TLC}}}$ range over types of the
simply–typed lambda calculus. Analogously to Sect. 3.1.2, we want to specify
the beta rule without referring to the set $T_{\operatorname{\mathsf{TLC}}}$,
but instead express it for an arbitrary representation $R$ of the typed
signature
$(S_{\operatorname{\mathsf{TLC}}},\Sigma_{\operatorname{\mathsf{TLC}}})$ (cf.
Sect. 3.1.1, 3.1.2), as in

${\operatorname{app}^{R}}\circ{(\operatorname{abs}^{R}\times\operatorname{id})}\enspace\leq\enspace\\_[*:=\\_]\enspace,$

where both the left and the right side of the inequation are given by suitable
$R$–module morphisms of degree 2. Source and target of a _half–equation_
accordingly are given by functors from representations of a typed signature
$(S,\Sigma)$ to a suitable category of modules. A half–equation then is a
natural transformation between its source and target functor:

######  3.24 Definition (Category of Half–Equations):

Let $(S,\Sigma)$ be a signature. An _$(S,\Sigma)$ –module_ $U$ of degree
$n\in\mathbb{N}$ is a functor from the category of representations of
$(S,\Sigma)$ as defined in Sect. 3.2 to the category
$\operatorname{\mathsf{LRMod}}_{n}({S},{\mathsf{Pre}})$ (cf. Def. 3.9)
commuting with the forgetful functor to the category of relative monads. We
define a morphism of $(S,\Sigma)$–modules to be a natural transformation which
becomes the identity when composed with the forgetful functor. We call these
morphisms _half–equations_ (of degree $n$). We write $U^{R}:=U(R)$ for the
image of the representation $R$ under the $S$–module $U$, and similar for
morphisms.

######  3.25 Definition (Substitution as Half–Equation):

Given a relative monad on ${\Delta}^{T}$, its associated
substitution–of–one–variable operation (cf. Def. 2.40) yields a family of
module morphisms, indexed by pairs $(s,t)\in T$. By Sect. 3.1.2 this family is
equivalent to a module morphism of degree 2. The assignment

$\operatorname{subst}:R\mapsto\operatorname{subst}^{R}:[{{R}_{2}^{1}}]_{2}\times[{{R}_{2}}]_{1}\to[{{R}_{2}}]_{2}$

thus yields a half–equation of degree $2$ over any signature $S$. Its domain
and codomain are classic.

######  3.26 Example (Sect. 3.1.2 continued):

The map

${\operatorname{app}}\circ{(\operatorname{abs}\times\operatorname{id})}:R\mapsto{\operatorname{app}^{R}}\circ{(\operatorname{abs}^{R},\operatorname{id}^{R})}:[{{R}_{2}^{1}}]_{2}\times[{{R}_{2}}]_{1}\to[{{R}_{2}}]_{2}$

is a half–equation over the signature $\operatorname{\mathsf{TLC}}$, as well
as over the signature of $\mathsf{PCF}$.

######  3.27 Definition:

Any classic arity of degree $n$,

$s=[{\Theta_{n}^{{{\tau_{1}}}}}]_{\sigma_{1}}\times\ldots\times[{\Theta_{n}^{{\tau_{m}}}}]_{\sigma_{m}}\to[{\Theta_{n}}]_{\sigma}\enspace,$

defines a classic $S$–module

$\operatorname{dom}(s):R\mapsto[{R^{\tau_{1}}_{n}}]_{\sigma_{1}}\times\ldots\times[{R^{\tau_{m}}_{n}}]_{\sigma_{m}}\enspace.$

######  3.28 Definition (Inequation):

Given a signature $(S,\Sigma)$, an _inequation over $(S,\Sigma)$_, or
_$(S,\Sigma)$ –inequation_, of degree $n\in\mathbb{N}$ is a pair of parallel
half–equations between $(S,\Sigma)$–modules of degree $n$. We write
$\alpha\leq\gamma$ for the inequation $(\alpha,\gamma)$.

######  3.29 Example (Beta Reduction):

For any suitable 1–signature — i.e. for any 1–signature that has an arity for
abstraction and an arity for application — we specify beta reduction using the
parallel half–equations of Defs. 3.25 and Sect. 3.3:

${\operatorname{app}}\circ{(\operatorname{abs}\times\operatorname{id})}\leq\operatorname{subst}:[{\Theta_{2}^{1}}]_{2}\times[{\Theta_{2}}]_{1}\to[{\Theta_{2}}]_{2}\enspace.$

######  3.30 Example (Fixpoints and Arithmetics of $\mathsf{PCF}$):

The reduction rules of $\mathsf{PCF}$ are specified by the inequations — over
the 1–signature of $\mathsf{PCF}$ as given in Sect. 3.1.2 — of Fig. 2.

$\displaystyle\mathbf{Fix}$
$\displaystyle\leq{\operatorname{app}}\circ{(\operatorname{id},\mathbf{Fix})}:[{\Theta_{1}}]_{1\Rightarrow
1}\to[{\Theta_{1}}]_{1}$
$\displaystyle{\operatorname{app}}\circ{(\mathbf{Succ},\mathbf{n})}$
$\displaystyle\leq\mathbf{n+1}:*\to[{\Theta}]_{\iota}$
$\displaystyle{\operatorname{app}}\circ{(\mathbf{Pred},\mathbf{0})}$
$\displaystyle\leq\mathbf{0}:*\to[{\Theta}]_{\iota}$
$\displaystyle{\operatorname{app}}\circ{\left(\mathbf{Pred},{\operatorname{app}}\circ{({\mathbf{Succ}},{\mathbf{n}})}\right)}$
$\displaystyle\leq\mathbf{n}:*\to[{\Theta}]_{\iota}$
$\displaystyle{\operatorname{app}}\circ{(\mathbf{Zero?},\mathbf{0})}$
$\displaystyle\leq\mathbf{T}:*\to[{\Theta}]_{o}$
$\displaystyle{\operatorname{app}}\circ{\left(\mathbf{Zero?},{\operatorname{app}}\circ{(\mathbf{Succ},\mathbf{n})}\right)}$
$\displaystyle\leq\mathbf{F}:*\to[{\Theta}]_{o}$ $\displaystyle\vdots$

Figure 2: Reduction Rules of $\mathsf{PCF}$

######  3.31 Definition (Representation of Inequations):

A _representation of an $(S,\Sigma)$–inequation $\alpha\leq\gamma:U\to V$_ (of
degree $n$) is any representation $R$ over a set of types $T$ of $(S,\Sigma)$
such that $\alpha^{R}\leq\gamma^{R}$ pointwise, i.e. if for any pointed
context $(X,\mathbf{t})\in{\mathsf{Set}}^{T}\times T^{n}$, any $t\in T$ and
any $y\in U^{R}_{(X,\mathbf{t})}(t)$,

$\alpha^{R}(y)\enspace\leq\enspace\gamma^{R}(y)\enspace,$ ((6))

where we omit the sort argument $t$ as well as the context $(X,\mathbf{t})$
from $\alpha$ and $\gamma$. We say that such a representation $R$ _satisfies_
the inequation $\alpha\leq\gamma$.

For a set $A$ of $(S,\Sigma)$–inequations, we call _representation of
$((S,\Sigma),A)$_ any representation of $(S,\Sigma)$ that satisfies each
inequation of $A$. We define the category of representations of the
2–signature $((S,\Sigma),A)$ to be the full subcategory of the category of
representations of $S$ whose objects are representations of $((S,\Sigma),A)$.
We also write $(\Sigma,A)$ for $((S,\Sigma),A)$.

According to Sect. 3.1.2, the inequation of Disps. (6) is equivalent to ask
whether, for any $\mathbf{t}\in T^{n}$, any $t\in T$ and any $y\in
U_{\mathbf{t}}^{R}(X)(t)$,

$\alpha_{\mathbf{t}}^{R}(y)\enspace\leq\enspace\gamma_{\mathbf{t}}^{R}(y)\enspace.$

###  3.4 Initiality for 2–Signatures

We are ready to state and prove an initiality result for typed signatures with
inequations:

######  3.32 Theorem:

For any set of classic $(S,\Sigma)$–inequations $A$, the category of
representations of $((S,\Sigma),A)$ has an initial object.

###### Proof.

The proof is analogous to that of the untyped case [1]. The fact that we now
consider _typed_ syntax introduces a minor complication, on the presentation
of which we put the emphasis during the proof. The basic ingredients for
building the initial representation are given by the initial representation
$(\hat{S},\hat{\Sigma})$ — or just $\hat{\Sigma}$ for short — in the category
$\operatorname{Rep}(S,\Sigma)$ of representations in monads on set families
[2]. Equivalently, the ingredients come from the initial object
$(\hat{S},\Delta_{*}\hat{\Sigma})$ — or just $\Delta_{*}\hat{\Sigma}$ for
short — of representations _without inequations_ in the category
$\operatorname{Rep}^{\Delta}(S,\Sigma)$ (cf. Sect. 3.2). We call
$\hat{\Sigma}$ resp. $\Delta_{*}\hat{\Sigma}$ the monad resp. relative monad
underlying the initial representation

The proof consists of 3 steps: at first, we define a preorder $\leq_{A}$ on
the terms of $\hat{\Sigma}$, induced by the set $A$ of inequations. Afterwards
we show that the data of the representation $\hat{\Sigma}$ — substitution,
representation morphisms etc. — is compatible with the preorder $\leq_{A}$ in
a suitable sense. This will yield a representation $\hat{\Sigma}_{A}$ of
$(\Sigma,A)$. Finally we show that $\hat{\Sigma}_{A}$ is the initial such
representation.

_— The monad underlying the initial representation:_

For any context $X\in{\mathsf{Set}}^{\hat{S}}$ and $t\in\hat{S}$, we equip
$\hat{\Sigma}X(t)$ with a preorder $A$ by setting — _morally_ , cf. below —,
for $x,y\in\hat{\Sigma}X(t)$,

$x\leq_{A}y\quad:\Leftrightarrow\quad\forall
R:\operatorname{Rep}(\Sigma,A),\quad i_{R}(x)\leq_{R}i_{R}(y)\enspace,$ ((7))

where $i_{R}:\Delta_{*}\hat{\Sigma}\to R$ is the initial morphism of
representations of $(S,\Sigma)$, cf. Sect. 3.2. Note that the above definition
in Disp. (7) is ill–typed: we have $x\in\hat{\Sigma}X(t)$, which cannot be
applied to (a fibre of) $i_{R}(X):\vec{g}(\hat{\Sigma}X)\to R(\vec{g}X)$. We
denote by $\varphi=\varphi_{R}$ the natural isomorphism induced by the
adjunction of Def. 2.13 obtained by retyping — along the initial morphism of
types $g:\hat{S}\to T=T_{R}$ — towards the set $T$ of “types” of $R$,

$\varphi_{X,Y}:{\mathsf{Pre}}^{T}\left(\vec{g}(\hat{\Sigma}X),R(\vec{g}X)\right)\cong{\mathsf{Pre}}^{\hat{S}}\left(\hat{\Sigma}X,{R(\vec{g}X)}\circ{g}\right)\enspace.$

Instead of the above definition in Disp. (7), we should really write

$x\leq_{A}y\quad:\Leftrightarrow\quad\forall
R:\operatorname{Rep}(\Sigma,A),\quad\left(\varphi(i_{R,X})\right)(x)\leq_{R}\left(\varphi(i_{R,X})\right)(y)\enspace,$
((8))

where we omit the subscript “$R$” from $\varphi$. We have to show that the map

$X\mapsto\hat{\Sigma}_{A}X:=(\hat{\Sigma}X,\leq_{A})$

yields a relative monad on $\Delta^{\hat{S}}$. The missing fact to prove is
that the substitution with a morphism

$f\in{\mathsf{Pre}}^{\hat{S}}(\Delta
X,\hat{\Sigma}_{A}Y)\cong{\mathsf{Set}}^{\hat{S}}(X,\hat{\Sigma}Y)$

is compatible with the order $\leq_{A}$: given any
$f\in{\mathsf{Pre}}^{\hat{S}}(\Delta X,\hat{\Sigma}_{A}Y)$ we show that

$\sigma^{\hat{\Sigma}}(f)\in{\mathsf{Set}}^{\hat{S}}(\hat{\Sigma}X,\hat{\Sigma}Y)$

is monotone with respect to $\leq_{A}$ and hence (the carrier of) a morphism

$\sigma^{\hat{\Sigma}_{A}}(f)\in{\mathsf{Pre}}^{\hat{S}}(\hat{\Sigma}_{A}X,\hat{\Sigma}_{A}Y)\enspace.$

We overload the infix symbol ${}\gg={}$ to denote monadic substitution. Note
that this notation now hides an implicit argument giving the sort of the term
in which we substitute. Suppose $x,y\in\hat{\Sigma}X(t)$ with $x\leq_{A}y$, we
show

${x}\gg={f}\enspace\leq_{A}\enspace{y}\gg={f}\enspace.$

Using the definition of $\leq_{A}$, we must show, for a given representation
$R$ of $(\Sigma,A)$,

$\left(\varphi(i_{R})\right)({x}\gg={f})\enspace\leq_{R}\enspace\left(\varphi(i_{R})\right)({y}\gg={f})\enspace.$
((9))

Let $g$ be the initial morphism of types towards the types of $R$. Since
$i:=i_{R}$ is a morphism of representations — and thus in particular a _monad_
morphism, it is compatible with the substitution of $\hat{\Sigma}$ and $R$; we
have

$\textstyle{\vec{g}(\hat{\Sigma}X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\vec{g}(\sigma(f))}$$\scriptstyle{i_{X}}$$\textstyle{\vec{g}(\hat{\Sigma}Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i_{Y}}$$\textstyle{R(\vec{g}X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma^{R}({i_{Y}}\circ{\vec{g}f})}$$\textstyle{R(\vec{g}Y).}$
((10))

By applying the isomorphism $\varphi$ on the diagram of Disp. (10), we obtain

$\displaystyle{\varphi(i_{Y})}\circ{\sigma(f)}$
$\displaystyle=\varphi\left({i_{Y}}\circ{\vec{g}(\sigma(f))}\right)$
$\displaystyle=\varphi\left({\sigma({i_{Y}}\circ{\vec{g}f})}\circ{i_{X}}\right)$
$\displaystyle={g^{*}\left(\sigma^{R}({i_{Y}}\circ{\vec{g}f})\right)}\circ{\varphi(i_{X})}\enspace.$
((11))

Rewriting the equality of Disp. (11) twice in the goal Disp. (9) yields the
goal

$g^{*}\left(\sigma^{R}({i_{Y}}\circ{\vec{g}f})\right)\left((\varphi(i_{X}))(x)\right)=g^{*}\left(\sigma^{R}({i_{Y}}\circ{\vec{g}f})\right)\left((\varphi(i_{X}))(y)\right)\enspace,$

which is true since $g^{*}\left(\sigma^{R}({i_{Y}}\circ{\vec{g}f})\right)$ is
monotone and $(\varphi(i_{X}))(x)\leq_{R}(\varphi(i_{X}))(y)$ by hypothesis.
We hence have defined a monad $\hat{\Sigma}_{A}$ over $\Delta^{\hat{S}}$.

It remains to show that this is a _reduction_ monad: for $f\leq f^{\prime}$,
we must prove that $\sigma(f)\leq\sigma(f^{\prime})$. By Disp. (11), it
suffices to show that

${g^{*}\left(\sigma^{R}({i_{Y}}\circ{\vec{g}f})\right)}\leq{g^{*}\left(\sigma^{R}({i_{Y}}\circ{\vec{g}f^{\prime}})\right)}$

which follows from the fact that $R$ is a reduction category.

######  3.33 Lemma:

Given a classic $S$–module
$V:\operatorname{Rep}^{\Delta}(S,\Sigma)\to\operatorname{\mathsf{LRMod}}({S},{\mathsf{Pre}})$
from the category of representations of $(S,\Sigma)$ in $S$–monads to the
large category of modules over $S$–monads and $x,y\in V(\hat{\Sigma})(X)(t)$,
we have

$x\leq_{A}y\in V^{\hat{\Sigma}}_{X}(t)\quad\Leftrightarrow\quad\forall
R:\operatorname{Rep}(S,A),\quad
V(i_{R})(x)\leq_{V^{R}_{X}}V(i_{R})(y)\enspace,$

where now and later we omit the arguments $X$ and $(i_{R}(t))$, e.g., in
$V(i_{R})(X)(i_{R}(t))(x)$.

###### Proof of Sects. 3.4.

The proof is done by induction on the derivation of “$V$ classic”. The only
interesting case is where $V=M\times N$ is a product:

$\displaystyle(x_{1},y_{1})\leq(x_{2},y_{2})$ $\displaystyle\Leftrightarrow
x_{1}\leq x_{2}\wedge y_{1}\leq y_{2}$ $\displaystyle\Leftrightarrow\forall
R,M(i_{R})(x_{1})\leq M(i_{R})(x_{2})\wedge\forall R,N(i_{R})(y_{1})\leq
N(i_{R})(y_{2})$ $\displaystyle\Leftrightarrow\forall R,M(i_{R})(x_{1})\leq
M(i_{R})(x_{2})\wedge N(i_{R})(y_{1})\leq N(i_{R})(y_{2})$
$\displaystyle\Leftrightarrow\forall R,V(i_{R})(x_{1},y_{1})\leq
V(i_{R})(x_{2},y_{2})\enspace.$

∎

_— Representing $\Sigma$ in $\hat{\Sigma}_{A}$:_

Any arity $s\in\Sigma$ should be represented by the module morphism
$s^{\hat{\Sigma}}$, i.e. by the representation of $s$ in $\hat{\Sigma}$. We
have to show that those representations are compatible with the preorder $A$.
Given $x\leq_{A}y$ in $\operatorname{dom}(s,\hat{\Sigma})(X)$, we show
(omitting the argument $X$ in $s^{\hat{\Sigma}}(X)(x)$)

$s^{\hat{\Sigma}}(x)\quad\leq_{A}\quad s^{\hat{\Sigma}}(y)\enspace.$

By definition, we have to show that, for any representation $R$ with initial
morphism $i=i_{R}:\hat{\Sigma}\to R$ as before,

$\varphi(i_{X})(s^{\hat{\Sigma}}(x))\quad\leq_{R}\quad\varphi(i_{X})(s^{\hat{\Sigma}}(y))\enspace.$

But these two sides are precisely the images of $x$ and $y$ under the
upper–right composition of the diagram of Def. 3.22 for the morphism of
representations $i_{R}$. By rewriting with this diagram we obtain the goal

$s^{R}\Bigl{(}\bigl{(}\operatorname{dom}(s)(i_{R})\bigr{)}(x)\Bigr{)}\quad\leq_{R}\quad
s^{R}\Bigl{(}\bigl{(}\operatorname{dom}(s)(i_{R})\bigr{)}(y)\Bigr{)}\enspace.$

We know that $s^{R}$ is monotone, thus it is sufficient to show

$\bigl{(}\operatorname{dom}(s)(i_{R})\bigr{)}(x)\quad\leq_{R}\quad\bigl{(}\operatorname{dom}(s)(i_{R})\bigr{)}(y)\enspace.$

This goal follows from Sects. 3.4 (instantiated for the classic $S$–module
$\operatorname{dom}(s)$, cf. Defs. 3.27) and the hypothesis $x\leq_{A}y$. We
hence have established a representation — which we call $\hat{\Sigma}_{A}$ —
of $S$ in $\hat{\Sigma}_{A}$.

_— $\hat{\Sigma}_{A}$ satisfies $A$:_

The next step is to show that the representation $\hat{\Sigma}_{A}$ satisfies
$A$. Given an inequation

$\alpha\leq\gamma:U\to V$

of $A$ with a classic $S$–module $V$, we must show that for any context
$X\in{\mathsf{Set}}^{\hat{S}}$, any $t\in\hat{S}$ and any $x\in
U(\hat{\Sigma}_{A})(X)_{t}$ in the domain of $\alpha$ we have

$\alpha^{\hat{\Sigma}_{A}}(x)\quad\leq_{A}\quad\gamma^{\hat{\Sigma}_{A}}(x)\enspace,$

where here and later we omit the context argument $X$ and the sort argument
$t$. By Sects. 3.4 the goal is equivalent to

$\forall R:\operatorname{Rep}(\Sigma,A),\quad
V(i_{R})(\alpha^{\hat{\Sigma}_{A}}(x))\quad\leq_{V^{R}_{X}}\quad
V(i_{R})(\gamma^{\hat{\Sigma}_{A}}(x))\enspace.$ ((12))

Let $R$ be a representation of $(\Sigma,A)$. We continue by proving Disp. (12)
for $R$. The half–equations $\alpha$ and $\gamma$ are natural transformations.
The fact that $i_{R}$ is the carrier of a morphism of
$(S,\Sigma)$–representations from $\Delta\hat{\Sigma}$ to $R$ allows to
rewrite the goal as

$\alpha^{R}\bigl{(}U(i_{R})(x)\bigr{)}\quad\leq_{V^{R}_{X}}\quad\gamma^{R}\bigr{(}U(i_{R})(x)\bigr{)}\enspace,$

which is true since $R$ satisfies $A$.

_— Initiality of $\hat{\Sigma}_{A}$:_

Given any representation $R$ of $(\Sigma,A)$, the morphism $i_{R}$ is monotone
with respect to the orders on $\hat{\Sigma}_{A}$ and $R$ by construction of
$\leq_{A}$. It is hence a morphism of representations from $\hat{\Sigma}_{A}$
to $R$. Unicity of the morphisms $i_{R}$ follows from its unicity in the
category of representations of $(S,\Sigma)$, i.e. without inequations. Hence
$(\hat{S},\hat{\Sigma}_{A})$ is the initial object in the category of
representations of $((S,\Sigma),A)$.

∎

######  3.34 Remark _Iteration Principle by Initiality_ :

The universal property of the language generated by a 2–signature yields an
_iteration principle_ to define maps — translations — on this language, which
are certified to be compatible with substitution and reduction in the source
and target languages. How does this iteration principle work? More precisely,
what data (and proof) needs to be specified in order to define such a
translation via initiality from a language, say, $(\hat{S},\hat{\Sigma}_{A})$
to another language $(\hat{S}^{\prime},\hat{\Sigma}^{\prime}_{A^{\prime}})$,
generated by signatures $(S,\Sigma,A)$ and
$(S^{\prime},\Sigma^{\prime},A^{\prime})$, respectively? The translation is a
morphism — an initial one — in the category of representations of the
signature $(S,\Sigma,A)$ of the source language. It is obtained by equipping
the relative monad $\hat{\Sigma}^{\prime}_{A^{\prime}}$ underlying the target
language with a representation of the signature $(S,\Sigma,A)$. In more
detail:

  1. 1.

we give a representation of the type signature $S$ in the set
$\hat{S}^{\prime}$. By initiality of $\hat{S}$, this yields a translation
$\hat{S}\to\hat{S}^{\prime}$ of sorts.

  2. 2.

Afterwards, we specify a representation of the term signature $\Sigma$ in the
monad $\hat{\Sigma}^{\prime}_{A^{\prime}}$ by defining suitable (families) of
morphisms of $\hat{\Sigma}^{\prime}_{A^{\prime}}$–modules. This yields a
representation $R$ of $(S,\Sigma)$ in the monad
$\hat{\Sigma}^{\prime}_{A^{\prime}}$.

By initiality, we obtain a morphism $f:(\hat{S},\hat{\Sigma})\to R$ of
representations of $(S,\Sigma)$, that is, we obtain a translation from
$(\hat{S},\hat{\Sigma})$ to $(\hat{S}^{\prime},\hat{\Sigma}^{\prime})$ as the
colax monad morphism underlying the morphism $f$. However, we have not yet
ensured that the translation $f$ is compatible with the respective reduction
preorders in the source and target languages.

  1. 3.

Finally, we verify that the representation $R$ of $(S,\Sigma)$ satisfies the
inequations of $A$, that is, we check whether, for each $\alpha\leq\gamma:U\to
V\in A$, and for each context $V$, each $t\in\hat{S}$ and $x\in U^{R}_{V}(t)$,

$\alpha^{R}(x)\enspace\leq\enspace\gamma^{R}(x)\enspace.$

After verifying that $R$ satisfies the inequations of $A$, the representation
$R$ is in fact a representation of $(S,\Sigma,A)$. The initial morphism $f$
thus yields a faithful translation from $(\hat{S},\hat{\Sigma}_{A})$ to
$(\hat{S}^{\prime},\hat{\Sigma}^{\prime}_{A^{\prime}})$.

######  3.35 Example (Translation from $\mathsf{PCF}$ to
$\operatorname{\mathsf{ULC}}$, Sects. 4):

We use the above explained iteration principle to specify a translation from
$\mathsf{PCF}$ to the untyped lambda calculus, that is semantically faithful
with respect to the usual reduction relation of $\mathsf{PCF}$ — generated by
the inequations of Sect. 3.3 — and beta reduction of the lambda calculus.

For the translation of $\mathsf{PCF}$ to the lambda calculus mapping the
fixedpoint operator of $\mathsf{PCF}$ to the Turing fixedpoint combinator, we
have formalized its specification via initiality in the proof assistant Coq
[9]. After constructing the category of representations of $\mathsf{PCF}$, we
equip the untyped lambda calculus with a representations of $\mathsf{PCF}$,
representing the arity $\mathbf{Fix}$ by the Turing operator ${\Theta}$. The
Coq source files as well as documentation is available on

http://math.unice.fr/laboratoire/logiciels.

Note that the translation is given by a Coq function and hence executable.

##  4 A Translation from $\mathsf{PCF}$ to $\operatorname{\mathsf{ULC}}$ via
Initiality, in Coq

In this section we describe the implementation of the category of
representations of $\mathsf{PCF}$, equipped with reduction rules, as well as
of its initial object. This yields an instance of Sects. 3.4. However, for the
implementation in Coq of this instance we make several simplifications
compared to the general theorem:

  * •

we do not define a notion of 2–signature, but specify directly a Coq type of
representations of semantic $\mathsf{PCF}$;

  * •

we use dependent Coq types to formalize arities of higher degree (cf. Def.
3.10), instead of relying on modules on pointed categories. A representation
of an arity of degree $n$ is thus given by a family of module morphisms (of
degree zero), indexed $n$ times over the respective object type as described
in Sect. 3.1.2;

  * •

the relation on the initial object is not defined via the formula of Disp.
(7), but directly through an inductive type, cf. Sect. 4.4, and various
closures, cf. Sect. 4.4.

###  4.1 Representations of $\mathsf{PCF}$

In this section we explain the formalization of representations of
$\mathsf{PCF}$ with reduction rules (cf. Fig. 1 and Fig. 2). According to Def.
3.21 and Defs. 3.31, such a representation consists of

  1. 1.

a representation of the types of $\mathsf{PCF}$ (in a Coq type U), cf. Sect.
3.1.1,

  2. 2.

a reduction monad P over the functor ${\Delta}^{U}$ (in the formalization:
IDelta U) and

  3. 3.

representations of the arities of $\mathsf{PCF}$ (cf. Sect. 3.1.2), i.e.
morphisms of $P$–modules with suitable source and target modules such that

  4. 4.

the inequations defining the reduction rules of $\mathsf{PCF}$ are satisfied.

A representation of $\mathsf{PCF}$ should be a “bundle”, i.e. a record type,
whose components — or “fields” — are these 4 items. We first define what a
representation of the term signature of $\mathsf{PCF}$ in a monad $P$ is, in
the presence of an $S_{\mathsf{PCF}}$–monad (cf. Def. 3.8). Unfolding the
definitions, we suppose given a type Sorts, a relative monad P over IDelta
Sorts and three operations on Sorts: a binary function Arrow — denoted by an
infixed “$\sim$$\sim$>” — and two constants Bool and Nat.

⬇

Variable Sorts : Type.

Variable P : RMonad (IDelta Sorts).

Variable Arrow : Sorts -> Sorts -> Sorts.

Variable Bool : Sorts.

Variable Nat : Sorts.

Notation "a $\sim$$\sim$> b" := (Arrow a b) (at level 60, right
associativity).

In this context, a representation of $\mathsf{PCF}$ is given by a bunch of
module morphisms satisfying some conditions. We split the definition into
smaller pieces, cf. Sect. 4.1 – 4.1 . Note that M[t] denotes the fibre module
of module M with respect to t, and d M // u denotes derivation of module M
with respect to u. The module denoted by a star * is the terminal module,
which is the constant singleton module.

4.1 Code (1–Signature of $\mathsf{PCF}$):

⬇

Class PCFPO_rep_struct := {

app : forall u v, (P[u $\sim$$\sim$> v]) x (P[u]) —> P[v]

where "A @ B" := (app _ _ _ (A,B));

abs : forall u v, (d P // u)[v] —> P[u $\sim$$\sim$> v];

rec : forall t, P[t $\sim$$\sim$> t] —> P[t];

tttt : * —> P[Bool];

ffff : * —> P[Bool];

nats : forall m:nat, * —> P[Nat];

Succ : * —> P[Nat $\sim$$\sim$> Nat];

Pred : * —> P[Nat $\sim$$\sim$> Nat];

Zero : * —> P[Nat $\sim$$\sim$> Bool];

CondN: * —> P[Bool $\sim$$\sim$> Nat $\sim$$\sim$> Nat $\sim$$\sim$> Nat];

CondB: * —> P[Bool $\sim$$\sim$> Bool $\sim$$\sim$> Bool $\sim$$\sim$> Bool];

bottom: forall t, * —> P[t];

…

These module morphisms are subject to some inequations specifying the
reduction rules of $\mathsf{PCF}$. The beta rule reads as

4.2 Code (Beta Rule for Representations of $\mathsf{PCF}$):

⬇

beta_red : forall r s V y z, abs r s V y @ z << y[*:= z] ;

…

where y[*:= z] is the substitution of the freshest variable (cf. Def. 2.40) as
a special case of simultaneous monadic substitution. The rule for the fixed
point operator says that $\mathbf{Y}(f)\leadsto f\left(\mathbf{Y}(f)\right)$:

4.3 Code (Inequation for Fixedpoint Operator):

⬇

Rec_A: forall V t g, rec t V g << g @ rec _ _ g

…

The other inequations concern the arithmetic and logical constants of
$\mathsf{PCF}$. Firstly, we have that the conditionals reduce according to the
truth value they are applied to:

4.4 Code (Logic Inequations of $\mathsf{PCF}$ Representations):

⬇

CondN_t: forall V n m, CondN V tt @ tttt _ tt @ n @ m << n ;

CondN_f: forall V n m, CondN V tt @ ffff _ tt @ n @ m << m ;

CondB_t: forall V n m, CondB V tt @ tttt _ tt @ n @ m << n ;

CondB_f: forall V n m, CondB V tt @ ffff _ tt @ n @ m << m ;

…

Furthermore, we have that $\operatorname{succ}(n)$ reduces to $n+1$ (which in
Coq is written S n), reduction of the $\operatorname{zero}?$ predicate
according to whether its argument is zero or not, and that the predecessor is
post–inverse to the successor function:

4.5 Code (Arithmetic Inequations of $\mathsf{PCF}$ Representations):

⬇

Succ_red: forall V n, Succ V tt @ nats n _ tt << nats (S n) _ tt ;

Zero_t: forall V, Zero V tt @ nats 0 _ tt << tttt _ tt ;

Zero_f: forall V n, Zero V tt @ nats (S n) _ tt << ffff _ tt ;

Pred_Succ: forall V n, Pred V tt @ (Succ V tt @ nats n _ tt) << nats n _ tt;

Pred_Z: forall V, Pred V tt @ nats 0 _ tt << nats 0 _ tt }.

After abstracting over the section variables we package all of this into a
record type:

⬇

Record PCFPO_rep := {

Sorts : Type;

Arrow : Sorts -> Sorts -> Sorts;

Bool : Sorts ;

Nat : Sorts ;

pcf_rep_monad :> RMonad (IDelta Sorts);

pcf_rep_struct :> PCFPO_rep_struct pcf_rep_monad Arrow Bool Nat }.

Notation "a $\sim$$\sim$> b" := (Arrow a b) (at level 60, right
associativity).

The type PCFPO_rep constitutes the type of objects of the category of
representations of $\mathsf{PCF}$ with reduction rules.

###  4.2 Morphisms of Representations

A morphism of representations (cf. Def. 3.22) is built from a morphism $g$ of
_type_ representations and a colax monad morphism over the retyping functor
associated to the map $g$. In the particular case of $\mathsf{PCF}$, a
morphism of representations from $P$ to $R$ consists of a morphism of
representations of the types of $\mathsf{PCF}$ — with underlying map Sorts_map
— and a colax morphism of relative monads which makes commute the diagrams of
the form given in Def. 3.22. We first define the diagrams we expect to
commute, before packaging everything into a record type of morphisms. The
context is given by the following declarations:

⬇

Variables P R : PCFPO_rep.

Variable Sorts_map : Sorts P -> Sorts R.

Hypothesis HArrow : forall u v, Sorts_map (u $\sim$$\sim$> v) = Sorts_map u
$\sim$$\sim$> Sorts_map v.

Hypothesis HBool : Sorts_map (Bool _ ) = Bool _ .

Hypothesis HNat : Sorts_map (Nat _ ) = Nat _ .

Variable f : colax_RMonad_Hom P R

(RETYPE (fun t => Sorts_map t))

(RETYPE_PO (fun t => Sorts_map t))

(RT_NT (fun t => Sorts_map t)).

We explain the commutative diagrams of Def. 3.22 for some of the arities. For
the successor arity we ask the following diagram to commute:

4.6 Code (Commutative Diagram for Successor Arity):

⬇

Program Definition Succ_hom’ :=

Succ ;; f [(Nat $\sim$$\sim$> Nat)] ;; Fib_eq_RMod _ _ ;; IsoPF == *—>* ;; f
** Succ.

Here the morphism Succ refers to the representation of the successor arity
either of P (the first appearance) or R (the second appearance) — Coq is able
to figure this out itself. The domain of the successor is given by the
terminal module $*$. Accordingly, we have that
$\operatorname{dom}(\operatorname{Succ},f)$ is the trivial module morphism
with domain and codomain given by the terminal module. We denote this module
morphism by *—>*. The codomain is given as the fibre of $f$ of type
$\iota\Rightarrow\iota$. The two remaining module morphisms are isomorphisms
which do not appear in the informal description. The isomorphism IsoPF is
needed to permute fibre with pullback (cf. Sect. 2.3). The morphism
Fib_eq_RMod M H takes a module M and a proof H of equality of two object types
as arguments, say, H : u = v. Its output is an isomorphism  M[u] —> M[v]. Here
the proof is of type

⬇

Sorts_map (Nat $\sim$$\sim$> Nat) = Sorts_map Nat $\sim$$\sim$> Sorts_map Nat

and Coq is able to figure out the proof itself. The diagram for application
uses the product of module morphisms, denoted by an infixed X:

4.7 Code (Commutative Diagram for Application Arity):

⬇

Program Definition app_hom’ := forall u v,

app u v;; f [( _ )] ;; IsoPF ==

(f [(u $\sim$$\sim$> v)] ;; Fib_eq_RMod _ (HArrow _ _);; IsoPF ) X (f [(u)] ;;
IsoPF ) ;;

IsoXP ;; f ** (app _ _ ).

In addition to the already encountered isomorphism IsoPF we have to insert an
isomorphism IsoXP which permutes pullback and product (cf. Sect. 2.3). As a
last example, we present the property for the abstraction:

4.8 Code (Commutative Diagram for Abstraction Arity):

⬇

Program Definition abs_hom’ := forall u v,

abs u v ;; f [( _ )] ==

DerFib_RMod_Hom _ _ _ ;; IsoPF ;; f ** (abs (_ u) (_ v)) ;; IsoFP ;;

Fib_eq_RMod _ (eq_sym (HArrow _ _ )) .

Here the module morphism DerFib_RMod_Hom f u v corresponds to the morphism
$\operatorname{dom}(\operatorname{Abs}(u,v),f)=[{f^{u}}]_{v}$, and IsoFP
permutes fibre with pullback, just like its sibling IsoPF, but the other way
round.

We bundle all those properties into a type class:

⬇

Class PCFPO_rep_Hom_struct := {

CondB_hom : CondB_hom’ ;

CondN_hom : CondN_hom’ ;

Pred_hom : Pred_hom’ ;

Zero_hom : Zero_hom’ ;

Succ_hom : Succ_hom’ ;

fff_hom : fff_hom’ ;

ttt_hom : ttt_hom’ ;

bottom_hom : bottom_hom’ ;

nats_hom : nats_hom’ ;

app_hom : app_hom’ ;

rec_hom : rec_hom’ ;

abs_hom : abs_hom’ }.

Similarly to what we did for representations, we abstract over the section
variables and define a record type of morphisms of representations from P to R
:

⬇

Record PCFPO_rep_Hom := {

Sorts_map : Sorts P -> Sorts R ;

HArrow : forall u v, Sorts_map (u $\sim$$\sim$> v) = Sorts_map u $\sim$$\sim$>
Sorts_map v;

HNat : Sorts_map (Nat _ ) = Nat R ;

HBool : Sorts_map (Bool _ ) = Bool R ;

rep_Hom_monad :> colax_RMonad_Hom P R (RT_NT Sorts_map);

rep_colax_Hom_monad_struct :> PCFPO_rep_Hom_struct

HArrow HBool HNat rep_Hom_monad }.

###  4.3 Equality of Morphisms, Category of Representations

We have already seen how some definitions that are trivial in informal
mathematics, turn into something awful in intensional type theory. Equality of
morphisms of representations is another such definition. Informally, two such
morphisms $a,c:P\to R$ of representations are equal if

  1. 1.

their map of object types $f_{a}$ and $f_{c}$ (Sorts_map) are equal and

  2. 2.

their underlying colax morphism of monads — also called $a$ and $c$ — are
equal.

In our formalization, the second condition is not even directly expressable,
since these monad morphisms do not have the same type: we have, for a context
$V\in{\mathsf{Set}}^{P}$,

$a_{V}:\vec{f_{a}}(PV)\to R(\vec{f_{a}}V)$

and

$c_{V}:\vec{f_{c}}(PV)\to R(\vec{f_{c}}V)\enspace.$

where ${\mathsf{Set}}^{P}$ is a notation for contexts typed over the set of
object types the representation $P$ comes with, formally the type Sorts P. We
can only compare $a_{V}$ to $c_{V}$ by composing each of them with a suitable
transport transp again, yielding morphisms

${{R(\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{transp}}}}}})}\circ{a_{V}}:\vec{f_{a}}(PV)\to
R(\vec{f_{a}}V)\to R(\vec{f_{c}}V)$

and

${{c_{V}}\circ{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{transp}}\textquoteright}}}}}:\vec{f_{a}}(PV)\to\vec{f_{c}}(PV)\to
R(\vec{f_{c}}V)\enspace.$

As before, for equal fibres $[{M}]_{u}$ and $[{M}]_{t}$ with $u=t$, the
carriers of those transports transp and transp’ are terms of the form eq_rect
_ _ _ H, where H is a proof term which depends on the proof of

⬇

forall x : Sorts P, Sorts_map c x = Sorts_map a x

of the first condition. Altogether, the definition of equality of morphisms of
representations is given by the following inductive proposition:

⬇

Inductive eq_Rep (P R : PCFPO_rep) : relation (PCFPO_rep_Hom P R) :=

| eq_rep : forall (a c : PCFPO_rep_Hom P R),

forall H : (forall t, Sorts_map c t = Sorts_map a t),

(forall V, a V ;; rlift R (Transp H V)

==

Transp_ord H (P V) ;; c V ) -> eq_Rep a c.

The formal proof that the relation thus defined is an equivalence is
inadequately long when compared to its mathematical complexity, due to the
transport elimination.

Composition of representations is done by composing the underlying maps of
sorts, as well as composing the underlying monad morphisms pointwise. Again,
this operation, which is trivial from a mathematical point of view, yields a
difficulty in the formalization, due to the fact that in the formalization

$\vec{g}(\vec{f}V)\not\equiv\vec{({g}\circ{f})}V\enspace.$

More precisely, suppose given two morphisms of representations $a:P\to Q$ and
$b:Q\to R$, given by families of morphisms indexed by $V$ resp. $W$,

$\displaystyle a_{V}$ $\displaystyle:\widetilde{PV}^{a}\to
Q(\widetilde{V}^{a})\quad\text{and}$ $\displaystyle b_{W}$
$\displaystyle:\widetilde{QW}^{b}\to R(\widetilde{W}^{b})\enspace,$

where we write $\widetilde{V}^{a}$ for $\vec{f_{a}}V$. The monad morphism
underlying the composite morphism of representations is given by the following
definition:

$\textstyle{\widetilde{PV}^{{b}\circ{a}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{b}\circ{a}_{V}}$match$\textstyle{R(\widetilde{V}^{{b}\circ{a}})}$$\textstyle{PV\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$ctype$\textstyle{R\left(\widetilde{\widetilde{V}^{a}}^{b}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R(\cong)}$$\textstyle{\widetilde{PV}^{a}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a_{V}}$$\textstyle{Q(\widetilde{V}^{a})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$ctype$\textstyle{\widetilde{Q(\widetilde{V}^{a})}^{b}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{b_{\widetilde{V}^{a}}}$

or, in Coq code,

⬇

Definition comp_rep_car : (forall c : ITYPE U,

RETYPE (fun t => f’ (f t)) (P c) —>

R ((RETYPE (fun t => f’ (f t))) c)) :=

fun (V : ITYPE U) t (y : retype (fun t => f’ (f t)) (P V) t) =>

match y with ctype _ z =>

lift (M:=R) (double_retype_1 (f:=f) (f’:=f’) (V:=V)) _

(b _ _ (ctype (fun t => f’ t)

(a _ _ (ctype (fun t => f t) z ))))

end.

where double_retype_1 denotes the isomorphism in the upper right corner. The
proof of the commutative diagrams for the composite monad morphism is lengthy
due to the number of arities of the signature of $\mathsf{PCF}$. Definition of
the identity morphisms is routine, and in the end we define the category of
representations of semantic $\mathsf{PCF}$:

⬇

Program Instance REP_s :

Cat_struct (obj := PCFPO_rep) (PCFPO_rep_Hom) := {

mor_oid P R := eq_Rep_oid P R ;

id R := Rep_id R ;

comp a b c f g := Rep_comp f g }.

###  4.4 One Particular Representation

We define a particular representation, which we later prove to be initial.
First of all, the set of object types of $\mathsf{PCF}$ is given as follows:

⬇

Inductive Sorts :=

| Nat : Sorts

| Bool : Sorts

| Arrow : Sorts -> Sorts -> Sorts.

For this section we introduce some notations:

⬇

Notation "’TY’" := PCF.Sorts.

Notation "’Bool’" := PCF.Bool.

Notation "’Nat’" := PCF.Nat.

Notation "’IT’" := (ITYPE TY).

Notation "a ’$\sim$>’ b" := (PCF.Arrow a b) (at level 69, right
associativity).

We specify the set of $\mathsf{PCF}$ constants through the following inductive
type, indexed by the sorts of $\mathsf{PCF}$:

⬇

Inductive Consts : TY -> Type :=

| Nats : nat -> Consts Nat

| ttt : Consts Bool

| fff : Consts Bool

| succ : Consts (Nat $\sim$> Nat)

| preds : Consts (Nat $\sim$> Nat)

| zero : Consts (Nat $\sim$> Bool)

| condN: Consts (Bool $\sim$> Nat $\sim$> Nat $\sim$> Nat)

| condB: Consts (Bool $\sim$> Bool $\sim$> Bool $\sim$> Bool).

The set family of terms of $\mathsf{PCF}$ is given by an inductive family,
parametrized by a context V and indexed by object types:

⬇

Inductive PCF (V: TY -> Type) : TY -> Type:=

| Bottom: forall t, PCF V t

| Const : forall t, Consts t -> PCF V t

| Var : forall t, V t -> PCF V t

| App : forall t s, PCF V (s $\sim$> t) -> PCF V s -> PCF V t

| Lam : forall t s, PCF (opt t V) s -> PCF V (t $\sim$> s)

| Rec : forall t, PCF V (t $\sim$> t) -> PCF V t.

Notation "a @ b" := (App a b)(at level 43, left associativity).

Notation "M ’" := (Const _ M) (at level 15).

Monadic substitution is defined recursively on terms:

⬇

Fixpoint subst (V W: TY -> Type)(f: forall t, V t -> PCF W t)

(t : TY)(v : PCF V t) : PCF W t :=

match v with

| Bottom t => Bottom W t

| c ’ => c ’

| Var t v => f t v

| u @ v => u >>= f @ v >>= f

| Lam t s u => Lam (u >>= shift f)

| Rec t u => Rec (u >>= f)

end

where "y >>= f" := (@subst _ _ f _ y).

Here shift f is the substitution map f extended to account for an extended
context under the binder Lam. It is equal to the shifted map of Def. 2.33.

Finally, we define a relation on the terms of type PCF via the inductive
definition

4.9 Code (Reduction Rules for $\mathsf{PCF}$):

⬇

Inductive eval (V : IT): forall t, relation (PCF V t) :=

| app_abs : forall (s t:TY) (M: PCF (opt s V) t) N,

eval (Lam M @ N) (M [*:= N])

| condN_t: forall n m, eval (condN ’ @ ttt ’ @ n @ m) n

| condN_f: forall n m, eval (condN ’ @ fff ’ @ n @ m) m

| condB_t: forall u v, eval (condB ’ @ ttt ’ @ u @ v) u

| condB_f: forall u v, eval (condB ’ @ fff ’ @ u @ v) v

| succ_red: forall n, eval (succ ’ @ Nats n ’) (Nats (S n) ’)

| zero_t: eval ( zero ’ @ Nats 0 ’) (ttt ’)

| zero_f: forall n, eval (zero ’ @ Nats (S n)’) (fff ’)

| pred_Succ: forall n, eval (preds ’ @ (succ ’ @ Nats n ’)) (Nats n ’)

| pred_z: eval (preds ’ @ Nats 0 ’) (Nats 0 ’)

| rec_a : forall t g, eval (Rec g) (g @ (Rec (t:=t) g)).

which we then propagate into subterms (cf. Sect. 4.4) and close with respect
to transitivity and reflexivity:

4.10 Code (Propagation of Reductions into Subterms):

⬇

Reserved Notation "x :> y" (at level 70).

Variable rel : forall (V:IT) t, relation (PCF V t).

Inductive propag (V: IT) : forall t, relation (PCF V t) :=

| relorig : forall t (v v’: PCF V t), rel v v’ -> v :> v’

| relApp1: forall s t (M M’ : PCF V (s $\sim$> t)) N, M :> M’ -> M @ N :> M’ @
N

| relApp2: forall s t (M : PCF V (s $\sim$> t)) N N’, N :> N’ -> M @ N :> M @
N’

| relLam: forall s t (M M’:PCF (opt s V) t), M :> M’ -> Lam M :> Lam M’

| relRec: forall t (M M’ : PCF V (t $\sim$> t)), M :> M’ -> Rec M :> Rec M’

where "x :> y" := (@propag _ _ x y).

The data thus defined constitutes a relative monad PCFEM on the functor
$\Delta^{T_{\mathsf{PCF}}}$ (IDelta TY). We omit the details.

Now we need to define a suitable morphism (resp. family of morphisms) of
PCFEM–modules for any arity (of higher degree). Let $\alpha$ be any such
arity, for instance the arity $\operatorname{App}$. We need to verify two
things:

  1. 1.

we show that the constructor of PCF which corresponds to $\alpha$ is monotone
with respect to the order on PCFEM. For instance, we show that for any two
terms r s:TY and any V : IDelta TY, the function

⬇

fun y => App (fst y) (snd y): PCFEM V (r$\sim$>s) x PCFEM V r -> PCFEM V s

is monotone.

  2. 2.

We show that the monadic substitution defined above distributes over the
constructor, i.e. we prove that the constructor is the carrier of a _module_
morphism.

All of these are very straightforward proofs, resulting in a representation
PCFE_rep of semantic $\mathsf{PCF}$:

⬇

Program Instance PCFE_rep_struct :

PCFPO_rep_struct PCFEM PCF.arrow PCF.Bool PCF.Nat := {

app r s := PCFApp r s;

abs r s := PCFAbs r s;

rec t := PCFRec t ;

tttt := PCFconsts ttt ;

ffff := PCFconsts fff;

Succ := PCFconsts succ;

Pred := PCFconsts preds;

CondN := PCFconsts condN;

CondB := PCFconsts condB;

Zero := PCFconsts zero ;

nats m := PCFconsts (Nats m);

bottom t := PCFbottom t }.

Definition PCFE_rep : PCFPO_rep := Build_PCFPO_rep PCFE_rep_struct.

Note that in the instance declaration PCFE_rep_struct, the Program framework
proves automatically the properties of Sect. 4.1, 4.1, 4.1 and 4.1.

###  4.5 Initiality

In this section we define a morphism of representations from PCFE_rep to any
representation R : PCFPO_rep. At first we need to define a map between the
underlying sorts, that is, a map Sorts PCFE_rep -> Sorts R. In short, each
$\mathsf{PCF}$ type goes to its representation in R:

⬇

Fixpoint Init_Sorts_map (t : Sorts PCFE_rep) : Sorts R :=

match t with

| PCF.Nat => Nat R

| PCF.Bool => Bool R

| u $\sim$> v => (Init_Sorts_map u) $\sim$$\sim$> (Init_Sorts_map v)

end.

The function init is the carrier of what will later be proved to be the
initial morphism to the representation R. It maps each constructor of
$\mathsf{PCF}$ recursively to its counterpart in the representation R:

⬇

Fixpoint init V t (v : PCF V t) :

R (retype (fun t0 => Init_Sorts_map t0) V) (Init_Sorts_map t) :=

match v with

| Var t v => rweta R _ _ (ctype _ v)

| u @ v => app _ _ _ (init u, init v)

| Lam _ _ v => abs _ _ _ (rlift R

(@der_comm TY (Sorts R) (fun t => Init_Sorts_map t) _ V ) _ (init v))

| Rec _ v => rec _ _ (init v)

| Bottom _ => bottom _ _ tt

| y ’ => match y in Consts t1 return

R (retype (fun t2 => Init_Sorts_map t2) V) (Init_Sorts_map t1) with

| Nats m => nats m _ tt

| succ => Succ _ tt

| condN => CondN _ tt

| condB => CondB _ tt

| zero => Zero _ tt

| ttt => tttt _ tt

| fff => ffff _ tt

| preds => Pred _ tt

end

end.

We write $i_{V}$ for init V and $g$ for Init_Sorts_map. Note that
$i_{V}:\mathsf{PCF}(V)\to g^{*}\left(R(\vec{g}V)\right)$ really is _the image
of the initial morphism under the adjunction $\varphi$_ of Def. 2.13.
Intuitively, passing from init V$=i_{V}$ to its adjunct $\varphi^{-1}(i_{V})$
is done by precomposing with pattern matching on the constructor ctype. We
informally denote $\varphi^{-1}(i_{V})$ by
${{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{init}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{V}}}}}}}\circ{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{match}}}}}}}$.

The map init is compatible with renaming and substitution in PCF and R,
respectively, in a sense made precise by the following two lemmas. The first
lemma states that, for any morphism $f:V\to W$ in
${\mathsf{Set}}^{T_{\mathsf{PCF}}}$, the following diagram commutes:

$\textstyle{\mathsf{PCF}(V)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$init
V$\scriptstyle{\mathsf{PCF}(f)}$$\textstyle{\mathsf{PCF}(W)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$init
W$\textstyle{g^{*}R(\vec{g}V)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g^{*}R(g^{*}f)}$$\textstyle{g^{*}R(\vec{g}W).}$

⬇

Lemma init_lift (V : IT) t (y : PCF V t) W (f : V —> W) :

init (y //- f) = rlift R (retype_map f) _ (init y).

The next commutative diagram concerns substitution; for any
$f:V\to\mathsf{PCF}(W)$, the diagram obtained by applying $\varphi$ to the
diagram given in Disp. (10) — i.e. the diagram corresponding to Disp. (11) —,
commutes:

$\textstyle{\mathsf{PCF}(V)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$init
V$\scriptstyle{\sigma^{\mathsf{PCF}}\left({f}\right)}$$\textstyle{\mathsf{PCF}(W)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$init
W$\textstyle{g^{*}R(\tilde{V})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$${\scriptstyle{g^{*}\sigma^{R}\left({{\varphi^{-1}(\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{init}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{W}}}}}})}\circ{(g^{*}f)}}\right)}$$\textstyle{g^{*}R(\tilde{W}).}$

In Coq the lemma init_subst proves commutativity of this latter diagram:

⬇

Lemma init_subst V t (y : PCF V t) W (f : IDelta _ V —> PCFE W):

init (y >>= f) =

rkleisli R (SM_ind (fun t v => match v with ctype t p => init (f t p) end))

_ (init y).

This latter lemma establishes almost the commutative diagram for the family
$\varphi^{-1}(i_{V})$ to constitute a (colax) _monad_ morphism, which reads as
follows:

$\textstyle{\vec{g}\left(\mathsf{PCF}(V)\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$${{\scriptstyle{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{init}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{V}}}}} }}\circ{\text{
\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{match}}}}}}}}$$\scriptstyle{\vec{g}\left(\sigma^{\mathsf{PCF}}\left({f}\right)\right)}$$\textstyle{\vec{g}\left({\mathsf{PCF}(W)}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$${{\scriptstyle{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{init}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{W}}}}} }}\circ{\text{
\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{match}}}}}}}}$$\textstyle{R(\vec{g}V)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$${{\scriptstyle{\sigma^{R}\left({{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{init}}}}}
}}\circ{{\text{
\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{match}}}}}
}}\circ{(\vec{g}f)}}}\right)}$$\textstyle{R(\vec{g}{W}).}$ ((13))

Before we can actually build a monad morphism with carrier map
${{{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{init}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{V}}}}}}}\circ{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{match}}}}}}}$,
we need to verify that init — and thus its adjunct — is monotone. We do this
in 3 steps, corresponding to the 3 steps in which we built up the preorder on
the terms of $\mathsf{PCF}$:

  1. 1.

init monotone with respect to the relation eval (cf. Sect. 4.4):

⬇

Lemma init_eval V t (v v’ : PCF V t) : eval v v’ -> init v <<< init v’.

  2. 2.

init monotone with respect to the propagation into subterms of eval;

⬇

Lemma init_eval_star V t (y z : PCF V t) : eval_star y z -> init y <<< init z.

  3. 3.

init monotone with respect to reflexive and transitive closure of above
relation.

⬇

Lemma init_mono c t (y z : PCFE c t) : y <<< z -> init y <<< init z.

We now have all the ingredients to define the initial morphism from
$\mathsf{PCF}$ to R. As already indicated by the diagram Disp. (13), its
carrier is not given by just the map init, since this map does not have the
right type: its domain is given, for any context
$V\in{\mathsf{Set}}^{T_{\mathsf{PCF}}}$, by $\mathsf{PCF}(V)$ and not, as
needed, by $\vec{g}\left(\mathsf{PCF}(V)\right)$. We thus precompose with
pattern matching in order to pass to its adjunct: for any context $V$, the
carrier of the initial morphism is given by

⬇

fun t y => match y with

| ctype _ p => init p

end

: retype _ (PCF V) —> R (retype _ W)

We recall that the constructor ctype is the carrier of the natural