Modular specification of monads through higher-order presentations

TL;DR

This paper introduces a modular framework for specifying monads with higher-order operations and equations, enabling structured language definitions like the lambda calculus, with formalization and effectiveness results.

Contribution

It develops a new approach to defining monads via higher-order signatures and equations, establishing modularity and effectiveness of such specifications.

Findings

Defines 2-signatures for monads with binding operations and equations.

Shows that effective 2-signatures have initial models representing specified monads.

Provides a computer formalization of the theoretical framework.

Abstract

In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of `models', and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair. In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating (`higher-order') operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to $\beta$- and $\eta$-equalities. Such a 2-signature is hence a pair $(\Sigma,E)$ of a binding signature $\Sigma$ and a family $E$ of equations for $\Sigma$. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. We associate, to each 2-signature $(\Sigma,E)$, a category of `models of $(\Sigma,E)$; and we say that a 2-signature is `effective' if this category has an initial object; the monad underlying this (essentially unique) object is the `monad specified by the 2-signature'. Not every 2-signature is effective; we identify a class of 2-signatures, which we call `algebraic', that are effective. Importantly, our 2-signatures together with their models enjoy `modularity': when we glue (algebraic) 2-signatures together, their initial models are glued accordingly. We provide a computer formalization for our main results.

Tables

Table 1. Table 1 : Examples of 1-signatures

Hypotheses	On objects	Name of the 1-signature
	$R\mapsto R$	$\Theta$
$\Sigma$ 1-signature, $F$ functor	$R\mapsto F\cdot \Sigma \left(R\right)$	$F\cdot \Sigma$
	$R\mapsto 1_R$	$1$
$\Sigma$, $\Psi$ 1-signatures	$R\mapsto \Sigma \left(R\right)\times \Psi \left(R\right)$	$\Sigma \times \Psi$
$\Sigma$, $\Psi$ 1-signatures	$R\mapsto \Sigma \left(R\right)+\Psi \left(R\right)$	$\Sigma +\Psi$
	$R\mapsto R^{\prime }$	${\Theta }^{\prime }$
$n\in \mathbb{N}$	$R\mapsto R^{\left(n\right)}$	${\Theta }^{\left(n\right)}$
$\left(a\right)=(a_1,\dots ,a_n)\in {\mathbb{N}}^n$	$R\mapsto R^{\left(a\right)}=R^{\left(a_1\right)}\times \dots \times R^{\left(a_n\right)}$	${\Theta }^{\left(a\right)}$ elementary signatures

Equations

$$T\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\rho \circ \rho R=\rho \circ M\mu ,\rho \circ M\eta =1_M.$$

$$\Sigma (R)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\mathsf{Mon}}^{\Sigma }\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${\Theta }^2\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$e_{\beta}:\vbox{\vbox{ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.65889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-7.65889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 11.1989pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{{\mathsf{abs}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 31.65889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 31.65889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 48.18279pt\raise 5.1875pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{{\mathsf{app}}_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 69.43669pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 69.43669pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}}$}}}}}}}{\hbox{\kern-7.65889pt\raise-16.38885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 33.79779pt\raise-21.64441pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.25555pt\hbox{$\scriptstyle{1}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 69.43669pt\raise-16.38885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 35.54779pt\raise-16.38885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 69.43669pt\raise-16.38885pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}}$}}}}}}}\ignorespaces}}}}\ignorespaces}}\qquad\text{and}\qquad e_{\eta}:\vbox{\vbox{ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-6.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 9.635pt\raise 5.1875pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{{\mathsf{app}}_{1}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 49.74669pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.43056pt\hbox{$\scriptstyle{{\mathsf{abs}}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 70.20668pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 70.20668pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}{\hbox{\kern-6.8889pt\raise-15.61108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 33.79779pt\raise-20.86664pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.25555pt\hbox{$\scriptstyle{1}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 70.20668pt\raise-15.61108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 35.54779pt\raise-15.61108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 70.20668pt\raise-15.61108pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}\ignorespaces}}}}\ignorespaces}}$$

$$2\mathsf{Mod}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$${{\rm Y}}_0\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$e_{1,\hat{\Sigma }/(f_i)},e_{2,\hat{\Sigma }/(f_i)}:U(\hat{\Sigma }/(f_i))⟶(\hat{\Sigma }/(f_i){)}^{(n)}$$

$$e_{1,\hat{\Sigma }/(f_i)}\circ U(p)=e_{2,\hat{\Sigma }/(f_i)}\circ U(p),$$

$${\Theta }^3\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 19.50137pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\crcr}}}\ignorespaces{\hbox{\kern-19.50137pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{(\Sigma_{1},E_{1})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 26.41109pt\raise 8.26387pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{f}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 43.50137pt\raise 2.15277pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 26.70642pt\raise-7.34026pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{g}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 43.50137pt\raise-2.15277pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 43.50137pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{(\Sigma_{2},E_{2})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 94.74315pt\raise 5.1875pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-0.8264pt\hbox{$\scriptstyle{p}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 106.50412pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 106.50412pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Xi=(\Sigma_{3},E_{2})}$}}}}}}}\ignorespaces}}}}\ignorespaces.$$

$${\Sigma }_1\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{aligned} \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-6.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 9.01007pt\raise 6.075pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.70833pt\hbox{$\scriptstyle{\eta_{T}\cdot\Theta}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{T\cdot\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 66.59145pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\tau}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 83.12148pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 83.12148pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}{\hbox{\kern-6.8889pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 40.25519pt\raise-20.08887pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.25555pt\hbox{$\scriptstyle{1}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 83.12148pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 42.00519pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 83.12148pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{aligned}\qquad\qquad\begin{aligned} \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 21.34367pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-21.34367pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{T\cdot T\cdot\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 23.09378pt\raise 6.075pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.70833pt\hbox{$\scriptstyle{\mu_{T}\cdot\Theta}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 45.34367pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 45.34367pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{T\cdot\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 81.04622pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\tau}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 97.57625pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 97.57625pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}{\hbox{\kern-21.34367pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{T\cdot T\cdot\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 26.28221pt\raise-20.22498pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.39166pt\hbox{$\scriptstyle{T{\tau}}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 45.34367pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 45.34367pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{T\cdot\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 81.04622pt\raise-19.34026pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\tau}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 97.57625pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 97.57625pt\raise-14.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{aligned}$$

$${\coprod }_{n\in \mathbb{N}}F(n)\times X^n\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$R^{\prime }$$

$$e_{\mathsf{fix}}:\vbox{\vbox{ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 7.65889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&\\&&\crcr}}}\ignorespaces{\hbox{\kern-7.65889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 14.01773pt\raise 8.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.5pt\hbox{$\scriptstyle{\langle 1,\tau\rangle}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 42.65889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 42.65889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}\times\Theta\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 88.2545pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\sigma}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 110.75444pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 110.75444pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}{\hbox{\kern-7.65889pt\raise-16.80553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern 54.29164pt\raise-21.31247pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.50694pt\hbox{$\scriptstyle{\tau}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 110.75444pt\raise-16.80553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 56.20667pt\raise-16.80553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 110.75444pt\raise-16.80553pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\Theta}$}}}}}}}\ignorespaces}}}}\ignorespaces}}$$

$$\mathsf{app}(t,\mathsf{app}(Y,t))=\mathsf{app}(Y,t).$$

Full text

Modular specification of monads through higher-order presentations

Benedikt Ahrens

  

André Hirschowitz

  

Ambroise Lafont

  

Marco Maggesi

In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating (‘higher-order’) operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to $\beta$- and $\eta$-equalities. Such a 2-signature is hence a pair ($\Sigma$,E) of a binding signature $\Sigma$ and a family $E$ of equations for $\Sigma$. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context.

We associate, to each 2-signature $(\Sigma,E)$, a category of ?models of $(\Sigma,E)$?; and we say that a 2-signature is ?effective? if this category has an initial object; the monad underlying this (essentially unique) object is the ?monad specified by the 2-signature?. Not every 2-signature is effective; we identify a class of 2-signatures, which we call ?algebraic?, that are effective.

Importantly, our 2-signatures together with their models enjoy ?modularity?: when we glue (algebraic) 2-signatures together, their initial models are glued accordingly.

We provide a computer formalization for our main results.

1 Introduction

The present work is devoted to the study of presentations of monads on the category of sets. More precisely, there is a well established theory of presentations of monads through generating (first-order) operations equipped with relations among the corresponding derived operations. Here we propose a counterpart of this theory, where we consider generation of monads by binding operations. Various algebraic structures generated by binding operations have been considered by many, going back at least to Fiore, Plotkin, and Turi [4], Gabbay and Pitts [5], and Hofmann [8]. Every such operation has a binding arity, which is a sequence of non-negative integers. For example, the binding arity of the application operation of the lambda calculus is $(0,0)$: it takes two arguments without binding any variable in them, while the abstraction operation on the monad of the lambda calculus has binding arity $(1)$, as it binds one variable in its single argument. For each family $\Sigma$ of binding arities, there is a generated ?free? monad $\hat{\Sigma}$ on ${\mathsf{Set}}$ which maps a set of free variables $X$ to the set of terms $\hat{\Sigma}(X)$ taking variables in $X$.

If $p:\hat{\Sigma}\to R$ is a monad epimorphism, we understand that $R$ is generated by a family of operations whose binding arities are given by $\Sigma$, subject to suitable identifications. In particular, for $\Sigma:=((0,0),(1))$, $\hat{\Sigma}$ may be understood as the monad ${\mathsf{LC}}$ of syntactic terms of the lambda calculus, and we have an obvious epimorphism $p:\hat{\Sigma}\to{\mathsf{LC}}_{\beta\eta}$, where ${\mathsf{LC}}_{\beta\eta}$ is the monad of lambda-terms modulo $\beta$ and $\eta$. In order to manage such equalities, the approach in the first-order case suggests to identify $p$ as the coequalizer of a double arrow from $T$ to $\hat{\Sigma}$ where $T$ is again a ?free? monad. Let us see what comes out when we attempt to find such an encoding for the $\beta$-equality of the monad ${\mathsf{LC}}_{\beta\eta}$. It should say that for each set $X$, the following two maps from $\hat{\Sigma}(X+\{*\})\times\hat{\Sigma}(X)$ to $\hat{\Sigma}(X)$,

• •

$(t,u)\mapsto{\mathsf{app}}({\mathsf{abs}}(t),u)$

• •

$(t,u)\mapsto t[*\mapsto u]$

are equal. Here a problem occurs, namely that the above collections of maps, which can be understood as a morphism of functors, cannot be understood as a morphism of monads. Notably, they do not send variables to variables.

On the other hand, we observe that the members of our equations, which are not morphisms of monads, commute with substitution, and hence are more than morphisms of functors: indeed they are morphisms of modules over $\hat{\Sigma}$. (In Section 2, we recall briefly what modules over a monad are.) Accordingly, a (second-order) presentation for a monad $R$ could be a diagram

[TABLE]

where $\Sigma$ is a binding signature, $\hat{\Sigma}$ is the associated free monad, $T$ is a module over $\hat{\Sigma}$, $f$ is a pair of morphisms of modules over $\hat{\Sigma}$, and $p$ is a monad epimorphism. And now we are faced with the task of finding a condition meaning something like ?$p$ is the coequalizer of $f$**?**111This cannot be the case stricto sensu since $f$ is a pair of morphisms of modules while $p$ is a morphism of monads..

To this end, we introduce the category $\mathsf{Mon}^{\Sigma}$ ?of models of $\Sigma$?, whose objects are monads ?equipped with an action of $\Sigma$?. Of course $\hat{\Sigma}$ is equipped with such an action which turns it into the initial object. Next, we define the full subcategory of models satisfying the equation $f$, and require $R$ to be the initial object therein. Our definition is suited for the case where the equation $f$ is parametric in the model: this means that now $T$ and $f$ are functions of the model $S$, and $f(S)=(u(S),v(S))$ is a pair of $S$-module morphisms from $T(S)$ to $S$. We say that $S$ satisfies the equation $f$ if $u(S)=v(S)$. Generalizing the case of one equation to the case of a family of equations yields the notion of 2-signature already introduced by Ahrens [1] in a slightly different context.

Now we are ready to formulate our main problem: given a 2-signature $(\Sigma,E)$, where $E$ is a family of parametric equations as above, does the subcategory of models of $\Sigma$ satisfying the family of equations $E$ admit an initial object?

We answer positively for a large subclass of 2-signatures which we call algebraic 2-signatures (see Theorem 4.30).

This provides a construction of a monad from an algebraic 2-signature, and we prove furthermore (see Theorem 4.25) that this construction is modular, in the sense that merging two extensions of 2-signatures corresponds to building an amalgamated sum of initial models. This is analogous to our previous result for 1-signatures shown in [2, Thm. 32].

As expected, our initiality property generates a recursion principle which is a recipe allowing us to specify a morphism from the presented monad to any given other monad.

We give various examples of monads arising ?in nature? that can be specified via an algebraic 2-signature (see Section 6), and we also show through a simple example how our recursion principle applies (see Section 7).

Computer-checked formalization

This work is accompanied by a computer-checked formalization of the main results, based on the formalization of a previous work [2]. We work over the UniMath library [13], which is implemented in the proof assistant Coq [11]. The formalization consists of about 9,500 lines of code, and can be consulted on https://github.com/UniMath/largecatmodules. A guide is given in the README, and a summary of our formalization is available at https://initialsemantics.github.io/doc/1539d1c/Modules.SoftEquations.Summary.html.

For the purpose of this article, we refer to a fixed version of our library, with the short hash 1539d1c. This version compiles with version b168417 of UniMath.

Throughout the article, statements are accompanied by their corresponding identifiers in the formalization. These identifiers are also hyperlinks to the online documentation stored at https://initialsemantics.github.io/doc/1539d1c/index.html.

Related work

The present work follows a previous work of ours [2] where we study a slightly different kind of presentation of monads. Specifically, in [2], we treat a class of 1-signatures which can be understood as quotients of algebraic 1-signatures. This should amount to considering a specific kind of equations, as suggested in Section 6.2, where we recover, in the current setting, all the examples given there.

In [2], we discussed related work on the general topic of monads and syntax. Let us focus here on related work on presentations of languages (or monads).

In an abstract setting, [9] explains how any finitary monad can be presented as a coequalizer of free monads. There, free monads correspond to our initial models of an algebraic 1-signature without any binding construction.

In [3], the authors introduce a notion of equation based on syntax with meta-variables: essentially, a specific syntax, say, $T:=T(M,X)$ considered there depends on two contexts: a meta-context $M$, and an object-context $X$. The terms of the actual syntax are then those terms $t\in T(\emptyset,X)$ in an empty meta-context. An equation for $T$ is, simply speaking, a pair of terms in the same pair of contexts. Transferring an equation to any model of the underlying algebraic 1-signature is done by induction on the syntax with meta-variables. The authors show a monadicity theorem which straightforwardly implies an initiality result very similar to ours.

As said before, Ahrens [1] introduces the notion of 2-signature which we consider here, in the slightly different context of (relative) monads on preordered sets, where the preorder models the reduction relation. In some sense, our result tackles the technical issue of quotienting the initial (relative) monad constructed in [1] by the preorder.

2 Categories of modules over monads

In this section, we recall the notions of monad and module over a monad, as well as some constructions of modules. We restrict our attention to the category ${\mathsf{Set}}$ of sets, although most definitions are straightforwardly generalizable. See [7] for a more extensive introduction.

A monad (over ${\mathsf{Set}}$) is a triple $R=(R,\mu,\eta)$ given by a functor $R\colon{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, and two natural transformations $\mu\colon R\cdot R\longrightarrow R$ and $\eta\colon I\longrightarrow R$ such that the well-known monadic laws hold. A monad morphism to another such monad $(R^{\prime},\mu^{\prime},\eta^{\prime})$ is a natural transformation $f:R\to R^{\prime}$ that commutes with the monadic structure. The category of monads is denoted by $\mathsf{Mon}$.

Let $R$ be a monad. A (left) $R$-module222The analogous notion of right $R$-module is not used in this work, we hence simply write ?$R$-module?** instead of ?left $R$-module? for brevity.** is given by a functor $M\colon{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ equipped with a natural transformation $\rho\colon M\cdot R\longrightarrow M$, called module substitution, which is compatible with the monad composition and identity:

[TABLE]

Let $f\colon R\longrightarrow S$ be a morphism of monads and $M$ an $S$-module. The module substitution $M\cdot R\stackrel{{\scriptstyle Mf}}{{\longrightarrow}}M\cdot S\stackrel{{\scriptstyle\rho}}{{\longrightarrow}}M$ turns $M$ into an $R$-module $f^{*}\!M$, called pullback of $M$ along $f$.

A natural transformation of $R$-modules $\varphi\colon M\longrightarrow N$ is linear if it is compatible with module substitution on either side, that is, if $\varphi\circ\rho^{M}=\rho^{N}\circ\varphi R$. Modules over $R$ and their morphisms form a category denoted $\mathsf{Mod}(R)$, which is complete and cocomplete: limits and colimits are computed pointwise.

We define the total module category $\int_{R}\mathsf{Mod}(R)$ as follows: its objects are pairs $(R,M)$ of a monad $R$ and an $R$-module $M$. A morphism from $(R,M)$ to $(S,N)$ is a pair $(f,m)$ where $f\colon R\longrightarrow S$ is a morphism of monads, and $m\colon M\longrightarrow f^{*}N$ is a morphism of $R$-modules. The category $\int_{R}\mathsf{Mod}(R)$ comes equipped with a forgetful functor to the category of monads, given by the projection $(R,M)\mapsto R$. This functor is a Grothendieck fibration with fibers $\mathsf{Mod}(R)$ over $R$. In particular, any monad morphism $f:R\longrightarrow S$ gives rise to a functor $f^{*}\colon\mathsf{Mod}(S)\longrightarrow\mathsf{Mod}(R)$ which preserves limits and colimits.

We give some important examples of modules:

Example 2.1**.**

Every monad $R$ is a module over itself, which we call the tautological module. 2. 2.

For any functor $F\colon{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ and any $R$-module $M\colon{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$, the composition $F\cdot M$ is an $R$-module (in the evident way). 3. 3.

For every set $W$ we denote by $\underline{W}\colon{\mathsf{Set}}\longrightarrow{\mathsf{Set}}$ the constant functor $\underline{W}:=X\mapsto W$. Then $\underline{W}$ is trivially an $R$-module since $\underline{W}=\underline{W}\cdot R$. 4. 4.

Given an $R$-module $M$, the $R$-module $M^{\prime}$ is defined, on objects, as $M^{\prime}(X):=M(X+\{*\})$, and the obvious module substitution. Derivation yields an endofunctor on $\mathsf{Mod}(R)$ that is right adjoint to the functor $M\mapsto M\times R$, ?product with the tautological module?. Details are given, e.g., in [2, Sec. 2.3]. 5. 5.

Derivation can be iterated. Given a list of non negative integers $(a)=(a_{1},\dots,a_{n})$ and a left module $M$ over a monad $R$, we denote by $M^{(a)}=M^{(a_{1},\dots,a_{n})}$ the module $M^{(a_{1})}\times\cdots\times M^{(a_{n})}$, with $M^{()}=1$ the final module.

3 1-signatures and their models

In this section, we review the notion of 1-signature studied in detail in [2] — there only called ?signature?.

A 1-signature is a section of the forgetful functor from the category $\int_{R}\mathsf{Mod}(R)$ to the category $\mathsf{Mon}$. A morphism between two 1-signatures $\Sigma_{1},\Sigma_{2}\colon\mathsf{Mon}\longrightarrow\int_{R}\mathsf{Mod}(R)$ is a natural transformation $m\colon\Sigma_{1}\longrightarrow\Sigma_{2}$ which, post-composed with the projection $\int_{R}\mathsf{Mod}(R)\longrightarrow\mathsf{Mon}$, is the identity. The category of 1-signatures is denoted by $\text{1-}\mathsf{Sig}$.

Limits and colimits of 1-signatures can be easily constructed pointwise: the category of 1-signatures is complete and cocomplete.

Table 1 lists important examples of 1-signatures.

An algebraic 1-signature is a (possibly infinite) coproduct of elementary signatures (defined in Table 1). For instance, the algebraic 1-signature of the lambda calculus is $\Sigma_{\mathsf{LC}}=\Theta^{2}+\Theta^{\prime}$.

Given a monad $R$ over ${\mathsf{Set}}$, we define an action of the 1-signature $\Sigma$ in $R$ to be a module morphism from $\Sigma(R)$ to $R$. For example, the application ${\mathsf{app}}\colon{\mathsf{LC}}^{2}\longrightarrow{\mathsf{LC}}$ is an action of the elementary 1-signature $\Theta^{2}$ into the monad ${\mathsf{LC}}$ of syntactic lambda calculus. The abstraction ${\mathsf{abs}}\colon{\mathsf{LC}}^{\prime}\longrightarrow{\mathsf{LC}}$ is an action of the elementary 1-signature $\Theta^{\prime}$ into the monad ${\mathsf{LC}}$. Then $[{\mathsf{app}},{\mathsf{abs}}]:{\mathsf{LC}}^{2}+{\mathsf{LC}}^{\prime}\longrightarrow{\mathsf{LC}}$ is an action of the algebraic 1-signature of the lambda-calculus $\Theta^{2}+\Theta^{\prime}$ into the monad ${\mathsf{LC}}$.

Given a 1-signature $\Sigma$, we build the category $\mathsf{Mon}^{\Sigma}$ of models of $\Sigma$ as follows. Its objects are pairs $(R,r)$ of a monad $R$ equipped with an action $r:\Sigma(R)\to R$ of $\Sigma$. A morphism from $(R,r)$ to $(S,s)$ is a morphism of monads $m:R\to S$ making the following diagram of $R$-modules commutes:

[TABLE]

Let $f\colon\Sigma\longrightarrow\Psi$ be a morphism of 1-signatures and $\mathcal{R}=(R,r)$ a model of $\Psi$. The linear morphism $\Sigma(R)\stackrel{{\scriptstyle f(R)}}{{\longrightarrow}}\Psi(R)\stackrel{{\scriptstyle r}}{{\longrightarrow}}R$ defines an action of $\Sigma$ in $R$. The induced model of $\Sigma$ is called pullback of $\mathcal{R}$ along $f$ and noted $f^{*}\!\mathcal{R}$.

The total category $\int_{\Sigma}\mathsf{Mon}^{\Sigma}$ of models is defined as follows:

• •

An object of $\int_{\Sigma}\mathsf{Mon}^{\Sigma}$ is a triple $(\Sigma,R,r)$ where $\Sigma$ is a 1-signature, $R$ is a monad, and $r$ is an action of $\Sigma$ in $R$.

• •

A morphism in $\int_{\Sigma}\mathsf{Mon}^{\Sigma}$ from $(\Sigma_{1},R_{1},r_{1})$ to $(\Sigma_{2},R_{2},r_{2})$ consists of a pair $(i,m)$ of a 1-signature morphism $i:\Sigma_{1}\longrightarrow\Sigma_{2}$ and a morphism $m$ of $\Sigma_{1}$-models from $(R_{1},r_{1})$ to $(R_{2},i^{*}(r_{2}))$.

The forgetful functor $\int_{\Sigma}\mathsf{Mon}^{\Sigma}\to\mathsf{Sig}$ is a Grothendieck fibration.

Given a 1-signature $\Sigma$, the initial object in $\mathsf{Mon}^{\Sigma}$, if it exists, is denoted by $\hat{\Sigma}$. In this case, the 1-signature $\Sigma$ is said effective333In our previous work [2], we call representable any 1-signature $\Sigma$ that has an initial model, called a representation of $\Sigma$, or syntax generated by $\Sigma$..

Theorem 3.1** ([6, Theorems 1 and 2]).**

Algebraic 1-signatures are effective.

4 2-Signatures and their models

In this section we study 2-signatures and models of 2-signatures. A 2-signature is a pair of a 1-signature and a family of equations over it.

4.1 Equations

Our equations are those of Ahrens [1], namely they are parallel module morphisms parametrized by the models of the underlying 1-signature. The underlying notion of 1-model is essentially the same as in [1], even if, there, such equations are interpreted instead as inequalities.

Throughout this subsection, we fix a 1-signature $\Sigma$, that we instantiate in the examples.

Definition 4.1**.**

We define a $\Sigma$-module to be a functor $T$ from the category of models of $\Sigma$ to the category $\int_{R}\mathsf{Mod}(R)$ commuting with the forgetful functors to the category $\mathsf{Mon}$ of monads,

[TABLE]

Example 4.2**.**

To each 1-signature $\Psi$ is associated, by precomposition with the projection from $\mathsf{Mon}^{\Sigma}$ to $\mathsf{Mon}$, a $\Sigma$-module still denoted $\Psi$. All the $\Sigma$-modules occurring in this work arise in this way from 1-signatures; in other words, they do not depend on the action of the 1-model. In particular, we have the tautological $\Sigma$-module $\Theta$, and, more generally, for any natural number $n\in{\mathbb{N}}$, a $\Sigma$-module $\Theta^{(n)}$. Also we have another fundamental $\Sigma$-module (arising in this way from) $\Sigma$ itself.

Definition 4.3**.**

Let $S$ and $T$ be $\Sigma$-modules. We define a morphism of $\Sigma$-modules from $S$ to $T$ to be a natural transformation from $S$ to $T$ which becomes the identity when postcomposed with the forgetful functor from the category of models of $\Sigma$ to the category of monads.

Example 4.4**.**

Each 1-signature morphism $\Psi\to\Phi$ upgrades into a morphism of $\Sigma$-modules. Further in that vein, there is a morphism of $\Sigma$-modules $\tau^{\Sigma}:\Sigma\to\Theta$. It is given, on a model $(R,m)$ of $\Sigma$, by $m:\Sigma(R)\to R$. (Note that it does not arise from a morphism of 1-signatures.) When the context is clear, we write simply $\tau$ for this morphism, and call it the tautological morphism of $\Sigma$-modules.

Proposition 4.5**.**

Our $\Sigma$-modules and their morphisms, with the obvious composition and identity, form a category.

Definition 4.6**.**

We define a $\Sigma$-equation to be a pair of parallel morphisms of $\Sigma$-modules. We also write $e_{1}=e_{2}$ for the $\Sigma$-equation $e=(e_{1},e_{2})$.

Example 4.7** (Commutativity of a binary operation).**

Here we instantiate our fixed 1-signature as follows: $\Sigma:=\Theta\times\Theta$. In this case, we say that $\tau$ is the (tautological) binary operation. Now we can formulate the usual law of commutativity for this binary operation.

We consider the morphism of 1-signatures ${\mathsf{swap}}:\Theta^{2}\longrightarrow\Theta^{2}$ that exchanges the two components of the direct product. Again by Example 4.4, we have an induced morphism of $\Sigma$-modules, still denoted ${\mathsf{swap}}$.

Then, the $\Sigma$-equation for commutativity is given by the two morphisms of $\Sigma$-modules

[TABLE]

See also Section 6.1 where we explain in detail the case of monoids.

For the example of the lambda calculus with $\beta$- and $\eta$-equality (given in Example 4.9), we need to introduce currying:

Definition 4.8**.**

By abstracting over the base monad $R$ the adjunction in the category of $R$-modules of Example 2.1, item 4, we can perform currying of morphisms of 1-signatures: given a morphism of signatures $\Sigma_{1}\times\Theta\to\Sigma_{2}$ it produces a new morphism $\Sigma_{1}\to\Sigma_{2}^{\prime}$. By Example 4.2, currying acts also on morphisms of $\Sigma$-modules.

Conversely, given a morphism of 1-signatures (resp. $\Sigma$-modules) $\Sigma_{1}\to\Sigma_{2}^{\prime}$, we can define the uncurryied map $\Sigma_{1}\times\Theta\to\Sigma_{2}$.

Example 4.9** ($\beta$- and $\eta$-conversions).**

Here we instantiate our fixed 1-signature as follows: $\Sigma_{\mathsf{LC}}:=\Theta\times\Theta+\Theta^{\prime}$. This is the 1-signature of the lambda calculus. We break the tautological $\Sigma$-module morphism into its two pieces, namely ${\mathsf{app}}:=\tau\circ\mathsf{inl}:\Theta\times\Theta\longrightarrow\Theta$ and ${\mathsf{abs}}:=\tau\circ\mathsf{inr}:\Theta^{\prime}\longrightarrow\Theta$. Applying currying to ${\mathsf{app}}$ yields the morphism ${\mathsf{app}}_{1}:\Theta\longrightarrow\Theta^{\prime}$ of $\Sigma_{\mathsf{LC}}$-modules. The usual $\beta$ and $\eta$ relations are implemented in our formalism by two $\Sigma_{\mathsf{LC}}$-equations that we call $e_{\beta}$ and $e_{\eta}$ respectively:

[TABLE]

4.2 2-signatures and their models

Definition 4.10**.**

A 2-signature is a pair $(\Sigma,E)$ of a 1-signature $\Sigma$ and a family $E$ of $\Sigma$-equations.

Example 4.11**.**

The 2-signature for a commutative binary operation is $(\Theta^{2},\tau\circ{\mathsf{swap}}=\tau)$ (cf. Example 4.7).

Example 4.12**.**

The 2-signature of the lambda calculus modulo $\beta$- and $\eta$-equality is $\Upsilon_{{\mathsf{LC}}_{\beta\eta}}=(\Theta\times\Theta+\Theta^{\prime},\{e_{\beta},e_{\eta}\})$, where $e_{\beta},e_{\eta}$ are the $\Sigma_{\mathsf{LC}}$-equations defined in Example 4.9.

Definition 4.13** ().**

We say that a model $M$ of $\Sigma$ satisfies the $\Sigma$-equation $e=(e_{1},e_{2}$) if $e_{1}(M)=e_{2}(M)$. If $E$ is a family of $\Sigma$-equations, we say that a model $M$ of $\Sigma$ satisfies $E$ if $M$ satisfies each $\Sigma$-equation in $E$.

Definition 4.14**.**

Given a monad $R$ and a 2-signature $\Upsilon=(\Sigma,E)$, an action of $\Upsilon$ in $R$ is an action of $\Sigma$ in $R$ such that the induced 1-model satisfies all the equations in $E$.

Definition 4.15** ().**

For a 2-signature $(\Sigma,E)$, we define the category $\mathsf{Mon}^{(\Sigma,E)}$ of models of $(\Sigma,E)$ to be the full subcategory of the category of models of $\Sigma$ whose objects are models of $\Sigma$ satisfying $E$, or equivalently, monads equipped with an action of $(\Sigma,E)$.

Example 4.16**.**

A model of the 2-signature $\Upsilon_{{\mathsf{LC}}_{\beta\eta}}=(\Theta\times\Theta+\Theta^{\prime},\{e_{\beta},e_{\eta}\})$ is given by a model $(R,{\mathsf{app}}^{R}:R\times R\to R,{\mathsf{abs}}^{R}:R^{\prime}\to R)$ of the 1-signature $\Sigma_{\mathsf{LC}}$ such that ${\mathsf{app}}^{R}_{1}\cdot{\mathsf{abs}}^{R}=1_{R^{\prime}}$ and ${\mathsf{abs}}^{R}\cdot{\mathsf{app}}^{R}_{1}=1_{R}$ (see Example 4.9).

Definition 4.17**.**

A 2-signature $(\Sigma,E)$ is said to be effective if its category of models $\mathsf{Mon}^{(\Sigma,E)}$ has an initial object, denoted $\widehat{(\Sigma,E)}$.

In Section 4.4, we aim to find sufficient conditions for a 2-signature $(\Sigma,E)$ to be effective.

4.3 Modularity for 2-signatures

In this section, we define the category $2\mathsf{Sig}$ of 2-signatures and the category $2\mathsf{Mod}$ of models of 2-signatures, together with functors that relate them with the categories of 1-signatures and 1-models. The situation is summarized in the commutative diagram of functors

[TABLE]

where

• •

$2\pi$ is a Grothendieck fibration;

• •

$\pi$ is the Grothendieck fibration defined in [2, Section 5.2];

• •

$U_{\mathsf{Sig}}$ is a coreflection and preserves colimits; and

• •

$U_{\mathsf{Mod}}$ is a coreflection.

As a simple consequence of this data, we obtain a modularity result in Theorem 4.25: it explains how the initial model of an amalgamated sum of 2-signatures is the amalgamation of the initial model of the summands.

We start by defining the category $2\mathsf{Sig}$ of 2-signatures:

Definition 4.18** ().**

Given 2-signatures $(\Sigma_{1},E_{1})$ and $(\Sigma_{2},E_{2})$, a morphism of 2-signatures from $(\Sigma_{1},E_{1})$ to $(\Sigma_{2},E_{2})$ is a morphism of 1-signatures $m:\Sigma_{1}\to\Sigma_{2}$ such that for any model $M$ of $\Sigma_{2}$ satisfying $E_{2}$, the $\Sigma_{1}$-model $m^{*}M$ satisfies $E_{1}$.

These morphisms, together with composition and identity inherited from 1-signatures, form the category $2\mathsf{Sig}$.

We now study the existence of colimits in $2\mathsf{Sig}$. We know that $\mathsf{Sig}$ is cocomplete, and we use this knowledge in our study of $2\mathsf{Sig}$, by relating the two categories:

Let $F_{\mathsf{Sig}}:\mathsf{Sig}\to 2\mathsf{Sig}$ be the functor which associates to any 1-signature $\Sigma$ the empty family of equations, $F_{\mathsf{Sig}}(\Sigma):=(\Sigma,\emptyset)$. Call $U_{\mathsf{Sig}}:2\mathsf{Sig}\to\mathsf{Sig}$ the forgetful functor defined on objects as $U(\Sigma,E):=\Sigma$.

Lemma 4.19** (, ).**

The forgetful functor $U_{\mathsf{Sig}}$ is a coreflection and is right adjoint to $F_{\mathsf{Sig}}$.

We are interested in specifying new languages by ?gluing together? simpler ones. On the level of 2-signatures, this is done by taking the coproduct, or, more generally, the pushout of 2-signatures:

Theorem 4.20** ().**

The category $2\mathsf{Sig}$ has pushouts.

Coproducts are computed by taking the union of the equations and the coproducts of the underlying 1-signatures. Coequalizers are computed by keeping the equations of the codomain and taking the coequalizer of the underlying 1-signatures. Thus, by decomposing any colimit into coequalizers and coproducts, we have this more general result:

Proposition 4.21**.**

The category $2\mathsf{Sig}$ is cocomplete and $U_{\mathsf{Sig}}$ preserves colimits.

We now turn to our modularity result, which states that the initial model of a coproduct of two 2-signatures is the coproduct of the initial models of each 2-signature. More generally, the two languages can be amalgamated along a common ?core language?, by considering a pushout rather than a coproduct.

For a precise statement of that result, we define a ?total category of models of 2-signatures?:

Definition 4.22**.**

The category $\int_{(\Sigma,E)}\mathsf{Mon}^{(\Sigma,E)}$, or $2\mathsf{Mod}$ for short, has, as objects, pairs $((\Sigma,E),M)$ of a 2-signature $(\Sigma,E)$ and a model $M$ of $(\Sigma,E)$.

A morphism from $((\Sigma_{1},E_{1}),M_{1})$ to $((\Sigma_{2},E_{2}),M_{2})$ is a pair $(m,f)$ consisting of a morphism $m:(\Sigma_{1},E_{1})\to(\Sigma_{2},E_{2})$ of 2-signatures and a morphism $f:M_{1}\to m^{*}M_{2}$ of $(\Sigma_{1},E_{1})$-models (or, equivalently, of $\Sigma_{1}$-models).

This category of models of 2-signatures contains the models of 1-signatures as a coreflective subcategory. Let $F_{\mathsf{Mod}}:\mathsf{Mod}\to 2\mathsf{Mod}$ be the functor which associates to any 1-model $(\Sigma,M)$ the empty family of equations, $F_{\mathsf{Mod}}(\Sigma,M):=(F_{\mathsf{Sig}}(\Sigma),M)$. Conversely, the forgetful functor $U_{\mathsf{Mod}}:2\mathsf{Mod}\to\mathsf{Mod}$ maps $((\Sigma,E),M)$ to $(\Sigma,M)$.

Lemma 4.23** (, ).**

We have $F_{\mathsf{Mod}}\dashv U_{\mathsf{Mod}}$. Furthermore, $U_{\mathsf{Mod}}$ is a coreflection.

The modularity result is a consequence of the following technical result:

Proposition 4.24** ().**

The forgetful functor $2\pi:2\mathsf{Mod}\to 2\mathsf{Sig}$ is a Grothendieck fibration.

The modularity result below is analogous to the modularity result for 1-signatures [2, Thm. 32]:

Theorem 4.25** **(Modularity for 2-signatures,

).

Suppose we have a pushout diagram of effective 2-signatures, as on the left below. This pushout gives rise to a commutative square of morphisms of models in $2\mathsf{Mod}$ as on the right below, where we only write the second components, omitting the (morphisms of) signatures. This square is a pushout square.

[TABLE]

Intuitively, the 2-signatures $\Upsilon_{1}$ and $\Upsilon_{2}$ specify two extensions of the 2-signature $\Upsilon_{0}$, and $\Upsilon$ is the smallest extension containing both these extensions. By Theorem 4.25 the initial model of $\Upsilon$ is the ?smallest model containing both the languages generated by $\Upsilon_{1}$ and $\Upsilon_{2}$?.

4.4 Initial Semantics for 2-Signatures

We now turn to the problem of constructing the initial model of a 2-signature $(\Sigma,E)$. More specifically, we identify sufficient conditions for $(\Sigma,E)$ to admit an initial object $\widehat{(\Sigma,E)}$ in the category of models. Our approach is very straightforward: we seek to construct $\widehat{(\Sigma,E)}$ by applying a suitable quotient construction to the initial object $\hat{\Sigma}$ of $\mathsf{Mon}^{\Sigma}$.

This leads immediately to our first requirement on $(\Sigma,E)$, which is that $\Sigma$ must be an effective 1-signature. (For instance, we can assume that $\Sigma$ is an algebraic 1-signature, see Theorem 3.1.) This is a very natural hypothesis, since in the case where $E$ is the empty family of $\Sigma$-equations, it is obviously a necessary and sufficient condition.

Some $\Sigma$-equations are never satisfied. In that case, the category $\mathsf{Mon}^{(\Sigma,E)}$ is empty. For example, given any 1-signature $\Sigma$, consider the $\Sigma$-equation $\mathsf{inl},\mathsf{inr}:\Theta\rightrightarrows\Theta+\Theta$ given by the left and right inclusion. This is obviously an unsatisfiable $\Sigma$-equation. We have to find suitable hypotheses to rule out such unsatisfiable $\Sigma$-equations. This motivates the notion of elementary equations.

Definition 4.26**.**

Given a 1-signature $\Sigma$, a $\Sigma$-module $S$ is nice if $S$ sends pointwise epimorphic $\Sigma$-model morphisms to pointwise epimorphic module morphisms.

Definition 4.27** ().**

Given a 1-signature $\Sigma$, an elementary $\Sigma$-equation is a $\Sigma$-equation such that

• •

the target is a finite derivative of the tautological 2-signature $\Theta$, i.e., of the form $\Theta^{(n)}$ for some $n\in{\mathbb{N}}$, and

• •

the source is a nice $\Sigma$-module.

Example 4.28**.**

Any algebraic 1-signature is nice [2, Example 43]. Thus, any $\Sigma$-equation between an algebraic 1-signature and $\Theta^{(n)}$, for some natural number $n$, is elementary.

Definition 4.29**.**

A 2-signature $(\Sigma,E)$ is said algebraic if $\Sigma$ is algebraic and $E$ is a family of elementary equations.

Theorem 4.30** ().**

Any algebraic 2-signature has an initial model.

The proof of Theorem 4.30 is given in Section 5.

Example 4.31**.**

The 2-signature of lambda calculus modulo $\beta$ and $\eta$ equations given in Example 4.12 is algebraic. Its initial model is precisely the monad ${\mathsf{LC}}_{\beta\eta}$ of lambda calculus modulo $\beta\eta$ equations.

The instantiation of the formalized Theorem 4.30 to this 2-signature is done in 444An initiality result for this particular case was also previously discussed and proved formally in the Coq proof assistant in [7]..

Let us mention finally that, using the axiom of choice, we can take a similar quotient on all the 1-models of $\Sigma$:

Proposition 4.32** **(,

).

Here we assume the axiom of choice. The forgetful functor from the category $\mathsf{Mon}^{(\Sigma,E)}$ of 2-models of $(\Sigma,E)$ to the category $\mathsf{Mon}^{\Sigma}$ of $\Sigma$-models has a left adjoint. Moreover, the left adjoint is a reflector.

5 Proof of Theorem 4.30

Our main technical result on effectiveness is the following Lemma 5.1. In Theorem 4.30, we give a much simpler criterion that encompasses all the examples we give.

Lemma 5.1** ().**

Let $(\Sigma,E)$ be a 2-signature such that:

$\Sigma$ sends epimorphic natural transformations to epimorphic natural transformations, 2. 2.

$E$ is a family of elementary equations, 3. 3.

the initial 1-model of $\Sigma$ exists, 4. 4.

the initial 1-model of $\Sigma$ preserves epimorphisms, 5. 5.

the image by $\Sigma$ of the initial 1-model of $\Sigma$ preserves epimorphisms.

Then, the category of 2-models of $(\Sigma,E)$ has an initial object.

Before tackling the proof of Lemma 5.1, we discuss how to derive Theorem 4.30 from it, and we prove some auxiliary results.

The ?epimorphism? hypotheses of Lemma 5.1 are used to transfer structure from the initial model $\hat{\Sigma}$ of the 1-signature $\Sigma$ onto a suitable quotient. There are different ways to prove these hypotheses:

• •

The axiom of choice implies conditions 4 and 5 since, in this case, any epimorphism in ${\mathsf{Set}}$ is split and thus preserved by any functor.

• •

Condition 5 is a consequence of condition 4 if $\Sigma$ sends monads preserving epimorphisms to modules preserving epimorphisms.

• •

If $\Sigma$ is algebraic, then conditions 1, 3, 4 and 5 are satisfied [2, Example 43 and Lemma 45].

From the remarks above, we derive the simpler and weaker statement of Theorem 4.30 that covers all our examples, which are algebraic.

This section is dedicated to the proof of the main technical result, Lemma 5.1. The reader inclined to do so may safely skip this section, and rely on the correctness of the machine-checked proof instead.

The proof of Lemma 5.1 uses some quotient constructions that we present now:

Proposition 5.2** ().**

Given a monad $R$ preserving epimorphisms and a collection of monad morphisms $(f_{i}:R\rightarrow S_{i})_{i\in I}$, there exists a quotient monad $R/(f_{i})$ together with a projection $p^{R}\colon R\longrightarrow R/(f_{i})$, which is a morphism of monads such that each $f_{i}$ factors through $p$.

Proof 5.3**.**

The set $R/(f_{i})(X)$ is computed as the quotient of $R(X)$ with respect to the relation $x\sim y$ if and only if $f_{i}(x)=f_{i}(y)$ for each $i\in I$. This is a straightforward adaptation of Lemma 47 of [2].

Note that the epimorphism preservation is implied by the axiom of choice, but can be proven for the monad underlying the initial model $\hat{\Sigma}$ of an algebraic 1-signature $\Sigma$ even without resorting to the axiom of choice.

The above construction can be transported on $\Sigma$-models:

Proposition 5.4** ().**

Let $\Sigma$ be a 1-signature sending epimorphic natural transformations to epimorphic natural transformations, and let $R$ be a $\Sigma$-model such that $R$ and $\Sigma(R)$ preserve epimorphisms. Let $(f_{i}:R\rightarrow S_{i})_{i\in I}$ be a collection of $\Sigma$-model morphisms. Then the monad $R/(f_{i})$ has a natural structure of $\Sigma$-model and the quotient map $p^{R}\colon R\longrightarrow R/(f_{i})$ is a morphism of $\Sigma$-models. Any morphism $f_{i}$ factors through $p^{R}$ in the category of $\Sigma$-models.

The fact that $R$ and $\Sigma(R)$ preserve epimorphisms is implied by the axiom of choice. The proof follows the same line of reasoning as the proof of Proposition 5.2.

Now we are ready to prove the main technical lemma:

Proof 5.5** (Proof of Lemma 5.1).**

Let $\Sigma$ be an effective 1-signature, and let $E$ be a set of elementary $\Sigma$-equations. The plan of the proof is as follows:

Start with the initial model $(\hat{\Sigma},\sigma)$, with $\sigma:\Sigma(\hat{\Sigma})\to\hat{\Sigma}$. 2. 2.

Construct the quotient model $\hat{\Sigma}/(f_{i})$ according to Proposition 5.4 where $(f_{i}:\hat{\Sigma}\rightarrow S_{i})_{i}$ is the collection of all initial $\Sigma$-morphisms from $\hat{\Sigma}$ to any $\Sigma$-model satisfying the equations. We denote by $\sigma/(f_{i}):\Sigma(\hat{\Sigma}/(f_{i}))\rightarrow\hat{\Sigma}/(f_{i})$ the action of the quotient model. 3. 3.

Given a model $M$ of the 2-signature $(\Sigma,E)$, we obtain a morphism $i_{M}:\hat{\Sigma}/(f_{i})\to M$ from Proposition 5.4. Uniqueness of $i_{M}$ is shown using epimorphicity of the projection $p:\hat{\Sigma}\rightarrow\hat{\Sigma}/(f_{i})$. For this, it suffices to show uniqueness of the composition $i_{M}\circ p:\hat{\Sigma}\to M$ in the category of 1-models of $\Sigma$, which follows from initiality of $\hat{\Sigma}$. 4. 4.

The verification that \bigl{(}\hat{\Sigma}/(f_{i}),\sigma/(f_{i})\bigr{)} satisfies the equations is given below. Actually, it follows the same line of reasoning as in the proof of Proposition 5.2 that $\hat{\Sigma}/(f_{i})$ satisfies the monad equations.

Let $e=(e_{1},e_{2}):U\to\Theta^{(n)}$ be an elementary equation of $E$. We want to prove that the two arrows

[TABLE]

are equal. As $p$ is an epimorphic natural transformation, $U(p)$ also is by definition of an elementary equation. It is thus sufficient to prove that

[TABLE]

which, by naturality of $e_{1}$ and $e_{2}$, is equivalent to $p^{(n)}\circ e_{1,\hat{\Sigma}}=p^{(n)}\circ e_{2,\hat{\Sigma}}$.

Let $x$ be an element of $U(\hat{\Sigma})$ and let us show that $p^{(n)}(e_{1,\hat{\Sigma}}(x))=p^{(n)}(e_{2,\hat{\Sigma}}(x))$. By definition of $\hat{\Sigma}/(f_{i})$ as a pointwise quotient (see Proposition 5.2), it is enough to show that for any $j$, the equality $f_{j}^{(n)}(e_{1,\hat{\Sigma}}(x))=f_{j}^{(n)}(e_{2,\hat{\Sigma}}(x))$ is satisfied. Now, by naturality of $e_{1}$ and $e_{2}$, this equation is equivalent to $e_{1,S_{j}}(U(f_{j})(x)))=e_{2,S_{j}}(U(f_{j})(x)))$ which is true since $S_{j}$ satisfies the equation $e_{1}=e_{2}$.

6 Examples of algebraic 2-signatures

We already illustrated our theory by looking at the paradigmatic case of lambda calculus modulo $\beta$- and $\eta$-equations (Examples 4.9 and 4.31). This section collects further examples of application of our results.

In our framework, complex signatures can be built out of simpler ones by taking their coproducts. Note that the class of algebraic 2-signatures encompasses the algebraic 1-signatures and is closed under arbitrary coproducts: the prototypical examples of algebraic 2-signatures given in this section can be combined with any other algebraic 2-signature, yielding an effective 2-signature thanks to Theorem 4.30.

6.1 Monoids

We begin with an example of monad for a first-order syntax with equations. Given a set $X$, we denote by $M(X)$ the free monoid built over $X$. This is a classical example of monad over the category of (small) sets. The monoid structure gives us, for each set $X$, two maps $m_{X}\colon M(X)\times M(X)\longrightarrow M(X)$ and $e_{X}\colon 1\longrightarrow M(X)$ given by the product and the identity respectively. It can be easily verified that $m\colon M^{2}\longrightarrow M$ and $e\colon 1\longrightarrow M$ are $M$-module morphisms. In other words, $(M,\rho)=(M,[m,e])$ is a model of the 1-signature $\Sigma=\Theta\times\Theta+1$.

We break the tautological morphism of $\Sigma$-modules (cf. Example 4.4) into constituent pieces, defining $\mathsf{m}:=\tau\circ\mathsf{inl}:\Theta\times\Theta\to\Theta$ and $\mathsf{e}:=\tau\circ\mathsf{inr}:1\to\Theta$.

Over the 1-signature $\Sigma$ we specify equations postulating associativity and left and right unitality as follows:

[TABLE]

and we denote by $E$ the family consisting of these three $\Sigma$-equations. All are elementary since their codomain is $\Theta$, and their domain a product of $\Theta$s.

One checks easily that $(M,[m,e])$ is the initial model of $(\Sigma,E)$.

Several other classical (equational) algebraic theories, such as groups and rings, can be treated similarly, see Section 6.3 below. However, at the present state we cannot model theories with partial construction (e.g., fields).

6.2 Colimits of algebraic 2-signatures

In this section, we argue that our framework encompasses any colimit of algebraic 2-signatures.

Actually, the class of algebraic 2-signatures is not stable under colimits, as this is not even the case for algebraic 1-signatures. However, we can weaken this statement as follows:

Proposition 6.1**.**

Given any colimit of algebraic 2-signatures, there is an algebraic 2-signature yielding an isomorphic category of models.

Proof 6.2**.**

As the class of algebraic 2-signatures is closed under arbitrary coproducts, using the decomposition of colimits into coproducts and coequalizers, any colimit $\Xi$ of algebraic 2-signatures can be expressed as a coequalizer of two morphisms $f,g$ between some algebraic 2-signatures $(\Sigma_{1},E_{1})$ and $(\Sigma_{2},E_{2})$,

[TABLE]

where $\Sigma_{3}$ is the coequalizer of the 1-signatures morphisms $f$ and $g$. Note that the set of equations of $\Xi$ is $E_{2}$, by definition of the coequalizer in the category of 2-signatures. Now, consider the algebraic 2-signature $\Xi^{\prime}=(\Sigma_{2},E_{2}+\eqref{eq:colim-of-algs})$ consisting of the 1-signature $\Sigma_{2}$ and the equations of $E_{2}$ plus the following elementary equation (see Example 4.28):

[TABLE]

We show that $\mathsf{Mon}^{\Xi}$ and $\mathsf{Mon}^{\Xi^{\prime}}$ are isomorphic. A model of $\Xi^{\prime}$ is a monad $R$ together with an $R$-module morphism $r:\Sigma_{2}(R)\to R$ such that $r\circ f_{R}=r\circ g_{R}$ and that the equations of $E_{2}$ are satisfied. By universal property of the coequalizer, this is exactly the same as giving an $R$-module morphism $\Sigma_{3}(R)\to R$ satisfying the equations of $E_{2}$, i.e., giving $R$ an action of $\Xi=(\Sigma_{3},E_{2})$.

It is straightforward to check that this correspondence yields an isomorphism between the category of models of $\Xi$ and the category of models of $\Xi^{\prime}$.

This proposition, together with the following corollary, allow us to recover all the examples presented in [2], as colimits of algebraic 1-signatures: syntactic commutative binary operator, maximum operator, application à la differential lambda calculus, syntactic closure operator, integrated substitution operator, coherent fixpoint operator.

Corollary 6.3**.**

If $F$ is a finitary endofunctor on ${\mathsf{Set}}$, then there is an algebraic 2-signature whose category of models is isomorphic to the category of 1-models of the 1-signature $F\cdot\Theta$.

Proof 6.4**.**

It is enough to prove that $F\cdot\Theta$ is a colimit of algebraic 1-signatures.

As $F$ is finitary, it is isomorphic to the coend $\int^{n\in{\mathbb{N}}}F(n)\times\_^{n}$ where ${\mathbb{N}}$ is the full subcategory of ${\mathsf{Set}}$ of finite ordinals (see, e.g., [12, Example 3.19]). As colimits are computed pointwise, the 1-signature $F\cdot\Theta$ is the coend $\int^{n\in{\mathbb{N}}}F(n)\times\Theta^{n}$, and as such, it is a colimit of algebraic 2-signatures.

However, we do not know whether we can recover our theorem [2, Theorem 35] stating that any presentable 1-signature is effective.

6.3 Algebraic theories

From the categorical point of view, several fundamental algebraic structures in mathematics can be conveniently and elegantly described using finitary monads. For instance, the category of monoids can be seen as the category of Eilenberg–Moore algebras of the monad of lists. Other important examples, like groups and rings, can be treated analogously. A classical reference on the subject is the work of Manes, where such monads are significantly called finitary algebraic theories [10, Def. 3.17].

We want to show that such ?algebraic theories? fit in our framework, in the sense that they can be incorporated into an algebraic 2-signature, with the effect of enriching the initial model with the operations of the algebraic theory, subject to the axioms of the algebraic theory.

For a finitary monad $T$, Corollary 6.3 says how to encode the 1-signature $T\cdot\Theta$ as an algebraic 2-signature $(\Sigma_{T},E_{T})$. Models are monads $R$ together with an $R$-linear morphism $r:T\cdot R\to R$.

Now, for any model $(R,m)$ of $T\cdot\Theta$, we would like to enforce the usual $T$-algebra equations on the action $m$. This is done thanks to the following equations, where $\tau$ denotes the tautological morphism of $T\cdot\Theta$-modules:

[TABLE]

The first equation is clearly elementary. The second one is elementary thanks to the following lemma:

Lemma 6.5**.**

Let $F$ be a finitary endofunctor on ${\mathsf{Set}}$. Then $F$ preserves epimorphisms.

Proof 6.6**.**

As $F$ is finitary, it is isomorphic to the coend $\int^{n\in{\mathbb{N}}}F(n)\times\_^{n}$ [12, Example 3.19]. By decomposing it as a coequalizer of coproducts, we get an epimorphism $\alpha:\coprod_{n\in{\mathbb{N}}}F(n)\times\_^{n}\to F$. Now, let $f:X\to Y$ be a surjective function between two sets. We show that $F(f)$ is epimorphic. By naturality, the following diagram commutes:

[TABLE]

The composition along the top-right is epimorphic by composition of epimorphisms. Thus, the bottom left is also epimorphic, and so is $F(f)$ as the last morphism of this composition.

In conclusion, we have exhibited the algebraic 2-signature $(\Sigma_{T},E^{\prime}_{T})$, where $E^{\prime}_{T}$ extends the family $E_{T}$ with the two elementary equations of Diagram 3. This signature allows to enrich any other algebraic 2-signature with the operations of the algebraic theory $T$, subject to the relevant equations.

6.4 Fixpoint operator

Here, we show the algebraic 2-signature corresponding to a fixpoint operator. In [2, Section 9.4] we studied fixpoint operators in the context of 1-signatures. In that setting, we treated a syntactic fixpoint operator called coherent fixpoint operator, somehow reminiscent of mutual letrec. We were able to impose many natural equations to this operator but we were not able to enforce the fixpoint equation. In this section, we show how a fixpoint operator can be fully specified by an algebraic 2-signature. We restrict our discussion to the unary case; the coherent family of multi-ary fixpoint operators presented in [2, Section 9.4], now including the fixpoint equations, can also be specified, in an analogous way, via an algebraic 2-signature.

Let us start by recalling the following

Definition 6.7**.**

A unary fixpoint operator for a monad $R$ [2, Definition 50] is a module morphism $f$ from $R^{\prime}$ to $R$ that makes the following diagram commute, where $\sigma$ is the substitution morphism defined as the uncurrying (see Definition 4.8) of the identity morphism on $\Theta^{\prime}$:

[TABLE]

In order to rephrase this definition, we introduce the obviously algebraic 2-signature $\Upsilon_{\mathsf{fix}}$ consisting of the 1-signature $\Sigma_{\mathsf{fix}}=\Theta^{\prime}$ and the family $E_{\mathsf{fix}}$ consisting of the single following $\Sigma_{\mathsf{fix}}$-equation:

[TABLE]

This allows us to rephrase the previous definition as follows: a unary fixpoint operator for a monad $R$ is just an action of the 2-signature $\Upsilon_{\mathsf{fix}}$ in $R$.

The name ?fixpoint operator? is motivated by the following proposition:

Proposition 6.8** ([2, Proposition 51]).**

Fixpoint combinators are in one-to-one correspondence with actions of $\Upsilon_{\mathsf{fix}}$ in the monad ${\mathsf{LC}}_{\beta\eta}$ of the lambda calculus modulo $\beta$- and $\eta$-equality.

Recall that fixpoint combinators are lambda terms $Y$ satisfying, for any (possibly open) term $t$, the equation

[TABLE]

Explicitly, such a combinator $Y$ induces a fixpoint operator $\hat{Y}:{\mathsf{LC}}_{\beta\eta}^{\prime}\rightarrow{\mathsf{LC}}_{\beta\eta}$ which associates, to any term $t$ depending on an additional variable $*$, the term $\hat{Y}(t):={\mathsf{app}}(Y,{\mathsf{abs}}\>\,t)$.

7 Recursion

In this section, we explain how a recursion principle can be derived from our initiality result, and give an example of a morphism—a translation—between monads defined via the recursion principle.

7.1 Principle of recursion

In our context, the recursion principle is a recipe for constructing a morphism from the monad underlying the initial model of a 2-signature to an arbitrary monad.

Proposition 7.1** (Recursion principle).**

Let $S$ be the monad underlying the initial model of the 2-signature $\Upsilon$. To any action $a$ of $\Upsilon$ in $T$ is associated a monad morphism $\hat{a}:S\to T$.

Proof 7.2**.**

The action $a$ defines a 2-model $M$ of $\Upsilon$, and $\hat{a}$ is the monad morphism underlying the initial morphism to $M$.

Hence the recipe consists in the following two steps:

give $T$ an action of the 1-signature $\Sigma$; 2. 2.

check that all the equations in $E$ are satisfied for the induced model.

In the next section, we illustrate this principle.

7.2 Translation of lambda calculus with fixpoint to lambda calculus

In this section, we consider the 2-signature $\Upsilon_{{\mathsf{LC}}_{\beta\eta,{\mathsf{fix}}}}:=\Upsilon_{{\mathsf{LC}}_{\beta\eta}}+\Upsilon_{{\mathsf{fix}}}$ where the two components have been introduced above (see Example 4.16 and Section 6.4).

As a coproduct of algebraic 2-signatures, $\Upsilon_{{\mathsf{LC}}_{\beta\eta,{\mathsf{fix}}}}$ is itself algebraic, and thus the initial model exists. The underlying monad ${\mathsf{LC}}_{\beta\eta,{\mathsf{fix}}}$ of the initial model can be understood as the monad of lambda calculus modulo $\beta$ and $\eta$ enriched with an explicit fixpoint operator ${\mathsf{fix}}:{\mathsf{LC}}_{\beta\eta,{\mathsf{fix}}}^{\prime}\longrightarrow{\mathsf{LC}}_{\beta\eta,{\mathsf{fix}}}$. Now we build by recursion a monad morphism from this monad to the ?bare? monad ${\mathsf{LC}}_{\beta\eta}$ of lambda calculus modulo $\beta$ and $\eta$.

As explained in Section 7.1, we need to define an action of $\Upsilon_{{\mathsf{LC}}_{\beta\eta,{\mathsf{fix}}}}$ in ${\mathsf{LC}}_{\beta\eta}$, that is to say an action of $\Upsilon_{{\mathsf{LC}}_{\beta\eta}}$ plus an action of $\Upsilon_{{\mathsf{fix}}}$. For the action of $\Upsilon_{{\mathsf{LC}}_{\beta\eta}}$, we take the one yielding the initial model.

Now, in order to find an action of $\Upsilon_{{\mathsf{fix}}}$ in ${\mathsf{LC}}_{\beta\eta}$, we choose a fixpoint combinator $Y$ (say the one of Curry) and take the action $\hat{Y}$ as defined at the end of Section 6.4.

In more concrete terms, our translation is a kind of compilation which replaces each occurrence of the explicit fixpoint operator ${\mathsf{fix}}(t)$ with ${\mathsf{app}}(Y,{\mathsf{abs}}\>\,t)$.