À mon ami Nicolas Tholance, disparu trop tôt

INTRODUCTION 1.1 Résumé long (en français)

Cette thèse s'intéresse à la mathématisation de la notion de langage de programmation, en portant une attention particulière à la notion de substitution.

La recherche dans le domaine des langages de programmation s'appuie traditionnellement sur une définition de syntaxe modulo renommage des variables liées, avec la sémantique opérationnelle associée. Nous nous intéressons à des outils mathématiques permettant de générer automatiquement la syntaxe et la sémantique à partir de données élémentaires.

En ce qui concerne la syntaxe, la spécification de structures algébriques avec variables liées est un enjeu majeur. Deux lignes principales de recherche sont en concurrence : les ensembles nominaux [START_REF] Gabbay | A New Approach to Abstract Syntax Involving Binders[END_REF] et les algèbres de substitution [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF]. Dans cette thèse, nous explorons une variante des algèbres de substitution, proposée par [HM07 ; HM10], qui s'appuie sur la notion de module sur une monade. Nous abordons également dans cet esprit la mathématisation de la sémantique opérationnelle. Pour cela, nous introduisons d'abord les monades de réduction, puis leur généralisation, les monades opérationnelles : elles constituent notre approximation mathématique de la notion informatique de langage de programmation.

Dans cette thèse, nous nous intéressons à la spécification des objets de la catégorie des monades (chapitres 3 et 4), de la catégorie des monades de réduction (chapitre 5), et de la catégorie des monades opérationnelles (chapitre 6), notre objectif étant de définir un langage formel 1 , modélisé par un objet d'une catégorie adéquate.

Introduction sémantique initiale peut être décrite selon les étapes suivantes :

1. Introduire une notion de signature (pour la catégorie C).

2. Construire une notion de modèle associée, s'organisant en une catégorie munie d'un foncteur vers la catégorie C.

3. Definir l'objet spécifié par la signature comme le modèle initial, s'il existe (la signature est alors dite effective).

4. Trouver une condition suffisante pour qu'une signature soit effective2 .

Les modèles d'une signature constituent le domaine atteint par le principe de récurrence, lequel est induit par l'initialité de l'objet spécifié par la signature. Dans le chapitre 2, nous définissons une notion générale de signature permettant de caractériser un objet d'une catégorie arbitraire C, avec la notion de modèle associée. Une telle signature est donnée par une liste de familles d'arités spécifiant des opérations ou des équations. Les chapitres suivants en fournissent divers cas particuliers, de la spécification de la syntaxe à la spécification de la sémantique, en identifiant à chaque fois une classe de signatures effectives.

Finalement, nous proposons un protocole fondé sur une signature à trois niveaux pour spécifier un langage de programmation :

1. spécification des constructions, par exemple une opération binaire + ; 2. spécification des équations, par exemple a + b = b + a (commutativité de l'opération binaire +) ; 3. spécification des réductions entre termes, par exemple 0 + a a, par des règles schématiques.

Les deux premiers points définissent ce que nous appelons la syntaxe du langage de programmation, tandis que le dernier point concerne la sémantique du langage : une réduction entre deux termes correspond à un chemin d'exécution du programme évoluant du premier terme vers le second. A titre d'exemple de langage intégrant les trois niveaux, nous proposons dans la section 5.6 une spécification du lambda calcul avec substitution explicite décrit dans [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF].

Afin de motiver les notions mathématiques mises en jeu, nous examinons dans ce résumé le langage de programmation fonctionnel le plus simple que l'on puisse envisager : le lambda calcul pur. Dans la section 1.1.1, nous donnons une première présentation de sa syntaxe, et la dotons d'une opération de substitution. Nous expliquons ensuite, dans la section 1.1.2, comment la notion mathématique de monade permet d'en rendre compte, puis, dans la section 1.1.3, comment la notion de morphisme de modules fournit un moyen d'exprimer une propriété essentielle des constructions de la syntaxe : la compatibilité à la substitution. Dans la section 1.1.4, nous caractérisons la syntaxe par son principe de récurrence, que nous formulons par une propriété d'initialité. Nous expliquons dans la section 1.1.5 que préciser cette propriété d'initialité requiert une notion de modèle adéquate, laquelle est déterminée par la signature : c'est l'occasion de présenter notre définition générale de signature pour spécifier les objets d'une catégorie arbitraire. Nous examinons ensuite le cas de syntaxes vérifiant des équations (section 1.1.6), avant d'aborder, dans la section 1.1.7, la spécification de la sémantique, modélisée dans le cadre des monades de réduction par un ensemble de réductions entre chaque paire de termes.

Présentation naïve de la syntaxe du lambda calcul

Nous donnons ici une présentation de la syntaxe du lambda calcul, ainsi qu'un aperçu de quelques difficultés habituellement associées à une telle présentation. On fixe un ensemble infini V de variables, et l'on caractérise récursivement l'ensemble des termes ou expressions valides du lambda calcul :

• chaque variable x ∈ V est un terme du lambda calcul,

• si t et u sont des termes, alors t u est un terme, appelé application de t à u ;

• si t est un terme, alors λx.t est un terme, appelé lambda abstraction de t, où x est une variable qui peut apparaître dans t.

L'expression λx.t correspond à la notation mathématique x → t. Il s'agit de définir une fonction dépendant de la variable x, le corps de cette fonction étant donné par le terme t. L'expression f t correspond à la notation mathématique f (t) : c'est l'application de la fonction f à l'argument t. En mathématique, le nom de la variable choisie pour définir une fonction est purement conventionnel : les fonctions x → f (x) et y → f (y) sont identiques. Transposons cette identification dans le langage du lambda calcul : nous voulons égaliser le terme λx.t avec le terme λy.t ′ , où t ′ est obtenu à partir du terme t en remplaçant toutes les occurrences de la variable x par la variable y. Dans cette situation, on dit que x est une variable liée dans λx.t, et les occurrences de x dans t sont alors qualifiées de liées. Les occurrences de variables qui ne sont pas liées sont dites libres3 . Ici, les termes λx.t et λy.t ′ sont dits α-équivalents. Plus généralement, deux termes sont α-équivalents si l'on peut renommer les variables liées de l'un pour obtenir l'autre terme. La définition précise de la relation d'α-équivalence requiert quelques précautions. Par exemple, dans le cas précédent, il est sous-entendu que la variable y n'apparait pas dans t ; autrement, nous identifierions (contre notre gré) les termes λx.y et λy.y.

La substitution est un autre aspect essentiel de la syntaxe du lambda calcul : étant donné un terme t, si l'on remplace toutes les occurrences (libres) d'une variable x par un même terme u, nous obtenons une nouvelle expression valide, que nous notons t{x := u}. L'opération de substitution permet d'exprimer l'intuition mathématique suivante : le résultat d'une fonction x → t appliquée à un argument u est obtenu en remplaçant la variable x dans t par u. Cette affirmation se transpose, pour le lambda calcul, en la β-équation (λx.t) u = t{x := u}.

(1.1)

Cette substitution dite unaire est un cas particulier de l'opération de substitution parallèle t{x → u x }, qui remplace simultanément toutes les variables d'un terme t par un terme correspondant.

La substitution ne remplace que les occurrences libres d'une variable, afin de préserver la propriété suivante : étant donné deux termes λx.t et λy.t ′ supposés αéquivalents, substituer le même terme à la même variable dans chacun d'eux fournit deux termes α-équivalents. Si la variable concernée est identique à la variable abstraite, le terme (λx.t){x := u} est donc tout simplement égal à λx.t : par exemple (λx.x){x := u} = λx.x est bien α-équivalent à (λy.y){x := u} = λy.y.

La monade du lambda calcul

Le concept de monade fournit une contrepartie mathématique de la notion intuitive de syntaxe munie d'une opération de substitution. Nous motivons cette définition par l'exemple du lambda calcul. Dans le point de vue que nous adoptons ici, les termes α-équivalents sont considérés comme identiques : ainsi, λx.x = λy.y.

Au lieu de considérer un ensemble unique de termes avec un ensemble de variables V fixé à l'avance, nous définissons des classes de termes qui utilisent les mêmes variables libres. Notons L(X) l'ensemble des termes dont les variables libres sont choisies dans l'ensemble X. Remarquons qu'un terme t ∈ L(X) se retrouve également dans L(Y ) pour tout inclusion X ⊂ Y : en effet, si les variables libres sont choisies parmi les éléments d'un ensemble X, elles sont en particulier choisies parmi les élements de n'importe quel ensemble Y qui contient X.

Toute variable est en particulier un terme valide ; il y a donc une inclusion var X : X → L(X) pour tout ensemble X. D'autre part, si l'on se donne pour toute variable x ∈ X un terme u x dont les variables libres sont choisies dans Y , nous obtenons, à partir de n'importe quel terme t ∈ L(X), un terme t{x → u x } ∈ L(Y ). Cette opération de substitution parallèle vérifie les propriétés suivantes :

• chaque variable est remplacée par le terme adéquat :

x ′ {x → u x } = u x ′
• la substitution identité est neutre :

t{x → x} = t
• toute succession de substitutions est équivalente à une substitution composée : t{x → u x }{y → v y } = t{x → u x {y → v y }} L'inclusion des variables dans les termes et l'opération de substitution parallèle satisfaisant les équations ci-dessus définissent une monade sur la catégorie des ensembles. Cet objet mathématique est au coeur des développements que nous exposons dans cette thèse.

Les constructions sont des morphismes de modules

Les concepts mathématiques de modules et de morphismes de modules offrent un cadre permettant d'exprimer la compatibilité d'une construction de la syntaxe avec l'opération de substitution. Nous illustrons ceci avec l'application t u du lambda calcul.

La compatibilité de l'application avec la substitution se traduit par la commutation

(t u){x → v x } = t{x → v x } u{x → v x }
Informellement, cette équation signifie qu'il n'y a pas de différence entre effectuer la substitution avant l'application et effectuer la substitution après l'application, comme l'exprime le diagramme commutatif suivant : Ce constat s'appuie implicitement sur l'opération de substitution suivante dont bénéficie la collection d'ensembles (L(X) × L(X)) X :

L(X) × L(X) (t, u) a p p li c a ti o n ' ' L(Y ) × L(Y ) (t{x → v x }, u{x → v x })
(t, u){x → v x } = (t{x → v x }, u{x → v x })
Cette substitution vérifie les propriétés suivantes :

• la substitution identité est neutre :

(t, u){x → x} = (t, u)
• toute succession de substitutions est équivalente à une seule substitution composée :

(t, u){x → u x }{y → v y } = (t, u){x → u x {y → v y }} À ce titre, la collection des ensembles de paires de termes définit un module sur la monade L, que nous notons L × L.

Les définitions de monade et de module sont similaires ; d'ailleurs toute monade définit un module sur elle-même. En fait, L × L définit aussi une monade, mais la substitution associée ne dérive pas de sa structure de module. Étant donné une paire de termes (t, u) dont les variables libres sont choisies dans X, et pour toute variable

x ∈ X, une paire de termes (v x , w x ) dont les variables libres sont choisies dans Y , cette substitution monadique fournit une paire de termes dont les variables libres sont dans Y . La substitution donnée par la structure de module ne convient pas, puisqu'elle ne s'applique que dans le cas où l'on a associé à chaque variable un terme de la monade L, plutôt qu'une paire de termes.

L'application du lambda calcul induit une collection de fonctions

L(X) × L(X) → L(X)
qui associent à toute paire (t, u) le terme t u. La propriété de commutation avec la substitution sus-mentionnée en fait un morphisme de modules de L × L vers L, où L est vu comme un module sur la monade homonyme.

De même, l'abstraction du lambda calcul induit une collection de fonctions L(X ∐ {⋆}) → L(X) qui, à tout terme t dont les variables libres sont choisies dans l'ensemble X étendu avec un nouvel élément ⋆, associe le terme λ ⋆ .t. La famille L(X ∐ {⋆}) X est canoniquement munie d'une opération de substitution et définit donc un module. La collection des fonctions d'abstraction induit alors un morphisme de modules, en raison de la commutation avec la substitution :

(λ ⋆ .t){x → u x } = λ ⋆ .   t      x →      ⋆ si x = ⋆ u x sinon.        
La construction de module que nous rencontrons ici se généralise à n'importe quel module M sur une monade R : le module dérivé M ′ se définit comme la collection d'ensembles (M (X ∐ {⋆})) X munie d'une opération de substitution canonique.

Dans cette thèse, nous nous intéressons exclusivement à des langages de pro-grammation dont les constructions et les réductions sont compatibles avec la substitution, d'où notre intérêt pour les notions de module et de morphisme de modules.

Récursion et initialité

La présentation naïve du lambda calcul induit naturellement un principe de récurrence sur la syntaxe. Supposons, par exemple, que nous voulons calculer l'ensemble des variables libres d'un terme t du lambda calcul. Pour ce faire, nous raisonnons par récurrence sur la structure du terme. Si t est une variable x, alors le singleton {x} constitue l'ensemble de ses variables libres. Si t est une application u v, alors l'ensemble de ses variables libres est la réunion des variables libres de u et v. Si t est une lambda abstraction λx.u, alors n'importe quelle variable libre de u différente de x est une variable libre de t.

Dans notre cadre, nous adoptons le point de vue de la sémantique initiale : le principe de récurrence est alors une conséquence d'une propriété d'initialité. Le lambda calcul est ainsi caractérisé comme la monade "minimale" munie d'une application et d'une lambda abstraction, dans un sens que nous allons illustrer par l'exemple du calcul des variables libres (cet exemple est étudié plus formellement dans la Section 3.5.2).

Considérons la monade P qui associe à X l'ensemble P(X) de ses parties : une variable x ∈ X induit un "terme" {x} ∈ P(X) ; la substitution t{x → u x } est calculée par la réunion ∪ z∈t u z . L'union de deux sous-ensembles fournit une opération binaire pour P, que nous assimilons à une "opération d'application" par analogie avec l'opération binaire d'application du lambda calcul. Cette opération associe le sous-ensemble t ∪ u au couple (t, u). De même, une opération adéquate d'abstraction P(X ∐ {⋆}) → P(X) est donnée par t → t ∩ X, ou, de manière équivalente, par t → t\{x}. Comme nous l'expliquerons dans la section suivante, ces constructions font de la monade P un modèle de la signature du lambda calcul.

La propriété d'initialité du lambda calcul mentionnée s'instancie alors par l'existence d'une unique famille de fonctions (free X : L(X) → P(X)) X vérifiant les propriétés suivantes :

• free préserve les variables : free X (var(x)) = {x} (rappelons que pour la monade P, la variable x est vue comme le sous-ensemble {x})

• free préserve la substitution :

free Y (t{x → u x }) = z∈free X (t)
free Y (u z )

• free préserve l'application : free(t u) = free(t) ∪ free(u)

• free préserve l'abstraction : free(λx.t) = free(t)\{x} Les deux premiers points caractérisent free comme un morphisme de monades entre L et P. La section suivante définit la notion de modèle de sorte que L et P, munies leurs opérations respectives d'application et d'abstraction, sont des modèles de la signature du lambda calcul. Le morphisme de monades free est alors un morphisme de modèles de cette signature, grâce aux deux derniers points.

Signatures et modèles (Chapitre 2)

Dans le chapitre 2, nous proposons une notion de signature générale, définie comme une liste de famille d'arités, pour spécifier les objets d'une catégorie arbitraire C. Une arité est la donnée d'un diagramme de foncteurs Comme nous l'avons dit, une signature est une liste de familles d'arités : une première famille d'arités pour la catégorie C de base, puis une famille d'arités pour la catégorie de modèles induite, et ainsi de suite.

Nous illustrons ces définitions pour les signatures monadiques (c'est-à-dire spécifiant des monades) envisagées dans le chapitre 3, qui sont composées d'une unique arité. Considérons l'exemple de la syntaxe du lambda calcul. Dans la section précédente, nous l'avons caractérisée comme la monade initiale munie d'une application et d'une abstraction. Plus précisément, en généralisant l'exemple de la monade des parties P étudiée dans la section précédente, nous disons qu'une monade R est munie d'une application et d'une abstraction si elle est dotée à la fois d'une opération binaire, c'est-à-dire d'un morphisme de modules app R : R × R → R, et d'un morphisme de modules abs R : R ′ → R. De manière équivalente, c'est une monade R avec un morphisme de modules de (R × R) ∐ R ′ vers R, c'est-à-dire, d'une action pour l'arité

Mon Σ LC / / o o Θ / / Mod (1.2)
que nous allons préciser. La catégorie Mon est la catégorie des monades ; la catégorie Mod rassemble toutes les catégories de modules sur des monades différentes 4 : un objet est une paire d'une monade et d'un module sur cette monade, et un morphisme entre (R, M ) et (S, N ) est une paire d'un morphisme de monades f : R → S et d'un morphisme de modules g : M → f * N sur la monade R, où f * N est le module sur R obtenu canoniquement à partir de N , en précomposant ses opérations de substitution par f . Le foncteur Mod → Mon renvoie la première projection. Une section de ce foncteur, ou module paramétrique, associe fonctoriellement à toute monade un module sur elle-même. Par exemple, le module paramétrique Θ associe à toute monade R le module R (rappelons en effet que toute monade est un module sur elle-même). Par ailleurs, le module paramétrique Σ LC du lambda calcul associe à toute monade R le module (R × R) ∐ R ′ sur R.

Un module paramétrique quelconque Σ induit une arité de manière similaire à Σ LC dans l'équation 1.2. Considérons la catégorie de modèles associée à la signature composée de cette unique arité. Un modèle (R, ρ) (parfois noté simplement R) de cette signature est une monade R munie d'un morphisme de modules ρ : Σ(R) → R. Ainsi, la monade des parties P et la monade du lambda calcul L induisent des modèles de Σ LC . En fait, le lambda calcul est le modèle initial : si R est un modèle, alors il existe un unique morphisme de monades f : L → R qui préserve l'opération binaire et l'abstraction.

Plus généralement, la monade S spécifiée par la signature induite par un module paramétrique Σ est munie d'une action σ : Σ(R) → R qui en fait un modèle initial : étant donné un modèle (R, ρ), il existe un unique morphisme de monades f : S → R qui préserve la structure de modèle, i.e., vérifiant pour tout t ∈ Σ(R)(X)

f (σ(t)) = ρ(f (t)) (1.3)
Un tel morphisme de monades constitue un morphisme de modèles entre (S, σ) et (R, ρ). Notons que le membre de droite de l'équation 1.3 nécessite de donner un sens à l'expression f (t) lorsque t est un élément de Σ(S) X : par fonctorialité de Σ, c'est tout simplement Σ(f )(t). En effet, tout morphisme de monades f : R → T induit un morphisme de modules Σ(R) → f * Σ(T ) sur la monade R, morphisme que nous notons abusivement f , ou Σ(f ). Dans le cas de l'opération binaire, on a Σ(S) X = S(X)×S(X). • pour chaque modèle R de la signature Σ, de deux morphismes de modules e R , e ′ R de même domaine

Donc t est une paire (u, v) et l'on définit Σ(f )(u, v) par (f (u), f (v)
A R et codomaine B R (dans l'exemple ci-dessus, e R , e ′ R : R × R × R → R associent respectivement b(b(t, u), v) et b(t, b(u, v))) à un même triplet (t, u, v) ∈ R 3 (X)) ;
• pour tout morphisme de modèles f : R → S, de deux morphismes de modules

A f : A R → A S et B f : B R → B S tels que les diagrammes suivants commutent : A R e R / / A f B R B f A S e ′ S / / B S A R e ′ R / / A f B R B f A S e ′ S / / B S
Ces données sont soumises comme d'habitude à une condition additionnelle de fonctorialité. On dit qu'un modèle R de la signature Σ vérifie l'équation lorsque e R = e ′ R . En fait, nous donnons une définition équivalente d'équation dans le chapitre 4, en tant qu'arité équationnelle d'une forme particulière. La vérification de l'équation se reformule en tant qu'une action pour l'arité.

Nous considérons alors les 2-signatures : il s'agit de signatures composées d'une arité induite par un module paramétrique et d'une famille de ces arités équationnelles. Un modèle (ou 2-modèle) d'une 2-signature est un modèle R de la signature induite par le module paramétrique sous-jacent qui vérifie toutes les équations. Nous parlons de 2-signatures algébriques lors que le module paramétrique est algébrique, et que les équations sont élémentaires (Définition 104). Techniquement, il s'agit d'équations dont l'action fonctorielle du domaine envoie des morphismes surjectifs de monades sur des morphismes surjectifs de foncteurs, et dont le codomaine est de la forme R → (((R ′ ) ′ ) ... ) ′ . Tout exemple de signature présentable que nous considérons dans le chapitre 3 peut être reformulé en tant que 2-signature algébrique, induisant la même catégorie de modèles (à isomorphisme près). Nous montrons que toute 2-signature algébrique est effective (Théorème 107).

Sémantique (chapitres 5 and 6)

Il est possible de spécifier par une 2-signature la syntaxe du lambda calcul quotientée par la β-équivalence (1.1) : les termes (λx.t) u et t{x := u} sont ainsi égalisés. Cependant, cette équation est habituellement orientée, et considérée comme une étape d'exécution lorsque l'on considère le lambda calcul comme un langage de programmation fonctionnel. A ce titre, il est plus adéquat d'intégrer la β-réduction à la sémantique du langage, plutôt que d'imposer la β-équation dans la syntaxe. Ceci motive la notion de monade de réduction, que nous introduisons dans le chapitre 5, étendant celle de monade, pour rendre compte de la structure additionnelle de réduction. Intuitivement, une monade de réduction est une monade R munie, pour chaque paire de termes (t, u) ∈ R(X), d'un ensemble de réductions entre t et u que l'on note t ◮ u, et d'une opération de substitution associée : pour toute famille de termes

(v x ) x∈X avec v x ∈ R(Y ), pour toute réduction m entre t et u, cette substitution associe une réduc- tion m{x → v x } entre t{x → v x } et u{x → v x }.
Des équations analogues à celles intervenant dans la définition de module sont requises.

Dans ce contexte, une signature de réduction est une signature d'une forme spécifique pour la catégorie des monades de réductions, déterminée par une 2-signature pour monades et une famille de règles de réductions. Par exemple, la règle de réduction pour la congruence de l'application du lambda calcul s'exprime informellement ainsi, en désignant explicitement l'application du lambda calcul par la construction app :

T T ′ U U ′ app(T, U ) app(T ′ , U ′ )
diagrammes suivants sont commutatifs :

R 4 f 4 h i,j (R) / / R f S 4 h i,j (S) / / S R 4 f 4 c i (R) / / R f S 4 c i (S)
/ / S Ainsi formulée, cette règle de congruence entre dans notre définition de règle de réduction détaillée en Section 5.3. Une action de cette règle dans une monade de réduction R munie d'une opération binaire app est la donnée d'une réduction app-cong(m T , m U ) entre app(T,

T ′ ) et app(U, U ′ ) pour tout (T, T ′ , U, U ′ ) ∈ R 4 (X), toute réduction m T entre T et T ′ , et toute réduction m U entre U et U ′ .
Il faut de plus que app-cong commute avec la substitution, c'est-à-dire que l'équation suivante soit vérifiée :

app-cong(m T , m U ){x → v x } = app-cong(m T {x → v x }, m U {x → v x })
Le théorème principal (Théorème 150) du chapitre 5 affirme l'effectivité d'une signature de réduction composée d'une 2-signature effective et de n'importe quelle famille de règles de réduction. Détaillons la notion de modèle mise en jeu ici : il s'agit d'une monade de réduction munie • d'une structure de modèle de la 2-signature pour la monade sous-jacente,

• d'une action de chaque règle de réduction de la signature.

Le modèle initial est construit à partir du modèle initial de la 2-signature, et la structure additionnelle de réductions est construite inductivement à partir des règles de réduction.

En guise d'exemples, nous proposons quelques signatures pour des variantes du lambda calcul avec β-réduction, puis, dans la section 5.6, une signature pour le lambda calcul avec substitution explicite, tel que décrit dans [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF] par un ensemble de constructions soumises à une équation syntaxique, auquel s'ajoutent des règles de réduction entre termes. Cette spécification se fait en trois étapes : une 1-signature pour les opérations du langage, une 2-signature prenant en compte l'équation syntaxique, et une signature de réduction spécifiant les réductions adéquates.

Dans le chapitre 6, nous généralisons ces développements, et traitons de nouveaux exemples, comme le lambda calcul en appel par valeurs avec réduction à grands pas : la syntaxe est celle du lambda calcul classique, mais dans cette variante, un terme se réduit en une valeur, c'est-à-dire en une variable ou bien en une lambda abstraction. La notion de valeur n'est pas stable par substitution arbitraire : par exemple, x{x := y y} = y y n'est pas une valeur. En revanche, elle est stable par substitution de valeurs : si v et (w x ) x∈X sont des valeurs, alors v{x → w x } est une valeur. Nous pouvons ainsi définir la monade LC v des valeurs du lambda calcul : elle est munie d'une inclusion dans la monade L du lambda calcul qui nous permet de considérer cette dernière comme un module sur LC v .

Dans cette variante du lambda calcul, la β-réduction est formulée ainsi :

t λx.t ′ u u ′ t ′ {x := u ′ } v t u v
Une autre règle de réduction assure que toute valeur, en tant que terme, se réduit vers elle-même.

Les réductions sont stables par substitution : si t ∈ L(X) se réduit en une valeur v ∈ LC v (X) et (u x ) x∈X est une famille de valeurs indexée par l'ensemble des variables libres X, alors t{x → u x } se réduit en v{x → u x }. La collection des ensembles de réductions entre un terme et une valeur est définie par induction, en appliquant successivement les règles de réduction envisagées. Elle est munie d'une opération de substitution adéquate, comme expliqué précédemment.

Remarquons qu'un lambda terme peut être représenté par un arbre binaire dont les feuilles sont des valeurs et les noeuds correspondent aux applications. Cette représentation induit une bijection : un tel arbre binaire détermine un lambda terme de manière unique.

(

• d'une monade R (dans notre exemple, R = LC v ) ; • d'une paire d'endofoncteurs (T 1 , T 2 ) sur Set (dans notre exemple, T 1 = B et T 2 = Id) ; • d'un ensemble de réductions entre t et u, pour chaque paire (t, u) ∈ T 1 (R(X)) × T 2 (R(X)) ;
• d'une opération de substitution appropriée sur ces ensembles de réductions.

Nous définissons ensuite les signatures opérationnelles permettant de spécifier ce type d'objet mathématique : ce sont des cas particuliers de signatures pour la catégorie des monades opérationnelles. Nous démontrons un résultat d'effectivité pour ces signatures (Théorème 207).

Formalisation

Les preuves des résultats principaux des chapitres 3 et 4 ont été vérifiées à l'aide de l'assistant de preuve Coq. Il s'agit d'un logiciel dans lequel il est possible de reproduire (ou formaliser ) des définitions mathématiques ainsi que des démonstrations qui, si elles sont validées par le logiciel, sont en principe incontestables. En pratique, cette garantie est à nuancer dans la mesure où des défauts d'implémentation permettant de prouver des énoncés contradictoires sont régulièrement exhibés (et corrigés). D'autre part, la correspondance entre les énoncés formalisés dans la théorie des types de Coq et les énoncés mathématiques est une question théorique qui n'est pas évidente. Mais plus pragmatiquement, il est possible de se tromper dans la formalisation d'une définition, et le logiciel Coq ne nous est d'aucune aide dans cette étape. Il arrive, par exemple, qu'on formalise une mauvaise caractérisation d'un certain ensemble, cette caractérisation se révélant contradictoire par la suite. Cette erreur peut passer inaperçue car elle n'empêchera pas de montrer que ses éléments vérifient les propriétés qui intéressent le mathématicien (en effet, les éléments de l'ensemble vide satisfont n'importe quelle propriété). Le lecteur d'une formalisation peut donc certes se dispenser d'examiner les démonstrations acceptées par le logiciel, mais il doit vérifier consciencieusement les définitions.

Pour nos développements, nous avons choisi de nous appuyer sur la bibliothèque UniMath de Coq. Celle-ci présente quelques avantages, malgré un problème de "taille" (que nous mentionnerons brièvement) : i elle comporte un certain nombre de définitions et de résultats que nous avons pu directement exploiter ;

ii elle utilise un nombre limité de fonctionnalités du langage ;

iii elle intègre l'axiome d'univalence.

Concernant le point i, UniMath propose, entre autres, une implémentation élaborée de la théorie des catégories et des ensembles quotients.

Le point ii permet de limiter la complexité de la théorie des types en laquelle il nous faut faire confiance (cependant, le problème de taille dont il est question plus loin affaiblit grandement cet argument). Il réduit également le risque d'être confronté à des erreurs d'implémentation de Coq, en se restreignant à des fonctionnalités éprouvées.

L'axiome d'univalence mentionné par le point iii en tant que tel n'est pas utilisé de manière cruciale. Il a cependant un certain nombre de conséquences utiles, par exemple l'extensionnalité fonctionnelle (deux fonctions sont égales si elles envoient chaque élément sur la même image : contrairement à ce qui se passe dans la théorie des ensembles, cet énoncé est indépendant de la théorie des types de Coq), ou encore l'extensionnalité propositionnelle (deux propositions logiquement équivalentes sont égales) qui permet de manipuler convenablement la notion de sous-ensemble.

Pour finir, la bibliothèque UniMath présente un important défaut dû à un problème de "taille". En effet, elle nécessite une option de compilation qui rend le système contradictoire, en rendant possible l'implémentation d'une variante du paradoxe de Russel. Cette option est en pratique utilisée dans la définition (imprédicative) des quotients. Nous avons ignoré l'existence de cette faille logique dans les raisonnements mathématiques que nous avons par la suite formalisés.

Long summary

This section is an English translation of the previous one. This thesis deals with the mathematization of the notion of language of programming, paying particular attention to the notion of substitution.

Research in the field of programming languages traditionally relies on a definition of syntax modulo renaming of bound variables, with its associated operational semantics.

We are interested in mathematical tools allowing to automatically generate syntax and semantics from basic data.

As regards the mathematization of syntax, the specification of algebraic structures with related variables is a major issue. Two main lines of research are in competition:

nominal sets [GP99] and substitution algebras [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF]. In this thesis, we explore a variant of substitution algebras, proposed by [HM07; HM10], which is based on the notion of module over a monad. Following the same spirit, we tackle the mathematization of operational semantics. To this end, we introduce first the reduction monads, then their generalization, the operational monads: they are our mathematical approximation of the notion of programming language.

In this thesis, we look at the specification of objects in the category of monads (Chapters 3 and 4), the category of reduction monads (Chapter 5), and the category of operational monads (Chapter 6), our objective being to define a formal language6 , modeled by an object of a relevant category.

The concept of characterising an object of a given type (i.e., of a certain category C) through an initiality property is standard in computer science, where it is known under the terms Initial Semantics and Algebraic Specification [START_REF] Thatcher | An initial algebra approach to the specification, correctness and implementation of abstract data types[END_REF], and has been popularised by the movement of Algebra of Programming [START_REF] Bird | Algebra of programming[END_REF]. The general methodology of the initial semantics can be described according to the following steps:

1. Introduce a notion of signature (for the category C).

Construct a notion of associated model, organizing into a category with a functor

to the category C.

3. Define the object specified by the signature as the initial model, if it exists (the signature is then called effective).

4. Find a sufficient condition for a signature to be effective7 .

The models of a signature form the domain reached by the principle of recursion, which is induced by the initiality of the object specified by the signature.

In Chapter 2, we define a general notion of signature to characterize an object of an arbitrary category C, with its associated category of models. Such a signature is given by a list of families of arities specifying operations or equations. The remaining chapters provide various special cases, from the specification of the syntax to the specification of the semantics. Each time, we identify a class of effective signatures.

Finally, we propose a protocol based on a three-level signature to specify a programming language:

1. specification of constructions, for example a binary operation +; 2. specification of equations, for example a + b = b + a (commutativity the binary operation);

3. specification of reductions between terms, for example 0 + a a, by schematic rules.

The first two points define what we call the syntax of the programming language, while the last point concerns the semantics of language: a reduction between two terms is a program execution path evolving from the first term to the second. As an example of language integrating the three levels, we propose in the section 5.6 a specification of lambda calculus with explicit substitution described in [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF].

In order to motivate the mathematical notions involved, we examine in this summary the simplest functional programming language that can be considered: the pure lambda calculus. In section 1.2.1, we give a first presentation of its syntax, and endow it with an operation of substitution. We then explain, in section 1.2.2, how the mathematical notion of monad can account for it, then, in the section 1.2.3, how the notion of morphism of modules provides a way to express an essential property of the constructions of the syntax: compatibility with substitution. In the section 1.2.4, we characterize the syntax by its principle of recursion, which we formulate by a property of initiality. We explain in section 1.2.5 that specify this property of initiality requires an adequate notion of model, which is determined by the signature: this is the opportunity to present our general definition of signature to specify objects of an arbitrary category. We examine then the case of syntaxes satisfying equations (section 1.2.6), before approaching, in section 1.2.7, the specification of semantics, modeled as part of the reduction monads by a set of reductions between each pair of terms.

Naive presentation of the lambda calculus syntax

We give here a presentation of the syntax of lambda calculus, as well as a overview of some of the difficulties usually associated with such a presentation. We fix an infinite set V of variables, and we characterize recursively all of the valid terms or expressions of the lambda calculus:

• each variable x ∈ V is a term of the lambda calculus,

• if t and u are terms, then t u is a term, called application of t to u ;

• if t is a term, then λx.t is a term, called lambda abstraction of t, where x is a variable that can appear in t.

The expression λx.t corresponds to the mathematical notation x → t. It is about defining a function depending on the variable x, the body of this function being given by the term t. The expression f t corresponds to the mathematical notation f (t): it is the application of the function f to the argument t.

In mathematics, the name of the variable chosen to define a function is purely conventional: the functions x → f (x) and y → f (y) are identical. Let us transpose this identification into the language of lambda calculus: we want to equalize the term λx.t with the term λy.t ′ , where t ′ is obtained from the term t by replacing all occurrences of the variable x with the variable y. In this situation, we say that x is a variable bound in λx.t, and the occurrences of x in t are then qualified as bound. Occurrences of variables that are not bound are said free. 8Here, the terms λx.t and λy.t ′ are said α-equivalent. More generally, two terms are α-equivalents if we can rename the bound variables of one to get the other term. The precise definition of the α-equivalence requires some precautions. For example, in the previous case, it is implied that the variable y does not appear in t; otherwise, we would identify (against our will) the terms λx.y and λy.y.

Introduction

Substitution is another essential aspect of the syntax of lambda calculus: given a term t, if we replace all (free) occurrences of a variable x by the same term u, we get a new valid expression, which we note t{x := u}. The substitution operation allows to express the following mathematical intuition: the result of a function x → t applied to an argument u is obtained by replacing the variable x in t by u. This statement is transposed, for the lambda calculus, in the β-equation

(λx.t) u = t{x := u}.
(1.4)

This so-called unary substitution is a special case of the operation of simultaneous substitution t{x → u x }, which replaces simultaneously each variable of a term t by a corresponding term.

Substitution only replaces the free occurrences of a variable, so as to preserve the following property: given two terms λx.t and λy.t ′ assumed α-equivalent, replacing the same variable with the same term yields two α-equivalent terms. If the involved variable is identical to the abstracted variable, the term (λx.t){x := u} is simply equal to λx.t: for example (λx.x){x := u} = λx.x is indeed α-equivalent to (λy.y){x := u} = λy.y.

The lambda calculus monad

The concept of monad provides a mathematical counterpart to the intuitive notion of syntax with a substitution operation. We motivate this definition by the example of the lambda calculus. In the point of view that we adopt here, the α-equivalent terms are considered identical: thus, λx.x = λy.y.

Instead of considering a single set of terms with a set V of variables fixed in advance, we define classes of terms which use the same set of free variables. Let L(X) be the set of terms whose free variables are selected from the set X. Note that a term t ∈ L(X) is also found in L(Y ) for any inclusion X ⊂ Y : indeed, if the free variables are chosen from the elements of a set X, they are also chosen from the elements of any superset Y of X.

Any variable is in particular a valid term: there is an inclusion var X : X → L(X) for any set X. On the other hand, if one gives for all variable x ∈ X a term u x whose free variables are chosen in Y , we get, from any term t ∈ L(X), a term t{x → u x } ∈ L(Y ). This simultaneous substitution operation satisfies the following properties:

• each variable is replaced by the appropriate term:

x ′ {x → u x } = u x ′
• identity substitution is neutral:

t{x → x} = t
• any succession of substitutions is equivalent to a composed substitution:

t{x → u x }{y → v y } = t{x → u x {y → v y }}
The inclusion of variables in terms and the simultaneous substitution operation satisfying the equations above define a monad on the category of sets. This mathematical object is at the heart of developments that we expose in this thesis.

Constructions are morphisms of modules

The mathematical concepts of modules and morphisms of modules provide a framework for expressing the compatibility of a construction in the syntax with the substitution operation. We illustrate this with the t u application of the lambda calculus.

The compatibility of the application with the substitution results in the commutation

(t u){x → v x } = t{x → v x } u{x → v x }
Informally, this equation means that there is no difference between performing the substitution before the application and performing the substitution after the application, as

L(X) × L(X) (t, u) a p p li c a ti o n ' ' L(Y ) × L(Y ) (t{x → v x }, u{x → v x }) w w s u b s ti tu ti o n a p p li c a ti o n ' ' L(X) t u L(Y ) t{x → v x } u{x → v x } w w s u b s ti tu ti o n
This observation implicitly relies on the following substitution operation of which the collection of sets (L(X) × L(X)) X :

(t, u){x → v x } = (t{x → v x }, u{x → v x })
This substitution verifies the following properties:

• identity substitution is neutral:

(t, u){x → x} = (t, u)
• any succession of substitutions is equivalent to a single compound substitution:

(t, u){x → u x }{y → v y } = (t, u){x → u x {y → v y }}
As such, the collection of sets of terms pairs defines a module over the monad L , which we note L × L.

The definitions of monad and module are similar. Every monad defines a module on itself. In fact, L × L also defines a monad, but the associated substitution does not derive from its module structure. Given a pair of terms (t, u) whose free variables are chosen in X, and for any variable x ∈ X, a pair of terms (v x , w x ) whose free variables are chosen in Y , this monadic substitution provides a pair of terms whose free variables are in Y . The given substitution by the module structure is not appropriate, since it does not apply to the case where each variable is associated with a term in the monad L, rather than a pair of terms.

The application of lambda calculus induces a collection of functions

L(X) × L(X) → L(X)
that associate with any pair (t, u) the term t u. The commutativity property with the aforementioned substitution makes it a morphism of modules from L × L to L, where L is seen as a module on the homonymous monad.

Similarly, the abstraction of lambda calculus induces a collection of functions

L(X ∐ {⋆}) → L(X)
which to any term t whose free variables are chosen in the set X extended with a new ⋆ element, associates the term λ ⋆ .t. The family L(X ∐ {⋆}) X is canonically equipped with an operation of substitution and therefore defines a module. The collection of functions of abstraction then induces a morphism of modules, due to the commutation with substitution:

(λ ⋆ .t){x → u x } = λ ⋆ .   t      x →      ⋆ if x = ⋆ u x otherwise.        
The module construction that we encounter here generalizes to any module M on a monad R: the derived module M ′ is defined as the collection of sets (M (X ∐ {⋆})) X equipped with a canonical substitution operation.

In this thesis, we are interested exclusively in programming languages whose constructions and reductions are compatible with substitution, hence our interest in the notions of module and morphism of modules.

Recursion and initiality

The naive presentation of lambda calculus naturally induces a principle of recursion on the syntax. Suppose, for example, that we want calculate the set of free variables of a term t of the lambda calculus. To do this, we reason by recursion on the structure of the term. If t is a x variable, then the set of its free variables is the singleton {x}. If t is an application u v, then the set of its free variables is the union of the free variables of u and v. If t is a lambda abstraction λx.u, then any free variable of u different from x is a free variable of t.

In our framework, we adopt the point of view of Initial Semantics: the principle of recursion is then a consequence of a property of initiality. The lambda calculus is thus characterized as the "minimal" monad provided with an application and a lambda abstraction, in a sense that we will illustrate with the example of computation of free variables (this example is studied more formally in Section 3.5.2).

Consider the monad P that associates to X its powerset P(X): a variable x ∈ X induces a "term" {x} ∈ P(X) ; the substitution t{x → u x } is calculated by the meeting ∪ z∈t u z . The union of two subsets provides a binary operation for P, which we call an "application operation" by analogy with the binary application operation of the lambda calculus. This operation associates the subset t ∪ u to the pair (t, u). Similarly, an adequate abstraction operation P(X ∐ {⋆}) → P(X) is given by t → t ∩ X, or equivalently, by t → t\{x}. As we will explain in the following section, these constructions make the monad P a model of the signature of lambda calculus.

The initiality property of the mentioned lambda calculus then instantiates by the existence of a single family of functions (free X : L(X) → P(X)) X verifying the following properties:

• free preserves the variables: free X (var(x)) = {x} (remember that for the monad P, the variable x is seen as the subset {x})

• free preserves the substitution:

free Y (t{x → u x }) = z∈free X (t) free Y (u z )
• free preserves the application: free(t u) = free(t) ∪ free(u)

• free preserves abstraction:

free(λx.t) = free(t)\{x}
The first two points characterize free as a morphism of monads between L and P. The following section defines the notion of model so that L and P, with their respective operations of application and abstraction, are models of the signature of the lambda calculus. The morphism of monads free is then a morphism of models of this signature, thanks to the last two points.

Signatures and models (Chapter 2)

In Chapter 2, we define a general notion of signature, as a list of families of arities, to characterize an object of an arbitrary category C. An arity is given by a functor diagram

C u / / o o v / / D .
where u and v are sections of the functor F : D → C, that is, functors which, postcomposed with F , yield the identity functor on C. An object c of C is euqipped with an action of this arity if it is equipped with a morphism h : u(c) → v(c) whose image by F is the identity morphism in c. Note that if the only morphisms mapped by F to identity morphisms are themselves identity morphisms, then an object c is equipped with an action if and only if u(c) = v(c). We call equational such an arity.

Objects equipped with an action of a (fixed) family of arities form a category: morphisms are those of the category C satisfying a commutation condition with the actions. This is how the category of models of a signature consisting of a single family of arities is defined. For example, the category of algebras of an endofunctor G : C → C is the category of models of the signature consisting of a single arity

C (G,Id C ) / / o o (Id C ,Id C ) / / C × C
where the functor C × C → C is the second projection.

As we said, a signature is a list of families of arities: a first family of arities for the base category C, then a family of arities for the induced category of models, and so on.

We illustrate these definitions with the monadic signatures (that is, signatures specifying monads) that we consider in Chapter 3, consisting of a single arity. Consider the example of the syntax of lambda calculus. In the previous section, we characterized it as the initial monad equipped with an application and an abstraction. More specifically, generalizing the example of the powerset monad P studied in the previous section we say that a monad R is equipped with application and abstraction if it has both a binary operation, that is to say a morphism of modules app R : R × R → R, and a module morphism abs R : R ′ → R. Equivalently, it is a monad R with a morphism of modules from (R × R) ∐ R ′ to R, that is, an action of the arity

Mon Σ LC / / o o Θ / / Mod (1.5)
that we now detail: Mon is the category of monads; Mod gather all the category of modules over different monads:9 an object is a pair of a monad et a module over this monad, and a morphism between (R, M ) and (S, N ) is a pair of a monad morphism f : R → S and a module of morphisms g : M → f * N over the monad R, where f * N is the module over R built canonically out of N , by precomposing its substitution operations with f . The functor Mod → Mon is the first projection. A section of this functor, or parametric module, maps functorially any monad R to a module over itself. For example, the parametric module Θ maps a monad R to the module R (recall indeed that any monad is canonically a module over itself). The parametric module Σ LC of lambda calculus maps any monad R to the module (R × R) ∐ R ′ over R.

A parametric module Σ induces an arity, as does Σ LC in Equation 1.5. Let us consider the category of models associated to the signature consisting of this unique arity. A model (R, ρ) (sometimes simply noted R) of this signature is then a monad R with a module morphism ρ : Σ(R) → R. Thus, the powerset monad P and the lambda calculus monad L induce models of Σ LC . In fact, the lambda calculus is the initial model: if R is a model, then there is a unique morphism of monads f : L → R which preserves binary operation and abstraction.

More generally, the monad S specified by a signature induced by a parametric module Σ is equipped with an action σ : Σ(R) → R which makes it the initial model: given a model (R, ρ), there exists a unique morphism of monads f : S → R which preserves the model structure, i.e., verifying for any t ∈ Σ(R)(X)

f (σ(t)) = ρ(f (t)) (1.6)
Such a morphism of monads constitutes what a morphism of models between (S, σ) and (R, ρ). Note that the right-hand side of Equation 1.6 requires making sense of the expression f (t) when t is an element of Σ(S) X : by functoriality of Σ, this is just Σ(f ). Indeed, any morphism of monads f : R → T induces a morphism of modules Σ(R) → f * Σ(T ) on the monad R, morphism that we denote Σ(f ), or just f . The effectivity of a signature induced by a parametric module, that is, the existence of the associated initial model, is not systematic.10 This is nevertheless the case with any parametric module that we call algebraic, which specifies a syntax that has a set of n-ary operations, some of which bind variables in their arguments. The signature of lambda calculus comes from an algebraic parametric module: the application is a classic binary operation, while abstraction is a unary operation binding a single variable in its unique argument.

Syntaxes with equations (Chapters 3 and 4)

The syntax of a language is sometimes defined modulo some equations: this is the case of the differential lambda calculus [START_REF] Ehrhard | The differential Lambda-calculus[END_REF], of the pi calculus with its structural congruence rules, and of lambda calculus with explicit substitution as described in [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF]. An example of possible equation for the lambda calculus is given by the the β-equivalence (λx.t) u = t{x := u} for the lambda calculus, is common practice. In this thesis, we deal with the specification of monads corresponding to languages satisfying this kind of syntactic equations.

In Chapter 3, we study the parametric modules that we call presentable: these are, in a way, quotients of algebraic parametric modules. A signature induced by a presentable parametric module is also called presentable. We show that such a signature is effective (Theorem 57). It becomes possible to specify a commutative binary operation (Section 3.8.1). For that, it suffices to notice that the data of such an operation is equivalent to the data of an operation taking as argument an unordered pair of terms. Now let us describe the associated presentable parametric module Σ comm-bin : this is a quotient of the algebraic parametric module Σ bin of a binary operation that associates to any monad R the module R × R. More specifically, to any monad R, the parametric module Σ comm-bin associates the module (S 2 R(X))) X , where S 2 R(X) is the set of pairs of elements of R(X) × R(X) quotiented by the relation (t, u) ∼ (u, t), that is, the set of unordered pairs. The syntax then comes with an operation that takes as argument a non ordered of pair of terms, as desired.

Nevertheless, the class of presentable signatures seems limited. Consider the example of an associative binary operation: we do not know how to give a signature, presentable or not. Note that we can nevertheless give an intuitive definition of model in this particular case: it is a monad R equipped with a binary operation b : R × R → R such that for all x, y, z in R(X) the expressions b(b(x, y), z) and b(x, b(y, z)) are equal. In other words, it is a model (R, b) of the signature of a binary operation, such that the two morphisms of R-modules from R × R × R to R, associating to any triple (x, y, z) the two considered expressions are equal.

In Chapter 4, we give a definition of equations generalizing this example for models of any monadic signature Σ: this is the data,

• for each R model of the signature Σ, of two morphisms of modules e R , e ′ R with the same domain A R and codomain B R (in the example above, e R , e ′ R :

R×R×R → R associate respectively b(b(t, u), v) and b(t, b(u, v)) to the same triple (t, u, v) ∈ R 3 (X));
• for any morphism of f : R → S models, of two morphisms of modules A f : A R → A S and B f : B R → B S such that following diagrams commute:

A R e R / / A f B R B f A S e ′ S / / B S A R e ′ R / / A f B R B f A S e ′ S / / B S
These data are submitted as usual to an additional condition of functoriality. It is said that a model R of the signature Σ satisfies the equation when e R = e ′ R . In fact, we give an equivalent definition of equation in Chapter 4, as particular equational arities. A monad satisfies the equation if and only it is equipped with an action of the arity.

We then consider 2-signatures: they are signatures consisting of an arity induced by a parametric module and a family of these equational arities. A model (or 2-model) of a 2-signature is a model R of the signature induced by the underlying parametric module that satisfies all the equations. A 2-signature is said algebraic if the underlying parametric module is, and if the equations are elementary (Definition 104). Technically, they are equations whose functorial action of the domain sends surjective morphisms of monads on surjective morphisms of functors, and whose codomain is of the form R → (((R ′ ) ′ ) ... ) ′ . All the examples of presentable signature that we consider in Chapter 3 can be reformulated as an algebraic 2-signature, inducing the same category of models (up to isomorphism). We show that any algebraic 2-signature is effective. (Theorem 107).

Semantics (Chapters 5 and 6)

It is possible to specify by a 2-signature the syntax of the lambda calculus quotiented by the β-equivalence (1.1): the terms (λx.t) u and t{x := u} are thus equalized. However, this equation is usually oriented, and considered as an execution step when we consider lambda calculus as a functional programming language. As such, it is more appropriate to integrate the β-reduction into the semantics of language, rather than impose the β-equation in the syntax. This motivates the concept of reduction monad, which we introduce in the chapter 5, extending that of monad, to account for the additional structure of reduction. Intuitively, a reduction monad is a monad R equipped, for each pair of terms (t, u) ∈ R(X), with a set of reductions between t and u that we note t ◮ u, and an associated substitution operation: for any family of terms (v x ) x∈X with v x ∈ R(Y ), for any reduction m between t and u, this substitution associates a reduction m{x → v x } between t{x → v x } and u{x → v x }. Equations analogous to those involved in the definition of module are required.

In this context, a reduction signature consists of a signature for monads, that is to say a 2-signature, and a family of reduction rules. For example, the reduction rule for the congruence of the application of the lambda calculus is informally expressed as follows, by explicitly designating the application of the lambda calculated by the app construction:

T T ′ U U ′ app(T, U ) app(T ′ , U ′ )
This rule breaks down into three pairs of terms: the hypotheses (T, T ′ ) and (U, U ′ ), and the conclusion (app(T, U ), app(T ′ , U ′ )), constructed from the "metavariables" T , T ′ , U , and U ′ . These parameterized pairs induce pairs of morphisms

(h 1,1 (R), h 1,2 (R)), (h 2,1 (R), h 2,2 (R)) and (c 1 (R), c 2 (R)) of R-modules between R 4
and R for any model R of the monadic signature of lambda calculus. In addition, this construction is functorial. More precisely, if f : R → S is a morphism of models, then the following diagrams are commutative:

R 4 f 4 h i,j (R) / / R f S 4 h i,j (S) / / S R 4 f 4 c i (R) / / R f S 4 c i (S)
/ / S Thus formulated, this rule of congruence fits into our definition of reduction rule detailed in Section 5.3. An action of this rule in a reduction monad R equipped with a binary operation app is given by a reduction app-cong(m T , m U ) between app(T, T ′ ) and

app(U, U ′ ), for all (T, T ′ , U, U ′ ) ∈ R 4 (X)
, any reduction m T between T and T ′ , and any reduction m U between U and U ′ . It is moreover necessary that app-cong commutes with substitution, that is, the following equation is verified:

app-cong(m T , m U ){x → v x } = app-cong(m T {x → v x }, m U {x → v x })
The main theorem (Theorem 150) of Chapter 5 asserts the effectivity of a reduction signature composed of an effective 2-signature and any family of reduction rules.

Let us detail the involved notion of model here: it is a reduction monad equipped with • a model structure of the 2-signature for the underlying monad,

• an action of each reduction rule of the signature.

The initial model is built from the initial model of the 2-signature, and the additional structure of reductions is built inductively from the reduction rules. Besides some signatures for variants of lambda calculus with β-reduction, we propose in the section 5.6 a signature for the lambda calculus with explicit substitution, as described in [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF], as a set of opertaions subject to a syntactic equation, with the addition of reduction rules between terms. This specification is done in three steps: a 1-signature for language operations, a 2-signature taking into account the syntactic equation, and a reduction signature specifying the relevant reductions.

In Chapter 6, we generalize these developments, and deal with new examples, such as lambda calculus in call by value with big-step reductions: the syntax is that of lambda calculus, but in this variant, a term reduces to a value, that is to say in a variable or a lambda abstraction. The notion of value is not stable by arbitray substitutions: for example, x{x := y y} = y y is not a value. On the other hand, it is stable by substitution of values: v and (w x ) x∈X are values, then v{x → w x } is a value. We can thus define the monad LC v of the values of lambda calculus: it is equipped with an inclusion in the monad L of lambda calculus that allows us to consider the latter as a module over LC v .

In this variant of lambda calculus, the β-reduction is formulated as:

t λx.t ′ u u ′ t ′ {x := u ′ } v t u v
Another reduction rule ensures that any value, as a term, reduces to itself.

The reductions are stable by substitution

: if t ∈ L(X) reduces to a value v ∈ LC v (X) and (u x ) x∈X is a family of values indexed by the set of free variables X, then t{x → u x } reduces to v{x → u x }.
The collection of sets of reductions between a term and a value is defined by induction, by successively applying the redution rules. It is equipped with an adequate substitution operation, as explained previously.

Note that a lambda term can be represented by a binary tree whose leaves are values and the nodes correspond to applications. This induced representation yields a bijection: such a binary tree determines a lambda term in a unique way. Thus we can identify the module L of lambda terms with the composition B •LC v , where B is the monad of binary trees: B(X) is the set of binary trees whose leaves are chosen in X.

Inspired by this example, we define the concept of operational monad. It consists of

• a monad R (in our example, R = LC v );
• a pair (T 1 , T 2 ) of endofunctors on Set (in our for example, T 1 = B and T 2 = Id);

• a set of reductions between t and u for each pair

(t, u) ∈ T 1 (R(X)) × T 2 (R(X));
• an appropriate substitution operation on these sets of reductions.

We then define the operational signatures that allow to specify this type of mathematical object, and prove an initiality result for these signatures (Theorem 207).

Formalization

Proofs of the main results of chapters 3 and 4 have been verified using the Coq proof assistant. This is a software in which it is possible to reproduce (or formalize) mathematical definitions as well as proofs which, if validated by the software, are indisputable in principle. This guarantee must in practice be qualified: software bugs allowing to prove contradictory statements are regularly found (and corrected). Furthermore, the correspondance between statements proved in Coq's type theory and mathematical statements is a non obvious theoretical question. More pragmatically, it is possible to make a mistake in the formalization of a definition, and the software Coq does not help in this step. It happens, for example, that we formalize a wrong characterization of a given set, this characterization being contradictory. This error may not be noticed because it does not prevent to show that the elements of this set satisfy some mathematical property, as the elements of the empty set satisfy any property. The reader of a formalization can thus certainly dispense to check the demonstrations, but he must pay close attention to the definitions.

For our developments, we chose to rely on the Coq library UniMath. This has some advantages, despite a "size" issue (which we will briefly mention): i it contains useful definitions and results for our purpose;

ii it uses a limited amount of language features; iii it incorporates the axiom of univalence and many of its consequences.

Regarding point i, UniMath proposes, among other things, an implementation of the theory of categories, and quotients of sets.

Point ii limits the complexity of the type theory in which we must trust, although this argument is highly questionable in view of the size issue. It also reduces the risk to be confronted with implementation bugs, by restricting itself to tried and tested features of Coq.

The axiom of univalence mentioned in point iii as such is not used crucially. It has the advantage, however, of gathering in this single axiom a number of useful consequences, for example functional extensionality (two functions are equal if they send each element on the same image), or propositional extensionality (logically equivalent propositions are equal) which makes it possible to handle the notion of subset.

Finally, the UniMath library has a major flaw due to a "size" issue. Indeed, it requires a compilation option that makes the system contradictory, allowing the implementation of a variant of Russel's paradox. This option is in practice used in the (impredicative) definition of quotients. We have ignored the existence of this particular inconsistency in the system in the proofs that we have formalized. We thus believe that our formalization does not exploit this logical flaw.

Synopsis

We give a synopsis of this thesis before presenting related work.

Chapter 2 concerns an arbitrary category C and presents a general notion of signature to specify objects of this category. Each of other chapters concerns a single category C and provides a class of effective signatures specifying objects of this category.

In Chapters 3 and 4, we have C = Mon the category of monads on Set. They are respectively adapted from [START_REF] Ahrens | High-level signatures and initial semantics[END_REF] High-level signatures and initial semantics and [Ahr+19b] Modular specification of monads through higher-order presentations.

In Chapter 5, C is the category of reduction monads, which model both the syntax (as a monad) and the semantics of a language. We generalize them in Chapter 6 where we focus on the category of operational monads.

We suppose a certain familiarity with category theory and basic notions such as categories, functors, natural transformations, monads.

Computer-checked formalization

The intricate nature of our main results made it desirable to provide a mechanically checked proof of these results. We achieved this work for Chapters 3 and 4.

Our computer-checked proof is based on the UniMath library [VAG+], which itself is based on the proof assistant Coq [START_REF]The Coq Proof Assistant, version 8.9[END_REF]. The main reasons for our choice of proof assistant are twofold: firstly, the logical basis of the Coq proof assistant, dependent type theory, is well suited for abstract algebra, in particular, for category theory. Secondly, a suitable library of category theory, ready for use by us, had already been developed [START_REF] Ahrens | Displayed Categories[END_REF].

The formalization can be consulted on https://github.com/UniMath/largecatmodules. A guide is given in the README.

For the purpose of this thesis, we refer to a fixed version of our library, with the short hash 50fd617. This version compiles with version 10839ee of UniMath.

Throughout the thesis, statements are annotated with their corresponding identifiers in the formalization. These identifiers are also hyperlinks to the online documentation stored at https://initialsemantics.github.io/doc/50fd617/index.html.

Related work 1.5.1 General signatures

A general notion of signature as an endofunctor with strength 11 (on a monoidal category) is suggested in the work on syntax of Fiore and his collaborators, starting with [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF]. This notion is also studied in Matthes and Uustalu [START_REF] Matthes | Substitution in non-wellfounded syntax with variable binding[END_REF] and Ghani, Uustalu, and Hamana [START_REF] Ghani | Explicit substitutions and higher-order syntax[END_REF]. Their treatment rests on the technical device of strength that we avoid here. Any such signature gives rise to a signature in our sense (cf. Proposition 44 for the particular case of specifying monads).

Fiore and Hur's equational systems [FH09] yield a notion of signature which generalize signatures with strength (see [FH09, Section 6.1]). In this article, the authors provide a notion of equation for an algebra of an endofunctor, yielding a subcategory of algebras satisfying this equation as a definition of category of models, equipped with a forgetful functor to the base category. Equational systems yield particular signatures in our sense (Example 14), but contrary to the work of Fiore and Hur, we don't provide a general sufficient condition ensuring an initiality result.

Syntax and monads

In a classical paper, Barr [Bar70] explained the construction of the "free monad" generated by an endofunctor 12 . In another classical paper, Kelly and Power [START_REF] Kelly | Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads[END_REF] explained how any finitary monad can be presented as a coequalizer of free monads 13 . There, free monads correspond to our initial models of a signature by an algebraic parametric module without any binding construction.

Fiore, Plotkin, and Turi [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF] develop a notion of substitution monoid. Following [START_REF] Altenkirch | Monads need not be endofunctors[END_REF], this setting can be rephrased in terms of relative monads and modules over them [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF]. Accordingly, our present contributions could probably be customised for this "relative" approach.

Hamana [START_REF] Hamana | Term Rewriting with Variable Binding: An Initial Algebra Approach[END_REF] proposes initial algebra semantics for "binding term rewriting systems", based on Fiore, Plotkin, and Turi's presheaf semantics of variable binding and Lüth and Ghani's monadic semantics of term rewriting systems [START_REF] Lüth | Monads and Modular Term Rewriting[END_REF].

The work by Fiore with collaborators [FPT99; FH10; FM10] and the work by Uustalu with collaborators [MU04; GUH06] share two traits: firstly, the modelling of variable binding by nested abstract syntax, and, secondly, the reliance on tensorial strengths in the specification of substitution.

The signatures for monads that we present here is actually closely related to that of Fiore and collaborators:

• Our notion of equations and that of model for them in Chapter 4 is very close to the notion of equational systems and that of algebra for them in [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF]: in particular, the preservation of epimorphisms, which occurs in their construction of inductive free algebras for equational systems, appears here in our definition of elementary equation.

• In [START_REF] Fiore | Second-Order Equational Logic (Extended Abstract)[END_REF], Fiore and Hur 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 ∈ T (∅, 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. That monadicity result is furthermore an instance of a more general theorem by Fiore and Mahmoud [FM10, Theorem 6.2].

• Translations between languages similar to the translation we present in Section 5.7 are also studied in [START_REF] Fiore | Second-Order Algebraic Theories (Extended Abstract)[END_REF]. It would be interesting to understand formal connections.

• At this stage, our work only concerns untyped syntax, but we anticipate it will generalize to the sorted setting as in [START_REF] Fiore | Second-Order Equational Logic (Extended Abstract)[END_REF] (see also the more general [START_REF] Fiore | Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic[END_REF]).

We should mention several other mathematical approaches to syntax. Gabbay and Pitts [GP99] employ a different technique for modelling variable binding, based on nominal sets. This nominal approach to binding syntax has been actively studied 14 . We highlight some contributions:

• Clouston [START_REF] Clouston | Binding in Nominal Equational Logic[END_REF] discusses signatures, structures (a.k.a. models), and equations over signatures in nominal style.

• Fernández and Gabbay [START_REF] Fernández | Closed nominal rewriting and efficiently computable nominal algebra equality[END_REF] study signatures and equational theories as well as rewrite theories over signatures.

• Kurz and Petrisan [START_REF] Kurz | On universal algebra over nominal sets[END_REF] study closure properties of subcategories of algebras under quotients, subalgebras, and products. They characterize full subcategories closed under these operations as those that are definable by equations. They also show that the signature of the lambda calculus is effective, and study the subcategory of algebras of that signature specified by the β-and η-equations.

Yet another approach to syntax is based on Lawvere Theories. This is clearly illustrated in the paper [START_REF] Hyland | The category theoretic understanding of universal algebra: Lawvere theories and monads[END_REF], where Hyland and Power also outline the link with the language of monads and put in an historical perspective.

Finally, let us mention the classical approach based on Cartesian closed categories recently revisited and extended by T. Hirschowitz [START_REF] Hirschowitz | Cartesian closed 2-categories and permutation equivalence in higher-order rewriting[END_REF].

Semantics

Structural operational semantics (SOS) are tackled by the seminal paper of Turi and Plotkin [START_REF] Turi | Towards a mathematical operational semantics[END_REF]. It introduced a largely accepted setting, rich of results and examples. However, this setting does not cover languages with binding constructions. The extension of this setting to the binding cases has been explored, notably by Staton [START_REF] Staton | General Structural Operational Semantics through Categorical Logic[END_REF], but it does not cover lambda calculus. Several first steps towards it have been proposed [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF][START_REF] Lüth | Monads and modular term rewriting[END_REF], where reductions are modeled by preorders. We propose a new one, based on graphs of reductions, starting with the reduction signatures in Chapter 5. They allow for the specification of 1. term constructions, including constructions that bind variables, e.g., abstraction; 2. syntactic equalities between terms; and 3. reduction rules, including reduction rules with hypotheses, e.g., congruence rules for the term constructions.

Ahrens [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF] gives a notion of signature that allows for the specification of syntax with binding operations, as well as reduction rules on that syntax. The format for reduction rules considered there does not allow expressing rules with hypotheses, e.g., the aforementioned congruence rules. Instead, the congruence rules are hard-coded in [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF], so that the head-β-reduction (and other limited variants) cannot be specified by that formalism. The constructors are modelled by morphisms of modules between modules into preordered sets, i.e., by families of preorder-preserving maps. Signatures for rewriting systems, and initial semantics for them, are given by Hamana [START_REF] Hamana | Term Rewriting with Variable Binding: An Initial Algebra Approach[END_REF] under the name "binding term rewriting system (BTRS)". Hamana considers preorder-valued functors. There, signatures for rewrite rules allow for rules without hypotheses only, though some rules with hypotheses, in particular, congruence rules, seem to be hard-coded in Hamana's framework (see [START_REF] Hamana | Term Rewriting with Variable Binding: An Initial Algebra Approach[END_REF]Figure 3]).

CHAPTER 2

GENERAL SIGNATURES

In this chapter, we give an abstract notion of signature for specifying objects of a category C. All the notions of signatures presented in this manuscript are instances of these. In Chapters 3 and 4, we study the case when C = Mon the category of monads on sets; in Chapter 5, we focus on the case when C is the category of reduction monads, and in Chapter 6, we consider the more general category of operational monads.

For each signature S, there is an associated category of models C S equipped with a forgetful functor U S : C S → C. For example, the category of models of the empty signature is just C. By definition, the object of C specified by a signature S is the image by U S of the initial model, if any.

For each signature S, we define a notion of S-arity, specifying operations or equations. A family E of such arities induces an extended signature S, E, equipped with a functor

U E from C S,E to C S , factorizing U S,E : C S,E → C.
Any signature is constructed inductively in this manner from the empty signature.

Arities over a category

We first define arities over a category C, fixed in this section. Then, S-arities will be defined as arities over the category of models of the signature S.

We define what is an action of an arity in an object c ∈ C, and the associated notion of compatible morphism of C between objects equipped with such an action.

We begin by introducing the general notion of arity over a category in Section 2.1.1, before considering the particular case of equational arities in Section 2.1.2, allowing to specify equations.

General arities

Definition 1. An arity over C is a quadruple (D, a, u, v) consisting of:

• a category D;

• a functor a : D → C;

• two sections u, v : C → D of a : D → C.
Remark 2. We will mainly consider the case where a is a Grothendieck fibration. In this case, thanks to the Grothendieck construction, an arity over C can be defined as a pseudo functor a : C o → Cat, and two natural transformations u, v : 1 → a, where 1 is the terminal functor from C to Cat.

Example 3. Any endofunctor F : C → C induces an arity (D, a, u, v) specifying algebra structures for this endofunctor, as we will explain in Example 6:

• a : C × C → C is the first projection; • u = Id C , F maps an object c to the pair (c, F (c));
• v is the diagonal functor, mapping an object c to (c, c).

Next, we define the notion of action of an arity in an object of C, and the associated notion of compatible morphism of C.

Definition 4. An action of an arity

A = (D, a, u, v) in an object c ∈ ob C is a morphism h : u(c) → v(c) such that a(h) = id c .
Definition 5. Let A = (D, a, u, v) be an arity over C. Let c 1 and c 2 be two objects of C equipped with actions h 1 : u(c 1 ) → v(c 1 ) and h 2 : u(c 2 ) → v(c 2 ). A morphism f : c 1 → c 2 is compatible with the actions h 1 and h 2 if the following diagram commutes:

u(c 1 ) h 1 / / u(f ) v(c 1 ) v(f ) u(c 2 ) h 2 / / v(c 2 )
Example 6. Let F be an endofunctor on C. In Example 3, we constructed from it an arity . An action of it in an object c ∈ ob C is a morphism h : F (c) → c. A compatible morphism between c and c ′ equipped with actions h and h ′ is a morphism between the induced algebras of F .

Equational arities

Definition 7. An arity (D, a, u, v) over C is said equational if for every object c ∈ C, the category a -1 (c) is discrete (that is, any morphism is an identity morphism), where a -1 (c) is the subcategory of objects of D mapped to c and morphisms mapped to id c by a.

Remark 8. Let (D, a, u, v) be an arity. If a is a Grothendieck fibration, then this arity is equational if and only if a is a discrete fibration.

Remark 9. An action of an equational arity (D, a, u, v) in an object c ∈ C is always an identity morphism. Thus, an object c is equipped with an action if and only if

u c = v c .
Any morphism is then compatible with actions of an equational arity.

Example 10. An equational system [FH09] induces an equational arity over a category of algebras. More precisely, an equational system S = (C : Σ ⊲ Γ ⊢ L = R) consists of endofunctors Σ, Γ : C → C, and functors L, R : Σ -alg → Γ -alg between categories of algebras preserving the underlying object, that is, such that the following diagram commutes:

Σ -alg L / / R / / " " Γ -alg | | C .
Such a structure defines an equational arity (D, a, u, v) over the category Σ -alg as follows.

• D is the category of objects c ∈ C equipped with an algebra structure for both Σ and Γ. More formally, D is defined as the pullback

D / / a Γ -alg Σ -alg / / C .
• a : D → Σ -alg is induced by the definition of D as a pullback.

• u maps a Σ-algebra c to the underlying object of c equipped with the same Σalgebra structure and the Γ-algebra given by L(c).

• v maps a Σ-algebra c to the underlying object of c equipped with the same Σalgebra structure and the Γ-algebra given by R(c).

Then, the category of S-algebras [FH09, Definition 3.4] is retrieved as the category of objects of Σ -alg equipped with an action of this arity and compatible morphisms. More concretely, it is the full subcategory of algebras of Σ that have the same image by L and R.

Family of arities and their models

Definition 11. Let E be a family of arities over C. The category C E of models of E is defined as follows:

• objects are objects c of C equipped with an action of each arity in E;

• morphisms are those which are compatible with the action of any arity in E.

• composition and identities are the obvious ones.

It is equipped with a forgetful functor

U E : C E → C.

Signatures over a category

Here we define signatures and their models.

Definition 12. A signature over a category C is a finite list E 1 , . . . , E n consisting of families of arities over categories such that:

• E 1 is a family of arities over C.

• each E i is a family of arities over the category of models of E i-1 , for i > 1.

The empty list is called the empty signature. The category of models C S of a signature S = E 1 , . . . , E n is defined as the category of models of E n , if n > 0, or as C otherwise. Given a signature S, a S-arity is an arity over the category of models C S . Each signature S = E 1 , . . . , E n is equipped with a forgetful functor U S from its category of models to C defined as the composition: In the following chapters, we consider different instances of signatures:

C En U En / / C E n-1 U E n-1 / / . . . / / C E 1 U E 1 / / C An action of a signature S = E 1 , . . . , E n in an object c ∈ ob C is an action of E 1 in c, inducing a model m 1 of E 1 ,
• In Chapter 3, signatures consist of a single arity over the category of monads.

• In Chapter 4, these signatures are extended with a family of equational arities.

• In Chapters 5 and 6, we introduce the category of reduction monads, and then of their generalization, the operational monads. They are monads with additionnal structure. Thus, signatures over the category of monads are relevant for specifying the monadic part: we explain how to make it formal in the next section.

In Chapter 5, we construct arities specifying the additional structure of reduction monads. Signatures for operational monads of Chapter 6 extend them with arities for specifying the state functors.

Pulling back arities and signatures

In this section, we explain how a functor F : B → C can turn any signature S over C into a pullback signature F * S over B. This will be used in Chapters 5 and 6 to upgrade signatures for monads into signatures for reduction or operational monads. We explain how it works for arities.

Pullback of arities

In this section, we fix a functor F : B → C.

Definition 16. Let A = (D, a, u, v) be an arity over C. The pullback of A along F is the arity

F * A = (D ′ , a ′ , u ′ , v ′ ) over B as follows: • a ′ : D ′ → B is the pullback of a along F , considering the pullback diagram D ′ d / / a ′ D a B F / / C
• u ′ and v ′ are the universal morphisms from B to D ′ factorizing the cones The process of taking the category of models commutes with pullback:

B u•F / / id B D a B F / / C B v•F / /
Proposition 18. Let E be a family of arities over C. Then there is a functor p F,E :

B F * E → C E inducing a pullback diagram B F * E p F,E / / U F * E C E U E B F / / C

Pullback of signatures

In this section, we fix a functor F : B → C.

Definition 19. The pullback F * S of a signature S = E 1 , . . . , E n over C along F is the signature p * 1 E 1 , p * 2 E 2 , . . . , p * n E n over B,
where the functors p i are defined inductively as follows:

• p 1 : B → C is F ; • p i : B p * i-1 E i-1 → C E i-1 is p p i-1 ,E i-1 for i > 1.
We denote by p F,S : B F * S → C S the functor F if n = 0, or p pn,En otherwise.

Again, the process of taking the category of models commutes with pullback:

Proposition 20. Let S be a signature over C. Then we have the following pullback diagram:

B F * S p F,S / / U F * S C S U S B F / / C
Pullbacks allow to combine multiple signatures over a category C into a single one:

Definition 21. We define the product S 1 × • • • × S n of signatures S 1 , . . . , S n over C as the signature over C defined inductively on n as follows:

• if n = 0, then the resulting signature is the empty signature;

• if n > 0, then the resulting signature is the pullback of

S 1 × • • • × S n-1 along U Sn : C S n → C.
CHAPTER 3

PRESENTABLE SIGNATURES FOR MONADS

The present chapter is adapted from [START_REF] Ahrens | High-level signatures and initial semantics[END_REF]. We identify the class of presentable signatures over the category of monads and we show that they are effective. Monads account for the syntax of some untyped programming languages with variable binding.

These signatures are fairly more general than those introduced in some of the seminal papers on this topic [FPT99; HHP93; GP99], which are essentially given by a family of lists of natural numbers indicating the number of variables bound in each subterm of a syntactic construction (we call them "algebraic signatures" below).

Examples are given in Section 3.8. This work improves on a previous attempt [START_REF] Hirschowitz | Initial Semantics for Strengthened Signatures[END_REF] in two main ways: firstly, it gives a much simpler condition for effectivity; secondly, it provides computer-checked proofs for all the main statements.

Organisation of the chapter

Section 3.1 gives a succinct account of the notion of module over a monad, which is the crucial tool underlying our definition of presentables signatures. Signatures and models are described in Sections 3.2 and 3.3 respectively. In Section 3.4, we give our definition of a syntax, and we present our first main result, a modularity result about merging extensions of syntax. In Section 3.5, we show through examples how recursion can be recovered from initiality. Our notion of presentation of a signature appears in Section 3.6. There, we also state our second main result: presentable signatures generate a syntax. The proof of that result is given in Section 3.7. Finally, in Section 3.8, we give examples of presentable signatures.

Categories of modules over monads

The main mathematical notion underlying our presentable signatures is that of module over a monad. In this section, we recall the definition and some basic facts about modules over a monad in the specific case of the category Set of sets, although most definitions are generalizable. See [START_REF] Hirschowitz | Modules over monads and initial semantics[END_REF] for a more extensive introduction on this topic.

Modules over monads

A monad (over Set) is a monoid in the category Set -→ Set of endofunctors of Set, i.e., a triple R = (R, µ, η) given by a functor R : Set -→ Set, and two natural transformations µ : R • R -→ R and η : I -→ R such that the following equations hold:

µ • µR = µ • Rµ, µ • ηR = 1 R , µ • Rη = 1 R . Given two monads R = (R, η, µ) and R ′ = (R ′ , η ′ , µ ′ ), a morphism f : R → R ′ of monads
is given by a natural transformation f : R -→ S between the underlying functors such that

f • η = η ′ , f • µ = µ ′ • (f • f ) .
Let R be a monad.

Definition 22 (Modules)

. A left R-module is given by a functor M : Set -→ Set equipped with a natural transformation ρ M : M • R -→ M , called module substitution, which is compatible with the monad composition and identity:

ρ M • ρ M R = ρ M • M µ, ρ M • M η = 1 M .
There is an obvious corresponding definition of right R-modules that we do not need to consider in this thesis. From now on, we will write "R-module" instead of "left R-module" for brevity.

Example 23.

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

• For any functor F : Set -→ Set and any R-module M : Set -→ Set, the composition F • M is an R-module (in the evident way).

• For every set W we denote by W : Set -→ Set the constant functor W := X → W . Then W is trivially an R-module since W = W • R.

• Let M 1 , M 2 be two R-modules. Then the product functor M 1 × M 2 is an R-module (see Proposition 25 for a general statement).

Definition 24 (Linearity). We say that a natural transformation of R-modules τ : M -→ N is linear1 if it is compatible with module substitution on either side:

τ • ρ M = ρ N • τ R.
We take linear natural transformations as morphisms among modules. It can be easily verified that we obtain in this way a category Mod(R).

Limits and colimits in the category of modules can be constructed pointwise:

Proposition 25 (LModule_Colims_of_shape, LModule_Lims_of_shape). Mod(R) is complete and cocomplete.

The total category of modules

We already introduced the category Mod(R) of modules with fixed base R. It is often useful to consider a larger category which collects modules with different bases. To this end, we need first to introduce the notion of pullback.

Definition 26 (Pullback). Let f : R -→ S be a morphism of monads and M an Smodule. The module substitution

M • R M f -→ M • S ρ M -→ M defines an R-module which is called pullback of M along f and noted f * M . 2
Definition 27 (The total module category). We define the total module category R Mod(R), or Mod for short, as follows3 :

• 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 : R -→ S is a morphism of monads, and m :

M -→ f * N is a morphism of R-modules.
Composition and identity morphisms are the expected ones. The category Mod comes equipped with a forgetful functor to the category of monads, given by the projection

(R, M ) → R.
Proposition 28 (cleaving_bmod). The forgetful functor Mod → Mon is a Grothendieck fibration with fibre Mod(R) over a monad R. In particular, any monad morphism f : R -→ S gives rise to a functor

f * : Mod(S) -→ Mod(R)
given on objects by Definition 26.

Proposition 29 (pb_LModule_colim_iso, pb_LModule_lim_iso). For any monad morphism f : R -→ S, the functor f * : Mod(S) -→ Mod(R) preserves limits and colimits.

Derivation

For our purposes, important examples of modules are given by the following general construction. Let us denote the final object of Set as * .

Definition 30 (Derivation). For any R-module M , the derivative of M is the functor

M ′ := X → M (X + * ). It is an R-module with the substitution ρ M ′ : M ′ • R -→ M ′ defined as in the diagram M (R(X) + * ) ρ M ′ X / / M ( [R(i X ), η X+ * • * ] ) M (X + * ) M (R(X + * )) ρ M X+ * 6 6 (3.1)
where i X : X -→ X + * and * : * -→ X + * are the canonical injections.

Derivation is a continuous and cocontinuous endofunctor on the category Mod(R) of modules over a fixed monad R. In particular, derivation can be iterated: we denote by M (k) the k-th derivative of M . Definition 31. Given a list of nonnegative integers (a) = (a 1 , . . . , a n ) and a left module M over a monad R, we denote by M (a) = M (a 1 ,...,an) the module M (a 1 ) × • • • × M (an) . Observe that, when (a) = () is the empty list, M () is the final module * .

Definition 32. For every monad R and R-module M we have a natural substitution morphism σ :

M ′ × R -→ M defined by σ X = ρ M X • w X , where w X : M (X + * ) × R(X) → M (R(X)) is the map w X : (a, b) → M ([η X , b])(a), b : * → b.
Lemma 33 (substitution_laws). The transformation σ is linear.

The substitution σ allows us to interpret the derivative M ′ as the "module M with one formal parameter added".

Abstracting over the module turns the substitution morphism into a natural transformation that is the counit of the following adjunction: Proposition 34 (deriv_adj). The endofunctor of Mod(R) mapping M to the R-module M × R is left adjoint to the derivation endofunctor, the counit being the substitution morphism σ.

Signatures for monads

In this section, we consider particular signatures over the category of monads consisting of a single arity in the sense of Chapter 2.

The purpose of a signature is to act on monads. An action of a signature Σ in a monad R is a morphism from the module Σ(R) to the tautological one R. For instance, in the case of the signature Σ of a binary operation, we have Remark 37. Any parametric module Σ defines uniquely a signature over the category of monads consisting of a single arity ( Mod, U, Σ, Θ), where U : Mod → Mon is the canonical forgetful functor. In this Chapter, we only consider such signatures, which we take as a definition of signature in the formalization. In the following we may use the same expression to designate both the parametric module and the induced signature. Now we give some basic examples of parametric modules, inducing signatures.

Σ(R) := R 2 = R × R.

Example 38.

1. For any functor F : Set -→ Set and any parametric module Σ, the assignment R → F • Σ(R) yields a parametric module which we denote F • Σ.

2. The assignment R → * R , where * R denotes the final module over R, yields a parametric module which we denote by * .

3. Given two parametric modules Σ and Υ, the assignment R → Σ(R) × Υ(R) yields a parametric module which we denote by Σ × Υ. For instance, Θ 2 = Θ × Θ is the parametric module of any (first-order) binary operation, and, more generally, Θ n is the parametric module of n-ary operations.

4. Given two parametric modules Σ and Υ, the assignment R → Σ(R) + Υ(R) yields a parametric module which we denote by Σ + Υ. For instance, Θ 2 + Θ 2 yields the signature of a pair of binary operations.

The last example above explains how we can combine multiple signatures induced by parametric modules into a single one. Hence we do not need to distinguish between such arities-used to specify a single syntactic construction-and families of such arities-used to specify a family of syntactic constructions. Our notion of signatures that we present here allow us to do both (via Proposition 42 for families that are not necessarily finitely indexed).

Elementary signatures are of a particularly simple shape: Definition 39. For each sequence of nonnegative integers s = (s 1 , . . . , s n ), the assignment R → R (s 1 ) × • • • × R (sn) (see Definition 31) is a parametric module, which we denote by Θ (s) , or by Θ ′ in the specific case of s = (1). Parametric modules of this form and their induced signatures are said elementary.

Remark 40. The product of two elementary parametric modules is elementary. Definition 41. A morphism between two parametric modules Σ 1 , Σ 2 : Mon -→ Mod is a natural transformation m : Σ 1 -→ Σ 2 which, post-composed with the projection Mod -→ Mon, becomes the identity. Parametric modules form a subcategory PMod of the category of functors from Mon to Mod.

Limits and colimits of parametric modules can be easily constructed pointwise:

Proposition 42 (Sig_Lims_of_shape, Sig_Colims_of_shape, Sig_isDistributive). The category of parametric modules is complete and cocomplete. Furthermore, it is distributive: for any parametric module Σ and family of parametric modules

(S o ) o∈O , the canonical morphism o∈O (S o × Σ) → ( o∈O S o ) × Σ is an isomorphism.
Definition 43. An algebraic parametric module is a (possibly infinite) coproduct of elementary parametric modules. The induced signature is said algebraic.

These signatures are those which appear in [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF]. For instance, the algebraic signature of the lambda-calculus is induced by the parametric module Σ LC = Θ 2 + Θ ′ .

To conclude this section, we explain the connection between signatures with strength (on the category Set) and our signatures induced by parametric modules.

Signatures with strength were introduced in [MU04] (even though they were not given an explicit name there). The relevant definitions regarding signatures with strength are summarized in [START_REF] Ahrens | From Signatures to Monads in UniMath[END_REF], to which we refer the interested reader.

We recall that a signature with strength [AMM18, Definition 4] is a pair of an endofunctor H : [C, C] → [C, C] together with a strength-like datum. Here, we only consider signatures with strength over the base category C := Set. Given a signature with strength H, we also refer to the underlying endofunctor on the functor category

[Set, Set] as H : [Set, Set] → [Set, Set].
A morphism of signatures with strength [AMM18, Definition 5] is a natural transformation between the underlying functors that is compatible with the strengths in a suitable sense. Together with the obvious composition and identity, these objects and morphisms form a category SigStrength [START_REF] Ahrens | From Signatures to Monads in UniMath[END_REF].

Any signature with strength H gives rise to a parametric module H [HM12, Section 7]. This parametric module associates, to a monad R, an R-module whose underlying functor is H(U R), where U R is the functor underlying the monad R. Similarly, given two signatures with strength H 1 and H 2 , and a morphism α : H 1 → H 2 of signatures with strength, we associate to it a morphism of parametric modules α : H1 → H2 . This morphism sends a monad R to a module morphism α(R) : H1 (R) -→ H2 (R) whose underlying natural transformation is given by α(U R), where, as before, U R is the functor underlying the monad R. These maps assemble into a functor: Proposition 44 (sigWithStrength_to_sig_functor). The maps sketched above yield a functor (-) : SigStrength -→ PMod.

Categories of models

We unfold the definitions of model of a signature and action of a signature (as introduced in the general setting in Chapter 2) to the case of signatures induced by parametric modules.

Definition 45 (Models and actions). Given a parametric module Σ, the category Mon Σ of models of Σ is defined as the category of models of the induced signature. Objects are pairs (R, r) of a monad R equipped with an action of Σ in R, that is, with a module morphism r : Σ(R) → R. A morphism from (R, r) to (S, s) is a morphism of monads m : R → S compatible with the actions, in the sense that the following diagram of R-modules commutes:

Σ(R) r / / Σ(m) R m m * (Σ(S)) m * s / / m * S
Here, the horizontal arrows come from the actions, the left vertical arrow comes from the functoriality of parametric modules, and m : R -→ m * S is the morphism of monads seen as morphism of R-modules. This is equivalent to asking that the square of underlying natural transformations commutes, i.e., m • r = s • Σ(m).

Example 46. The usual app : LC 2 -→ LC is an action of the elementary signature Θ 2 in the monad LC of syntactic lambda calculus. The usual abs : LC ′ -→ LC is an action of the elementary signature Θ ′ in the monad LC. Then [app, abs] : LC 2 + LC ′ -→ LC is an action of the algebraic signature of the lambda calculus Θ 2 + Θ ′ in the monad LC.

In the formalisation, the category of models of a signature Σ is recovered as the fiber category over Σ of the displayed category [START_REF] Ahrens | Displayed Categories[END_REF] of models, see rep_disp. We have also formalized a direct definition (rep_fiber_category) and shown that the two definitions yield isomorphic categories: catiso_modelcat.

Definition 47 (Pullback). Let f : Υ -→ Σ be a morphism of parametric modules and (R, r) a model of Σ. The linear morphism Υ(R)

f (R) -→ Σ(R) r -→ R defines an action of Υ in R.
The induced model of Υ is called pullback4 of (R, r) along f and denoted by f * (R, r).

Syntax

We are primarily interested in parametric modules Σ inducing effective signatures.

Effectivity and parametric modules

Definition 48. We call a parametric module effective if its induced signature is. If Σ is effective, that is, if Mon Σ has an initial object, this object is essentially unique; we call it the syntax generated by Σ, denoted by Σ. By abuse of notation, we also denote by Σ

the monad underlying the model Σ.

In this work, we aim to identify parametric modules that are effective. This is not automatic: below, we give a parametric module that is not effective. Afterwards, we give suitable sufficient criteria for parametric modules to be effective.

Non-example 49. Let P denote the powerset functor and consider the parametric module P • Θ (see Example 38, Item 1): it associates, to any monad R, the module P • R that sends a set X to the powerset P(RX) of RX. The induced signature is not effective.

Instead of giving a direct proof of the fact that P • Θ is not effective, we deduce it as a simple consequence of a stronger result that we consider interesting in itself: an analogue of Lambek's Lemma, given in Lemma 52.

The following preparatory lemma explains how to construct new models of a parametric module Σ from old ones: Lemma 50. Let (R, r) be a model of a parametric module Σ. Let η : Id → R be the unit of the monad R, and let ρ Σ(R) : Σ(R) • R → Σ(R) be the module substitution of the R-module Σ(R).

• The injection Id → Σ(R) + Id together with the natural transformation

(Σ(R) + Id) • (Σ(R) + Id) ≃ Σ(R) • (Σ(R) + Id) + Σ(R) + Id Σ(R)[r,η]+_+_ Σ(R) • R + Σ(R) + Id [ρ Σ(R) ,id]+_ Σ(R) + Id
give the endofunctor Σ(R) + Id the structure of a monad.

• Moreover, this monad can be given the following Σ-action: Lemma 52 (iso_mod_id_model). If Σ is effective, then the morphism of Σ-models ǫ Σ : Σ♯ -→ Σ is an isomorphism.

Σ Σ(R) + Id Σ([r,η]) / / Σ(R) • R ρ Σ(R) / / Σ(R) / / Σ(R) + Id (3.2) • The natural transformation [r, η] : Σ(R) + Id → R is a model morphism,

Syntax

We go back to considering the signature Σ := P • Θ. Suppose that Σ is effective. From Lemma 52 it follows that P ΣX + X ∼ = ΣX. In particular, we have an injective map from P ΣX to ΣX-contradiction.

On the other hand, as a starting point, we can identify the following class of effective parametric modules:

Theorem 53 (algebraic_sig_effective). Algebraic signatures are effective.

This result is proved in a previous work [HM07, Theorems 1 and 2]. The construction of the syntax proceeds as follows: an algebraic parametric module induces an endofunctor on the category of endofunctors on Set. Its initial algebra (constructed as the colimit of the initial chain) is given the structure of a monad with an action of the algebraic signature, and then a routine verification shows that it is actually initial in the category of models. The computer-checked proof uses the construction of a monad from an algebraic signature formalized in [START_REF] Ahrens | From Signatures to Monads in UniMath[END_REF].

In Section 3.6, we show a more general effectiveness result: Theorem 57 states that presentable signatures, which form a superclass of algebraic signatures, are effective.

Modularity

In this section, we study the problem of how to merge two syntax extensions. Our answer, a "modularity" result (Theorem 54), was stated already in the preliminary version [HM12, Section 6], there without proof. Suppose that we have a pushout square of effective parametric modules,

Σ 0 / / Σ 1 Σ 2 / / Σ
Intuitively, the signatures Σ 1 and Σ 2 specify two extensions of the signature Σ 0 , and Σ is the smallest extension containing both these extensions. Modularity means that the corresponding diagram of models,

Σ0 / / Σ1 Σ2 / /
Σ is a pushout as well-but we have to take care to state this in the "right" category. The right category for this purpose is the following total category Σ Mon Σ of models:

• An object of Σ Mon Σ is a triple (Σ, R, r) where Σ is a parametric module, R is a monad, and r is an action of Σ in R.

• A morphism in Σ Mon Σ from (Σ 1 , R 1 , r 1 ) to (Σ 2 , R 2 , r 2 ) consists of a pair (i, m) of a parametric module morphism i : Σ 1 -→ Σ 2 and a morphism m of Σ 1 -models from (R 1 , r 1 ) to (R 2 , i * (r 2 )).
• It is easily checked that the obvious composition turns Σ Mon Σ into a category. Now for each signature Σ, we have an obvious inclusion from the fiber Mon Σ into Σ Mon Σ , through which we may see the syntax Σ of any effective signature as an object in Σ Mon Σ . Furthermore, a morphism i : Σ 1 -→ Σ 2 of effective parametric modules yields a morphism i * := Σ1 -→ Σ2 in Σ Mon Σ . Hence our pushout square of effective parametric modules as described above yields a square in Σ Mon Σ .

Theorem 54 (pushout_in_big_rep). Modularity holds in Σ Mon Σ , in the sense that given a pushout square of effective parametric modules as above, the associated square in Σ Mon Σ is a pushout again.

The proof uses, in particular, the following fact:

Lemma 55 (rep_cleaving). The projection π : Σ Mon Σ → PMod is a Grothendieck fibration. In particular, given a morphism f : Υ -→ Σ of parametric modules, the pullback map defined in Definition 47 extends to a functor

f * : Mon Σ -→ Mon Υ .
Note that Theorem 54 does not say that a pushout of effective parametric modules is effective again; it only tells us that if all of the signatures in a pushout square are effective, then the syntax generated by the pushout is the pushout of the syntaxes. In general, we do not know whether a colimit (or even a binary coproduct) of effective parametric modules is effective again.

In Section 3.6 we study presentable parametric modules, which we show to be effective and closed under colimits.

Recursion

We now show through examples how certain forms of recursion can be derived from initiality.

Example: Translation of intuitionistic logic into linear logic

We start with an elementary example of translation of syntaxes using initiality, namely the translation of second-order intuitionistic logic into second-order linear logic [Gir87, page 6]. The syntax of second-order intuitionistic logic can be defined with one unary operator ¬, three binary operators ∨, ∧ and ⇒, and two binding operators ∀ and ∃. The associated (algebraic) signature is Σ LJ = Θ + 3 × Θ 2 + 2 × Θ ′ . As for linear logic, there are four constants ⊤, ⊥, 0, 1, two unary operators ! and ?, five binary operators &, `, ⊗, ⊕, ⊸ and two binding operators ∀ and ∃. The associated (algebraic) signature is

Σ LL = 4 × * + 2 × Θ + 5 × Θ 2 + 2 × Θ ′ .
By universal property of coproduct, a model of Σ LJ is given by a monad R with module morphisms:

• r ¬ : R -→ R • r ∧ , r ∨ , r ⇒ : R × R -→ R • r ∀ , r ∃ : R ′ -→ R
and similarly, we can decompose an action of Σ LL into as many components as there are operators.

The translation will be a morphism of monads between the initial models (i.e. the syntaxes) o : ΣLJ -→ ΣLL coming from the initiality of ΣLJ , satisfying the expected equations. Indeed, equipping ΣLL with an action r ′ α : α( ΣLL ) -→ ΣLL for each operator α of intuitionistic logic (¬,∨,∧,⇒,∀ and ∃) yields a morphism of monads o : ΣLJ -→ ΣLL such that o(r α (t)) = r ′ α (α(o)(t)) for each α. The definition of r ′ α is then straightforward to devise, following the recursive clauses given on the right:

r ′ ¬ = r ⊸ • (r ! × r 0 ) (¬A) o := (!A) ⊸ 0 r ′ ∧ = r & (A ∧ B) o := A o &B o r ′ ∨ = r ⊕ • (r ! × r ! ) (A ∨ B) o :=!A o ⊕!B o r ′ ⇒ = r ⊸ • (r ! × id) (A ⇒ B) o :=!A o ⊸ B o r ′ ∃ = r ∃ • r ! (∃xA) o := ∃x!A o r ′ ∀ = r ∀ (∀xA) o := ∀xA o
The induced action of Σ LJ in the monad ΣLL yields the desired translation morphism o : ΣLJ → ΣLL . Note that variables are automatically preserved by the translation because o is a monad morphism.

Example: Computing the set of free variables

As above, we denote by PX the powerset of X. Union gives a composition operator P(PX) → PX defined by u → s∈u s, which yields a monad structure on P.

We now define an action of the signature of lambda calculus Σ LC in the monad P. We take the binary union operator ∪ : P × P → P as action of the application signature Θ × Θ in P; this is a module morphism since binary union distributes over union of sets. Next, given S ∈ P(X + * ) we define Maybe -1 X (S) = S ∩ X. This defines a morphism of modules Maybe -1 : P ′ → P; a small calculation using a distributivity law of binary intersection over union of sets shows that this natural transformation is indeed linear. It can hence be used to model the abstraction signature Θ ′ in P.

Associated to this model of Σ LC in P we have an initial morphism free : LC → P. Then, for any t ∈ LC(X), the set free(t) is the set of free variables occurring in t.

Example: Computing the size of a term

We now consider the problem of computing the "size" of a λ-term, that is, for any set X, a function s X : LC(X) -→ N such that

s X (x) = 0 (x ∈ X variable) s X (abs(t)) = 1 + s X+ * (t) s X (app(t, u)) = 1 + s X (t) + s X (u)
To express this map as a morphism of models, we first need to find a suitable monad underlying the target model. The first candidate, the constant functor X → N, does not admit a monad structure; the problem lies in finding a suitable unit for the monad.

(More generally, given a monad R and a set A, the functor X → R(X) × A does not admit a monad structure whenever A is not a singleton.)

This problem hints at a different approach to the original question: instead of computing the size of a term (which is 0 for a variable), we compute a generalized size gs which depends on arbitrary (formal) sizes attributed to variables. We have gs :

X:Set LC(X) → (X → N) → N
Here, unsurprisingly, we recognize the continuation monad (see also [START_REF] Johann | Initial Algebra Semantics Is Enough![END_REF] for the use of continuation for implementing complicated recursion schemes using initiality)

Cont N := X → (X → N) → N with multiplication λf.λg.f (λh.h(g)).
Now we can define gs through initiality by endowing the monad Cont N with a structure of Σ LC -model as follows.

The function α(m, n) = 1 + m + n induces a natural transformation

c app : Cont N × Cont N -→ Cont N
thus an action for the application signature Θ × Θ in the monad Cont N .

Next, given a set X and k : X → N, define k :

X + { * } → N by k(x) = k(x) for all
x ∈ X and k( * ) = 0. This induces a function

c abs (X) : Cont ′ N (X) -→ Cont N (X) t → (k → 1 + t( k))
which is the desired action of the abstraction signature Θ ′ .

Altogether, the transformations c app and c abs form the desired action of Σ LC in Cont N and thus give an initial morphism, i.e., a natural transformation ι : LC → Cont N which respects the Σ LC -model structure. Now let 0 X be the function that is constantly zero on X. Then the sought "size" map s : X:Set LC(X) → N is given by s X (t) = ι X (t, 0 X ).

Example: Counting the number of redexes

We now consider an example of recursive computation: a function r such that r(t) is the number of redexes of the λ-term t of LC(X). Informally, the equations defining r are

r(x) = 0, (x variable) r(abs(t)) = r(t), r(app(t, u)) = r(t) + r(u) +      1 if t is an abstraction 0 otherwise.
In order to compute recursively the number of β-redexes in a term, we need to keep track, not only of the number of redexes in subterms, but also whether the head construction of subterms is the abstraction; in the affirmative case we use the value 1 and 0 otherwise. Hence, we define a Σ LC -action on the monad W := Cont N×{0,1} . We denote by π 1 , π 2 the projections that access the two components of the product N × {0, 1}.

For any set X and function k : X → N × {0, 1}, let us denote by k : X + { * } → N × {0, 1} the function which sends x ∈ X to k(x) and * to (0, 0). Now, consider the function c abs (X) :

W ′ (X) -→ W (X) t → (k → (π 1 (t( k)), 1)).
Then c abs is an action of the abstraction signature Θ ′ in W .

Next, we specify an action c app : W × W → W of the application signature Θ × Θ:

Presentations of signatures and syntaxes

Given a set X, consider the function

c app (X) : W (X) × W (X) -→ W (X) (t, u) → (k → (π 1 (t(k)) + π 1 (u(k)) + π 2 (t(k)), 0)).
Then c app is an action of the abstraction signature Θ × Θ in W .

Overall we have a Σ LC -action from which we get an initial morphism ι : LC → W . If 0 X is the constant function X → N × {0, 1} returning the pair (0, 0), then π 1 (ι(0 X )) : LC(X) → N is the desired function r.

Presentations of signatures and syntaxes

In this section, we identify a superclass of algebraic parametric modules that are still effective: we call them presentable parametric modules, inducing presentable signatures.

Definition 56. Given a parametric module Σ, a presentation 5 of Σ is given by an algebraic parametric module Υ and an epimorphism of parametric modules p : Υ -→ Σ. In that case, we say that Σ is presented by p : Υ -→ Σ.

A parametric module for which a presentation exists is called presentable. The induced signature is then called presentable.

Presentations for a signature are not essentially unique; indeed, signatures can have many different presentations.

Remark. By definition, any construction which can be encoded through a presentable signature Σ can alternatively be encoded through any algebraic signature "presenting" Σ. The former encoding is finer than the latter in the sense that terms which are different in the latter encoding can be identified by the former. In other words, a certain amount of semantics is integrated into the syntax.

The main desired property of our presentable signatures is that, thanks to the following theorem, they are effective:

Theorem 57 (PresentableisEffective). Any presentable signature is effective.

5. In algebra, a presentation of a group G is an epimorphism F → G where F is free (together with a generating set of relations among the generators).

The proof is discussed in Section 3.7.

Using the axiom of choice, we can prove a stronger statement:

Theorem 58 (is_right_adjoint_functor_of_reps_from_pw_epi_choice). We assume the axiom of choice. Let Σ be a parametric module, and let p : Υ -→ Σ be a presentation of Σ. Then the functor p * : Mon Σ -→ Mon Υ has a left adjoint.

In the proof of Theorem 58, the axiom of choice is used to show that endofunctors on Set preserve epimorphisms.

Theorem 57 follows from Theorem 58 since the left adjoint p ! : Mon Υ -→ Mon Σ preserves colimits, in particular, initial objects. However, Theorem 57 is proved in Section 3.7 without appealing to the axiom of choice: there, only some specific endofunctor on Set is considered, for which preservation of epimorphisms can be proved without using the axiom of choice.

Definition 59. We call a syntax presentable if it is generated by a presentable signature.

Next, we give important examples of presentable signatures:

Theorem 60. The following hold:

1. Any algebraic signature is presentable.

2. Any colimit of presentable parametric modules is presentable.

The product of two presentable parametric modules is presentable (in the case

when one of them is Θ, see har_ binprodR_ isPresentable )

Proof. Items 1-2 are easy to prove. For Item 3, if Σ 1 and Σ 2 are presented by i Υ i and j Φ j respectively, then Σ 1 × Σ 2 is presented by i,j Υ i × Φ j .

Corollary 61. Any colimit of algebraic parametric modules is effective.

Proof. A colimit of algebraic parametric modules is presentable, by Theorem 60, hence effective, by Theorem 57

Proof of Theorem 57

In this section, we prove Theorem 57. This proof is mechanically checked in our library; the reader may thus prefer to look at the formalised statements in the library.

Note that the proof of Theorem 57 rests on the more technical Lemma 66 below.

Proposition 62 (epiSig_equiv_pwEpi_SET). Epimorphisms of parametric modules are exactly pointwise epimorphisms. Using this characterization of epimorphisms, the proof follows from the fact that colimits are computed pointwise in the category of parametric modules.

Another important ingredient will be the following quotient construction for monads. Let R be a monad preserving epimorphisms, and let ∼ be a "compatible" family of relations on (the functor underlying) R, that is, for any X : Set 0 , ∼ X is an equivalence relation on RX such that, for any f : X → Y , the function R(f ) maps related elements in RX to related elements in RY . Taking the pointwise quotient, we obtain a quotient π : R → R in the functor category, satisfying the usual universal property. We want to equip R with a monad structure that upgrades π : R → R into a quotient in the category of monads. In particular, this means that we need to fill in the square

R • R π•π µ / / R π R • R µ / / R
with a suitable µ : R • R -→ R satisfying the monad laws. But π is epi, and hence so is π•π = πR•Rπ since epis are closed under composition and R preserves epimorphisms. Thus, this is possible when any two elements in RRX that are mapped to the same element by π • π (the left vertical morphism) are also mapped to the same element by π • µ (the top-right composition). It turns out that this is the only extra condition needed for the upgrade. We summarize the construction in the following lemma: Lemma 63 (projR_monad). Given a monad R preserving epimorphisms, and a compatible relation ∼ on R such that for any set X and x, y ∈ RRX, we have that if (π • π) X (x) ∼ (π • π) X (y) then π(µ(x)) ∼ π(µ(y)). Then we can construct the quotient π : R → R in the category of monads, satisfying the usual universal property.

Note that the axiom of choice implies that epimorphisms have sections, and thus that any endofunctor on Set preserves epimorphisms. Definition 64. An epi-parametric module is a parametric module Σ that preserves the epimorphicity in the category of endofunctors on Set: for any monad morphism f : R -→ S, if U (f ) is an epi of functors, then so is U (Σ(f )). Here, we denote by U the forgetful functor from monads resp. modules to endofunctors.

Example 65 (BindingSigAreEpiSig). All the algebraic parametric modules are epiparametric modules.

We are now in a position to state and prove the main technical lemma: Lemma 66 (push_initiality). Let Υ be effective, such that both Υ and Υ( Υ) preserve epimorphisms (as noted above, this condition is automatically fulfilled if one assumes the axiom of choice). Let F : Υ → Σ be a morphism of parametric modules. Suppose that Υ is an epi-parametric module and F is an epimorphism. Then Σ is effective.

Proof sketch. As before, we denote by Υ the initial Υ-model, as well as-by abuse of notation-its underlying monad. For each set X, we consider the equivalence relation ∼ X on Υ(X) defined as follows: for all x, y ∈ Υ(X) we stipulate that x ∼ X y if and only if i X (x) = i X (y) for each (initial) morphism of Υ-models i : Υ → F * S with S a Σ-model and F * S the Υ-model induced by F : Υ → Σ.

By Lemma 63, as Υ preserves epimorphisms, we obtain the quotient monad, which we call Υ/F , and the epimorphic projection π : Υ → Υ/F . We now equip Υ/F with a Σ-action, and show that the induced model is initial, in four steps:

(i) We equip Υ/F with a Σ-action, i.e., with a morphism of Υ/F -modules m Υ/F : Σ( Υ/F ) → Υ/F . We define u : Υ( Υ) → Σ( Υ/F ) as u = F Υ/F • Υ(π). Then u is epimorphic, by composition of epimorphisms and by using Proposition 62.

Let m Υ : Υ( Υ) → Υ be the action of the initial model of Υ. We define m Υ/F as the unique morphism making the following diagram commute in the category of endofunctors on Set:

Υ( Υ) Υ Σ( Υ/F ) Υ/F m Υ u π m Υ/F
Uniqueness follows from pointwise surjectivity of u. Existence follows from the compatibility of m Υ with the congruence ∼ X . The diagram necessary to turn m Υ/F into a module morphism on Υ/F is proved by pre-composing it with the epimorphism (Σ(π)

• F Υ) • π : Υ( Υ) • Υ → Σ( Υ/F ) • Υ/F (
this is where the preservation of epimorphims by Υ( Υ) is required) and unfolding the definitions.

(ii) Now, π can be seen as a morphism of Υ-models between Υ and F * Υ/F , by naturality of F and using the previous diagram.

It remains to show that ( Υ/F , m Υ/F ) is initial in the category of Σ-models.

(iii) Given a Σ-model (S, m s ), the initial morphism of Υ-models i S : Υ → F * S induces a monad morphism ι S : Υ/F → S. We need to show that the morphism ι is a morphism of Σ-models. Pre-composing the involved diagram by the epimorphism Σ(π)•F Υ : Υ( Υ) → Σ( Υ/F ) and unfolding the definitions shows that ι S : Υ/F → S is a morphism of Σ-models.

(iv) We show that ι S is the only morphism Υ/F → S. Let g be such a morphism. Then g • π : Υ → S defines a morphism in the category of Υ-models. Uniqueness of i S yields g • π = i S , and by uniqueness of the diagram defining ι S it follows that g = i ′ S .

Lemma 67 (algebraic_model_Epi and BindingSig_on_model_isEpi). Let Σ be an algebraic parametric module. Then Σ and Σ( Σ) preserve epimorphisms.

Proof. The initial model of an algebraic parametric module Σ is obtained as the initial chain of the endofunctor R → Id + Σ(R), where Σ denotes (by abuse of notation) the endofunctor on endofunctors on Set corresponding to the parametric module Σ.

Then the proof follows from the fact that this endofunctor preserves preservation of epimorphisms.

Proof of Theorem 57. Let p : Υ → Σ be a presentation of Σ. We need to construct an initial model for Σ.

As the parametric module Υ is algebraic, it is effective (by Theorem 53) and is an epi-parametric module (by Example 65). We can thus instantiate Lemma 66 to see that Σ is effective, thanks to Lemma 67.

Constructions of presentable signatures

Complex signatures are naturally built as the sum of basic components, generally referred as "arities" (which in our settings can be captured with a single parametric module, see remark after Example 38). Thanks to Theorem 60, Item 2, direct sums (or, indeed, any colimit) of presentable parametric modules are presentable, hence effective by Theorem 57.

In this section, we show that, besides algebraic signatures, there are other interesting examples of signatures which are presentable, and which hence can be safely added to any presentable signature. Safely here means that the resulting signature is still presentable.

Post-composition with a presentable functor

A functor F : Set → Set is polynomial if it is of the form F X = n∈N a n × X n for some sequence (a n ) n∈N of sets. Note that if F is polynomial, then the signature F • Θ is algebraic.
Definition 68. Let G : Set → Set be a functor. A presentation of G is a pair consisting of a polynomial functor F : Set → Set and an epimorphism p : F → G. The functor G is called presentable if there is a presentation of G.

Proposition 69. Given a presentable functor G, the signature G • Θ is presentable.

Proof. Let p : F → G be a presentation of G; then a presentation of G • Θ is given by the induced epimorphism

F • Θ → G • Θ.
Proposition 70. Here we assume the axiom of excluded middle. An endofunctor on Set is presentable if and only if it is finitary (i.e., it preserves filtered colimits).

Proof. This is a corollary of Proposition 5.2 of [START_REF] Adámek | On Tree Coalgebras and Coalgebra Presentations[END_REF], since ω-accessible functors are exactly the finitary ones.

We now give several examples of presentable signatures obtained from presentable functors.

Example: Adding a syntactic commutative binary operator, e.g., parallel-or

Consider the functor square : Set → Set mapping a set X to X × X; it is polynomial. The associated signature square • Θ encodes a binary operator, such as the application of the lambda calculus.

Sometimes such binary operators are asked to be commutative; a simple example of such a commutative binary operator is standard integer addition.

Another example, more specific to formal computer languages, is a "concurrency" operator P | Q of a process calculus, such as the π-calculus, for which it is natural to require commutativity as a structural congruence relation:

P | Q ≡ Q | P .
Such a commutative binary operator can be specified via the following presentable signature: we denote by S 2 : Set → Set the endofunctor that assigns, to each set X, the set (X × X)/(x, y) ∼ (y, x) of unordered pairs of elements of X. This functor is presented by the obvious projection square → S 2 . By Proposition 69, the signature S 2 • Θ is presentable; it encodes a commutative binary operator.

Example: Adding a maximum operator

Let list : Set → Set be the functor associating, to any set X, the set list(X) of (finite) lists with entries in X; specifically, it is given on objects as X → n∈N X n .

We now consider the syntax of a "maximum" operator, acting, e.g., on a list of natural numbers: max : list(N) → N It can be specified via the algebraic signature list • Θ. However, this signature is "rough" in the sense that it does not take into account some semantic aspects of a maximum operator, such as invariance under repetition or permutation of elements in a list.

For a finer encoding, consider the functor P fin : Set → Set associating, to a set X, the set P fin (X) of its finite subsets. This functor is presented by the epimorphism list → P fin .

By Proposition 69, the signature P fin • Θ is presentable; it encodes the syntax of a "maximum" operator accounting for invariance under repetition or permutation of elements in a list.

Example: Adding an application à la Differential LC

Let R be a commutative (semi)ring. To any set S, we can associate the free R-module R S ; its elements are formal linear combinations s∈S a s s of elements of S with coefficients a s from R; with a s = 0 almost everywhere. Ignoring the R-module structure on R S , this assignment induces a functor R _ : Set → Set with the obvious action on morphisms. For simplicity, we restrict our attention to the semiring (N, +, ×). This functor is presentable: a presentation is given by the polynomial functor list : Set → Set, and the epimorphism

p : list -→ N _ p X ([x 1 , . . . , x n ]) := x 1 + . . . + x n .
By Proposition 69, this yields a presentable signature, which we call N Θ .

The Differential Lambda Calculus (DLC) [START_REF] Ehrhard | The differential lambda-calculus[END_REF] of Ehrhard and Regnier is a lambda calculus with operations suitable to express differential constructions. The calculus is parametrized by a semiring R; again we restrict to R = (N, +, ×).

DLC has a binary "application" operator, written (s)t, where s ∈ T is an element of the inductively defined set T of terms and t ∈ N T is an element of the free (N, +, ×)module. This operator is thus specified by the presentable signature Θ × N Θ .

Example: Adding a syntactic closure operator

Given a quantification construction (e.g., abstraction, universal or existential quantification), it is often useful to take the associated closure operation. One well-known example is the universal closure of a logic formula. Such a closure is invariant under permutation of the fresh variables. A closure can be syntactically encoded in a rough way by iterating the closure with respect to one variable at a time. Here our framework allows a refined syntactic encoding which we explain below.

Let us start with binding a fixed number k of fresh variables. The elementary signature Θ (k) already specifies an operation that binds k variables. However, this encoding does not reflect invariance under variable permutation. To enforce this invariance, it suffices to quotient the signature Θ (k) with respect to the action of the group S k of permutations of the set k, that is, to consider the colimit of the following one-object diagram:

Θ (k) Θ (σ)
where σ ranges over the elements of S k . We denote by S (k) Θ the resulting signature presented by the projection Θ (k) → S (k) Θ. By universal property of the quotient, a model of it consists of a monad R with an action m : R (k) → R that satisfies the required invariance. Now, we want to specify an operation which binds an arbitrary number of fresh variables, as expected from a closure operator. One rough solution is to consider the coproduct k S (k) Θ. However, we encounter a similar inconvenience as for Θ (k) . Indeed, for each k ′ > k, each term already encoded by the signature S (k) Θ may be considered again, encoded (differently) through S (k ′ ) Θ.

Fortunately, a finer encoding is provided by the following simple colimit of presentable parametric modules. The crucial point here is that, for each k, all natural injections from Θ (k) to Θ (k+1) induce the same canonical injection from S (k) Θ to S (k+1) Θ. We thus have a natural colimit for the sequence k → S (k) Θ and thus a signature colim k S (k) Θ which, as a colimit of presentable parametric modules, is presentable (Theorem 60, Item 2).

Accordingly, we define a total closure on a monad R to be an action of the signature colim k S (k) Θ in R. It can easily be checked that a model of this signature is a monad R together with a family of module morphisms (e k : R (k) → R) k∈N compatible in the sense that for each injection i : k → k ′ the following diagram commutes:

R (k) e k # # R (i) / / R (k ′ ) e k ′ R

Example: Adding an explicit substitution

Explicit substitution was introduced by Abadi et al. [START_REF] Abadi | Explicit Substitutions[END_REF] as a theoretical device to study the theory of substitution and to describe concrete implementations of substitution algorithms. In this section, we explain how we can extend any presentable signature with an explicit substitution construction, and we offer some refinements from a purely syntactic point of view. In fact, we will show three solutions, differing in the amount of "coherence" which is handled at the syntactic level (e.g., invariance under permutation and weakening). We follow the approach initiated by Ghani, Uustalu, and Hamana in [START_REF] Ghani | Explicit substitutions and higher-order syntax[END_REF].

Let R be a monad. We have already considered (see Lemma 33) the (unary) substitution σ R : R ′ ×R → R. More generally, we have the sequence of substitution operations subst p : R (p) × R p -→ R.

(3.3)

We say that subst p is the p-substitution in R; it simultaneously replaces the p extra variables in its first argument with the p other arguments, respectively. (Note that subst 1 is the original σ R .)

We observe that, for fixed p, the group S p of permutations on p elements has a natural action on R (p) × R p , and that subst p is invariant under this action.

Thus, if we fix an integer p, there are two ways to internalise subst p in the syntax: we can choose the elementary signature Θ (p) × Θ p , which is rough in the sense that the above invariance is not reflected; and, alternatively, if we want to reflect the permutation invariance syntactically, we can choose the quotient Q p of the above parametric module by the action of S p .

By universal property of the quotient, a model of our quotient Q p is given by a monad R with an action m : R (p) × R p → R satisfying the desired invariance.

Before turning to the encoding of the entire series (subst p ) p∈N , we recall how, as noticed already in [START_REF] Ghani | Explicit substitutions and higher-order syntax[END_REF], this series enjoys further coherence. In order to explain this coherence, we start with two natural numbers p and q and the module R (p) × R q . Pairs in this module are almost ready for substitution: what is missing is a map u : I p -→ I q , where I n denotes the set {1, . . . , p}. But such a map can be used in two ways: letting u act covariantly on the first factor leads us into R (q) × R q where we can apply subst q ; while letting u act contravariantly on the second factor leads us into R (p) × R p where we can apply subst p . The good news is that we obtain the same result. More precisely, the following diagram is commutative:

R (p) × R q R (p) ×R u / / R (u) ×R q R (p) × R p substp R (q) × R q substq / / R (3.4)
Note that in the case where p equals q and u is a permutation, we recover exactly the invariance by permutation considered earlier.

Abstracting over the numbers p, q and the map u, this exactly means that our series factors through the coend p:F R (p) × R p , where covariant (resp. contravariant) occurrences of the bifunctor have been underlined (resp. overlined), and the category F is the full subcategory of Set whose objects are natural numbers. Thus we have a canonical morphism isubst R :

p:F R (p) × R p -→ R.
Abstracting over R, we obtain the following: Definition 71. Integrated substitution isubst :

p:F Θ (p) × Θ p -→ Θ
is the parametric module morphism obtained by abstracting over R the linear morphisms isubst R .

Thus, if we want to internalise the whole sequence (subst p ) p:N in the syntax, we have at least three solutions: we can choose the algebraic signature

p:N Θ (p) × Θ p
which is rough in the sense that the above invariance and coherence is not reflected; we can choose the presentable signature

p:N Q p ,
which reflects the invariance by permutation, but not more; and finally, if we want to reflect the whole coherence syntactically, we can choose the presentable signature

p:F Θ (p) × Θ p .
Thus, whenever we have a presentable signature, we can safely extend it by adding one or the other of the three above signatures, for a (more or less coherent) explicit substitution.

Ghani, Uustalu, and Hamana already studied this problem in [START_REF] Ghani | Explicit substitutions and higher-order syntax[END_REF]. Our solution proposed here does not require the consideration of a strength.

Example: Adding a coherent fixed-point operator

In the same spirit as in the previous section, we define, in this section,

• for each n ∈ N, a notion of n-ary fixed-point operator in a monad;

• a notion of coherent fixed-point operator in a monad, which assigns, in a "coherent" way, to each n ∈ N, an n-ary fixed-point operator.

We furthermore explain how to safely extend any presentable syntax with a syntactic coherent fixed-point operator.

There is one fundamental difference between the integrated substitution of the previous section and our coherent fixed points: while every monad has a canonical integrated substitution, this is not the case for coherent fixed-point operators.

Let us start with the unary case.

Definition 72. A unary fixed-point operator for a monad R is a module morphism f from R ′ to R that makes the following diagram commute,

R ′ R ′ × R R (id R ′ ,f ) f σ
where σ is the substitution morphism defined in Lemma 33.

Accordingly, the signature for a syntactic unary fixpoint operator is Θ ′ , ignoring the commutation requirement (which we address later in Section 4.4.4, after extending signatures induced by parametric modules with equations).

Let us digress here and examine what the unary fixpoint operators are for the lambda calculus, more precisely, for the monad LC βη of the lambda-calculus modulo βand η-equivalence. How can we relate the above notion to the classical notion of fixedpoint combinator? Terms are built out of two constructions, app : LC βη × LC βη → LC βη and abs : LC ′ βη → LC βη . A fixed-point combinator is a term Y satisfying, for any (possibly open) term t, the equation

app(t, app(Y, t)) = app(Y, t).
Given such a combinator Y , we define a module morphism Ŷ : LC ′ βη → LC βη . It associates, to any term t depending on an additional variable * , the term Ŷ (t) := app(Y, abs t). This term satisfies t{ * := Ŷ (t)} = Ŷ (t), which is precisely the diagram of Definition 72 for a unary fixed-point operator. Thus, Ŷ is a unary fixed-point operator for the monad LC βη . Conversely, we have: Proposition 73. Any fixed-point combinator in LC βη comes from a unique fixed-point operator.

Proof. We construct a bijection between the subset of LC βη ∅ consisting of (closed) fixed-point combinator on the one hand and the set of module morphisms from LC ′ βη to LC βη satisfying the fixed-point property on the other hand.

A closed lambda term t is mapped to the morphism u → t u := app(t, abs u). We have already seen that if t is a fixed-point combinator, then t is a fixed-point operator.

For the inverse function, note that a module morphism f from LC ′ βη to LC βη induces a closed term Y f := abs(f 1 (app( * , * * ))) where f 1 : LC βη ({ * , * * }) → LC βη ({ * }).

A small calculation shows that Y → Ŷ and f → Y f are inverse to each other. It remains to be proved that if f is a fixed-point operator, then Y f satisfies the fixedpoint combinator equation. Let t ∈ LC βη X, then we have

app(Y f , t) = app(abs f X (app( * , * * )), t) (3.5) = f X (app(t, * * )) (3.6) = app(t, f X (app(t, * * ))) (3.7) = app(t, app(Y f , t)) (3.8)
where (3.5) comes from the definition of Y f (and naturality of f ). Equality (3.6) follows from β-reduction, Equality 3.7 from the definition of a fixed-point operator. Finally, Equality 3.8 comes from the equality app(Y f , t) = f X (app(t, * * )), which is obtained by chaining the equalities from (3.5) to (3.6). This concludes the construction of the bijection.

After this digression, we now turn to the n-ary case.

Definition 74.

• A rough n-ary fixed-point operator for a monad R is a module morphism f : (R (n) ) n → R n making the following diagram commute:

(R (n) ) n id (R (n) ) n ,f ,..,f / / f (R (n) ) n × (R n ) n ∼ = R n (R (n) × R n ) n (substn) n o o
where subst n is the n-substitution as in Section 3.8.3.

• An n-ary fixed-point operator is just a rough n-ary fixed-point operator which is furthermore invariant under the natural action of the permutation group S n .

The type of f above is canonically isomorphic to

(R (n) ) n + (R (n) ) n + . . . + (R (n) ) n → R, which we abbreviate to 6 n × (R (n) ) n → R.
Accordingly, a natural signature for encoding a syntactic7 rough n-ary fixpoint operator is n × (Θ (n) ) n .

Similarly, a natural signature for encoding a syntactic n-ary fixpoint operator is (n × (Θ (n) ) n )/S n obtained by quotienting the previous parametric module by the action of S n . Now we let n vary and say that a total fixed-point operator on a given monad R assigns to each n ∈ N an n-ary fixpoint operator on R. Obviously, the natural signature for the encoding of a syntactic total fixed-point operator is n (Θ (n) ) n /S n . Alternatively, we may wish to discard those total fixed-point operators that do not satisfy some coherence conditions analogous to what we encountered in Section 3.8.3, which we now introduce.

Let R be a monad with a sequence of module morphisms fix n : n × (R (n) ) n → R. We call this family coherent if, for any p, q ∈ N and u : p → q, the following diagram commutes:

p × (R (p) ) q p×(R (p) ) u / / u×(R (u) ) q p × (R (p) ) p fixp q × (R (q) ) q fixq / / R (3.9)
These conditions have an interpretation in terms of a coend, just as we already encountered in Section 3.8.3. This leads us to the following Definition 75. Given a monad R, we define a coherent fixed-point operator on R to be a module morphism from n:F n × (R (n) ) n to R where, for every n ∈ N, the n-th component is a (rough) 8 n-ary fixpoint operator. Now, the natural signature for a syntactic coherent fixed-point operator is n:F n × (Θ (n) ) n . Thus, given a presentable signature Σ, we can safely extend it with a syntactic coherent fixed-point operator by adding the presentable signature

n:F n × (Θ (n) ) n to Σ.

ALGEBRAIC 2-SIGNATURES FOR MONADS

This chapter is adapted from [START_REF] Ahrens | Modular Specification of Monads Through Higher-Order Presentations[END_REF].

The presentable signatures of Chapter 3 allow to specify syntaxes satisfying some equations by considering colimits of algebraic parametric modules. However, it seems quite limited: for example, we don't know how to specify an associative operation by a presentable signature. This motivates the work of the present chapter: we identify the class of algebraic 2-signatures which are effective: they are particular signatures over the category of monads consists of extensions of signatures induced by parametric modules with a family of equational arities.

It is not clear if any syntax generated by a presentable signature can also be generated by an algebraic 2-signature, although we do not know of any counter-example. Conversely, algebraic 2-signatures take into account operations that we do not know how to specify using a presentable signature, such as an associative operation. Signatures induced by parametric modules and models in the sense of Chapter 3 are referred to as 1-signatures and 1-models in this chapter.

Introduction

There is a well-established theory of presentations of monads through generating (firstorder) operations equipped with relations among the corresponding derived operations. Algebraic 1-signatures can be considered as generating 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 [START_REF] Fiore | Abstract Syntax and Variable Binding[END_REF], Gabbay and Pitts [GP99], and Hofmann [START_REF] Hofmann | Semantical Analysis of Higher-Order Abstract Syntax[END_REF].

If p : Σ → R is a monad epimorphism, we understand that R is generated by a family of operations whose binding arities are given by Σ, subject to suitable identifications. In particular, for Σ := Θ × Θ + Θ ′ , Σ may be understood as the monad LC of syntactic terms of the lambda calculus (see Section 3.2), and we have an obvious epimorphism p : Σ → LC βη , where LC βη is the monad of lambda-terms modulo β and η. In order to cover such equations, the approach in the first-order case suggests to identify p as the coequalizer of a pair of parallel arrows from T to Σ where T is again a "free" monad. Let us see what comes out when we attempt to find such an encoding for the β-equation of the monad LC βη . It should say that for each set X, the following two maps from Σ(X + { * }) × Σ(X) to Σ(X),

• (t, u) → app(abs(t), u)

• (t, u) → t{ * → u} are equal.
Here a problem occurs, namely that the above collections of maps, which can be understood as mere natural transformations, cannot be understood as morphisms 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 natural transformations: indeed they are morphisms of modules over Σ. Accordingly, a (second-order) presentation for a monad R could be a diagram

T / / f / / Σ p / / R (4.1)
where Σ is an algebraic signature, Σ is the associated free monad, T is a module over Σ, f is a pair of morphisms of modules over Σ, 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 "1 . To this end, recall that we introduced the category Mon Σ "of models of Σ", whose objects are monads "equipped with an action of Σ" (Definition 45). Of course Σ is equipped with such an action which turns it into the initial object. Now, we define the full subcategory of models satisfying the equation f , and require R to be the initial object therein. Our definition is suited to 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 our notion of 2-signature, which is similar to that introduced by Ahrens [Ahr16] in a slightly different context and is a particular case of signature over the category of monads. Now we are ready to formulate our main problem: given a 2-signature (Σ, E), where E is a family of parametric equations as above, does the subcategory of models of Σ 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 107).

This provides a construction of a monad from an algebraic 2-signature, and we prove furthermore (see Theorem 102) 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 Theorem 54 for 1-signatures.

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 4.4), and we also show through a simple example how our recursion principle applies (see Section 4.5).

Computer-checked formalization A summary of our formalization regarding 2signatures is available at https://initialsemantics.github.io/doc/50fd617/Modules. SoftEquations.Summary.html.

2-Signatures and their models

In this section we study 2-signatures and models of 2-signatures. A 2-signature is a signature over the category of monads consisting of a 1-signature Σ and a family of particular equational Σ-arities. We first explain which equational Σ-arities are involved.

Equations

Our equations are analogous to those considered by Ahrens in [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF]: they are parallel module morphisms parametrized by the models of the underlying 1-signature. They are particular equational arities in the sense of Chapter 2. The underlying notion of 1-model is essentially the same as in [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF], even if, there, such equations are interpreted instead as inequalities.

Throughout this subsection, we fix an arbitray signature Σ over the category of monads, that we instantiate in the examples with particular 1-signatures.

We first give a direct definition as an equational arity (Definition 78), and then rephrase it to give a more intuitive one as a parallel pair of morphisms (Remark 82).

Definition 76. We define a Σ-module to be a functor T from the category of models of Σ to the category Mod commuting with the forgetful functors to the category Mon of monads,

Mon Σ # # T / / Mod z z

Mon

Example 77. To each parametric module Ψ is associated, by precomposition with the projection from Mon Σ to Mon, a Σ-module still denoted Ψ. All the Σ-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 Σ-module Θ, and, more generally, for any natural number n ∈ N, a Σ-module Θ (n) . Also we have another fundamental Σ-module (arising in this way from) Σ itself, if Σ is induced by a paremtric module.

Definition 78. A Σ-equation is a Σ-arity (D, a, u, v) in the sense of Chapter 2, where • D is the category determined by two Σ-modules Ψ and Φ as follows:

objects are models R of Σ equipped with a R-module morphism h : Ψ(R) →

Φ(R),

morphisms between (R, h) and (S, i) are model morphisms f : R → S such that the following diagram commutes in the category of functors

Ψ(R) h / / Ψ(f ) Φ(R) Φ(f ) Ψ(S) i / / Φ(S)
;

• a : D → Mon Σ is the canonical forgetful functor;

Note that such an arity is always equational (Definition 7).

In the following, we provide an alternative description of a Σ-equation as a parallel pair of Σ-module morphisms (Remark 82).

Definition 79. Let S and T be Σ-modules. We define a morphism of Σ-modules from S to T to be a natural transformation from S to T which becomes the identity when postcomposed with the forgetful functor Mod → Mon.

Example 80. Each parametric module morphism Ψ → Φ upgrades into a morphism of Σ-modules. Further in that vein, if Σ is a parametric module, there is a morphism of

Σ-modules τ Σ : Σ → Θ. It is given, on a model (R, m) of Σ, by m : Σ(R) → R.
(Note that it does not arise from a morphism of parametric modules.) When the context is clear, we write simply τ for this morphism, and call it the tautological morphism of Σ-modules.

Proposition 81. Our Σ-modules and their morphisms, with the obvious composition and identity, form a category.

Remark 82. A Σ-equation (D, a, u, v) is uniquely determined by a pair of parallel morphisms of Σ-modules e 1 , e 2 : Φ → Ψ:

• D is the category determined by the Σ-modules Φ and Ψ, as in Definition 78;

• a : D → Mon Σ is the canonical forgetful functor;

• u maps a model R to (R, e 1,R );

• v maps a model R to (R, e 2,R ).

Notation 83. Thanks to this remark, we allow ourselves to identify Σ-equations with pairs of parallel Σ-module morphisms e 1 , e 2 : Φ → Ψ in the following, that we denote e 1 = e 2 .

Example 84 (Commutativity of a binary operation). Here we instantiate our fixed 1signature as follows: Σ := Θ × Θ. In this case, we say that τ 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 swap : Θ 2 -→ Θ 2 that exchanges the two components of the direct product. Again by Example 80, we have an induced morphism of Σ-modules, still denoted swap.

Then, the Σ-equation for commutativity is given by the two morphisms of Σ-modules

Θ 2 swap / / Θ 2 τ / / Θ Θ 2 τ / / Θ .
See also Section 4.4.1 where we explain in detail the case of monoids.

For the example of the lambda calculus with β-and η-equality (given in Example 86), we need to introduce currying: Definition 85. By abstracting over the base monad R the adjunction in the category of R-modules of Proposition 34, we can perform currying of morphisms of parametric modules: given a morphism of parametric modules

Σ 1 × Θ → Σ 2 it produces a new morphism Σ 1 → Σ ′ 2 .
By Example 77, currying acts also on morphisms of Σ-modules. Conversely, given a morphism of parametric modules (resp.

Σ-modules) Σ 1 → Σ ′ 2 , we can define the uncurryied map Σ 1 × Θ → Σ 2 .
Example 86 (β-and η-conversions). Here we instantiate our fixed 1-signature as follows: Σ LC := Θ × Θ + Θ ′ . This is the 1-signature of the lambda calculus. We break the tautological Σ-module morphism into its two pieces, namely app := τ • inl : Θ × Θ -→ Θ and abs := τ • inr : Θ ′ -→ Θ. Applying currying to app yields the morphism app 1 : Θ -→ Θ ′ of Σ LC -modules. The usual β and η relations are implemented in our formalism by two Σ LC -equations that we call e β and e η respectively:

e β : Θ ′ abs / / Θ app 1 / / Θ ′ Θ ′ 1 / / Θ ′ and e η : Θ app 1 / / Θ ′ abs / / Θ Θ 1 / / Θ .

2-signatures and their models

Definition 87. A 2-parametric module (Σ, E) is a pair of a parametric module Σ and a family E of Σ-equations. Such a 2-parametric module induces a signature over the category of monads that we call a 2-signature also denoted (Σ, E): it consists of the extension of the signature induced by Σ with the family E of equational arities.

Example 88. The 2-signature for a commutative binary operation is

(Θ 2 , τ • swap = τ ) (cf. Example 84).
Example 89. The 2-signature of the lambda calculus modulo β-and η-equality is

Υ LC βη = (Θ × Θ + Θ ′ , {e β , e η })
, where e β , e η are the Σ LC -equations defined in Example 86. Now, we unfold Definition 12 of the category of models in the case of a 2-signature (Definition 92).

Definition 90 (satisfies_equation). We say that a model M of a 1-signature Σ satisfies the Σ-equation e = (e 1 , e 2 ) if there is an action of e in M , that is, if

e 1 (M ) = e 2 (M ). If E is a family of Σ-equations, we say that a model M of Σ satisfies E if M satisfies each Σ-equation in E.
Remark 91. Given a monad R and a 2-signature Υ = (Σ, E), an action of Υ in R is an action of Σ in R such that the induced 1-model satisfies all the equations in E.

Definition 92 (category_model_equations). For a 2-parametric module (Σ, E), the category of models Mon (Σ,E) of (Σ, E) is the category of models of the induced 2signature. More concretely, it is the full subcategory of the category of models of Σ whose objects are models of Σ satisfying E, or equivalently, monads equipped with an action of (Σ, E).

Example 93. A model of the 2-signature

Υ LC βη = (Θ × Θ + Θ ′ , {e β , e η }) is given by a model (R, app R : R × R → R, abs R : R ′ → R) of the 1-signature Σ LC such that app R 1 • abs R = 1 R ′ and abs R • app R 1 = 1 R (see Example 86).
Definition 94. A 2-parametric module (Σ, E) is said to be effective if the induced 2signature is, that is, if its category of models Mon (Σ,E) has an initial object, denoted

(Σ, E).
In Section 4.2.4, we aim to find sufficient conditions for a 2-parametric module (Σ, E) to be effective.

Modularity for 2-signatures

In this section, we define the category 2PMod of 2-parametric modules and the category 2Mdls of models of 2-signatures, together with functors that relate them with the categories PMod and Mdls of parametric modules and 1-models. The situation is summarized in the commutative diagram of functors

2Mdls U Mdls ) ) F Mdls i i ⊤ 2π Mdls π 2PMod U PMod
) )

F PMod i i ⊤ PMod where • 2π is a Grothendieck fibration;
• π is the Grothendieck fibration defined in Section 3.4.2;

• U PMod is a coreflection and preserves colimits; and

• U Mdls is a coreflection.

As a simple consequence of this data, we obtain, in Theorem 102, a modularity result in the sense of Ghani, Uustalu, and Hamana [START_REF] Ghani | Explicit substitutions and higher-order syntax[END_REF]: it explains how the initial model of a pushout of 2-parametric modules is the pushout of the initial models of the summands2 .

We start by defining the category 2PMod of 2-parametric modules:

Definition 95 (TwoSig_category). Given 2-parametric modules (Σ 1 , E 1 ) and (Σ 2 , E 2 ), a morphism of 2-parametric modules from

(Σ 1 , E 1 ) to (Σ 2 , E 2 ) is a morphism of parametric modules m : Σ 1 → Σ 2 such that for any model M of Σ 2 satisfying E 2 , the Σ 1 -model m * M satisfies E 1 .
These morphisms, together with composition and identity inherited from parametric modules, form the category 2PMod.

We now study the existence of colimits in 2PMod. We know that PMod is cocomplete, and we use this knowledge in our study of 2PMod, by relating the two categories:

Let F PMod : PMod → 2PMod be the functor which associates to any parametric module Σ the empty family of equations, F PMod (Σ) := (Σ, ∅). Call U PMod : 2PMod → PMod the forgetful functor defined on objects as U PMod (Σ, E) := Σ.

Lemma 96 (TwoSig_OneSig_is_right_adjoint, OneSig_TwoSig_fully_faithful). We have F PMod ⊣ U PMod . Furthermore, U PMod is a coreflection.

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

Theorem 97 (TwoSig_PushoutsSET). The category 2PMod has pushouts.

Coproducts are computed by taking the union of the equations and the coproducts of the underlying parametric modules. Coequalizers are computed by keeping the equations of the codomain and taking the coequalizer of the underlying parametric modules. Thus, by decomposing any colimit into coequalizers and coproducts, we have this more general result: Proposition 98. The category 2PMod is cocomplete and U PMod preserves colimits.

We now turn to our modularity result, which states that the initial model of a coproduct of two 2-parametric modules is the coproduct of the initial models of the summands. 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 2signatures": Definition 99. The category (Σ,E) Mon (Σ,E) , or 2Mdls for short, has, as objects, pairs

((Σ, E), M ) of a 2-parametric modules (Σ, E) and a model M of (Σ, E). A morphism from ((Σ 1 , E 1 ), M 1 ) to ((Σ 2 , E 2 ), M 2 ) is a pair (m, f ) consisting of a morphism m : (Σ 1 , E 1 ) → (Σ 2 , E 2 ) of 2-parametric modules and a morphism f : M 1 → m * M 2 of (Σ 1 , E 1 )-models (or, equivalently, of Σ 1 -models).
This category of models of 2-signatures contains the models of 1-signatures as a coreflective subcategory. Let F Mdls : Mdls → 2Mdls be the functor which associates to any 1-model (Σ, M ) the empty family of equations, F Mdls (Σ, M ) := (F PMod (Σ), M ). Conversely, the forgetful functor U Mdls : 2Mdls → Mdls maps ((Σ, E), M ) to (Σ, M ).

Lemma 100 (TwoMod_OneMod_is_right_adjoint, OneMod_TwoMod_fully_faithful). We have F Mdls ⊣ U Mdls . Furthermore, U Mdls is a coreflection.

The modularity result is a consequence of the following technical result: Proposition 101 (TwoMod_cleaving). The forgetful functor 2π from 2Mdls to 2PMod is a Grothendieck fibration.

The modularity result below is analogous to the modularity result for 1-signatures (Theorem 54):

Theorem 102 (Modularity for 2-signatures, pushout_in_big_rep). Suppose we have a pushout diagram of effective 2-parametric modules, as on the left below. This pushout gives rise to a commutative square of morphisms of models in 2Mdls as on the right below, where we only write the second components, omitting the (morphisms of) parametric modules. This square is a pushout square.

Υ 0 / / Υ 1 Υ 2 / / Υ Υ 0 / / Υ 1 Υ 2 / / Υ
Intuitively, the 2-signatures Υ 1 and Υ 2 specify two extensions of the 2-signature Υ 0 , and Υ is the smallest extension containing both these extensions. By Theorem 102 the initial model of Υ is the "smallest model containing both the languages generated by Υ 1 and Υ 2 ".

Initial Semantics for 2-Signatures

We now turn to the problem of constructing the initial model of a 2-signature (Σ, E). More specifically, we identify sufficient conditions for (Σ, E) to be effective. Our approach is very straightforward: we seek to construct the initial object (Σ, E) by applying a suitable quotient construction to the initial object Σ of Mon Σ . This leads immediately to our first requirement on (Σ, E), which is that Σ must be an effective 1-signature. (For instance, we can assume that Σ is an algebraic 1-signature, see Theorem 53.) This is a very natural hypothesis, since in the case where E is the empty family of Σ-equations, it is obviously a necessary and sufficient condition. Some Σ-equations are never satisfied. In that case, the category Mon (Σ,E) is empty. For example, given any 1-signature Σ, consider the Σ-equation inl, inr : Θ ⇒ Θ+Θ given by the left and right inclusion. This is obviously an unsatisfiable Σ-equation. We have to find suitable hypotheses to rule out such unsatisfiable Σ-equations. This motivates the notion of elementary equations.

Definition 103. Given a 1-signature Σ, a Σ-module S is nice if S sends pointwise epimorphic Σ-model morphisms to pointwise epimorphic module morphisms.

Definition 104 (elementary_equation). Given a 1-signature Σ, an elementary Σequation is a Σ-equation such that

• the target is a finite derivative of the tautological Σ-module Θ, i.e., of the form Θ (n) for some n ∈ N, and

• the source is a nice Σ-module.

Example 105. Any algebraic parametric module is nice (Example 65). Thus, any Σequation between an algebraic parametric module and Θ (n) , for some natural number n, is elementary.

Definition 106. A 2-parametric module (Σ, E) is said algebraic if Σ is algebraic and
E is a family of elementary equations. The induced 2-signature is then also called algebraic.

Theorem 107 (elementary_equations_on_alg_preserve_initiality). Any algebraic 2-signature is effective.

The proof of Theorem 107 is given in Section 4.3.

Example 108. The 2-signature of lambda calculus modulo β and η equations given in Example 89 is algebraic. Its initial model is precisely the monad LC βη of lambda calculus modulo βη equations. The instantiation of the formalized Theorem 107 to this 2-signature is done3 in LCBetaEta.

Let us mention finally that, using the axiom of choice, we can take a similar quotient on all the 1-models of Σ: Proposition 109 (ModEq_Mod_is_right_adjoint, ModEq_Mod_fully_faithful). Here we assume the axiom of choice. The forgetful functor from the category Mon (Σ,E) of 2-models of (Σ, E) to the category Mon Σ of Σ-models has a left adjoint. Moreover, the left adjoint is a reflector.

Proof of Theorem 107

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

Lemma 110 (elementary_equations_preserve_initiality). Let (Σ, E) be a 2-parametric module such that:

1. Σ sends epimorphic natural transformations to epimorphic natural transformations,

2. E is a family of elementary equations, 3. Σ is effective, 4. the initial 1-model of Σ preserves epimorphisms, 5. the image by Σ of the initial 1-model of Σ preserves epimorphisms.

Then, the 2-signature (Σ, E) is effective.

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

The "epimorphism" hypotheses of Lemma 110 are used to transfer structure from the initial model Σ of the 1-signature Σ 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 Set is split and thus preserved by any functor.

• Condition 5 is a consequence of Condition 4 if Σ sends monads preserving epimorphisms to modules preserving epimorphisms.

• If Σ is algebraic, then Conditions 1, 3, 4 and 5 are satisfied (Example 65 and Lemma 66).

2. Construct the quotient model Σ/(f i ) according to Proposition 112 where (f i : Σ → S i ) i is the collection of all initial Σ-morphisms from Σ to any Σ-model satisfying the equations. We denote by σ/(f i ) : Σ( Σ/(f i )) → Σ/(f i ) the action of the quotient model.

3. Given a model M of the 2-signature (Σ, E), we obtain a morphism i M : Σ/(f i ) →

M from Proposition 112. Uniqueness of i M is shown using epimorphicity of the projection p : Σ → Σ/(f i ). For this, it suffices to show uniqueness of the composition i M • p : Σ → M in the category of 1-models of Σ, which follows from initiality of Σ.

4. The verification that Σ/(f i ), σ/(f i ) satisfies the equations is given below. Actually, it follows the same line of reasoning as in the proof of Proposition 111 that Σ/(f i ) satisfies the monad equations.

Let e = (e 1 , e 2 ) : U → Θ (n) be an elementary equation of E. We want to prove that the two arrows

e 1, Σ/(f i ) , e 2, Σ/(f i ) : U ( Σ/(f i )) -→ ( Σ/(f i )) (n)
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

e 1, Σ/(f i ) • U (p) = e 2, Σ/(f i ) • U (p) ,
which, by naturality of e 1 and e 2 , is equivalent to

p (n) • e 1, Σ = p (n) • e 2, Σ.
Let x be an element of U ( Σ) and let us show that p (n) (e 1, Σ(x)) = p (n) (e 2, Σ(x)). By definition of Σ/(f i ) as a pointwise quotient (see Proposition 111), it is enough to show that for any j, the equality f

(n) j (e 1, Σ(x)) = f (n) j (e 2, Σ(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 .

Examples of algebraic 2-signatures

We already illustrated our theory by looking at the paradigmatic case of lambda calculus modulo β-and η-equations (Examples 86 and 108). 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-parametric modules encompasses the algebraic parametric modules 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 107.

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 : M (X) × M (X) -→ M (X) and e X : 1 -→ M (X) given by the product and the identity respectively. It can be easily verified that m : M 2 -→ M and e : 1 -→ M are M -module morphisms. In other words,

(M, ρ) = (M, [m, e]) is a model of the 1-signature Σ = Θ × Θ + 1.
We break the tautological morphism of Σ-modules (cf. Example 80) into constituent pieces, defining m := τ • inl : Θ × Θ → Θ and e := τ • inr : 1 → Θ.

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

Θ 3 Θ×m / / Θ 2 m / / Θ Θ 3 m×Θ / / Θ 2 m / / Θ Θ e×Θ / / Θ 2 m / / Θ Θ 1 / / Θ Θ Θ×e / / Θ 2 m / / Θ Θ 1 / / Θ
and we denote by E the family consisting of these three Σ-equations. All are elementary since their codomain is Θ, and their domain a product of Θs.

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

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

Colimits of algebraic 2-parametric modules

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

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

Proposition 113. Given any colimit of algebraic 2-parametric modules, there is an algebraic 2-signature yielding an isomorphic category of models.

Proof. As the class of algebraic 2-parametric modules is closed under arbitrary coproducts, using the decomposition of colimits into coproducts and coequalizers, any colimit Ξ of algebraic 2-parametric modules can be expressed as a coequalizer of two morphisms f, g between some algebraic 2-parametric modules

(Σ 1 , E 1 ) and (Σ 2 , E 2 ), (Σ 1 , E 1 ) f / / g / / (Σ 2 , E 2 ) p / / Ξ = (Σ 3 , E 2 ) .
where Σ 3 is the coequalizer of the parametric module morphisms f and g. Note that the set of equations of Ξ is E 2 , by construction of the coequalizer in the category of 2-parametric modules. Now, consider the algebraic 2-signature Ξ ′ = (Σ 2 , E 2 + (4.2)) consisting of the 1-signature Σ 2 and the equations of E 2 plus the following elementary equation (see Examples 80 and 105):

Σ 1 f / / Σ 2 τ Σ 2 / / Θ Σ 1 g / / Σ 2 τ Σ 2 / / Θ . (4.2)
We show that Mon Ξ and Mon Ξ ′ are isomorphic. A model of Ξ ′ is a monad R together with an R-module morphism r : Σ 2 (R) → R such that r • f R = r • 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 Σ 3 (R) → R satisfying the equations of E 2 , i.e., giving R an action of Ξ = (Σ 3 , E 2 ).

It is straightforward to check that this correspondence yields an isomorphism between the category of models of Ξ and the category of models of Ξ ′ . This proposition, together with the following corollary, allow us to recover all the examples presented in Chapter 3, as colimits of algebraic parametric modules: syntactic commutative binary operator, maximum operator, application à la differential lambda calculus, syntactic closure operator, integrated substitution operator, coherent fixpoint operator.

Corollary 114. If F is a finitary endofunctor on Set, then there is an algebraic 2signature whose category of models is isomorphic to the category of 1-models of the 1-signature F • Θ.

Proof. It is enough to prove that F • Θ is a colimit of algebraic parametric modules.

As F is finitary, it is isomorphic to the coend n∈F F (n) × _ n where F is the full subcategory of Set of finite ordinals (see, e.g., [VK11, Example 3.19]). As colimits are computed pointwise, the parametric module F • Θ is the coend n∈F F (n) × Θ n , and as such, it is a colimit of algebraic 2-parametric modules. However, we do not know whether we can recover Theorem 57 stating that any presentable 1-signature is effective.

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 [Man76, Definition 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 114 says how to encode the 1-signature T • Θ as an algebraic 2-signature (Σ T , E T ). Models are monads R together with an R-linear morphism r :

T • R → R.
Now, for any model (R, m) of T • Θ, we would like to enforce the usual T -algebra equations on the action m. This is done thanks to the following equations, where τ denotes the tautological morphism of T • Θ-modules:

Θ η T •Θ / / T • Θ τ / / Θ Θ 1 / / Θ T • T • Θ µ T •Θ / / T • Θ τ / / Θ T • T • Θ T τ / / T • Θ τ / / Θ (4.3)
The first equation is clearly elementary. The second one is elementary thanks to the following lemma:

Lemma 115. Let F be a finitary endofunctor on Set. Then F preserves epimorphisms.

Proof. This is a consequence of the axiom of choice, because then any epimorphism in the category of Set is split, and thus preserved by any functor. Here we provide an alternative proof which does not rely on the axiom of choice. (However, it may require the excluded middle, depending on the chosen definition of finitary functor.)

As F is finitary, it is isomorphic to the coend n∈F F (n)×_ n [VK11, Example 3.19]
. By decomposing it as a coequalizer of coproducts, we get an epimorphism α : n∈N F (n)× _ n → F . Now, let f : X → Y be a surjective function between two sets. We show that F (f ) is epimorphic. By naturality, the following diagram commutes:

n∈N F (n) × X n F (n)×f n / / α X n∈N F (n) × Y n α Y F (X) F (f ) / / F (Y )
. The top-right composite is epimorphic by composition of epimorphisms. Thus, the bottom-left composite is also epimorphic, hence so is F (f ) as the last morphism of this composition.

In conclusion, we have exhibited the algebraic 2-signature (Σ T , E ′ T ), where E ′ T extends the family E T with the two elementary equations of Diagram 4.3. This signature allows to enrich any other algebraic 2-signature with the operations of the algebraic theory T , subject to the relevant equations.

Fixpoint operator

Here, we show the algebraic 2-signature corresponding to a fixpoint operator. In Section 3.8.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 Section 3.8.4, now including the fixpoint equations, can also be specified, in an analogous way, via an algebraic 2-signature.

Let us start by recalling Definition 72: a unary fixpoint operator for a monad R is a module morphism f from R ′ to R that makes the following diagram commute, where σ is the substitution morphism defined as the uncurrying (see Definition 85) of the identity morphism on Θ ′ :

R ′ R ′ × R R (id R ′ ,f ) f σ R
In order to rephrase this definition, we introduce the obviously algebraic 2-signature Υ fix consisting of the 1-signature Σ fix = Θ ′ and the family E fix consisting of the single following Σ fix -equation:

e fix : Θ ′ 1,τ / / Θ ′ × Θ σ / / Θ Θ ′ τ / / Θ (4.4)
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 Υ fix in R.

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.

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 Υ = (Σ, E) to an arbitrary monad T .

Proposition 116 (Recursion principle). Let S be the monad underlying the initial model of the 2-signature Υ. To any action a of Υ in T is associated a monad morphism â : CHAPTER 5

REDUCTION MONADS AND THEIR SIGNATURES

In this chapter, we study reduction monads, which are essentially the same as monads relative to the free functor from sets into graphs and signatures over their category. The statements here are not formalized.

Reduction monads abstract two aspects of the lambda calculus: on the one hand, in the monadic viewpoint, it is an object equipped with a well-behaved substitution; on the other hand, in the graphical viewpoint, it is an oriented graph whose vertices are terms and whose edges witness the reductions between two terms.

We study presentations of reduction monads. To this end, we propose a notion of reduction signature. They are, in particular, signatures in the sense of Chapter 2 consisting of a signature over the category of monads (for example, a 2-signature, as introduced in Chapter 4) extended with a family of arities specifying reduction rules.

As usual, such a signature plays the role of a virtual presentation, and specifies arities for generating operations-possibly subject to equations-together with arities for generating reduction rules.

The main result of this chapter identifies a class of effective reduction signatures. In particular, the lambda calculus is naturally specified by such a signature.

Introduction

The lambda calculus has been a central object in theoretical computer science for decades. However, the corresponding mathematical structure does not seem to have been identified once and for all. In particular, two complementary viewpoints on the (pure untyped) lambda calculus have been widespread: some consider it as a graph (or a preorder, or a category), while others view it as a monad (on the category of sets).

The first account incorporates the β-reduction, while the second addresses substitution but incorporates only the β-equality. Merging these two perspectives led Lüth and Ghani [START_REF] Lüth | Monads and Modular Term Rewriting[END_REF] to consider monads on the category of preordered sets, and Ahrens [START_REF] Ahrens | Modules over relative monads for syntax and semantics[END_REF] to consider monads relative to the free functor from sets into preorders. In the present chapter, we propose a variant of their approaches. Here we call reduction monad a monad relative to the natural injection of sets in graphs, and of course the lambda-calculus yields such a reduction monad. Our main contribution concerns the generation of reduction monads by syntactic (possibly binding) operations (possibly subject to equations) and reduction rules. As is common in similar contexts, we propose a notion of signature for reduction monads, which we call "reduction signatures". Each reduction signature comes equipped with the category of its models: such a model is a reduction monad "acted upon" by the signature. A reduction signature may be understood as a virtual presentation: when an initial model exists (that is, when the signature is effective), it inherits a kind of presentation given by the action of the signature. We identify a natural criterion for a signature to be effective. As should be expected, we give an effective reduction signature specifying the lambda calculus with its reduction rules, which yields a new, high-level definition of the (pure untyped) lambda calculus.

Terminology and notations

In this section, we set up some terminology and notations that we use in this chapter.

Signature for monads By signatures for monads, we mean signatures over the category of monads. In the examples, they are in particular 2-signatures of Chapter 4, or just 1-signatures of Chapter 3. The letter Σ is usually associated with a signature for monads.

Models of signature for monads

In order to avoid any confusion with the notion of model of operational signatures that we introduce here, we refer to models of a signature Σ for monads as Σ-monads.

Substitution

Let R be a monad, M be a R-module, t an element of M (X) and f a function from X to R(Y ). Then, we denote by t{f } ∈ R(Y ) the substitution of all the variables in t by the corresponding term given by f .

Unary substitution

We abbreviate t{x → if x = y then u else x} as t{y := u}.

Plan of the chapter

In Section 5.2, we define reduction monads. In Section 5.3, we present our take on reduction rules. This enables us to define a class of signatures over the category of reduction monads-reduction signatures-in Section 5.4. Section 5.5 is devoted to the proof of our theorem of effectivity for these signatures, under some natural assumptions. Then, in Section 5.6, we give a detailed example of a reduction signature specifying the lambda calculus with explicit substitutions of [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF]. Finally, in Section 5.7, we explain the recursion principle which, as usual, can be derived from initiality in our categories of models.

Reduction monads

Here below, we define the category of reduction monads in Section 5.2.1. We also consider some examples of reduction monads, in Section 5.2.2.

The category of reduction monads

Definition 117. A reduction monad R is given by: 1. a monad on sets (the monad of terms), that we still denote by R, or by R when we want to be explicit;

2. an R-module Red(R) (the module of reductions);

3. a morphism of R-modules red R : Red(R) → R × R (source and target of rules).

We set source

R := π 1 • red R : Red(R) → R, and target R := π 2 • red R : Red(R) → R
Notation 118. For a reduction monad R, a set X, and elements s, t ∈ R(X), we think of the fiber red R (X) -1 (s, t) as the set of "reductions from s to t". We sometimes write m : s ◮ t : R(X), or even m : s ◮ t when there is no ambiguity, instead of m ∈ red R (X) -1 (s, t).

Remark 119. Note that for a given reduction monad R, set X, and s, t : R(X), there can be multiple reductions from s to t, that is, the fibre s ◮ t is not necessarily a subsingleton.

Remark 120. Let R be a reduction monad, X and Y two sets, f : X → R(Y ) a substitution, and u and v two elements of R(X) related by m : u ◮ v. The module structure on Red(R) yields a reduction denoted m{f } between u{f } and v{f }.

However, if we are given two substitutions f and g, and for all x ∈ X, a reduction m x : f (x) ◮ g(x), then it does not follow that there is a reduction between u{f } and u{g}. This leaves the door open for non-congruent reductions.

Our main examples of reduction monads are given by variants of the lambda calculus. We have collected these examples in Section 5.

Red(R) α / / red R Red(S) red S R × R f ×f / / S × S
commutes in the category of functors and natural transformations.

In Section 5.7 we specify morphisms of reduction monads via a recursion principle. Intuitively, a morphism (f, α) as above maps terms of R to terms of S via f , and reductions of R to reductions of S via α. Condition 3 states compatibility of the map of reductions with substitution. Condition 4 states preservation of source and target by the map of reductions: a reduction m : u ◮ v is mapped by α to a reduction α(m) :

f (u) ◮ f (v).
Proposition 122 (Category of reduction monads). Reduction monads and their morphisms, with the obvious composition and identity, form a category RedMon, equipped with a forgetful functor to the category of monads.

It turns out that reduction monads are the same as monads relative to the free functor from sets to graphs (for the definition of relative monads, see [ACU15, Definition 2.1]):

Theorem 123. The category of reduction monads is isomorphic to the category of monads relative to the functor mapping a set to its discrete graph.

Proof. This is obvious after unfolding the definitions.

Remark 124. In the previous theorem, the involved category of graphs has pairs of parallel functions E t / / s / / V as objects: E is the set of edges, V the set of vertices, s and t maps respectively any edge to its source and target. Adopting the indexed point of view rather than this fibrational approach, we obtain an equivalent (but not isomorphic) category: a graph is a set V of vertices, and for each pair of vertices there is a set of edges between them. Our notion of reduction monads could also be rephrased in this way, yielding an equivalent (but not isomorphic) category.

Examples of reduction monads

We are interested in reduction monads with underlying monad LC, the monad of syntactic lambda terms specified by the 1-signature Σ LC = Θ × Θ + Θ ′ .

Example 125 (Lambda calculus with head-β-reduction). Consider the reduction monad LC head-β given as follows:

1. the underlying monad is LC;

2. Red(R) is the module LC ′ × LC; 3. red R (X) is the morphism (u, v) → app(abs(u), v), u{ * := v} .
This reduction monad deserves to be called the reduction monad of the lambda calculus with head-β-reduction.

Example 126 (Lambda calculus with head-η-expansion). Consider the reduction monad LC head-η given as follows:

1. the underlying monad is LC; 2. Red(R) is the module LC; 3. red R (X) is the morphism t → t, abs(app(ιt, * )) , where ι : LC(X) → LC ′ (X) is the natural injection (weakening).

This reduction monad deserves to be called the reduction monad of the lambda calculus with head-η-expansion.

Obviously, to get the analogous reduction rule for the η-contraction, it is enough to swap, in the previous example, the components of the output of the morphism red R .

Given two reduction monads with the same underlying monad on sets, we define the amalgamation of the reduction monads as follows:

Definition 127. Given reduction monads R and S with the same underlying monad on sets, we define the reduction monad R ∐ S as follows:

1. the underlying monad on sets is still R (or, equivalently, S); 2. the R-module Red(R ∐ S) is the coproduct Red(R) ∐ Red(S).

3. the module morphism red R∐S is induced by red R and red S . This is the pushout, in the category of reduction monads, of uR → R and uR → S, with the reduction monad uR := (R, 0, !).

Example 128. The reduction monad LC head-β/η := LC head-β ∐LC head-η has, as reductions, β-reductions and η-expansions at the head of lambda terms.

So far we have only considered reductions at the root of a lambda term. The following construction allows us to propagate reductions into subterms. Definition 129. Let R be a reduction monad over the monad LC on sets. We define the reduction monad R cong as follows:

1. the underlying monad is LC; 2. Red(R cong )(X) is generated by the following constructions:

(a) for m : u ◮ v in Red(R), m is also in Red(R cong ) (b) for m : u ◮ v : LC(X) in Red(R cong ) and t ∈ LC(X), we have app-cong 1 (m, t) : app(u, t) ◮ app(v, t) (c) for m : u ◮ v : LC(X) in Red(R cong ) and t ∈ LC(X), we have app-cong 2 (t, m) :

app(t, u) ◮ app(t, v) (d) for m : u ◮ v : LC ′ (X) in Red(R cong ) we have abs-cong(m) : abs(u) ◮ abs(v) 3. red R cong is obvious.
Example 130. A reduction in the reduction monad LC β/η := (LC head-β/η ) cong is "one step" of β-reduction or η-expansion, anywhere in the source term.

The closure under identity and composition of reductions of a reduction monad is defined as follows:

Definition 131. Given a reduction monad R, we define the reduction monad R * as follows:

1. the underlying monad on sets is still R; 2. the R-module Red(R * ) is defined as follows. For n ∈ N we define the module Red(R) n of "n composable reductions", namely as the limit of the diagram

Red(R) source R v v target R ( ( Red(R) source R v v target R ( ( . . . source R w w R R R
with n copies of Red(R) (and hence n + 1 copies of R). We obtain n + 1 projections Example 132 (The reduction monad of the lambda calculus). The reduction monad of the lambda calculus is defined to be the reduction monad LC * β/η . In Section 5.4 we introduce signatures that allow for the specification of reduction monads. The signature specifying the reduction monad of lambda calculus of Example 130 is given in Example 152.

Reduction rules

In this section, we define an abstract notion of reduction rule over a signature for monads Σ (Section 5.3.2). We first focus, in Section 5.3.1, on the example of the congruence rule for the application construction in the signature Σ LC for the monad of the lambda calculus, in order to motivate the definitions. The purpose of a reduction rule over Σ is to be "validated" in a reduction monad equipped with an action of Σ (this is what we will call a reduction Σ-monad in Section 5.3.3). We make this notion of validation precise in Section 5.3.4, as an action of the reduction rule in the reduction Σ-monad. Finally, we give a protocol for specifying reduction rules in Section 5.3.5 that we apply in Section 5.3.6 to some examples.

Example: congruence rule for application

We give some intuitions of the definition of reduction rule with the example of the congruence rule for application, given, e.g., in Selinger's lecture notes [START_REF] Selinger | Lecture notes on the lambda calculus[END_REF], as follows:

T T ′ U U ′ app(T, U ) app(T ′ , U ′ )
This rule is parameterized by four metavariables: T , T ′ , U , and U ′ . The conclusion and the hypotheses are given by pairs of terms built out of these metavariables.

We formalize this rule as follows: for any monad R equipped with an application operation app : R×R → R, we associate a module of metavariables V(R) = R×R×R×R, one factor for each of the metavariables T , T ′ , U , and U ′ . Each hypothesis or conclusion is described by a parallel pair of morphisms from V(R) to R: for example, the conclusion c R : V(R) → R maps a set X and a quadruple (T, T ′ , U, U ′ ) to the pair (app(T, U ), app(T ′ , U ′ )). These assignments are actually functorial in R, and abstracting over R yields our notion of term-pair over the Σ-module V, as morphisms from V to Θ × Θ, where Σ is any signature including a single first-order binary operation app (for example, Σ LC ). The three term-pairs, one for each hypothesis and one for the conclusion, define the desired reduction rule. Now, we explain in which sense such a rule can be validated in a reduction monad R: intuitively, it means that for any set X, any quadrupe (T, T ′ , U, U ′ ) ∈ V(R), any reductions s : T ◮ T ′ and t : U ◮ U ′ , there is a reduction app-cong(s, t) : app(T, U ) ◮ app(T ′ , U ′ ). Of course, this only makes sense if the monad R underlying the reduction monad is equipped with an application operation, that is, with an operation of Σ app . We call such a structure a reduction Σ app -monad.

Definition of reduction rules

In this subsection, Σ is a signature for monads. We present our notion of reduction rule over Σ, from which we build reduction signatures in Section 5.4.

We begin with the definition of term-pair, alluded to already in Section 5.3.1:

Definition 133. Given a Σ-module V, a term-pair from V is a pair (n, p) of a natural number n and a morphism of Σ-modules p :

V → Θ (n) × Θ (n) .
Many term-pairs are of a particularly simple form, namely a pair of projections, which intuitively picks two among the available metavariables. Because of their ubiquity, we introduce the following notation: Definition 134. Let n 1 , . . . , n p be a list of natural numbers. For i, j ∈ {1, . . . p}, we define the pair projection π i,j and the projection π i as the following Σ-module morphisms, for any signature Σ:

π i,j : Θ (n 1 ) × . . . Θ (np) → Θ (n i ) × Θ (n j ) π i : Θ (n 1 ) × . . . Θ (np) → Θ (n i ) π i,j,R,X (T 1 , . . . , T p ) = (T i , T j ) π i,R,X (T 1 , . . . , T p ) = T i
Some term-pairs, such as the conclusions of the congruence rules for application and abstraction, are more complicated: intuitively, they are constructed from term constructions applied to metavariables.

Example 135 (term-pair of the conclusion of the congruence for application). The termpair corresponding to the conclusion app(T, U ) app(T ′ , U ′ ) of congruence for application (Section 5.3.1) is given by (0, c), on the Σ LC -module Θ 4 . Here, we have

c : V → Θ × Θ c R,X (T, T ′ , U, U ′ ) := app R,X (T, U ), app R,X (T ′ , U ′ )
More schematically:

c : Θ 4 app•π 1,3 ,app•π 2,4 / / Θ × Θ
We now give our definition of reduction rule, making precise the intuition developed in Section 5.3.1. Definition 136. A reduction rule A = (V, (n i , h i ) i∈I , (n, c)) over Σ is given by: • Metavariables: a Σ-module V of metavariables, that we sometimes denote by MVar A ;

• Hypotheses: a finite family of term-pairs (n i , h i ) i∈I from V;

• Conclusion: a term-pair (n, c) from V.

Example 137 (Reduction rule for congruence of application). The reduction rule A app-cong for congruence of application (Section 5.3.1) is defined as follows:

• Metavariables: V = Θ 4 for the four metavariables T , T ′ , U , and U ′ ;

• Hypotheses: Given by two term-pairs (0, h 1 ) and (0, h 2 ): More examples of reduction rules are given in Section 5.3.6.

h 1 : Θ 4 π 1,2 / / Θ × Θ h 2 : Θ 4 π 3,4 / / Θ × Θ

Reduction Σ-monads

As already said, the purpose of a reduction rule is to be validated in a reduction monad R. However, as the hypotheses or the conclusion of the reduction rule may refer to some operations specified by a signature Σ for monads, this reduction monad R must be equipped with an action of Σ, hence the following definition:

Definition 138. Let Σ be a signature for monads. The category RedMon Σ of reduction Σ-monads is the category of models of the pullback of Σ along the forgetful functor U : RedMon → Mon (see Chapter 2).

In other words, it is defined as the following pullback:

RedMon Σ / / RedMon Mon Σ / / Mon
More concretely, 123

• a reduction Σ-monad is a reduction monad R equipped with an action ρ of Σ in R, thus inducing a Σ-monad that we denote also by R, or by R when we want to be explicit;

• a morphism of reduction Σ-monads R → S is a morphism f : R → S of reduction monads compatible with the action of Σ, i.e, whose underlying monad morphism is a Σ-monad morphism.

Action of a reduction rule

Let Σ be a signature for monads. In this section, we introduce the notion of action of a reduction rule over Σ in a reduction Σ-monad. Intuitively, such an action is a "map from the hypotheses to the conclusion" of the reduction rule. To make this precise, we need to first take the product of the hypotheses; this product is, more correctly, a fibred product.

Definition 139. Let (n, p) be a term-pair from a Σ-module V, and R be a reduction Σ-monad. We denote by p * (Red(R) (n) ) the pullback of red

(n) R : Red(R) (n) → R (n) × R (n) along p R : V(R) → R (n) × R (n) : p * (Red(R) (n) ) / / Red(R) (n) red (n) R V(R) p R / / R (n) × R (n)
We denote by p * (red (n,c)) be a reduction rule, and R be a reduction

(n) R ) : p * (Red(R) (n) ) → V(R) the projection morphism on the left. Definition 140. Let A = (V, (n i , h i ) i∈I ,
Σ-monad. The R-module Hyp A (R) of hypotheses of A is i∈I/V(R) h * i Red(R) (n i ) , i.e.
, the fiber product of all the R-modules h * i Red(R) (n i ) along their projection to V(R). It thus comes with a projection hyp A (R) :

Hyp A (R) → V(R)
The R-module Con A (R) of conclusion of A is c * Red(R) (n) , and comes with a projection con A (R) :

Con A (R) → V(R).
Example 141. Let R be a reduction Σ LC -monad. The R-module of conclusion of the congruence reduction rule for application (Example 137) maps a set X to the set

Protocol for specifying reduction rules

In Section 5.3.6, we adopt the following schematic presentation of a reduction rule over a signature Σ:

s 1 (T 1 , . . . , T q )
t 1 (T 1 , . . . , T q ) . . . s n (T 1 , . . . , T q ) t n (T 1 , . . . , T q ) s 0 (T 1 , . . . , T q ) t 0 (T 1 , . . . , T q )

where s i and t i are expressions depending on metavariables T 1 , . . . , T q . Each pair (s i , t i ) defines a term-pair as follows:

p i : M 1 × • • • × M q → Θ (m i ) × Θ (m i )
p i,R,X (T 1 , . . . , T q ) := (s i (T 1 , . . . , T q ), t i (T 1 , . . . , T q )) (5.2)

where the Σ-modules M 1 , . . . , M q , and the natural numbers m 0 , . . . , m n are inferred for Equation (5.2) to be well defined for all i ∈ {0, . . . , n}.

The induced reduction rule is:

• Metavariables: the Σ-module of metavariables is V = M 1 × • • • × M q ;
• Hypotheses: the hypotheses are the term-pairs (m i , p i ) i∈{1,...,n} ;

• Conclusion: the conclusion is the term-pair (m 0 , p 0 ).

Typically, M i = Θ (n i ) for some natural number n i , as in the examples that we consider in this section. In practice, there are several choices for building the reduction rule out of such a schematic presentation, depending on the order in which the metavariables are picked. This order is irrelevant: the different possible versions of reduction rules are all equivalent, in the sense that taking one or the other as part of a reduction signature yields isomorphic category of models.

Examples of reduction rules

This section collects a list of motivating examples of reduction rules.

For the rest of this section, we assume that we have fixed a signature for monads Σ. For the example of the fixpoint operator (rule fix-Exp), we consider the 1-signature Σ fix , as described in Section 4.4.4. (without enforcing the fixpoint equation, which is replaced here by the reduction rule under consideration). A Σ fix -monad is a monad R equipped with an R-module morphism fix : R ′ → R.

Θ × Θ × Θ for (T, U, W ) (0, π 1,2 ), (0, π 2,3 ) (0, π 1,3 ) abs-Cong Σ LC Θ ′ × Θ ′ for (T, U ) (1, id) (0, abs × abs) β-Red Σ LC Θ ′ × Θ for (T, U ) (0, c β-Red ) η-Exp Σ LC Θ (0, (id, abs • ι)) fix-Exp Σ fix Θ ′ (0, c fix-Exp ) c β-Red,
Figure 5.2 lists the modules and term pairs for hypothesis and conclusion of each of these reduction rules. There, π i,j designates the pair projection described in Definition 134.

Signatures for reduction monads and Initiality

In this section, we define reduction signatures which are particular signatures over the category of reduction monads (see Section 5.4.1). They consist of a signature for monads Σ (more precisely, a pullback of such a signature along the forgetful functor from reduction monads to monads) and a family of arities induced by reduction rules over Σ (as explained in Remark 144). Our main result, Theorem 150 (see Section 5.4.3), states that a reduction signature is effective as soon as its underlying signature for Corollary 151. Let (Σ, R) be a reduction signature. If Σ is an algebraic 2-signature (Definition 106), then (Σ, R) is effective.

All the examples of reduction signatures considered here satisfy the condition of Corollary 151.

Example 152 (Reduction signature for Example 130). The reduction monad of Example 130 is generated by the reduction signature S LC β/η that is given by the signature Σ LC together with the following reduction rules (see Section 5.3.6):

• the reduction rule for β-reduction;

• the reduction rule for η-expansion;

• the congruence rule for abstraction;

• two unary congruence rules for application:

T T ′ app(T, U ) app(T ′ , U ) U U ′ app(T, U ) app(T, U ′ )
Remark 153 (Continuation of Remark 119). Just as our reduction monads are "proofrelevant" (cf. Remark 119), our notion of reduction signature allows for the specification of multiple reductions between terms. As a trivial example , duplicating the β-rule in the signature S LC β/η yields two distinct β-reductions in the initial model.

Example 154 (Reduction signature of lambda calculus with a fixpoint operator). The signature S LC fix specifying the reduction monad LC fix of the lambda calculus with a fixpoint operator extends the signature S LC β/η of Example 152 with:

• a new operation fix : Θ ′ → Θ (thus extending the signature for monads Σ LC );

• the reduction rule for the fixpoint reduction (cf. Section 5.3.6);

• a congruence rule for fix: T T ′ fix(T ) fix(T ′ ) .

Lemma 158. Using this alternative definition of action, a morphism between models R and T of a reduction signature S = (Σ, R) is a morphism f of reduction Σ-monads making the following diagram commute, for any reduction rule A = (V, (n i , l i , r i ) i∈I , (n, l, r)) of R:

Hyp A (R) / / Hyp A (f ) Red(R) (n) Red(f ) (n)
Hyp A (T ) / / Red(T ) (n) We now prove Lemma 156 using these alternative definitions:

Proof of Lemma 156. The reduction rule A ′ = (V ′ , (n j , h ′ j ) j∈J , (0, c ′ )) is defined as follows:

• Metavariables:

V ′ = V × Θ n • Hypotheses: For each j ∈ J, h ′ j : V ′ → Θ (n j ) × Θ (n j ) is defined as the composition of π 1 : V × Θ n → V with h j : V → Θ (n j ) × Θ (n j ) . • Conclusion: The morphism c ′ : V × Θ n → Θ × Θ is the n th uncurrying (see Defini- tion 85) of c : V → Θ (n) × Θ (n) .
Now, consider an action for the reduction rule A in a reduction Σ-monad R: it is an Rmodule morphism τ : Hyp A (R) → Red(R) (n) such that the following square commutes:

Hyp A (R) τ / / Red(R) (n) red (n) R V(R) c / / R (n) × R (n)
.

Equivalently, through the adjunction mentioned above, it is given by an R-module morphism τ * : Hyp R × R m → M such that the following diagram commutes:

Hyp A (R) × R n τ * / / Red(R) red R V(R) × R n c * / / R × R
This is exactly the definition of an action of A ′ . It is then straightforward to check that one action is preserved by a reduction monad morphism if and only if the other one is.

that p(v) = Z b / / Y a / / X . We need to show that there exists a unique algebra morphism w : s → ρ such that v = a • w and p(w) = b. F (S)

F (v) * * F (w) $ $ s F (a * R) F (a) / / ρ F (R) r S v * * w % % a * R a / / R Z p(v) * * b % % Y a / / X
Uniqueness follows from the fact that a is cartesian for the fibration p : E → B. Moreover, as a is cartesian, we get a morphism w : S → a * R. We turn it into an algebra morphism by showing that the following square commutes:

F (S) F (w) / / s F (a * R) ρ S w / / a * R
As a is cartesian and both w and F (w) are sent to b by p, it is enough to show equalities of both morphisms after postcomposing with a. The fact that v is an algebra morphism allows us to conclude.

We want to apply this lemma for proving Lemma 162. We thus need to show that U Σ : RedMon Σ → Mon Σ is a fibration:

Lemma 164. The forgetful functors RedMon → Mon and U Σ : RedMon Σ → Mon Σ are fibrations.

as the limit of the following finite diagram:

V(R) h i ′ ,R & & h i,R x x + + R (n i ) × R (n i ) R (n i ′ ) × R (n i ′ ) . . . π(q) (n i ) α (n i ) q O O π(q) (n i ′ ) α (n i ′ ) q O O Let J : C → Mod(R)/R 2 be a filtered diagram.
As π preserves colimits (since it creates them), π(F (colim J)) is the limit of the following diagram:

V(R) h i ′ ,R ' ' h i,R x x + + R (n i ) × R (n i ) R (n i ′ ) × R (n i ′ ) . . . colim π(J) (n i ) α (n i ) colim J O O colim π(J) (n i ′ ) α (n i ′ ) colim J O O
Now, as limits and colimits are computed pointwise in the category of modules, and as finite limits commute with filtered colimits in Set ([ML98, Section IX.2, Theorem 1]), we have that π(F (colim J)), as the limit of such a diagram, is canonically isomorphic to the colimit of π • F • J. Now, consider a signature S with a family of reduction rules (A i ) i . The functor that we are concerned with is F S|R = i F A i |R , for a given Σ-monad R: Lemma 170. For any Σ-monad R, the functor

F S|R = i F A i |R is finitary.
Proof. This is a coproduct of finitary functors (by Lemma 169), and so is finitary as colimits commute with colimits, by [ML98, Equation V.2.2]. Now we are ready to tackle the proof of our main result:

Proof of Theorem 150. We assume that Σ is effective; let R be the initial Σ-monad. We want to show that S has an initial model. We apply Lemma 165 with p the fibration from models to Σ-monads (Lemma 162): we are left with providing an initial object in the fiber category over R. By Lemma 166, this boils down to constructing an initial algebra for the endofunctor F S|R on the category Mod(R)/R 2 . We apply Lemma 167: Mod(R)/R 2 is indeed cocomplete by Lemma 168, and F S|R is finitary by Lemma 170).

Example: Lambda calculus with explicit substitutions

Here, we give a signature specifying the reduction monad of the lambda calculus with explicit substitutions as described in [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF]. One feature of this example is that it involves operations subject to some equations, and on top of this syntax with equations, a "graph of reductions".

In Section 5.6.1, we present the underlying signature for monads, and in Section 5.6.2, we list the reduction rules of the signature.

Signature for the monad of the lambda calculus with explicit substitutions

We give here the signature for the monad of the lambda calculus with explicit substitutions: first the syntactic operations, and then the equation that the explicit substitution must satisfy.

Operations

The lambda calculus with explicit substitutions extends the lambda calculus with an explicit unary substitution operator t[x/u]. Here, the variable x is assumed not to occur freely in u. In our setting, it is specified as an operation esubst X : LC ′ (X) × LC(X) → LC(X). It is thus specified by the signature induced by the parametric module Θ ′ ×Θ. An action of this signature in a monad R yields a map esubst X : R(X +{ * })×R(X) → R(X) for each set X, where esubst X (t, u) is meant to model the explicit substitution t[ * /u].

Definition 171. The signature Υ LCex for the monad of the lambda calculus with explicit substitutions without equations is the coproduct of Θ ′ × Θ and Σ LC .

β-red (λx.t)u t[x/u] x / ∈ fv(t) Gc t[x/u] t var[] x[x/u] u app[] (t u)[x/v] t[x/v] u[x/v] abs[] (λy.t)[x/v] λy.t[x/v] x / ∈ fv(v) y ∈ fv(u) [][] t[x/u][y/v] t[y/v][x/u[y/v]]
Figure 5.3: Reduction rules of lambda calculus with explicit substitutions.

T T ′ esubst(T, U ) esubst(T ′ , U ) U U ′ esubst(T, U ) esubst(T, U ′ )
They are translated into reduction rules through the protocol described in Section 5.3.5. We propose an approach based on the informal intuitive idea of defining inductively the submodule R * of R ′ depending on the fresh variable * as follows, for a given Σ LCexmonad R:

• η( * ) ∈ R * (X), for any set X;

• (application) -if t ∈ R(X) and u ∈ R * (X), then app(ι(t), u) ∈ R * (X) -if t ∈ R * (X) and u ∈ R(X), then app(t, ι(u)) ∈ R * (X) -if t ∈ R * (X) and u ∈ R * (X), then app(t, u) ∈ R * (X) • if t ∈ R * (X + {x}), then λx.t ∈ R * (X); • (explicit substitution) -if t ∈ R(X + {x}) and u ∈ R * (X), then ι(t)[x/u] ∈ R * (X); -if t ∈ R * (X + {x}) and u ∈ R(X), then t[x/ι(u)] ∈ R * (X); β-red app(abs(T ), U ) esubst(T, U ) Gc esubst(ι(T ), U ) T app[] esubst(app(T, U ), V ) app(esubst(T, V ), esubst(U, V )) var[] esubst( * , T ) T abs[] esubst(abs ′ (T ), V ) abs(esubst ∨ (T, ι(V ))) [][] esubst(esubst ′ (T, κ(U )), V ) esubst(esubst ∨ (T, ι(V )), esubst(κ(U ), V )) κ : Θ * → Θ ′ esubst ∨ : Θ ′′ × Θ ′ → Θ ′
where Θ * is the 1-hole context Σ LCex -submodule of Θ ′ (Definition 174), and esubst ∨ is defined as the composition

Θ ′′ × Θ ′ swap×Θ ′ / / Θ ′′ × Θ ′ esubst / / Θ ′
Here, swap exchanges the fresh variables: Lemma 177. The reduction signature S LCex is effective.

swap X,R : R((X + { * 1 }) + { * 2 }) → R((X + { * 1 }) + { * 2 })(t) swap X,R : t → t{ * 1 := * 2 ; * 2 := * 1 }
Proof. Apply Theorem 150. The underlying signature for monads is effective by Lemma 173.

Recursion

In this section, we derive, for any effective reduction signature S, a recursion principle from initiality. In Section 5.7.1, we state this recursion principle, then we give an example of application in Section 5.7.2, by translating lambda calculus with a fixpoint operator to lambda calculus. In Section 5.7.2, we apply this principle to translate lambda calculus with explicit substitutions into lambda calculus with unary congruent substitution. Then, in Section 5.7.4, we translate this latter variant of lambda calculus into lambda calculus closed under identity and composition of reductions.

Recursion principle for effective signatures

The recursion principle associated to an effective signature provides a way to construct a morphism from the reduction monad underlying the initial model of that signature to a given reduction monad.

Proposition 178 (Recursion principle). Let S be an effective reduction signature, and R be the reduction monad underlying the initial model. Let T be a reduction monad.

Any action τ of S in T induces a reduction monad morphism τ : R → T .

Proof. The action τ defines a model M of S. By initiality, there is a unique model morphism from the initial model to M , and τ is the reduction monad morphism underlying it.

In the next sections, we illustrate this principle.

Translation of lambda calculus with fixpoint to lambda calculus

In this section, we consider the signature S LC fix of Example 154 for the lambda calculus with an explicit fixpoint operator. We build, by recursion, a reduction monad morphism from the initial model LC fix of this signature to LC * β/η , the "closure under identity and composition of reductions" (Definition 131) of the initial model LC β/η of the signature

S LC β/η (Example 152).
As explained in Section 5.7.1, we need to define an action of S LC fix in LC * β/η . Note that S LC fix is an extension of S LC β/η (Example 154). First, we focus on the core S LC β/η part: we show that the reduction monad LC * β/η inherits the canonical action of S LC β/η in LC β/η . Lemma 179. There is an action

1 of S LC β/η in LC * β/η .
Proof. The challenge is to give an action of reduction rules with hypotheses: now the input reductions of the rule may be actually sequences of reductions. This concerns congruence for application and abstraction. We take the example of abstraction: suppose we have a sequence of reductions r 1 . . . r n going from t 0 to t n . We want to provide a reduction between abs(t 0 ) and abs(t n ). For each i, we have a reduction between abs(t i-1 ) and abs(t i ). By composing the corresponding sequence, we obtain the desired reduction.

The action for the extra parts of S LC fix requires the following:

• an operation fix : LC * β/η ′ → LC * β/η : for this, we choose a fixpoint combinator Y and set fix X (t) = app(Y, abs(t)), in accordance with Section 3.8.4;

• an action of the reduction rule fix(T ) T { * := fix(T )}

A fixpoint combinator Y is a closed term with the property that for any other term t, the term app(Y, t) β-reduces in some steps to app(t, app(Y, t)). We denote by r ∈ Red(LC * β/η )({ * }) a reduction between app(Y, * ) and app( * , app(Y, * )). Then, r induces an LC β/η -module morphism r : LC β/η → Red(LC * β/η ) by mapping an element t ∈ LC β/η (X) to r{ * := t}. We define the action of this reduction rule as the composition of the following reductions: app(Y, abs(t)) r(abs(t)) app(abs(t), app(Y, abs(t))) β t{ * := app(Y, abs(t))}

• an action of the congruence rule

T T ′ fix(T ) fix(T ′ )
that can be defined in the obvious way using the congruences of application and abstraction.

In more concrete terms, our translation is a kind of compilation which replaces each occurrence of the explicit fixpoint operator fix(t) with app(Y, abs(t)), and each fixpoint reduction with a composite of β-reductions.

Translation of lambda calculus with explicit substitutions into lambda calculus with congruent unary substitution

Here, we consider the reduction signature S LCex = (Σ LCex , R LCex ) introduced in Definition 176. The underlying monad of the initial model LC ex is the monad of lambda calculus with an application and abstraction operation, and an explicit substitution operator LC ex ′ × LC ex → LC ex satisfying Equation 5.5, for R = LC ex . The associated reduction monad has all the rules specified in Section 5.6.

We build, by recursion, a reduction monad morphism from the initial model LC ex of this signature to LC 1-cong , a variant of the lambda calculus specified by the signature S LC β/η (Example 152) extended with the congruence for unary substitution:

T T ′ U { * := T } U { * := T ′ }
Note that this reduction rule accounts for the reflexivity rule, and makes congruences for application (but not congruence for abstraction) redundant:

Reflexivity Any U ∈ LC(X) can be weakened into ι(U ) ∈ LC ′ (X). Then, consider any reduction m : T ◮ T ′ . The action of the reduction rule above yields a reduction between ι(U ){ * := T } = U and ι(U ){ * := T ′ } = U . By choosing adequatly m (for example, take the beta-reduction between app(abs( * ), abs( * )) and abs( * )), this yields an action of the reflexivity reduction rule.

Congruence Consider the left congruence rule (the cases of the right one and the congruence for abstraction are similar): from any reduction m : T ◮ T ′ , we want a reduction between app(T, U ) and app(T ′ , U ), for T, T ′ , U ∈ LC(X). We get it by applying the action of unary congruent substitution to m for the term app( * , U ). One checks that this indeed defines an action for the left congruence reduction rule of application.

As explained in Section 5.7.1, we need to define an action of S LCex in LC 1-cong :

• the operations of application and abstraction are those of LC 1-cong as the initial Σ LC -monad (recall that the underlying monad of LC 1-cong is just LC);

• the explicit substitution operation LC 1-cong ′ × LC 1-cong → LC 1-cong is defined using the monadic substitution, mapping a pair (t, u) ∈ LC 1-cong (X + { * }) × LC 1-cong (X) to the monadic substitution t{ * := u};

• Equation 5.5 for the underlying monad is satisfied thanks to the usual monadic equations;

• the action of the congruence rules for application and abstraction are induced by the action of the congruence rule for unary substitution, as explained above;

• LC 1-cong has already an action for β-reduction;

• all the actions for the remaining reduction rules involving explicit substitution (except the congruences for explicit substitution that are discussed below) are given by an action of the reflexivity reduction rule;

• the non-obvious actions are the ones of the congruence rules for explicit substitution:

T T ′ T [x/U ] T ′ [x/U ] U U ′ T [x/U ] T [x/U ′ ]
The left one is obtained from the substitution of the module of reductions (see Remark 120). The right one is exactly given by the action of the congruence rule for unary substitution.

Finally, by the recursion principle, we get a reduction monad morphism from LC ex to LC 1-cong . This translation replaces the explicit substitution operator t[x/u] with the corresponding monadic substitution t{x := u}, and all the reductions are translated to reflexivity except for the ones for the β-reduction and congruences.

Translation of lambda calculus with congruent unary substitution into lambda calculus

In the previous section, we translated lambda calculus with explicit substitution into lambda calculus with congruent unary substitution. In this section, we translate this variant of lambda calculus into LC * β/η (introduced in Section 5.7.2), the closure under identity and composition of reductions the initial model LC β/η of the signature S LC β/η (Example 152).

As per Section 5.7.1, we need to define an action in LC * β/η of the signature S LC β/η extended with the reduction rule:

T T ′ U { * := T } U { * := T ′ } (5.6)
Thanks to Lemma 179, we have an action of S LC βη in LC * β/η . Thus, the main challenge consists in equipping LC * β/η with an action of the rule (5.6).

Proposition 180. The reduction monad LC * β/η can be equipped 2 with an action of the rule (5.6).

Proof. We will write r : R → LC × LC in place of red LC * β/η : Red(LC * β/η ) → LC × LC. Such an action is equivalently given (see Lemma 160) by a morphism α : LC ′ × R → R such that the following diagram commutes, where q X (t, m) = t{ * := source(m)}, t{ * := target(m)} .

LC ′ × R α / / q * * R r v v LC × LC (5.7)
We first construct the collection of functions (α X ) X with α X : LC ′ (X)×R(X) → R(X) and then shows the two required properties, i.e., that it commutes with substitution (thus inducing a LC-module morphism), and that it satisfies Equation 5.7.

The construction of the collection of functions (without naturality conditions) is worked out in the functor category [Set 0 , Set], where Set 0 is the discretized category of sets (this base category allows us to get rid of naturality conditions). This is done by recursion on the first argument. More formally, we exploit some initiality property of LC ′ • j, where j : Set 0 → Set is the inclusion of the discretized category of sets into sets. Indeed, LC ′ •j 2. A formalized proof in Agda of this statement is available at https://github.com/amblafont/ unary-subst-LCstar/blob/master/fiberlambda.agda.

(c) The morphism (R × R) R → R R corresponds to the case of an application. We expect that α X (app(t, u), m) = app-cong(α X (t, m), α X (u, m)), where app-cong : R×R → R is the action of the reduction rule of congruence for application defined as app-cong(m 1 , m 2 ) = trans(app-cong 1 (m 1 ), app-cong 2 (m 2 )), where trans denotes an action of the transitivity reduction rule with which we can equip LC * β/η (by concatenating sequences of reductions). Accordingly, the morphism is defined as app-cong R .

(d) The morphism R ′R ′ → R R corresponds to the case of an abstraction. We expect that α X (abs(t), m) = abs-cong X (α X+1 (t, Rι X (m))), where ι : Id → Id ′ is the canonical inclusion. Accordingly, we take abs-cong Rι as the the required morphism.

By initiality, we get an algebra morphism from LC • j to R R , which by uncurrying yields a morphism α :

LC ′ • j × R → R.
2. Upgrading α into a module morphism from LC ′ × R to R consists in showing compatibility with substitution in the following sense: for any map f : X → LC(Y ), for any pair (t, m) ∈ LC ′ (X) × R(X), the equality α X (t, m){f } = α Y (t{f }, m{f }) is satisfied. This is shown by induction on t ∈ LC ′ (X). The case of variables requires a preliminary step: for t = η(x), the equation amounts to refl(f (x)) = α(LCi(f (x)), m), which is not straightforward. We hence first prove by induction on t ∈ LC(X) that α(LCi(t), m) = refl(t). We do not detail these straightforward inductions, but rather explain the general methodology to perform induction on LC ′ (the case of LC is similar). Suppose given, for each t ∈ LC ′ (X), a predicate P X (t). Then, one can form the functor LC ′ |P : Set 0 → Set mapping a set X to the subset of LC ′ (X) satisfying the predicate P X . It follows that LC ′ |P embeds into LC, and if LC ′ |P inherits the algebra structure for Ψ through this embedding, then by initiality we get a section of the embedding, which exactly translates the fact that any term t ∈ LC ′ (X) satisfies the property.

OPERATIONAL MONADS AND THEIR SIGNATURES

In this chapter, we consider operational monads, extending the notion of reduction monad of Chapter 5. Our goal is to deal with programming languages whose terms may not form a monad, or whose reductions are not stable under substitution of terms.

Consider the example of the call-by-value lambda calculus: variables can be replaced with values only, rather than any term. Yet, we are interested in reductions between terms rather than values. In this situation, there is a monad of values, and terms form a module over this monad. Although terms form the monad of lambda calculus, reductions are not stable under its monadic substitution: they are stable under the monadic substitution of values.

To be more precise, we limit ourselves to languages whose terms form a free module over a monad R, that is, a module of the shape T • R for some endofunctor T : Set → Set. This is indeed the case of the call-by-value lambda calculus: each term can be decomposed uniquely as a binary tree whose leaves are values. For this specific example, R is the monad of values of the lambda calculus, and T is the endofunctor of binary trees with leaves in its argument.

We also generalize to the case of heterogeneous reductions. This allows us to cover the call-by-value lambda calculus with big-step operational semantics, where terms reduce to values.

We adopt the same terminology and notation as in Chapter 5. We are quicker here, as all the definitions and proofs are straightforward generalizations.

Plan of the chapter

In Section 6.1, we define operational monads, a generalization of the reduction monads of Chapter 5. In Section 6.2, we adapt the definition of reduction rules to the new setting. This enables us to define signatures for operational monads-operational signatures-in Section 6.3, that are particular signatures over the category of operational monads. Then, in Section 6.4, we give some examples of operational signatures.

Operational monads

We define operational monads in Section 6.1.1, and then consider some examples of operational monads, in Section 6.1.2.

Operational monads

Before defining operational monads, we need the intermediate notion of T -reduction monads, when T is a pair of endofunctors on Set.

Definition 181. Let T = (T 1 , T 2 ) be a pair of endofunctors on Set. A T -reduction monad R is given by: 1. a monad on sets (the monad of terms), that we still denote by R, or by R when we want to be explicit; Notation 182. For a T -reduction monad R, a set X, and elements s ∈ T 1 (R(X)), t ∈ T 2 (R(X)), we think of the fiber red R (X) -1 (s, t) as the set of "reductions from s to t".

We sometimes write m : s ◮ t : T (R(X)), or even m : s ◮ t when there is no ambiguity, instead of m ∈ red R (X) -1 (s, t). • a natural transformation α 2 : T 2 → T ′ 2 ;

• a (T ′ 1 , T ′ 2 )-reduction monad morphism f between (α 1 , α 2 ) ! R and R ′ , where the (T ′ 1 , T ′ 2 )-reduction monad (α 1 , α 2 ) ! R is defined as follows:

the underlying monad is R;

-Red((α 1 , α 2 ) ! R) is defined as Red(R);

red (α 1 ,α 2 ) ! R is defined as the composition

Red(R) red R / / (T 1 • R) × (T 2 • R) (α 1 •R)×(α 2 •R) / / (T ′ 1 • R) × (T ′ 2 • R) .
Proposition 189 (Category of operational monads). Operational monads and their morphisms with the obvious composition and identity morphisms form a category OpMon.

Examples of operational monads

Any example of reduction monad R of Chapter 5 yields an operational monad whose state functors are the identity endofunctors.

Example 190 (Call-by-value lambda calculus). In call-by-value, reductions between terms are not stable under substitution of variables with terms in general. However, they are stable under substitution of variables with values. A value is either a variable or a lambda abstraction of an arbitrary term. Note that values are stable under substitution: they induce a monad LC v = Id + LC ′ equipped with a monad morphism i : LC v → LC. Now, reductions are between terms rather than between values, so we need to devise a functor B : Set → Set such that B • LC v is isomorphic to LC: then, the callby-value lambda calculus is a (B, B)-reduction monad. Note that a lambda term can always be decomposed as a binary tree whose leaves are values, that is variables or lambda abstractions: each node of this tree is an application. Hence, we choose B to be the functor underlying the monad of binary trees specified by the 1-signature Θ × Θ: then, there is an isomorphism α : LC → B • LC v in the category of LC v -modules (LC is indeed equipped with a structure of LC v -module thanks to the inclusion i of LC v in LC as a monad morphism). The operational monad of call-by-value lambda calculus is the pair ((B, B), LC v ) where the (B, B)-reduction monad LC v is defined as follows: We call this operational monad the operational monad of the call-by-value lambda calculus. A signature for it is given in Section 6.4.1.

Example 191 (Big-step call-by-value lambda calculus). In the call-by-value lambda calculus with big-step operational semantics, reductions happen between a term and a value. The underlying monad is LC v , and the pair of state functors is (B, Id), where B is defined in Example 190. We denote abs v : LC ′ → LC v the inclusion of lambda abstractions into values. The module of reductions is defined inductively as follows:

• for each value v ∈ LC v (X), the induced term α(i(v)) reduces to v;

• given a reduction m t : α(t) ◮ abs v (t ′ ), a reduction m u : α(u) ◮ u ′ , and a reduction m : α(t ′ ){ * := u ′ } ◮ v, we get a reduction β(m t , m u , m) : α(app(t, u)) ◮ v.

We specify more formally this operational monad in Section 6.4.2.

≡ P ′ P ′ Q ′ Q ′ ≡ Q P Q
In π-calculus all we substitute is channel names, so the monad is just the identity.

There is no need for process variables: no binding of process variable is involved, nor substitution of variables with processes.

The state functor T maps any X ∈ Set to the set of processes with free channel names in X, considered equivalent up to structural congruence. Finally, let Red(R)(X) denote the set of reductions between (equivalence classes of) processes in T (X).

We specify more formally this operational monad in Section 6.4.3.

S-reduction rules

This section is a straightforward generalization of the notion of reduction rules of Section 5.3 to the setting of operational monads, when S is a pair of signatures over the category of endofunctors on Set (in the sense of Chapter 2): S-reduction rules are defined in Section 6.2.1, and the associated notion of action in a S-reduction monad is explained in Section 6.2.2, after introducing S-reduction Σ-monads in Section 6.2.2, when Σ is a signature for monads.

Definition of S-reduction rules

In this subsection, Σ is a signature for monads, and S = (S 1 , S 2 ) is a pair of signatures over the category of endofunctors on Set. We present our notion of S-reduction rule over Σ, from which we build operational signatures in Section 6.3.

We need first to generalize the notion of Σ-module from Definition 76 to that of (Σ, S)-module:

Definition 193. We define a (Σ, S)-module to be a functor T from the product of the three categories of models of Σ, S 1 , and S 2 to the category Mod commuting with the Definition 198. Let Σ be a signature for monads, and S = (S 1 , S 2 ) be a pair of signatures over the category of endofunctors on Set. The category S-RedMon Σ of Sreduction Σ-monads is the category of models of the product of the following signatures:

• the pullback of Σ along the forgetful functor from operational monads to monads;

• the pullback of S 1 along the functor mapping an operational monad to its first state functor;

• the pullback of S 2 along the functor mapping an operational monad to its second state functor.

In other words, it is the following pullback.

S-RedMon

Σ / / OpMon Mon Σ × [Set, Set] S 1 × [Set, Set] S 2 / / Mon × [Set, Set] 2
More concretely,

• a S-reduction Σ-monad is an operational monad (R, T 1 , T 2 ) equipped with an action ρ of Σ in R, thus inducing a Σ-monad that we denote also by R, or by R when we want to be explicit; -an action of S i in T i for i ∈ {1, 2}, inducing a model of S i that we denote also by T i ;

• a morphism of S-reduction Σ-monads R → S is a morphism f : R → S of operational monads compatible with the actions of Σ, S 1 , and S 2 , i.e, whose underlying monad morphism is a Σ-monad morphism and whose underlying natural transformations between state functors are model morphisms.

Action of a S-reduction rule

Let Σ be a signature for monads and S = (S 1 , S 2 ) be a pair of signatures over the category of endofunctors on Set. In this section, we introduce the notion of action of a S-reduction rule over Σ in a S-reduction Σ-monad. Intuitively, such an action is a "map • a : D → S-RedMon Σ is the fibration corresponding (through the Grothendieck construction) to the functor mapping a S-reduction Σ-monad R to Mod(R)/MVar A (R).

• u maps a S-reduction Σ-monad to hyp A (R) : Hyp A (R) → MVar A (R);

• v maps a S-reduction Σ-monad to con A (R) : Con A (R) → MVar A (R).

This arity yields the same notion of action.

Signatures for operational monads and Initiality

In this section, we define the notion of operational signature, as particular signatures over the category of operational monads. They consist of three parts:

• a specification of the pair T of state functors, as a pair of signatures S = (S 1 , S 2 ) over the category of endofunctors on Set,

• a signature for the monad underlying R,

• and a family of S-reduction rules over Σ.

In Section 6.3.4, we review Fiore and Hur's notion of equational system [FH09] that yield effective signatures for specifying endofunctors. In Sections 6.3.1 and 6.3.3, we describe the category of models associated to each operational signature. Our main result, Theorem 207, states that an operational signature is effective as soon as its underlying signatures for monads and for endofunctors are effective.

Operational signatures

We define here operational signatures and their models.

Definition 203. An operational signature is a signature over the category of operational monads consisting of:

• the product signature of the pullback of a signature Σ for monads along the forgetful functor from operational monads to monads;

• par : M × M → M mapping (P, Q) to P |Q;

• out : Id × Id × M → M mapping (a, b, P ) to a b .P ;

• in : Id × M ′ → M mapping (a, P ) ∈ X × M (X + { * }) to a( * ).P ;

• abs : M ′ → M mapping P ∈ M (X + { * }) to ν * .P . To conclude, the operational signature is (S, Id Set , 0, R).

Note that the monad

CONCLUSION

In this thesis, we have studied different notions of signatures that are all particular instances of the general definition that we give in Chapter 2.

In Chapters 3 and 4, we have presented notions of signatures for monads and their models. More precisely, in Chapter 3, we have defined the class of presentable signatures, which are quotients of traditional algebraic signatures. Presentable signatures are closed under various operations, including colimits. One of the main results of this chapter says that any presentable signature is effective. Despite the fact that the constructions in Section 3.7 make heavy use of quotients, there is no need to appeal to the axiom of choice. While a previous version of the formalisation did use the axiom of choice to show that certain functors preserve epimorphisms, we managed subsequently to prove this without using the axiom of choice. This analysis, and subsequent reworking, of the proof was significantly helped by the formalisation.

One difference to other work on Initial Semantics, e.g., [MU04; GU03; Fio08; FM10], is that we do not rely on the notion of strength. However, a signature endofunctor with strength as used in the aforementioned articles can be translated to a high-level signature as presented in this work (Proposition 44).

In Chapter 4, we extend the notion of signature for monads to take into account more general equations. This yields the definition of a 2-signature, as a pair of a 1signature Σ (that is, a signature in the sense of Chapter 3) and a set of Σ-equations that must be satisfied.

Finally, in Chapter 5, we have introduced the notions of reduction monad and reduction signature: they are meant to model syntax with a notion of reduction. For each such signature, we define a category of models, equipped with a forgetful functor to the category of reduction monads. We say that a reduction signature is effective if its associated category of models has an initial object; in this case, we say that the reduction monad underlying the initial object is generated by the signature. We identify a simple sufficient condition for a reduction signature to be effective. Chapter 6 generalizes the notion of reduction monad to that of operational monad, and adapts the statement of Chapter 5 accordingly. These two chapters is a first step towards a theory for the al-gebraic specification of programming languages and their semantics. In future work, we aim at generalizing our notion of signature to encompass richer languages and to present a notion of signature that allows for the specification of equalities between reductions (cf. Remark 153).

We anticipate that our work extends to simply-typed languages, by changing the base category Set to a presheaf category Set T , where T is the set of simple types that we are interested in.

  t{x → v x } u{x → v x } w w s u b s ti tu ti o n

  D . où u et v sont des sections du foncteur F : D → C, c'est-à-dire, des foncteurs qui, post-composés avec F , donnent le foncteur identité sur C. Un objet c de C est muni d'une action de cette arité s'il est muni d'un morphisme h : u(c) → v(c) dont l'image par le foncteur F est le morphisme identité en c. Notons que si les seuls morphismes que F envoie sur un morphisme identité sont eux mêmes des morphismes identité, alors un objet c est muni d'une action si et seulement si u(c) = v(c). Nous qualifions d'équationnelle une arité vérifiant cette propriété, qui spécifie donc des équations. Les objets munis d'une action d'une famille d'arités (fixée à l'avance) forment une catégorie : les morphismes sont ceux de la catégorie C vérifiant une condition de commutation avec les actions. C'est ainsi qu'est définie la catégorie de modèles d'une signature composée d'une seule famille d'arités. Par exemple, la catégorie d'algèbres d'un endofoncteur G : C → C est la catégorie de modèles de la signature composée d'une seule arité C (G,Id C ) / / o o (Id C ,Id C ) / / C × C où le foncteur C × C → C est la deuxième projection.

Néanmoins, la classe

  des signatures présentables paraît limitée. Considérons en effet l'exemple d'une opération binaire associative : nous ne savons pas en donner une signature, présentable ou non. Remarquons que nous pouvons malgré cela donner une définition intuitive de modèle dans ce cas particulier : il s'agit d'une monade R munie d'une opération binaire b : R × R → R telle que pour tous x, y, z dans R(X) les expressions b(b(x, y), z) et b(x, b(y, z)) sont égales. En d'autres termes, il s'agit d'un modèle (R, b) de la signature d'une opération binaire, tel que les deux morphismes de modules de R × R × R vers R, associant à tout triplet (x, y, z) les deux expressions envisagées, sont égaux. Dans le chapitre 4, nous donnons une définition d'équation généralisant cet exemple pour les modèles d'une signature monadique quelconque Σ : il s'agit de la donnée,

Introduction

  shown in the following commutative diagram:

  Definition 17. Let E be a family of arities over C. The pullback of E along F is the family of arities F * E over B consists of the pullbacks of arities of E along F .

  Hence a signature assigns, to each monad R, a module over R in a functorial way: this motivates the definition of parametric modules. Definition 35. A parametric module is a section Σ of the forgetful functor from the category Mod to the category Mon, that is, a functor Σ : Mod → Mon making the following diagram commute: Mon Σ / / Mod z z Mon We give first a basic example: Example 36. The assignment R → R yields a parametric module, which we denote by Θ.

  that is, it commutes suitably with the Σ-actions of Diagram (3.2) in the source and r : Σ(R) -→ R in the target. Definition 51. Given a model M of Σ, we denote by M ♯ the Σ-model constructed in Lemma 50, and by ǫ M : M ♯ -→ M the morphism of models defined there.

Proof.

  In any category, a morphism f : a → b is an epimorphism if and only if the following diagram is a pushout diagram ([ML98, Exercise III.4.4]) :

  8. As in Section 3.8.3, invariance follows from coherence.CHAPTER 4

  2.2. Definition 121. A morphism of reduction monads from R to S is given by a pair (f, α) of 1. a monad morphism f : R → S, and 2. a natural transformation α : Red(R) → Red(S) satisfying the following two conditions: 3. α is an R-module morphism between Red(R) and the pullback module f * Red(S) of Red(S) along f (see Definition 26), and 4. the square

  π i : Red(R) n → R, and we call p n := (π 0 , π n ) :Red(R) n → R × R. We set Red(R * ) := n Red(R) n .3. the module morphism is red R* := [p n ] n∈N : n Red(R) n → R × R the universalmorphism induced by the family (p n ) n∈N .

•

  Conclusion: Given by the term-pair (0, c) of Example 135.

  Figure 5.1: Examples of reduction rules. Rule Signature Metavariables Hypothesis Conclusion Refl any Θ (0, (id, id))Trans any Θ × Θ × Θ for (T, U, W ) (0, π 1,2 ), (0, π 2,3 ) (0, π 1,3 ) abs-Cong Σ LC Θ ′ × Θ ′ for (T, U ) (1, id) (0, abs × abs) β-Red Σ LC Θ ′ × Θ for (T, U ) (0, c β-Red ) η-Exp Σ LC Θ (0, (id, abs • ι)) fix-Exp Σ fix Θ ′ (0, c fix-Exp )

  Figure 5.2: Modules and term pairs relative to the reduction rules of Figure 5.1.

  Figure 5.3 gives Kesner's rules. Five out of six of Kesner's rules translate straightforwardly, see Figure 5.4. Note how the explicit weakening ι : Θ → Θ ′ accounts for the side condition x / ∈ fv(t) of the Gc-rule in Figure 5.3. Expressing the side condition y ∈ fv(u) of the [][]-rule of Figure 5.3 requires the definition of the Σ LCex -module Θ * such that LC ex * is the submodule of LC ex ′ of terms that really depend on the fresh variable.

Figure 5 . 4 :

 54 Figure 5.4: Reduction rules of Figure 5.3 reformulated in our setting.

3.

  It remains to show the commutation of Diagram 5.7. Again, an induction on the first argument (thus exploiting initiality of LC ′ • j) is enough to conclude. CHAPTER 6

2

  . an R-module Red(R) (the module of reductions);3. a morphism of R-modules red R : Red(R) → (T 1 • R) × (T 2 • R) (source and target of rules). We set source R := π 1 • red R : Red(R) → T 1 • R, and target R := π 2 • red R : Red(R) → T 2 • R.

Remark 183 .

 183 We recover Chapter 5 by taking T = (Id Set , Id Set ). Definition 184. Let T = (T 1 , T 2 ) be a pair of endofunctors on Set. A morphism of T -reduction monads from R to S is given by a pair (f, α) of 1. a monad morphism f : R → S, and 2. a natural transformation α : Red(R) → Red(S)satisfying the following two conditions:3. α is an R-module morphism between Red(R) and f * Red(S), • R) × (T 2 • R) T 1 f ×T 2 f / / (T 1 • S) × (T 2 • S)commutes in the category of natural transformations. Proposition 185 (Category of T -reduction monads). Let T = (T 1 , T 2 ) be a pair of endofunctors on Set. Then, T -reduction monads and their morphisms, with the obvious composition and identity, form a category T -RedMon, equipped with a forgetful functor to the category of monads. We get an analogue of Theorem 123: Theorem 186. Let T = (T 1 , T 2 ) be a pair of endofunctors on Set. The category of T -reduction monads is isomorphic to the category of monads relative to the functor mapping a set to its discrete T -graph, where the category of T -graphs is the comma category Set/(T 1 × T 2 ). Definition 187. An operational monad is a pair (T, R) where R is a T -reduction monad. The pair T = (T 1 , T 2 ) of endofunctors on Set is called the pair of state functors of the operational monad. Operational monads may be organized into a category: Definition 188 (Morphism of operational monads). A morphism between operational monads ((T 1 , T 2 ), R) and ((T ′ 1 , T ′ 2 ), R ′ ) is a triple (α 1 , α 2 , f ) consisting of • a natural transformation α 1 : T 1 → T ′ 1 ;

  1. the underlying monad is LCv = Id + LC ′ ; 2. red LCv : Red(LC v ) → (B•LC v )×(B•LC v ) is generated by the following constructions: (a) for t ∈ LC ′ (X) and u ∈ LC v (X), we have β(t, u) : α(app(abs(t), i(u))) ◮ α(t){ * := u}; (b) for m : α(u) ◮ α(v) : B(LC v (X)) in Red(LC v ) and t ∈ LC(X), we have app-cong 1 (m, t) : α(app(u, t)) ◮ α(app(v, t)); (c) for m : α(u) ◮ α(v) : B(LC v (X)) in Red(LC v ) and t ∈ LC(X), we have app-cong 2 (t, m) : α(app(t, u)) ◮ α(app(t, v)); (d) for m : α(u) ◮ α(v) : B(LC ′ v (X)) in Red(LC v )we have abs-cong(m) : α(abs(u)) ◮ α(abs(v)).

Example 192 .

 192 Let us recall the following simple variant of π-calculus. The syntax for processes is given by P, Q ::= 0 | (P |Q) | !P | νa.P | a b .P | a(b).P, where a and b range over a fixed, countable set of channel names. In νa.P , the channel name a is bound, and in a(b).P , the channel name b is bound. Processes will be considered equivalent up to structural congruence, the smallest equivalence relation ≡ stable under context and such that 0|P ≡ P , P |(Q|R) ≡ (P |Q)|R, (νa.P )|Q ≡ νa.(P |Q) when a does not occur free in Q, and !P ≡ P |!P . Reduction is then given by the following inductive rules, the last one enforcing the quotient by structural congruence. a b .P |a(c).Q P |(Q{c := b})

•

  Id Set is the initial model of the empty signature 0. The family R of reduction rules over 0 consists of the following: Original rule As a S-reduction rule a b .P |a(c).Q P |(Q{c := b}) par(out(a, b, j 1(P )), in(a, j 1 (Q))) par(j 2 (P ), j 2 (T [id, b](Q)))) P Q P |R Q|R P Q par(P, j 1 (R)) par(Q, j 2 (R)) j i : T → M i isthe initial S-model morphism to the underlying state functor M i of a S-reduction Σ-monad, for i ∈ {1, 2}; • T [id, b] is the function T [id, b] : T (R(X) + 1) → T (R(X)), for b : 1 → R(X) the function selecting b ∈ R(X).

  ). leurs arguments. La signature du lambda calcul provient d'un module paramétrique Σ LC algébrique : l'application est une opération binaire classique, tandis que l'abstraction est une opération unaire liant une seule variable dans son unique argument.La syntaxe d'un langage est parfois définie modulo certaines équations : c'est le cas du lambda calcul différentiel[START_REF] Ehrhard | The differential Lambda-calculus[END_REF], du pi calcul avec ses règles de congruence structurelle, et du lambda calcul avec substitution explicite décrit par[START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF]. Dans cette thèse, nous abordons la spécification de monades correspondant à des syntaxes vérifiant ce type d'équations.

	1.1.6 Syntaxes avec équations (chapitres 3 et 4)

Dans le chapitre 3, nous étudions les modules paramétriques que nous appellons présentables : ce sont, en quelque sorte, des quotients de modules paramétriques algébriques. Une signature induite par un module paramétrique présentable est également qualifiée de présentable. Nous montrons qu'une telle signature est effective (Théorème 57). Il devient possible de spécifier une opération binaire commutative (Section 3.8.1). Pour cela, il suffit de remarquer que la donnée d'une telle opération est équivalente à la donnée d'une opération prenant en argument une paire non ordonnée de termes. Décrivons maintenant le module paramétrique Σ comm-bin associé : il s'agit d'un quotient du module paramétrique algébrique Σ bin d'une opération binaire qui associe à toute monade R le module R × R. Plus précisément, à toute monade R, le module paramétrique Σ comm-bin associe le module (S 2 R(X))) X , où S 2 R(X) est l'ensemble des paires d'éléments de R(X) × R(X) quotienté par la relation (t, u) ∼ (u, t), c'est-à-dire, l'ensemble des paires non ordonnées. La syntaxe bénéficie alors d'une opération qui prend en argument un couple non ordonné de termes, comme désiré.

  then an action of E 2 in c, inducing a model m 2 of E 2 , and so on. An endofunctor Σ : C → C induces a signature consisting of a single arity constructed in Example 3: it is easily verified that the category of models of this signature is the category of algebras of Σ. An equational system C : Σ ⊲ Γ ⊢ L = R yields a signature extending the one induced by the endofunctor Σ (as explained in Example 13) with a singleton family consisting of the equational arity induced by the equational system (Example 10).

	Example 13. Example 14.

The associated category of models coincides with the category of algebras of this equational system, as defined in [FH09, Definition 3.4]. More concretely, as explained in Example 10, models are objects of C equipped with a Σ-algebra structure that is mapped to the same image by L and R, and morphisms are algebra morphisms. Definition 15. A signature S is said effective if its category of models has an initial object Ŝ.

Dans la littérature, le mot signature est souvent réservé au cas où une telle condition suffisante est automatiquement satisfaite.

Une variable peut avoir une occurrence liée et une occurrence libre dans le même terme : par exemple, x dans (λx.x) x est liée dans λx.x, mais apparaît librement à droite.

En termes catégoriques, la catégorie Mod est obtenue par la construction de Grothendieck pour le foncteur qui à toute monade associe sa catégorie de modules.

Here, the word "language" encompasses data types, programming languages and logic calculi, as well as languages for algebraic structures as considered in Universal Algebra.

In the literature, the word signature is often reserved for the case where such a sufficient condition is automatically satisfied.

A variable can have a bound instance and a free occurrence in the same term: for example, x in (λx.x) x is bound in λx.x, but appears freely on the right.

Categorically speaking, the category Mod is obtained by performing the Grothendieck construction for the functor mapping a monad to its category of modules.

The counterexample 49 is the signature associating to any monad R the module (P(R(X))) X .

The approaches by Fiore and collaborators and Gabbay and Pitts[START_REF] Gabbay | A New Approach to Abstract Syntax Involving Binders[END_REF] are nicely compared by Power[START_REF] Power | Abstract Syntax: Substitution and Binders: Invited Address[END_REF], who also comments on some generalization of the former approach.

Given a monoidal category C, there is a notion of (left or right) module over a monoid object in C (see, e.g., [Bra14, Section 4.1] for details). The term "module" comes from the case of rings: indeed, a ring is just a monoid in the monoidal category of Abelian groups. Similarly, our monads are just the monoids in the monoidal category of endofunctors on Set, and our modules are just modules over these monoids. Accordingly, the term "linear(ity)" for morphisms among modules comes from the paradigmatic case of rings.

The term "pullback" is standard in the terminology of Grothendieck fibrations (see Proposition 28).

Our notation for the total category is modelled after the category of elements of a presheaf, and, more generally, after the Grothendieck construction of a pseudofunctor.

Following the terminology introduced in Definition 26, the term "pullback" is justified by Lemma 55.

In the following, we similarly write n instead of I n in order to make equations more readable.

The adjective syntactic means here that we do not deal with the equation.

This cannot be the case stricto sensu since f is a pair of module morphisms while p is a monad morphism.

This definition of "modularity" does not seem related to the specific meaning it has in the rewriting community (see, for example,[START_REF] Gramlich | Modularity in term rewriting revisited[END_REF]).

An initiality result for this particular case was also previously discussed and proved formally in the Coq proof assistant in[START_REF] Hirschowitz | Modules over monads and initial semantics[END_REF].

A formalized proof in Agda of this statement is available at https://github.com/amblafont/ unary-subst-LCstar/blob/master/fiberlambda.agda.

PART I

Syntax

From the remarks above, we derive the simpler and weaker statement of Theorem 107 that covers all our examples, which are algebraic. This section is dedicated to the proof of the main technical result, Lemma 110. 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 110 uses some quotient constructions that we present now:

Proposition 111 (u_monad_def). Given a monad R preserving epimorphisms and a collection of monad morphisms (f i : R → S i ) i∈I , there exists a quotient monad R/(f i ) together with a projection p R : R -→ R/(f i ), which is a morphism of monads such that each f i factors through p.

Proof. The set R/(f i )(X) is computed as the quotient of R(X) with respect to the relation x ∼ y if and only if f i (x) = f i (y) for each i ∈ I. This is a straightforward adaptation of Lemma 63.

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

The above construction can be transported to Σ-models: Proposition 112 (u_rep_def). Let Σ be a parametric module sending epimorphic natural transformations to epimorphic natural transformations, and let R be a Σ-model such that R and Σ(R) preserve epimorphisms. Let (f i : R → S i ) i∈I be a collection of Σmodel morphisms. Then the monad R/(f i ) has a natural structure of Σ-model and the quotient map p R : R -→ R/(f i ) is a morphism of Σ-models. Any morphism f i factors through p R in the category of Σ-models.

The fact that R and Σ(R) preserve epimorphisms is implied by the axiom of choice. The proof follows the same line of reasoning as the proof of Proposition 111. Now we are ready to prove the main technical lemma:

Proof of Lemma 110. Let Σ be an effective parametric module, and let E be a set of elementary Σ-equations. The plan of the proof is as follows:

1. Start with the initial model ( Σ, σ), with σ : Σ( Σ) → Σ.

S → T .

Proof. The action a defines a 2-model M of Υ, and â is the monad morphism underlying the initial morphism to M .

Hence the recipe consists in the following two steps:

1. give T an action of the 1-signature Σ;

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

In the next section, we illustrate this principle.

Translation of lambda calculus with fixpoint to lambda calculus

In this section, we consider the 2-signature Υ LC βη,fix := Υ LC βη + Υ fix where the two components have been introduced above (see Example 93 and Section 4.4.4).

As a coproduct of algebraic 2-parametric modules, Υ LC βη,fix is itself algebraic, and thus the initial model exists. The underlying monad LC βη,fix of the initial model can be understood as the monad of lambda calculus modulo β and η enriched with an explicit fixpoint operator fix : LC ′ βη,fix -→ LC βη,fix . Now we build by recursion a monad morphism from this monad to the "bare" monad LC βη of lambda calculus modulo β and η.

As explained in Section 4.5.1, we need to define an action of Υ LC βη,fix in LC βη , that is to say an action of Υ LC βη plus an action of Υ fix . For the action of Υ LC βη , we take the one yielding the initial model. Now, in order to find an action of Υ fix in LC βη , we choose a fixpoint combinator Y (say the one of Curry) and take the action Ŷ as defined at the end of Section 4.4.4.

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

PART II

Semantics

of quintuples (T, T ′ , U, U ′ , m) where (T, T ′ , U, U ′ ) ∈ R 4 (X) and m is a reduction m :

The R-module of hypotheses of this reduction rule maps a set X to the set of sextuples (T, T ′ , U, U ′ , m, n) where (T, T ′ , U, U ′ ) ∈ R 4 (X), m : T ◮ T ′ , and n : U ◮ U ′ . Definition 142. Let A be a reduction rule over Σ. An action of A in a reduction Σmonad R is a morphism in the slice category Mod(R)/MVar A (R) between hyp A (R) and

making the following diagram commute:

Example 143 (Action of the congruence rule for application). Consider the reduction rule of the congruence for application of Example 137. Let R be a reduction Σ LCmonad R. An action in R is a R-module morphism mapping, for each set X, a sextuple (T, T ′ , U, U ′ , r, s) with r : T ◮ T ′ and s : U ◮ U ′ to a quintuple (A, A ′ , B, B ′ , m) with m : app(A, B) ◮ app(A ′ , B ′ ). The commutation of the triangle (5.1) ensures that

Alternatively (as justified formally by Lemma 157), an action is a morphism mapping the same sextuple to a reduction m : app(T, U ) ◮ app(T ′ , U ′ ).

Remark 144. Any reduction rule A over Σ induces an arity (D, a, u, v) over RedMon Σ defined as follows:

• a : D → RedMon Σ is the Grothendieck fibration corresponding (through the Grothendieck construction) to the functor mapping a reduction Σ-monad R to the category

Then, the notion of action of this induced arity (see Chapter 2) coincides with the one introduced in this section. monads is effective.

Reduction signatures

We define here reduction signatures and their models.

Definition 145. A reduction signature is a signature over the category of reduction monads, consisting of:

• the pullback of a signature for monads Σ along the forgetful functor from reduction monads to monads;

• a family of arities induced by reduction rules over Σ (as explained in Remark 144).

A reduction signature is thus determined by a signature for monads Σ and a family of reduction rules R over Σ. We denote (Σ, R) the induced reduction signature.

We unfold the definition of model for reduction signatures:

Remark 146. Given a reduction monad R and a reduction signature S = (Σ, R), an action of S in R consists of an action of Σ in its underlying monad R and an action of each reduction rule of R in R. A model of S is a reduction monad equipped with an action of S, or equivalently, a reduction Σ-monad equipped with an action of each reduction rule of R.

Morphisms of models

Here we unfold the definition of morphism between models of a reduction signature: it relies on the functoriality of the assignments R → Hyp A (R) and R → Con A (R), for a given reduction rule A on a signature Σ for monads.

Definition 147. Let Σ be a signature for monads, and A be a reduction rule over Σ. Definition 140 assigns to each Σ-monad R the R-modules Hyp A (R) and Con A (R).

These assignments extend to functors Hyp A , Con A : RedMon Σ → Mod.

Proposition 148. Given the same data, the functors Hyp A and Con A commute with the forgetful functors to Mon:

Mon

Let S = (Σ, R) be a reduction signature. As usual, we denote RedMon S the category of models of S. More concretely, a morphism between models R and T of S is a morphism f of reduction Σ-monads commuting with the action of any reduction rule, in the sense that for any reduction rule A ∈ R, the following diagram of natural transformations commutes:

Example 149 (Example 143 continued). Consider the reduction signature consisting of the signature Σ app of a binary operation app and a single reduction rule of congruence for application (Example 137).

Let R and T be models for this signature: they are reduction Σ app -monads equipped with an action ρ and τ , in the alternative sense of Example 143. A Σ app -monad morphism (f, α) between R and T is a model morphism if, for any set X, any sextuple

The main result

We state our main result, Theorem 150, which gives a sufficient condition for S to be effective.

Theorem 150. Let (Σ, R) be a reduction signature. If Σ is effective, then so is (Σ, R).

The proof of this theorem is given in Section 5.5. Theorem 107 entails the following corollary:

Proof of Theorem 150

This section details the proof of Theorem 150.

Let S = (Σ, (A i ) i∈I )) be a reduction signature. We denote by U Σ the forgetful functor from the category of reduction Σ-monads to the category of Σ-monads.

In Section 5.5.1, we first reduce to the case of reduction rules (V, (n j , h j ) j∈J , (n, c)) for which n = 0, that we call normalized. Then, in Section 5.5.2, we give an alternative definition of the category of models that we make use of in the proof of effectivity, in Section 5.5.3.

Normalizing reduction rules

Definition 155. A reduction rule (V, (n j , h j ) j∈J , (n, c)) is said to be normalized if n = 0. Lemma 156. Let A = (V, (n j , h j ) j∈J , (n, c)) be a reduction rule over Σ. Then there exists a normalized reduction rule A ′ over Σ such that the induced notion of action is equivalent, in the sense that:

• for a reduction Σ-monad R, there is a bijection between actions of A in R and actions of A ′ in R;

• a morphism between reduction Σ-monads equipped with an action of A preserves the action (in the sense of Section 5.4.2) if and only if it preserves the corresponding action of A ′ through the bijection.

Before tackling the proof, we give an alternative definition of action and model morphism: (n,c)) be a reduction rule over Σ. By universal property of the pullback Con A (R) = c * Red(R) (n) , an action can be alternatively be defined as an R-module morphism σ :

.

(5.3)

Corollary 159. For each reduction signature, there exists a reduction signature yielding an isomorphic category of models and whose underlying reduction rules are all normalized.

Proof. Just replace each reduction rule with the one given by Lemma 156.

Thanks to this lemma, we assume in the following that all the reduction rules of the given signature S are normalized.

Models as vertical algebras

In this section, we give an alternative definition for the category of models of S that is convenient in the proof of effectivity.

First we rephrase the notion of action of a reduction rule as an algebra structure for a suitably chosen endofunctor. Indeed, an action of a normalized reduction rule

such that the following square commutes:

We can rephrase this commutation by stating that this morphism τ is a morphism in the slice category Mod(R)/R 2 from an object that we denote by F A|R (Red(R), red R ), to (Red(R), red R ). Here, we use the notation R to refer explicitly to the underlying monad of R. Actually, the domain is functorial in its argument, and thus the action τ can be thought of as an algebra structure on (Red(R), red R ):

yields an endofunctor F A|R on Mod(R)/R 2 . An action of A in a reduction Σ-monad R is exactly the same as an algebra structure for this endofunctor on

Furthermore, the assignment R → F A|R (Red(R), red R ) yields an endofunctor F A on the category of reduction Σ-monads. This functor preserves the underlying Σ-monad, in the sense that

Proof. This is a consequence of the functoriality of Hyp A , as noticed in Section 5.4.2. Now, we give our alternative definition of the category of models: Proposition 161. Let F S : RedMon Σ → RedMon Σ be the coproduct i F A i . Then, the category of models of S is isomorphic to the category of vertical algebras of F S defined as follows:

• an object is an algebra r : F S (R) → R such that r is mapped to the identity by U Σ

• morphisms are the usual F S -algebra morphisms.

We adopt this definition in the following. We show now a property of the category of models that will prove useful in the proof of effectivity: Lemma 162. The forgetful functor from the category of models of S to the category of Σ-monads is a fibration.

The proof relies on some additional lemmas, in particular the following one, that we will specialize by taking p = U Σ (requiring to show that U Σ : RedMon Σ → Mon Σ is a fibration) and F = F S : Lemma 163. Let p : E → B be a fibration and F an endofunctor on E satisfying p • F = p. Then the category of vertical algebras of F is fibered over B.

Let a : a * R → R be the associated cartesian morphism in E. We define the reindexing of r along a as follows: the base object is a * R, and the algebra structure ρ : F (a * R) → R is given by the unique morphism which factors F (a * R)

/ / F (R) r / / R through the cartesian morphism a : a * R → R. Thus, the square

commutes, so a is a morphism of algebras between ρ and r. Next, we prove that it is a cartesian morphism: let s : F (S) → S be a vertical algebra over an object Z of B, and v : s → r be a morphism of algebras such that there exists b : Z → Y such Proof. We have the two following pullbacks:

where V ( Mod) is the full subcategory of arrows of Mod which are vertical (that is, they are mapped to the identity monad morphism by the functor from Mod to Mon), and cod maps such an arrow to its codomain. By Propositions 25 and 29, the category Mod has fibred finite limits , so that cod is a fibration ([See00, Exercise 9.4.2 (i)]). Now, Proposition 8.1.15 of [START_REF] Borceux | Encyclopedia of Mathematics and its Applications[END_REF] states that a pullback of a fibration is a fibration. Thus, the middle functor RedMon → Mon is a fibration, and then, U Σ : RedMon Σ → Mon Σ also is.

Finally, gathering all these lemmas yields a proof that the category of models of S is indeed fibered over the category of Σ-monads:

Proof of Lemma 162. Apply Lemma 163 with the fibration p = U Σ (Lemma 164) and F = F S .

Effectivity

In this section, we prove that S has an initial model, provided that there exists an initial Σ-monad. The category of models of S is fibered over the category of Σ-monads. A promising candidate for the initial model is the initial object, if it exists, in the fiber category over the initial Σ-monad: Lemma 165. Let p : E → B be a fibration, b 0 be an initial object in B and e 0 be an object over b 0 that is initial in the fiber category over b 0 . Then e 0 is initial in E.

In the following, we thus construct the initial object in a fiber category over a given Σ-monad R. This fiber category can be characterized as a category of algebras: Lemma 166. The fiber category over a given Σ-monad R through the fibration from models of S (Lemma 162) is the category of algebras of the endofunctor

Thus, our task is to construct the initial algebra of some specific endofunctor.

Adámek's theorem [START_REF] Adámek | Free algebras and automata realizations in the language of categories[END_REF] provides a sufficient condition for the existence of an initial algebra:

Lemma 167 (Adámek). Let F be a finitary endofunctor on a cocomplete category C.

Then the category of algebras of F has an initial object.

This initial object can be computed as a colimit of a chain, but we do not rely here on the exact underlying construction.

The first requirement to apply this lemma is that the base category is cocomplete, and this is indeed the case: Lemma 168. The category Mod(R)/R 2 is cocomplete for any monad R.

Proof. The category of modules Mod(R) over a given monad R is cocomplete by Proposition 25, so any of its slice categories is, by the dual of [ML98, Exercise V.1.1], in particular Mod(R)/R 2 .

Let us show that the finitarity requirement of Lemma 167 is also satisfied for the case of a signature with a single reduction rule: Lemma 169. Let A = (V, (n i , h i ) i∈I , (0, c)) be a normalized reduction rule over Σ, and R be a Σ-monad. Then, F A|R is finitary. Given a filtered diagram we want to show that the image by F of the colimiting cocone is colimiting. As π creates colimits, this is enough to show that the image by π • F of the colimiting cocone is colimiting. Thus, it is enough to prove that π • F :

Given any q ∈ Mod(R)/R 2 the module π(F (q)) is Hyp A (R), which can be computed

Equation

The syntax of lambda calculus with explicit substitutions of [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF] is subject to the equation (see [Kes09, Figure 1, "Equations"])

(5.4)

We rephrase it as an equality between two parallel Υ LCex -module morphisms from Θ ′′ × Θ × Θ, modelling the metavariables t, u, and v, to Θ:

Here, ι denotes the inclusion Θ → Θ ′ , and esubst ∨ is the composition of esubst ′ with swap : Θ ′′ → Θ ′′ swapping the two fresh variables. Now we are ready to define the signature of the lambda calculus monad with explicit substitutions:

Definition 172. The signature Σ LCex of the lambda calculus monad with explicit substitutions consists of Υ LCex and the single Σ LCex -equation stating the equality between the two morphisms of Equation 5.5.

Lemma 173. The signature Σ LCex for monads is effective Proof. This is a direct consequence of Corollary 151.

Reduction rules for lambda calculus with explicit substitutions

The reduction signature for the lambda calculus with explicit substitutions consists of two components: the first one is the signature for monads Σ LCex of Definition 172; the second one is the list of reduction rules that we enumerate here, taken from [Kes09, Figure 1, "Rules"]. Except for congruence, none of them involve hypotheses.

First, let us state the congruence rules (that are implicit in [START_REF] Kesner | A Theory of Explicit Substitutions with Safe and Full Composition[END_REF]):

Guided by this intuition, we now formally define a Σ LCex -module Θ * equipped with a morphism κ : Θ * → Θ ′ .

The previous informal inductive definition is translated as an initial algebra for an endofunctor on the category of Σ LCex -modules, which is cocomplete (colimits are computed pointwise). This endofunctor maps a Σ LCex -module M to the coproduct of the following Σ LCex -modules:

• the terminal Σ LCex -module 1, playing the rôle of the fresh variable;

• the coproduct M × Θ + Θ × M + M × M , one summand for each case of the application;

• the derived module M ′ for abstraction;

• the coproduct M ′ × Θ + Θ ′ × M + M ′ × M , one summand for each case of the explicit substitution.

This functor is finitary, so the initial algebra exists thanks to Adámek's theorem (already cited, as Theorem 167). Unfortunately, the resulting Σ LCex -module does not yield the module that we are expecting in the case of the monad LC ex : it does not satisfy Equation 5.5, and thus contains more terms than necessary. To obtain the desired Σ LCex -module, we equip Θ ′ with its canonical algebra structure, inducing a morphism from the initial algebra, and we define Θ * as the image of this morphism, thus equipped with an inclusion κ : Θ * → Θ ′ .

Definition 174. We define the Σ LCex -module of "one-hole contexts" to be Θ * , equipped with an inclusion κ : Θ * → Θ ′ .

Remark 175. Such a definition can be worked out for any algebraic signature for monads.

Now we define the signature of the reduction monad of lambda calculus with explicit substitutions: Definition 176. The reduction signature S LCex of the lambda calculus reduction monad with explicit substitutions consists of the signature Σ LCex of Definition 172 and all the reduction rules specified in this section.

is the initial algebra of the endofunctor

where F ′ is the functor mapping a set X to F (X + 1).

The two properties that we want to show about the collection of functions (α X ) X are then done by induction on the first argument, again exploiting initiality of LC ′ • j, as we explain below. The proof goes as follows:

1. construct (by initiality) a morphism from LC ′ • j to the exponential of R • j with itself, that is, to the functor R R : Set 0 → Set defined on objects by X → R(X) R(X) ; 2. show that the induced morphism from

3. show the commutation required by Equation 5.7.

Note how working in the functor category [Set 0 , Set] allows us to define the functor R R as above, without worrying about the functorial action on morphisms. Below we sometimes omit the explicit precomposition with j in order to simplify the notation. Now we perform the steps explained above.

1. As we argued before, LC ′ • j is the initial algebra of Ψ, so our task consists in equipping R R with an algebra structure for Ψ, that we split into the following four components, using the universal properties of the coproduct and the exponential in the category [Set 0 , Set]:

(a) The morphism j × R → R corresponds to the case of variables. We expect that the resulting module morphism α :

refl X (x) for any x ∈ X, where refl : LC → R maps a term to the reflexive reduction on itself and η : Id → LC ′ is the unit of the monad LC. Accordingly, we define the morphism j × R → R as mapping a pair (x, m) ∈ X × R(X) to refl X (η(x)).

(b) The morphism R → R corresponds to the case of the fresh variable * . We expect that α X ( * , m) = m. Accordingly, the required morphism is taken as the identity on R.

forgetful functors to the category Mon of monads,

Mon

Example 194. To each Σ-module Ψ is associated, by precomposition with the projection to Mon Σ , a (Σ, S)-module still denoted Ψ.

Definition 195. Let S and T be (Σ, S)-modules. We define a morphism of (Σ, S)modules from S to T to be a natural transformation from S to T which becomes the identity when postcomposed with the forgetful functor Mod → Mon.

Then we define S-term-pairs:

Definition 196. Given a Σ-module V, a S-term-pair from V is a pair (n, p) of a natural number n and a morphism of (Σ, S)-modules p :

, where

We now give our definition of S-reduction rule.

Definition 197. A S-reduction rule A = (V, (n i , h i ) i∈I , (n, c)) over Σ is given by:

• Metavariables: a Σ-module V of metavariables, that we sometimes denote by

• Hypotheses: a finite family of S-term-pairs (n i , h i ) i∈I from V;

• Conclusion: a S-term-pair (n, c) from V.

S-Reduction Σ-monads

Similarly to Chapter 5, the purpose of a S-reduction rule is to be validated in a Sreduction monad R, that is, an operational monad whose underlying state functors are models of S. Here again, as the hypotheses or the conclusion of the S-reduction rule may refer to some operations specified by a signature Σ for monads, this S-reduction monad R must be equipped with an action of Σ, hence the following definition.

from the hypotheses to the conclusion" of the S-reduction rule. To make this precise, we need to first take the product of the hypotheses; this product is, more correctly, a fibred product.

Definition 199. Let (n, p) be a S-term-pair from a Σ-module V, and R be a S-reduction Σ-monad. We denote by p * (Red(R) (n) ) the pullback of red

. We denote by p * (red (n,c)) be a S-reduction rule, and R be a Sreduction Σ-monad.

The R-module

the fiber product of all the R-modules h * i RedR (n i ) along their projection to V(R). It thus comes with a projection hyp A (R) :

The R-module Con A (R) of conclusion of A is c * Red(R) (n) . It comes with a projection con A (R) :

Definition 201. Let A be a S-reduction rule over Σ. An action of A in a S-reduction Σ-monad R is a morphism, in the slice category Mod(R)/MVar A (R), between hyp A (R) and con A (R), that is, a morphism of R-modules τ :

making the following diagram commute:

Remark 202. Any S-reduction rule A over Σ defines an arity (D, a, u, v) over the category of S-reduction Σ-monads (in the sense of Chapter 2) as follows:

the pullback of a signature S 1 for endofunctors along the functor mapping an operational monad to its first state functor;

the pullback of a signature S 2 for endofunctors along the functor mapping an operational monad to its second state functor.

• a family of arities induced by (S 1 , S 2 )-reduction rules over Σ, as explained in Remark 202.

An operational signature is thus determined by two signatures for endofunctors S 1 and S 2 , a signature for monads Σ, and a family of reduction rules R over Σ. We denote

Examples are given in Section 6.4.

We unfold the definition of model for operational signatures:

Remark 204. Let O = (S 1 , S 2 , Σ, R) be an operational signature. Let S := ( Ŝ1 , Ŝ2 ). A model of O is a S-reduction Σ-monad equipped with an action of each reduction rule of R.

Morphisms of models

Here we unfold the definition of morphism between models of a operational signature: it relies on the functoriality of the assignments R → Hyp A (R) and R → Con A (R), for a given reduction rule A on a signature Σ for monads.

Definition 205. Let S be a pair of signatures over the category of endofunctors on Set.

Let Σ be a signature for monads, and A be a S-reduction rule over Σ. Definition 200 assigns to each S-reduction Σ-monad R the R-modules Hyp A (R) and Con A (R). These assignments extend to functors Hyp A , Con A : S-RedMon Σ → Mod.

Proposition 206. Given the same data, the functors Hyp A and Con A commute with the forgetful functors to Mon:

Mon

Now, a morphism between models R and S of a signature O = (S 1 , S 2 , Σ, R) is a morphism f of S-reduction Σ-monads commuting with the action of any S-reduction rule, in the sense that for any S-reduction rule A ∈ R, the following diagram of natural transformations commutes:

The main result

We state our main result, Theorem 207, which gives a sufficient condition for an operational signature to be effective.

Theorem 207. Let O = (S 1 , S 2 , Σ, R) be an operational signature. If S 1 , S 2 , and Σ are effective, then so is O.

Proof. This is a close adaptation of the proof detailed in Section 5.5. Therefore, we only sketch the main arguments. Consider the two following pullbacks, the left one defining OpMon Σ,S :

Then, the left vertical arrow is a fibration by the same argument detailed in Lemma 164. Moreover, the category of models of O is isomorphic to the category of vertical algebras of an endofunctor F O on OpMon Σ,S , by the same argument as in Proposition 161. Then, this category of models is fibered over

by Lemma 163, and the fiber category over (R, T 1 , T 2 ) is the category of algebras of the restriction of

, following an argument similar to that of Lemmas 166 and 169. Now, we apply Lemma 165: we only need to show that the fiber category over ( Σ, S 1 , S 2 ) has an initial object, that is, we must construct an initial algebra for a finitary endofunctor thanks to the previous remark. Adámek's theorem (Lemma 167) allows to conclude.

We already know a class of effective signatures for monads: they are the algebraic 2-signatures (Theorem 107). In the next section, we introduce a similar notion of algebraic signature for endofunctors based on equational systems whose effectivity is ensured by [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF]. This will allow us to state Corollary 220, as a consequence of Theorem 207, that we will use for our examples.

Specifying the state functors

We choose to rely on Fiore and Hur's notion of equational system [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF]. Thanks to Example 14, they can be considered as signatures in the sense of Chapter 2.

A first definition of signature for endofunctors on Set that we can think of is an endofunctor on [Set, Set] whose algebras are the models of the signature. Definition 208. A 1-signature for endofunctor (or just 1-signature in this subsection) is a signature over the category of endofunctors on Set consisting of a single arity induced by an endofunctor Σ on Set, as described in Example 3. A 1-signature is thus uniquely determined by an endofunctor Σ on [Set, Set], and for this reason we identify 1-signatures with endofunctors on the category [Set, Set] in the following.

Proposition 209. The category of endofunctors on [Set, Set] is complete and cocomplete: limits and colimits are computed pointwise.

Notation 210. The following is reminiscent of 1-signatures for monads:

• Θ is the identity endofunctor Id on the category of endofunctors on Set;

• if Σ is a 1-signature for endofunctors, we denote by Σ (n) its n th derivative, where Σ (n) (F ) := Σ(F ) (n) mapping a set X to the set Σ(F )(X + n), for any endofunctor F ;

• Σ ′ := Σ (1) , for any 1-signature Σ for endofunctors;

• if F is an endofunctor on Set, the constant 1-signature mapping any functor to F is denoted by F ;

) is an algebraic parametric module, we denote Σ the 1-signature for endofunctors defined by the same formula.

The clash of notations with parametric modules is justified by the fact that given any monad R and algebraic parametric module Σ for monads, the functor underlying the image of R by Σ is the image of the functor underlying R by Σ. More formally: Proposition 211. Let Σ be an algebraic parametric module. Then, the following diagram commutes:

We now introduce algebraic 1-signatures for endofunctors, which satisfy an initiality theorem:

Example 213. If Σ is an algebraic 1-signature for monads, then Σ is an algebraic 1signature for endofunctors.

Proposition 214. Any algebraic 1-signature Σ for endofunctors is effective.

Proof. This follows from Adámek's theorem (Lemma 167), as the endofunctor underlying an algebraic 1-signature is finitary.

Actually, the functor underlying the initial model of an algebraic 1-signature for monads is specified by an appropriate algebraic 1-signature for endofunctors: Proposition 215. Let Σ be an algebraic 1-signature for monads. Then the functors underlying Σ and Σ + Id Set are isomorphic.

Next, we would like to specify equations. To this end, we use equational systems [START_REF] Fiore | On the construction of free algebras for equational systems[END_REF], that we rephrase using our terminology. We focus on equations of the shape

• R is an algebra of a an endofunctor Σ (that is, R is a monad of the induced 1-signature by Σ);

• Ψ(R) is an endofunctor on Set;

• u R and v R are parallel natural transformations between Ψ(R) and R.

The assignment R → (Ψ(R), u R , v R ) is required to be functorial. Set → Set, such that T (A) denotes the set of π-calculus processes up to structural congruence with free channels in A. For this, let us consider the endofunctor on [Set, Set] defined for all X ∈ [Set, Set] and γ ∈ Set by

(with corresponding pieces of syntax below each term of the sum, and using the notations of Definition 212 for the last line). As an example of Σ-equation (Ψ, u, v), commutativity of parallel composition would have Ψ(X)(γ) = X(γ) 2 . The first natural transformation u : Ψ → Θ maps any Σ -alg, say ρ : ΣX → X, to the natural transformation with component u X,ρ,γ : Ψ(X)(γ) = X(γ) 2 → X(γ) at γ given by parallel composition, i.e., the composite

and v X,ρ,γ given by swapping, and then parallel composition. All equations may be treated similarly, forming a signature S for endofunctors which is algebraic, whose initial algebra is the desired T .

Proposition 218 and Theorem 207 entail the following corollary of Theorem 207.

Corollary 220. Let O = (S 1 , S 2 , Σ, R) be an operational signature. If S 1 and S 2 are algebraic 2-signatures for endofunctors and Σ is an algebraic 2-signature for monads, then O is effective.

All the examples of operational signatures considered here satisfy the algebraicity condition of Corollary 220.

Examples of operational signatures

We give examples of operational signatures for the call-by-value lambda calculus in Section 6.4.1, for the big-step operational semantics variant in Section 6.4.2, and for the π-calculus in Section 6.4.3. The reduction rules are given following the schematic presentation described in Section 5.3.5. These signatures all satisfy the hypotheses of Corollary 220, and thus are effective.

Call-by-value lambda calculus

We give an operational signature for the operational monad ((B, B), LC v ) of the callby-value lambda calculus from Example 190. Recall that B is the monad of binary trees underlying the initial model of the 1-signature Θ × Θ. By Proposition 215, the corresponding algebraic signature for endofunctor is S = (Θ × Θ + Id Set , ∅). A model T of S comes equipped with a binary operation app : T × T → T and a variable operation v : Id Set → T . We denote by j T : B → T the initial morphism. Now, we give a signature for the monad LC v of values of the lambda calculus. A value is either a variable or an abstracted lambda term, and we argued in Example 190 that a lambda term can be specified as a binary tree whose leaves are values. Thus, we choose the 1-signature B • Θ ′ to specify the monad of values. Note that this is algebraic as B is polynomial: we have

where B n is the set of binary trees with n leaves. A model of this signature is a monad R with a module morphism abs R : B • R ′ → R.

We give now the family R of reduction rules:

app(v(abs(T )), v(U ))) j(T ){ * := U } j(T ) j(T ′ ) v(abs(T ))

v(abs(T ′ ))

app(T, U ′ ) .

To conclude, the operational signature is (S, S, B • Θ ′ , R).

Call-by-value lambda calculus with big-step operational semantics

We give a signature for the operational monad ((B, Id), LC v ) of the call-by-value lambda calculus with big-step operational semantics (Example 191). The first state functor B is specified by S as in Section 6.4.1, whereas the second one Id is specified by the algebraic 1-signature for functors Id Set : a model M is an endofunctor with a natural transformation w : Id Set → M

The underlying signature for monads is the same as the one of the call-by-value lambda calculus (Section 6.4.1). Now, we give the family R of reduction rules, using the same notations as in Section 6.4.1:

T w(abs(T ′ )) U w(U ′ ) j(T ′ ){ * := U ′ } V app(T, U ))

V .

To conclude, the operational signature is (S, Id Set , B • Θ ′ , R), where S is defined in Section 6.4.1.

π-calculus

We give an operational signature for the operational monad ((T, T ), Id) of the π-calculus described in Example 192. In Example 219, we gave an algebraic signature S for specifying the endofunctor T . A model M of S comes equipped with the following natural transformations: