10.6092/issn.1972-5787/2066
Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof assistant. The main theorem was first proved on paper in the second author’s PhD thesis in 2010, and verified formally shortly afterwards.
To a simply–typed binding signature S over a fixed set T of object types we associate a category called the category of representations of S. We show that this category has an initial object Sigma(S), i.e. an object Sigma(S) from which there is precisely one morphism i_R : Sigma(S) -> R to any object R of this category. From its construction it will be clear that the object Sigma(S) merits the name abstract syntax associated to S: it is given by an inductive set – parametrized by a set of free variables and dependent on object types – the type of whose constructors are each given by the arities of the signature S.
Our theorem is implemented and proved correct in the proof assistant Coq through heavy use of dependent types. The approach through monads gives rise to an implementation of syntax where both terms and variables are intrinsically typed, i.e. where the object types are rejected in the meta–level types. Terms are implemented as a Coq data type – which play the role of sets – dependent on an object type as well as on a type family of free variables.
This article is to be seen as a research article rather than about the formalization of a classical mathematical result. The nature of our theorem – involving lengthy, technical proofs and complicated algebraic structures – makes it particularly interesting for formal verification. Our goal is to promote the use of computer theorem provers as research tools, and, accordingly, a new way of publishing mathematical results: a parallel description of a theorem and its formalization should allow the verification of correct transcription of definitions and statements into the proof assistant, and straightforward but technical proofs should be well–hidden in a digital library. We argue that Coq’s rich type theory, combined with its various features such as implicit arguments, allows a particularly readable formalization and is hence well–suited for communicating mathematics.
application/pdf
1972-5787
2066
1
en
Julianna Zsido
Journal of Formalized Reasoning
Initial Semantics for higher-order typed syntax in Coq
Text.Serial.Journal
https://jfr.unibo.it/
4
Articles
2011-09-08
2011-02-18
2011-04-14
2016-01-29
25-69
JFR
Julianna Zsido
2011/09/08
10.6092/issn.1972-5787/2066
25
Universite' Montpellier II, France
1972-5787
1
en
69
Initial Semantics for higher-order typed syntax in Coq
https://jfr.unibo.it/article/download/2066/1674
4
Initial Semantics for higher-order typed syntax in Coq
BENEDIKT AHRENS
Université Nice – Sophia Antipolis, France
ahrens@unice.fr
and
JULIANNA ZSIDÓ
Université Montpellier II, France
jzsido@univ-montp2.fr


Initial Semantics aims at characterizing the syntax associated to a signature as the initial object
of some category. We present an initial semantics result for typed syntax with variable binding
together with its formalization in the Coq proof assistant. The main theorem was first proved on
paper in the second author’s PhD thesis in 2010, and verified formally shortly afterwards.
    To a simply–typed binding signature S over a fixed set T of object types we associate a category
called the category of representations of S. We show that this category has an initial object Σ(S),
i.e. an object Σ(S) from which there is precisely one morphism iR : Σ(S) → R to any object R of
this category. From its construction it will be clear that the object Σ(S) merits the name abstract
syntax associated to S: it is given by an inductive set — parametrized by a set of free variables
and dependent on object types — the type of whose constructors are each given by the arities of
the signature S.
    Our theorem is implemented and proved correct in the proof assistant Coq through heavy use
of dependent types. The approach through monads gives rise to an implementation of syntax
where both terms and variables are intrinsically typed, i.e. where the object types are reflected in
the meta–level types. Terms are implemented as a Coq data type — Coq types play the role of
sets — dependent on an object type as well as on a type family of free variables.
    This article is to be seen as a research article rather than about the formalization of a classical
mathematical result. The nature of our theorem – involving lengthy, technical proofs and compli-
cated algebraic structures – makes it particularly interesting for formal verification. Our goal is
to promote the use of computer theorem provers as research tools, and, accordingly, a new way of
publishing mathematical results: a parallel description of a theorem and its formalization should
allow the verification of correct transcription of definitions and statements into the proof assistant,
and straightforward but technical proofs should be well–hidden in a digital library. We argue that
Coq’s rich type theory, combined with its various features such as implicit arguments, allows a
particularly readable formalization and is hence well–suited for communicating mathematics.




                                          Journal of Formalized Reasoning Vol. 4, No. 1, 2011 Pages 25–69.
26     ·     B. Ahrens and J. Zsidó

Contents

1 Introduction                                                                   27
  1.1 Inductive Types, Categorically . . . . . . . . . . . . . . . . . . . . . 28
  1.2 Overview of the paper . . . . . . . . . . . . . . . . . . . . . . . . . . 31
  1.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

2 Preliminaries                                                                 33
  2.1 About the proof assistant Coq . . . . . . . . . . . . . . . . . . . . . . 33
  2.2 How to formalize algebraic structures . . . . . . . . . . . . . . . . . . 34

3 Categories, Monads & Modules                                                                                             36
  3.1 Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .                                     .   .   36
      3.1.1 Which Definition to Formalize – Dependent Hom–Types?                                                   .   .   37
      3.1.2 Setoidal Equality on Morphisms . . . . . . . . . . . . . .                                             .   .   37
      3.1.3 Coq Setoids and their morphisms . . . . . . . . . . . . . .                                            .   .   38
      3.1.4 Coq implementation of categories . . . . . . . . . . . . . .                                           .   .   39
      3.1.5 Interlude on the Program feature . . . . . . . . . . . . . .                                           .   .   40
  3.2 Invertible morphisms, Initial objects . . . . . . . . . . . . . . . .                                        .   .   40
  3.3 Functors & Natural Transformations . . . . . . . . . . . . . . . .                                           .   .   41
  3.4 Monads, modules and their morphisms . . . . . . . . . . . . . . .                                            .   .   41
  3.5 Constructions on modules . . . . . . . . . . . . . . . . . . . . . .                                         .   .   48
  3.6 Fibres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .                                     .   .   49
  3.7 Derivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .                                     .   .   50

4 Signatures & Representations                                                    52
  4.1 Arities & Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
  4.2 Representations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
  4.3 Morphisms of Representations . . . . . . . . . . . . . . . . . . . . . . 55

5 The      Initial Object                                                                                                  60
  5.1      The Syntax associated to a Signature .      .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   60
  5.2      Monad Structure on Syntax . . . . . .       .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   61
  5.3      A representation in the Syntax . . . .      .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   62
  5.4      Weak Initiality . . . . . . . . . . . . .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   63
  5.5      Uniqueness & Initiality . . . . . . . . .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   .   64

6 Conclusions & Future Work                                                                                                65




Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                           Initial Semantics in Coq       ·     27

1.     INTRODUCTION
Computer theorem proving is a subject of active research, and provers are under
heavy development, evolving rapidly. However, we believe that the provers at hand
— and in particular, our favourite prover Coq [Coq] — have reached a state where
they are well usable as a research tool. Instead of benchmarking it with one of
the classical mathematical results, as is done e.g. in Wiedijk’s list “Formalizing 100
theorems” 1 (cf. also [Wie08]), we use Coq to prove a recent theorem about typed
abstract syntax with variable binding 2 . Through the use of Coq features such as
implicit arguments, coercions and overloading through type classes the formal text
remains close to its informal counterpart, thus easing the verification of correct
transcription of definitions and statements into the formal language.
   Category–theoretic concepts have been introduced to computer science, more
specifically to programming, in order to give mathematical structure to programs,
e.g. by Wadler [Wad95]. This development culminates in the programming language
Haskell, whose basic programming idioms are indeed category–theoretic notions.
In particular, the notion of monad, which we also use extensively, has a prominent
rôle in Haskell.
   In his PhD thesis, Vene [Ven00] studies different classes of recursive functions
and characterizes them as morphisms in some category.
   All these examples concern category theoretic concepts which can be found within
the programming language, i.e. on the object level. In this paper, however, category
theory is used on the meta level in order to give a definition of the programming
language associated to a signature.
   Indeed, our goal is to characterize the set of terms of a language given by a typed
binding signature via a universal property, and give a category–theoretic justification
for the recursion principle it is equipped with.
   A universal property characterizes its associated object — if it exists — up to a
unique isomorphism, for a suitable notion of morphism. Universal properties are
ubiquitous in mathematics, and fundamental concepts such as the cartesian product
of two sets, the free group associated to a set or the field of quotients associated to
an integral domain can be defined as objects verifying a suitable universal property.
   The universal property we use to characterize syntax is initiality (cf. Def. 3.5):
given a signature S, we construct a category in which the syntax Σ(S) associated
to S is initial, thus characterizing Σ(S) up to isomorphism.
   This is precisely what the expression “Initial Semantics” stands for: the objects
of this category can be thought of as “semantics” of S, and the syntax Σ(S) is the
initial such semantics 3 .
   In this paper, category–theoretic concepts appear in two places: firstly, as ex-
plained above, we characterize the syntax Σ(S) associated to a signature S as the

1 http://www.cs.ru.nl/∼freek/100/index.html
2 We  use the term “higher–order” synonymous to “with variable binding”. The term is also used
in the expression “Higher–Order Abstract Syntax”, where it refers to the way in which variable
binding is modeled, e.g. as in lam : (T → T ) → T . We do not model variable binding in this way.
3 We use the word “semantics” with two different meanings. Accompanied by the word “initial”,

i.e. in the expression “initial semantics”, it refers to the syntax associated to some signature S
being the initial “model” or “semantics”, in a category of “semantics of S”. The word “semantics”
by itself signifies a relation on terms, usually a reduction relation, e.g. beta reduction.
                                               Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
28     ·     B. Ahrens and J. Zsidó

initial object of some category. Secondly, the objects of said category are built from
monads (cf. Def. 3.9) over the category of (families of) sets. Indeed, we consider
an untyped programming language to be given by such a monad, i.e. a map which
associates to any set V a set of terms with free variables in V , together with some
extra structure (cf. Ex. 3.14). For simply–typed syntax over a set T of types, we
regard families of sets, indexed by T , rather than just sets, cf. Ex. 3.15.
   We consider the syntax Σ(S) to be given as an inductive family of sets, parame-
trized by free variables and indexed by the set of object types. Initial Semantics
can hence also be seen as the study of a restricted class of inductive data types.
   In Subsec. 1.1 we introduce initiality using a particularly simple inductive set —
the natural numbers — and outline its generalization to abstract syntax as a para-
metrized and dependent inductive type. In Subsec. 1.2 we give a technical overview
of the paper. In Subsec. 1.3 we give an overview over various initial semantics
results.
   The complete Coq code can be obtained from the first author’s web page 4 .

1.1   Inductive Types, Categorically
Initial Semantics has its origins in the Initial Algebras as studied by Goguen et al.
[GTWW77]. It can be considered as a category–theoretic treatment of recursion
and induction. A prominent example is given by the Peano axioms: consider the
category N an object of which is a triple (X, Z, S) of a set X together with a
constant Z ∈ X and a unary operation S : X → X. A morphism to another such
object (X 0 , Z 0 , S 0 ) is a map f : X → X 0 such that
                            f (Z) = Z 0      and       f ◦ S = S0 ◦ f .          (1.1)
This category has an initial object (N, Zero, Succ) given by the natural numbers N
equipped with the constant Zero = 0 and the successor function Succ. Initiality of
N gives a way to define iterative functions [Ven00] from N to any set X by equipping
X with a constant Z ∈ X and a unary map S : X → X, i.e. making the set X the
carrier of an object (X, Z, S) ∈ N .
   Using the preceding example, we now informally introduce some vocabulary
which is used (and properly defined) later. For specifying a syntax, an arity indi-
cates the number of arguments of a constructor. The arities of Z and S are 0 and
1, respectively. A representation of an arity n in a set X is then given by an n–ary
operation on X. A signature is a family – indexed by some arbitrary set J – of
arities. A representation of a signature is given by a set X and a representation of
each arity of S in X. The signature N of the preceding example is given by
                                  N := {z 7→ 0 ,         s 7→ 1} ,
and a representation of this signature is any triple (X, S, Z) as above.
   Adding variables. When considering syntax with variable binding, the set of terms
is indexed by a set of variables whose elements may appear freely in those terms.

4 http://math.unice.fr/∼ahrens




Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                     Initial Semantics in Coq       ·     29

   Example 1.1. As an example, consider the following inductive set LC : Set → Set
of terms of the untyped lambda calculus:
                 LC(V ) ::=    Var : V → LC(V )
                              | Abs : LC(V ∗ ) → LC(V )
                              | App : LC(V ) → LC(V ) → LC(V ) ,
where V ∗ := V + {∗} is the set V enriched with a new distinguished variable —
the variable which is bound by the Abs constructor (cf. Sec. 3.7). We continue this
example in the course of the paper (cf. Ex. 3.14, 3.21, 3.22 , 3.25, 4.5, 4.11).
In this case arities need to carry information about the binding behaviour of the
constructor they are associated to. One way to define such arities is using lists
of natural numbers. The length of a list then indicates the number of arguments
of the constructor, and the i-th entry denotes the number of variables that the
constructor binds in the i-th argument. The signature LC of LC is given by
                       LC := {app 7→ [0, 0] ,    abs 7→ [1]} .
   Representations in sets are not adequate any more for such a syntax; instead
we should represent the signature LC in objects with the same type as LC, i.e.
in maps F : Set → Set associating a set F (V ) to any given set V “of variables”.
Accordingly, a representation of an arity now is not simply an n–ary operation, but
a family of maps, indexed by the set V of variables. Indeed, a representation of,
e.g. the arity abs of LC, in a suitable map F : Set → Set, should have the same
type as the constructor Abs, that is,
                           absF (V ) : F (V ∗ ) → F (V ) .
   Interlude on monads. Instead of maps F : Set → Set as in the preceding para-
graph, we consider in fact monads on the category Set of sets. Monads are such
maps equipped with some extra structure, which we explain by the example of the
untyped lambda calculus. The map V 7→ LC(V ) comes with a (capture–avoiding)
substitution operation: let V and W be two sets (of variables) and f be a map
f : V → LC(W ). Given a lambda term t ∈ LC(V ), we can replace each free vari-
able v ∈ V in t by its image under f , yielding a term t0 ∈ LC(W ). Furthermore
we consider the constructor VarV as a “variable–as–term” map, indexed by a set
of variables V ,
                                VarV : V → LC(V ) .
There is a well–known algebraic structure which captures those two operations and
their properties: substitution and variable–as–term map turn LC into a monad
(Def. 3.9) on the category of sets, an observation first made by Altenkirch and
Reus [AR99]. We expand on this in Ex. 3.14.
  The monad structure of LC should be compatible in a suitable sense with the
constructors Abs and App of LC. One mathematical structure which would express
such a compatibility is that of a monad morphism. This fails in 2 ways:
  firstly, it is unclear how to equip the domain map V 7→ LC(V ) × LC(V ) of App
with a monad structure.

                                         Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
30     ·     B. Ahrens and J. Zsidó

   Secondly, while the domain of the constructor Abs, the map LC∗ : V 7→ LC(V ∗ ),
inherits a monad structure from LC (cf. Ex. 3.16), the constructor Abs does not
verify the properties of a morphism of monads (cf. Ex. 3.18 and [HM07]).
   As a remedy, Hirschowitz and Maggesi [HM07] consider modules over a monad
(cf. Def. 3.19), which generalize monadic substitution, and suitable morphisms of
modules. Indeed, the maps LC : V 7→ LC(V ) and LC∗ : V 7→ LC(V ∗ ) are the
underlying maps of such modules (cf. Ex. 3.21, 3.22), and the constructors Abs and
App are morphisms of modules (cf. Ex. 3.25).
   Typed syntax. Typed syntax exists with varying complexity, ranging from simply–
typed syntax to syntax with dependent types, kinds, polymorphism, etc. By
simply–typed syntax we mean a non–polymorphic typed syntax where the set of
types is independent from the set of terms, i.e. one has a fixed set of types, the
elements of which are used to type variables and terms. A simply–typed syntax
does not allow type constructors in its associated signatures, only (typed) term con-
structors. In more sophisticated type systems types may depend on terms, leading
to more complex definitions of arities and signatures.
   This work is only concerned with simply–typed languages, such as the simply–
typed lambda calculus and PCF. For such a simply–typed syntax, we first fix a set
T of (object) types. Variables then are equipped with a type t ∈ T , i.e. instead of
one set of variables we consider a family (Vt )t∈T of sets of variables, where Vt is
the set of variables of type t. Similarly the terms of a simply–typed syntax come
as a family of sets, indexed by the (object) types. As an example we consider the
simply–typed lambda calculus TLC:
  Example 1.2. Let T ::= ∗ | T ⇒ T be the set of types of the simply–typed
lambda calculus. For each family V : T → Set of sets and t ∈ T we denote by
Vt := V (t) the set associated to object type t. The set of simply–typed lambda
terms with free variables in the family of sets V is given by the following inductive
declaration:
  TLC(V ) : T → Set ::=           Var : ∀t, Vt → TLC(V )t
                                | Abs : ∀s t, TLC(V ∗s )t → TLC(V )(s⇒t)
                                | App : ∀s t, TLC(V )(s⇒t) → TLC(V )s → TLC(V )t ,
where V ∗s := V + {∗s} is obtained by enriching the family V with a new distin-
guished variable of type s ∈ T — the variable which is bound by the constructor
Abs (s, t). The variables s and t range over the set T of types. The signature
describing the simply–typed lambda calculus is given in Ex. 4.1. The preceding
paragraph about monads and modules applies to the simply–typed lambda calcu-
lus when replacing sets by families of sets indexed by T : the simply–typed lambda
calculus can be given the structure of a monad (cf. Ex. 3.15)
                                  TLC : [T , Set] → [T , Set]
over the category of families of sets indexed by T (Def. 3.3). The constructors of
TLC are morphisms of modules (cf. Ex. 3.23, 3.26).



Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                        Initial Semantics in Coq       ·     31

1.2   Overview of the paper
We present an initial semantics result and its formalization for typed higher–order
syntax with types. The term “higher–order” refers to the fact that the syntax
allows for variable binding in terms. Our types are, more specifically, simple types,
e.g. there is no binding on the level of types.
   Our theorem is not the first of its kind, cf. Sec. 1.3 for related work. It is, however,
the only one which is based on monads and modules and is fully implemented in a
proof assistant.
   In order to account for types, our basic category of interest is the category [T, Set]
of families of sets indexed by a set T . Its objects will also be called “typed sets”
Our monads are monads over [T, Set].
   The notion of module over a monad [HM07] generalizes monadic substitution: a
module is a functor with a substitution map. Morphisms of modules are natural
transformations which are compatible with the module substitution.
   We interpret the syntax associated to a signature S as an initial object in the
category of so–called representations of S. An object of this category is a monad
over typed sets equipped with a morphism of modules for each arity of S. A
morphism of representations is a morphism between the underlying monads which
is compatible with the morphisms of modules. For the initial representation these
module morphisms are given by the constructors of the syntax, and the property
of being a module morphism captures their compatibility with substitution.
   Our theorem is implemented in the proof assistant Coq [Coq]. This implemen-
tation can be seen as a formal proof of a mathematical theorem in a constructive
setting, and as such delivers confidence in the correctness of the theorem.
   Perhaps more importantly, the theorem translates to an implementation of syntax
using exclusively intrinsic typing, a style of implementation that has been advertised
by Benton et al. [BHKM11]. Here typing is not done by a typing judgement,
given by, say, an inductive predicate. Instead it relies on type parameters, i.e.
on dependent types, in the meta–language. The technique and its benefits are
discussed in [BHKM11].
1.3   Related Work
The theorem we present was first proved in Zsidó’s PhD thesis [Zsi10]. It is a
generalization of the work by Hirschowitz and Maggesi on untyped syntax [HM10a]
based on the notion of monads and modules over monads. Monads were identified
by Altenkirch and Reus [AR99] as a convenient categorical device to talk about
substitution.
   Initial semantics. For untyped first-order syntax the notion of initial algebra was
coined by Goguen et al. [GTWW77] in the 1970s.
   Initial semantics has then been extended to account for additional features, as
illustrated by the following scheme:




                                            Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
32     ·     B. Ahrens and J. Zsidó



                        binding                        / binding + types


                                                               
               binding + reductions              / binding + types + reduction

   Another criterion to classify initiality results is the way in which variable binding
is modeled. Frequently used for representing binding are the following techniques:
(1) Nominal syntax using named abstraction ,
(2) Higher–Order Abstract Syntax (HOAS), e.g. lam : (T → T ) → T and its weak
    variant, e.g. lam : (var → T ) → T and
(3) Nested Datatypes as introduced in [BM98] .
Initial semantics for untyped syntax were presented by Gabbay and Pitts [GP99,
(1)] , Hofmann [Hof99, (2)] and Fiore et al. [FPT99, (3)]. The numbers given in
parentheses correspond to the way variable binding is modeled, according to the
list given above. Hirschowitz and Maggesi [HM07, (3)] prove an initiality result for
arbitrary untyped syntax based on the notion of monads.
   The extension to simply–typed syntax was done, for the HOAS approach, by
Miculan and Scagnetto [MS03, (2)].
   Fiore et al.’s approach was generalized to encompass the simply–typed lambda
calulus in [Fio02], and detailed for general simply–typed syntax in Zsidó’s PhD
thesis [Zsi10].
   There, she also generalized Hirschowitz and Maggesi’s approach [HM07] to simply–
typed syntax. It is this result and its formalization in Coq that the present article
is about.
   Both lines of work, Hirschowitz and Maggesi’s and Fiore et al.’s, are deeply
connected. Zsidó [Zsi10] made this connection precise, by establishing an adjunction
between the resp. categories under consideration.
   Semantic aspects were integrated in initiality results by several people.
   Hirschowitz and Maggesi [HM07] characterize the terms of the lambda calculus
modulo beta and eta reduction as an initial object in some category.
   Another idea mentioned in [HM07] is to consider not sets of terms, quotiented by
reduction relations, but sets equipped with a preorder. This idea is being pursued
by the first author.
   Fiore and Hur [FH07] extended Fiore et al.’s approach to “second–order universal
algebras”. In particular, Hur’s PhD thesis [Hur10] is dedicated to this extension.
   While the present paper does not treat semantic aspects, one of the goals is to set
up and formalize the techniques which will be necessary for understanding semantic
aspects in the simply typed case.
   Implementation of syntax. The implementation and formalization of syntax has
been studied by a variety of people. The PoplMark challenge [ABF+ 05] is a
benchmark which aims to evaluate readability and provability when using different
techniques of variable binding. The technique we use, called Nested Abstract Syntax,
is used in a partial solution by Hirschowitz and Maggesi [HM10b], but was proposed

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                     Initial Semantics in Coq       ·     33

earlier by others, e. g. [BM98, AR99]. The use of intrinsic typing by dependent
types of the meta–language was advertised in [BHKM11].
  During our work we became aware of Capretta and Felty’s framework for reason-
ing about programming languages [CF09]. They implement a tool — also in the
Coq proof assistant — which, given a signature, provides the associated abstract
syntax as a data type dependent on the object types, hence intrinsically typed
as well. Their data type of terms does not, however, depend on the set of free
variables of those terms. Variables are encoded with de Brujin indices. There are
two different constructors for free and bound variables which serve to control the
binding behaviour of object level constructors. In our theorem, there is only one
constructor for (free) variables, and binding a variable is done by removing it from
the set of free variables.
  Capretta and Felty then add a layer to translate those terms into syntax using
named abstraction, and provide suitable induction and recursion principles. Their
tool may hence serve as a practical framework for reasoning about programming
languages. Our implementation remains on the theoretical side by not providing
named syntax and exhibiting the category–theoretic properties of abstract syntax.
Synopsis
In the second section we give a very brief description of Coq, the theorem prover
we use for the formalization. Afterwards we explain how we deal with the problem
of formalizing algebraic structures.
The third section presents categorical concepts and their formalization. We state
the definition of category, initial object of a category, monad (as Kleisli structure)
and module over a monad as well as their resp. morphisms. Some constructions on
monads and modules are explained, which will be of importance in what follows.
The fourth section introduces the notions of arity, signature and representations of
signatures in suitable monads. The category of representations of a given signature
is defined. The main theorem 4.13 states that this category has an initial object.
In the fifth part the formal construction of said initial object is explained.
Some conclusions and future work are stated in the last section.

2.    PRELIMINARIES
2.1   About the proof assistant Coq
The proof assistant Coq [Coq] is an implementation of the Calculus of Inductive
Constructions (CIC) which itself is a constructive type theory. Bertot and Cast-
eran’s book Coq’Art [BC04] gives a comprehensive introduction to Coq. The Coq
web page [Coq] carries links to more howtos and specialised tutorials. In Coq a
typing judgment is written t : T, meaning that t is a term of type T . Function
application is simply denoted by a blank, i.e. we write f x for f (x).
  The CIC also treats propositions as types via the Curry–Howard isomorphism,
hence a proof of a proposition P is in fact a term of type P . In the proof assistant
Coq a user hence proves a proposition P by providing a term p of type P. Coq
checks the validity of the proof p by verifying whether p : P.
  Coq comes with extensive support to interactively build the proof terms of a given
proposition. In proof mode so-called tactics help the user to reduce the proposition

                                         Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
34     ·     B. Ahrens and J. Zsidó

they want to prove – the goal – into one or more simpler subgoals, until reaching
trivial subgoals which can be solved directly.
   Particular concepts of Coq such as records and type classes, setoids, implicit
arguments and coercions are explained in a call-by-need fashion in the course of
the paper. One important feature is the Section mechanism (cf. also the Coq man-
ual [The10]). Parameters and hypotheses declared in a section automatically get
discharged when closing the section. Constants of the section then become func-
tions, depending on an argument of the type of the parameter they mentioned.
When necessary, we will either give a slightly modified, fully discharged version of
a statement, or mention the section parameters in the text.
2.2   How to formalize algebraic structures
The question of how to formalize algebraic structures is a subject of active research.
We do not attempt to give an answer of any kind here. However, we need to choose
from the existing solutions.
   In Coq there are basically two possible answers: type classes [SO08], as used
by Spitters and v. d. Weegen [SvdW11] and records, employed e.g. by Garillot et
al. [GGMR09].
   Coq records are implemented as an inductive data type with one constructor,
However, use of the vernacular command Record (instead of plain Inductive) allows
the optional automatic definition of the projection functions to the constructor ar-
guments – the “fields” of the record. Additionally, one can declare those projections
as coercions, i.e. they can be inserted automatically by Coq, and left out in print-
ing. As an example for a coercion, it allows us to write c : C for an object c of a
category C. Here the projection from the category type to the type of objects of a
category is declared as a coercion (cf. Listing 1). This is the formal counterpart to
the convention introduced in the informal definition of categories in Def. 3.1. An-
other example of coercion is given in the definition of monad (cf. Def. 3.9), where
it corresponds precisely to the there–mentioned abuse of notation.
   Type classes are implemented as records. Similarly to the difference between
records and inductive types, type classes are distinguished from records — from a
technical point of view — only in that some meta–theoretic features are automati-
cally enabled when declaring an algebraic structure as a class rather than a record.
For details we refer to Sozeau’s article about the implementation of type classes
[SO08] and Spitters and v. d. Weegen’s work [SvdW11].
   Type classes differ from records in their usage, more specifically, in which data
one declares as a parameter of the structure and which one declares as a field. The
following example, borrowed from [SvdW11], illustrates the different uses; we give
two definitions of the algebraic structure of reflexive relation, one in terms of classes
and one in terms of records:
Class Reflexive {A : Type}{R : relation A} :=
   reflexive : forall a, R a a.

Record Reflexive := {
  carrier : Type ;
  car rel : relation carrier ;

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                         Initial Semantics in Coq       ·     35

  rel refl : forall a, car rel a a }.
   Our main interest in classes comes from the fact that by using classes many of the
arguments of projections are automatically declared as implicit arguments. This
leads to easily readable code in that superfluous arguments which can be deduced
by Coq do not have to be written down. Thus it corresponds precisely to the
mathematical practice of not mentioning arguments (e.g. indices) which “are clear
from the context”. In particular, the structure argument of the projection, that is,
the argument specifying the instance whose field we want to access, is implicit and
deduced automatically by Coq. This mechanism allows for overloading, a prime
example being the implementation of setoids (cf. Sec. 3.1.3) as a type class; in
a term “a == b” denoting setoidal equality, Coq automatically finds the correct
setoid instance from the type of a and b 5 .
   We decide to define our algebraic structures in terms of type classes first, and
bundle the class together with some of the class parameters in a record afterwards.
as is shown in the following example for the type class Cat struct (cf. Listing 3) and
the bundling record Cat.
Record Cat := {
     obj :> Type ;
     mor : obj −> obj −> Type ;
     cat struct :> Cat struct mor }.

                     Listing 1.    Bundling a type class into a record
In this code snippet the projections obj and cat struct are defined as coercions, as
explained at the beginning of this subsection, by using the notation “:>” rather
than just a colon.
   The duplication of Coq definitions as classes and records is a burden rather than
a feature. We still proceed like this for the following reasons:
   In our case the use of records is unavoidable since we want to have a Coq type
of categories, of functors between two given categories etc. This is necessary when
categories, functors, etc. shall themselves be the objects or morphisms of some
category, as will be clear from Listing 3. However, we profit from aforementioned
features of type classes, notably automatic declaration of some arguments as implicit
and the resulting overloading.
   Apart from that, we do not employ any feature that makes the use of type
classes comfortable — such as maximally inserted arguments, operational classes,
etc. — since we usually work with the bundled versions. Readers who want to
know how to use type classes in Coq properly, should take a look at Spitters and
v. d. Weegen’s paper [SvdW11]. They also employ the mentioned bundling of type
classes in records whenever they need to build a category of algebraic structures. In
the following we will only present the type class definition of each defined object.

5 Beware! In case several instances of setoid have been declared on one and the same Coq type,

the instance chosen by Coq might not be the one intended by the user. This is the main reason
for Spitters and v. d. Weegen to restrict the fields of type classes to propositions.



                                             Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
36      ·     B. Ahrens and J. Zsidó

3.     CATEGORIES, MONADS & MODULES
Mac Lane’s book [ML98] may serve as a reference for the following definitions,
unless stated otherwise. Note that we write “f ; g” for the composite of morphisms
f : a → b and g : b → c in any category, instead of g ◦ f .
3.1     Categories
     Definition 3.1. A category C is given by
—a collection – which we will also call C – of objects,
—for any two objects c and d of C, a collection of morphisms, written C(c, d),
—for any object c of C, a morphism idc in C(c, c) and
—for any three objects c, d, e of C a composition operation
                              ( ; )c,d,e : C(c, d) × C(d, e) → C(c, e)
such that the composition is associative and the morphisms of the form idc for
suitable objects c are left and right neutral w.r.t. this composition 6 :
            ∀a b c d : C, ∀f : C(a, b), g : C(b, c), h : C(d, e), f ; (g; h) = (f ; g); h
            ∀c d : C, ∀f : C(c, d), f ; idd = f and idc ; f = f .
We write f : c → d for a morphism f of C(c, d).
  Example 3.2. The category Set is the category of sets and, as morphisms from
set A to set B, the collection of total maps from A to B, together with the usual
composition of maps.
  Definition 3.3. Let T be a set. We denote by [T, Set] the category whose objects
are collections of sets indexed by T . We also refer to such collections as type families
indexed by T , since this is how we chose to implement them (cf. Sec. 3.1.4). Given
a type family V and t ∈ T we set Vt := V (t). A morphism f : V → W between
two type families V and W is a family of maps indexed by T ,
                                f : t 7→ ft := f (t) : Vt → Wt .
     Remark 3.4. Equivalently to Def. 3.1, a category C is given by
—a collection C0 of objects and a collection C1 of morphisms,
—two maps
                                          src, tgt : C1 → C0
—a partially defined composition function
                                        ( ; ) : C1 × C1 → C1 ,
     such that f ; g is defined only for composable morphisms f and g, i.e. if tgt(f ) =
     src(g). In this case we require that src(f ; g) = src(f ) and tgt(f ; g) = tgt(g),

6 We  omit the “object” parameters from the composition operation, since those are deducible from
the morphisms we compose. This omission is done in our library as well, via implicit arguments
(cf. Sec. 2.2).


Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                      Initial Semantics in Coq       ·     37

—identity morphisms and properties analoguous to those of the preceding defini-
 tion. The associative law, e.g., reads as
       ∀f g h : C1 , tgt(f ) = src(g) =⇒ tgt(g) = src(h) =⇒ f ; (g; h) = (f ; g); h
   3.1.1 Which Definition to Formalize – Dependent Hom–Types?. The main dif-
ference w.r.t. formalization between these two definitions is that of composability of
morphisms. The first definition can be implemented directly only in type theories
featuring dependent types, such as the Calculus of Inductive Constructions (CIC).
The ambient type system, i.e. the prover, then takes care of composability – terms
with compositions of non–composable morphisms are rejected as ill–typed terms.
   The second definition can be implemented also in provers with a simpler type
system such as the family of HOL theorem provers. However, since those (as well as
the CIC) are theories where functions are total, one is left with the question of how
to implement composition. Composition might then be implemented either as a
functional relation or as a total function about which nothing is known (deducible)
on non–composable morphisms. The second possibility is implemented in O’Keefe’s
development [O’K04]. There the author also gives an overview over available for-
malizations in different theorem provers with particular attention to the choice of
the definition of category.
   In our favourite prover Coq, both definitions have been employed in significant de-
velopments: the second definition is used in Simpson’s construction of the Gabriel–
Zisman localization [Sim06], whereas Huet and Saı̈bi’s ConCaT [HS00] uses type
families of morphisms as in the first definition. To our knowledge there is no li-
brary in a prover with dependent types such as Coq or NuPrl [CAA+ 86] which
develops and compares both definitions w.r.t. provability, readability etc.
   We decided to construct our library using type families of morphisms. In this
way the proof of composability of two morphisms is done by Coq type computation
automatically.
   Coq’s implicit argument mechanism allows us to omit the deducible arguments,
as we do in Def. 3.1 for the “object arguments” c, d and e of the composition.
Together with the possibility to define infix notations this brings our formal syntax
close to informal mathematical syntax.
   3.1.2 Setoidal Equality on Morphisms. All the properties of a category C con-
cern equality of two parallel morphisms, i.e. morphisms with same source and
target. In Coq there is a polymorphic equality, called Leibniz equality, readily avail-
able for any type. However, this equality actually denotes syntactic equality, which
already in the case of maps does not coincide with the “mathematical” equality on
maps – given by pointwise equality – that we would rather consider. With the use
of axioms – for the mentioned example of maps the axiom functional extensionality
from the Coq standard library – one can often deduce Leibniz equality from the
“mathematical equality” in question. But this easily gets cumbersome, in particular
when the morphisms – as will be in our case – are sophisticated algebraic struc-
tures composed of a lot of data and properties. Instead, we require any collection
of morphisms C(c, d) for objects c and d of C to be equipped with an equivalence
relation, which plays the rôle of equality on this collection. In the Coq standard
library equivalence relations are implemented as a type class with the underlying

                                          Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
38     ·      B. Ahrens and J. Zsidó

type as a parameter A, and the relation as well as a proof of it being an equivalence
as fields:
Class Setoid A := {
  equiv : relation A ;
  setoid equiv :> Equivalence equiv }.

                                 Listing 2.     Setoid type class
   Setoids as morphisms of a category have been used by Aczel [Acz93] in LEGO
(there a setoid is simply called “set”) and Huet and Saı̈bi (HS) [HS00] in Coq. HS’s
setoids are implemented as records of which the underlying type is a component
instead of a parameter. This choice makes it necessary to duplicate the definitions
of setoids and categories in order to make them available with a “higher” type 7 .
   3.1.3 Coq Setoids and their morphisms. Setoids in Coq are implemented as a
type class (cf. Listing 2) with a type parameter A and a relation on A as well as
a proof of this relation being an equivalence as fields. For the term equiv a b the
infix notation “a == b” is introduced. The instance argument of equiv is implicit
(cf. Sec. 2.2).
   A morphism of setoids between setoids A and B is a Coq function, say f, on the
underlying types which is compatible with the setoid relations on the source and
target. That is, it maps equivalent terms of A to equivalent terms of B, or, in
mathematical notation,
                                a ≡A a0 =⇒ f (a) ≡B f (a0 ) .                                    (3.1)
In the Coq standard library such morphisms are implemented as a type class
Class Proper {A} (R : relation A) (m : A) : Prop :=
  proper prf : R m m.
where the type A is instantiated with a function type A −> B and the relation R
on A −> B is instantiated with pointwise compatibility 8 :
Definition respectful {A B : Type} (R : relation A) (R’ : relation B) :
            relation (A −> B) :=
 fun f g => forall x y, R x y −> R’ (f x) (g y).
Notation ” R ==> R’ ” := (@respectful           (R%signature) (R’%signature))
    (right associativity, at level 55) : signature scope.
Given Coq types A and B equipped with relations R : relation A and R’ : relation
B, resp., and a map f : A −> B, the statement Proper (R ==> R’)f — replacing
aforementioned notation — really means
Proper (respectful R R’) f ,

7 InHS’s ConCaT, a type T which is defined after the type of setoids cannot be the carrier of a
setoid itself. What is done in HS’s library is to define a type Setoid’ isomorphic to Setoid after the
definition of T. The type of Setoid’ now being higher than that of T, one can define an element
of this type whose carrier is T.
8 In the Coq standard library the definition of respectful is actually a special case of a more general

definition of a heterogeneous relation respectful hetero.
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                           Initial Semantics in Coq       ·     39

which is the same as respectful R R’ f f, which itself just means
forall x y, R x y −> R’ (f x) (f y) .
This is indeed the statement of Display (3.1) in the special case that R and R’ are
equivalence relations.
   For any component of an algebraic structure that is a map defined on setoids, we
add a condition of the form Proper... in the formalization. Examples are the cate-
gorical composition (Lst. 3) and the monadic substitution map (Lst. 4). Rewriting
related terms under those equivalence relations is tightly integrated in the rewrite
tactic of Coq.
   3.1.4 Coq implementation of categories. Finally we adopt Sozeau’s definition
of category [SO08], which itself is a type class version of the definition given by
Huet and Saı̈bi [HS00]. The type class of categories is parametrized by a type
of objects and a type family of morphisms, whose parameters are the source and
target objects.
Class Cat struct (obj : Type)(mor : obj −> obj −> Type) := {
  mor oid :> forall a b, Setoid (mor a b) ;
  id : forall a, mor a a ;
  comp : forall {a b c}, mor a b −> mor b c −> mor a c ;
  comp oid :> forall a b c, Proper (equiv ==> equiv ==> equiv) (@comp a b c) ;
  id r : forall a b (f: mor a b), comp f (id b) == f ;
  id l : forall a b (f: mor a b), comp (id a) f == f ;
  assoc : forall a b c d (f: mor a b) (g:mor b c) (h: mor c d),
       comp (comp f g) h == comp f (comp g h) }.

                            Listing 3.   Type class of categories
Compared to the informal definition 3.1 there are two additional fields: the field
mor oid of type forall a b, Setoid (mor a b) equips each collection of morphisms mor
 a b with a custom equivalence relation. The field comp oid states that the com-
position comp of the category is compatible with the setoidal structure on the
morphisms given by the field mor oid as explained in Sec. 3.1.3. We recall that
setoidal equality is overloaded and denoted by the infix symbol ‘==’. In the fol-
lowing we write ‘a −−−> b’ for mor a b and f;;g for the composition of morphisms
f : a −−−> b and g : b −−−> c 9 .
   The implementation of the category [T, Set] of Def. 3.3 uses Coq types as sets:
(the properties being proved automatically by a suitable tactic invoked by the
Program framework, cf. Subsec. 3.1.5):
Program Instance ITYPE struct : Cat struct (obj := T −> Type)
          (fun A B => forall t, A t −> B t) := {
  mor oid := INDEXED TYPE oid ; (* pointwise equality in each component of the
        family of maps *)

9 Coq  deduces and inserts the missing “object” arguments a, b and c of the composition automat-
ically from the type of the morphisms. For this reason those object arguments are called implicit
(cf. Sec. 2.2).

                                               Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
40     ·     B. Ahrens and J. Zsidó

  comp A B C f g := fun t => fun x => g t (f t x) ;
  id A := fun t x => x }.
The objects of this category are hence implemented as families of Coq types, indexed
by a fixed Coq type T. Morphisms between two such objects are suitable families
of Coq functions.
   3.1.5 Interlude on the Program feature. The Program Instance vernacular allows
to fill in fields of an instance of a type class by means of tactics. Indeed, when
omitting a field in an instance declaration — such as the proofs of associativity
assoc and left and right identity id l and id r in the instance ITYPE struct in the
previous listing — the Program framework creates an obligation for each missing
field, making use of the information that the user provided for the other fields. As
an example, the obligation created for the field assoc of the previous example is to
prove associativity for the composition defined by
comp f g := fun t => fun x => g t (f t x) .
It then tries to solve the resulting obligations using the tactic that the user has
specified via the Obligation Tactic command. In case the automatic resolution of
the obligation fails, the user can enter the interactive proof mode finish the proof
manually.
   It is technically possible to fill in both data and proof fields automatically via
the Program framework. However, in order to avoid the automatic inference of data
which we cannot control, we always specify data directly as is done in the case of
ITYPE struct, and rely on automation via Program only for proofs.
3.2   Invertible morphisms, Initial objects
Given a category C, a morphism f : c → d from object c to object d is called
invertible, if there exists a left– and right–inverse g : d → c, that is, a morphism
g : d → c such that f ; g = idc and g; f = idd . In this case the objects c and d are
called isomorphic.
   An initial object of a category is an object for which there is precisely one mor-
phism to any object of the category:
   Definition 3.5. Let C be a category, and c ∈ C an object of C. The object c is
called initial if for any object d ∈ C there exists a unique morphism id : c → d from
c to d in C.
   Remark 3.6. It is easy to see that any two initial objects of a category C are
isomorphic via a unique isomorphism. This justifies the use of the definite article,
i.e. speaking about “the” initial object of a category — if it exists.
Formally, we implement the initiality structure as a type class which inherits from
the class of categories. Its fields are given by an object Init of the category, a map
InitMor mapping each object a of the category to a morphism from Init to a and a
proposition stating that InitMor a is unique for any object a.
Variable ob : Type.
Variable mor : ob −> ob −> Type.
Class Initial (C : Cat struct mor) := {
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                         Initial Semantics in Coq      ·     41

  Init : ob;
  InitMor: forall a : ob, mor Init a;
  InitMorUnique: forall a (f : mor Init a), f == InitMor a }.
Note that the initial morphism is not given by an existential statement of the form
∀a, ∃f : . . ., or, in Coq terms, using an exists statement. This is because the Coq
existential lies in Prop and hence does not allow for elimination – witness extraction
– when building anything but proofs.
3.3   Functors & Natural Transformations
Given two categories C and D, a functor F : C → D maps objects of C to objects
of D, and morphisms of C to morphisms of D, while preserving source and target:
  Definition 3.7. A functor F from C to D is given by
—a map F : C → D on the objects of the categories involved and
—for any pair of objects (c, d) of C, a map
                             F(c,d) : C(c, d) → D(F c, F d) ,
such that
—∀c : C, F (idc ) = idF c and
—∀c d e : C, ∀f : c → d, ∀g : d → e, F (f ; g) = F f ; F g.
Here we use the same notation for the map on objects and that on morphisms. For
the latter we also omit the subscript “(c, d)” as instances of implicit arguments.
For its implementation we refer to the Coq source files.
   Definition 3.8. Let F, G : C → D be two functors from C to D. A natural
transformation τ : F → G associates to any object c ∈ C a morphism
                                     τc : F c → Gc
such that for any morphism f : c → d in C the following diagram commutes:

                                     Fc
                                            τc
                                                 / Gc

                                   Ff               Gf
                                                   
                                     Fd          / Gd
                                            τd

3.4   Monads, modules and their morphisms
Monads have long been known to capture the notion of substitution, cf. [AR99].
The closely connected notion of module over a monad was recently introduced in
the context of abstract syntax by Hirschowitz and Maggesi [HM07]. Similarly to
the two equivalent definitions of monads as presented by Manes [Man76] there are
two equivalent definitions of modules over a monad. Contrary to the given reference
[HM07] we use the definition of monad as a Kleisli triple, since this definition is
well–known for its use in the functional programming language Haskell and hence
accessible to a relatively wide audience.
  Definition 3.9. A monad P over a category C is given by
                                            Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
42     ·        B. Ahrens and J. Zsidó

—a map P : C → C on the objects of C (by abuse of notation it carries the same
 name as the monad),
—for each object c of C, a morphism ηc ∈ C(c, P c) and
—for all objects c and d of C a substitution map
                                     σc,d : C(c, P d) → C(P c, P d)
such that the following diagrams commute for all suitable morphisms f and g:
                                                                                 σ (f )
           c@
                  ηc
                       / Pc            Pc                                PcB             / Pd
             @@                                                                 BB
               @@                                   σ (ηc )
                                                                                  BB
                  @@                                                                BB
                    @@                                                                B
                                                                         σ (f ;σ (g)) BB
                            σ (f )                                                             σ (g)
                f     @@                                                                BB
                                           id                                            ! 
                        P d,                           * P c,
                                                                                           P e.
We omit the subscripts of the substitution map as done in the diagrams.
   Example Lists. Consider the map [ ] : Set → Set mapping any set X to the set
list(X) of lists over X, together with the following maps:
Definition eta (X : Type) (x : X) := x::nil. (* the singleton list *)

Fixpoint sigma X Y (f : X −> list Y) (l : list X) :=
     match l with nil => nil | x::l’ => app (f x) (sigma f l’) end. (* app = append *)
This defines a monad structure on lists, the axioms are easily verified.
  Example 3.11. Let R be a commutative ring. To any set X we associate the set
R(X) of polynomials with variables in X and coefficients in R:
                                          R : X 7→ R(X) .
We equip the map R with a monad structure by defining the unit η as
                           ηX : x 7→ x (considered as a polynomial) .
The monad substitution is best defined using two auxiliary functions:
  firstly, for f : X → Y , we set
              R(f ) : R(X) → R(Y ) ,        p(x1 , . . . , xn ) 7→ p(f (x1 ), . . . , f (xn )) ,
yielding a functor with object map X 7→ R(X).
  Secondly, for any set X, we define a multiplication
                                     µX : R(R(X)) → R(X)
                                                                                
which, given a polynomial p p1 (x1 , . . . , xn ), . . . , pm (x1 , . . . , xn ) with polynomials
as variables, allows to consider it as a polynomial p(x1 , . . . , xn ) after expansion.
Here we can suppose all polynomials pi to have variables in the same finite set
{x1 , . . . , xn }. The substitution map is then defined using those auxiliary maps:
      σX,Y : (X → R(Y )) → R(X) → R(Y ) ,                       σX,Y (f )(x) := R(f ); µY .            (3.2)
Later (cf. Def. 3.19) we define the notion of module over a monad. In Ex. 3.20 we
show how any module over R in the classical sense gives rise to a module over R
in the sense of Def. 3.19.
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                     Initial Semantics in Coq       ·     43

   Remark 3.12. The preceding example actually illustrates a use of the aforemen-
tioned equivalent definition of monad as a triple (T, η, µ) where T is an endofunctor
on a category C and η : Id → T and µ : T T → T are natural transformations verify-
ing some properties. Display (3.2) indicates how to define the monad substitution
σ from monad multiplication µ. We refer to [Man76] for details.
  Remark 3.13. Let A be an algebra over the ring R of Ex. 3.11. Then A is an R–
algebra (we refer to [ML98] for the definition): the map α : R(A) → A is induced
by the module operation φ : R × A → A and the bilinear product on A. The
commutation properties of the following diagrams is a consequence of the rules the
module operation φ verifies.

                    R(R(A))
                               Rα     / R(A)        AD
                                                          ηA
                                                            / R(A)
                                                      DD
                                                        DD
                     µR                   α               DD       α
                      A
                                                       id    DD
                                                             ! 
                     R(A)               /A                      A
                                α

  Example 3.14. (Ex. 1.1 cont.) This example is due to Altenkirch and Reus
[AR99]. We consider the map LC associating to any set X the set of untyped
lambda terms with free variables in X. Given any set X, the constructor Var(X) :
X → LC(X) maps a variable to itself, this time seen as a lambda term. The
substitution map is defined recursively, using a helper function shift when going
under the binding constructor Abs:
Fixpoint subst V W (f : V −> LC W) (y : LC V) : LC W :=
  match y in LC return LC W with
  | Var v => f v
  | Abs v => Abs (subst (shift f) v)
  | App s t => App (subst f s) (subst f t)
  end.
The function shift is of type shiftV,W : (V → LC(W )) → V ∗ → LC(W ∗ ), sending
the additional variable of V ∗ to Var(∗W ). These definitions yield a monad LC with
η := Var and µ := subst.
  Example 3.15. Consider the simply–typed lambda calculus as in Ex. 1.2. Defi-
nitions similar to those of Ex. 3.14, but additionally indexed by object types of T ,
turn TLC into a monad on the category [T , Set]. The definition of the substitution
map σ reads as follows:
Fixpoint subst (V W : IT) (f : V −−−> TLC W) t (y : TLC V t) : TLC W t :=
  match y with
  | Var v => f v
  | Abs    v => Abs (subst (shift f) v)
  | App     u v => App (subst f u) (subst f v)
  end.
where the object type arguments are partially implicit and otherwise denoted by
the underscore “ ” in the pattern matching branches. The shift map is – similarly
to the preceding, untyped example – necessary to adapt the substitution map f to
the enlarged domain and codomain under binders (cf. Sec. 3.7).
                                         Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
44     ·     B. Ahrens and J. Zsidó

   Example 3.16. For any set X, let X ∗ := X q {∗}. Given any monad P on the
category of sets, the map P ∗ : X 7→ P (X ∗ ) inherits a monad structure from P . In
detail, a monadic substitution for P ∗ is defined, for a morphism f : X → P ∗ (Y ),
as
                                 ∗
                              σ P (f ) := σ P (default(f, ηY ∗ (∗))) .
The map
                               default(f, ηY ∗ (∗)) : X ∗ → P ∗ (Y )
sends the additional variable ∗ to η(∗).
Given a monad P over C and a morphism f : c → d in C, we define
                                 P (f ) := liftP (f ) := σ(f ; ηd ) ,
thus equipping P with a functorial structure (lift). In case P is a syntax, e.g.
the monad LC of Ex. 3.14, the lift operation corresponds to variable renaming
according to the map f . Note that f is not necessarily bijective, and hence P (f )
not necessarily a permutation of variables.
  The formal definition of monad is almost a literal translation of Def. 3.9. The
only difference is an additional field kleisli oid stating that the substitution map is
a map of setoids (cf. Sec. 3.1.3):
Class Monad struct (C : Cat) (F : C −> C) := {
  weta : forall c, c −−−> F c ;
  kleisli : forall a b, (a −−−> F b) −> (F a −−−> F b) ;
  kleisli oid :> forall a b, Proper (equiv ==> equiv) (kleisli (a:=a) (b:=b)) ;
  eta kl : forall a b (f : a −−−> F b), weta a ;; kleisli f == f ;
  kl eta : forall a, kleisli (weta a) == id ;
  dist : forall a b c (f : a −−−> F b) (g : b −−−> F c),
       kleisli f ;; kleisli g == kleisli (f ;; kleisli g) }.

                               Listing 4.         Type class of monads
As in the informal Def. 3.9 the “object” arguments of the substitution map kleisli
are implicit.
  For two monads P and Q over the same category C a morphism of monads is a
family of morphisms τc ∈ C(P c, Qc) that is compatible with the monadic structure:
   Definition 3.17. A morphism of monads (Monad Hom) from P to Q is given by
a collection of morphisms τc ∈ C(P c, Qc) such that the following diagrams commute
for any morphism f : c → P d:
                                 σ P (f )                         ηcP
                          Pc                   / Pd         c@          / Pc
                                                              @@
                                                                @@
                                                                   @@
                         τc                       τd                 @@      τc
                                                               ηcQ     @@
                                                                         
                          Qc                   / Qd,                      Qc.
                                σ Q (f ;τd )



Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                        Initial Semantics in Coq     ·     45

Two monad morphisms are said to be equal if they are equal on each object.
  The formal definition is a straightforward transcription, even if the diagrams do
not read as nicely there:
Class Monad Hom struct (Tau: forall c, P c −−−> Q c) := {
  monad hom kl: forall c d (f: c −−−> P d),
      kleisli f ;; Tau d == Tau c ;; kleisli (f ;; Tau d) ;
  monad hom weta: forall c: C, weta c ;; Tau c == weta c }.
Observe that some arguments are inferred by Coq, such as to which monad the
respective kleisli and weta operations belong.
   It follows from these commutativity properties that the family τ is a natural
transformation between the functors induced by the monads P and Q. Monads
over C and their morphisms form a category MONAD C where identity and compo-
sition of morphisms are simply defined by pointwise identity resp. composition of
morphisms:
Variables P Q R : Monad C.
Variable S : Monad Hom P Q.
Variable T : Monad Hom Q R.
Instance Monad Hom comp struct : Monad Hom struct (fun c => S c ;; T c).
Instance Monad Hom id struct : Monad Hom struct (fun c => id (P c)).

           Listing 5.   Composition and identity for monad morphisms
  We illustrate the concept of monad morphism by showing how abstraction fails
to be such a morphism. The map V 7→ LC(V ) is object function of a monad, as is
the map LC∗ : V 7→ LC(V ∗ ) (cf. Ex. 3.16). However, the constructor Abs, while
having the suitable type, is not a morphism of monads from LC∗ to LC; it does not
verify the square diagram of Def. 3.17:
  Example 3.18. The following diagram fails to commute for the map
                                   f : a 7→ Var(∗) ;
the term Var(a) ∈ LC({a}) maps to λx.x when taking the upper route, while
mapping to λxy.y when taking the lower route:
                                              ∗
                                          σ LC (f )
              Var(a) ∈ LC∗ ({a})                           / LC∗ (∅)                     (3.3)
                                                              AbsY
                                                             
                         Abs{a}                             LC∗ (∅) 3 λx.x

                               
                         LC({a})                           / LC(∅) 3 λxy.y
                                         σ (f ;AbsY )

This is due to the additional abstraction appearing through the lower vertical sub-
stitution morphism.
   Instead, we will equip the constructor Abs with the structure of a module mor-
phism (Def. 3.24), cf. Exs. 3.21, 3.22 and 3.25. Module morphisms verify a diagram
                                          Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
46      ·    B. Ahrens and J. Zsidó

similar to the square diagram of monad morphisms, with the difference that the
underlying natural transformation (here Abs) does not appear in the lower vertical
substitution.
   The preceding example for the constructor Abs shows the need for a concept that
is more general than that of monads and monad morphisms, while still expressing
compatibility of the underlying natural transformation with substitution.
   For this reason, we consider modules over monads, which generalize the notion
of monadic substitution, and module morphisms:
  Definition 3.19. Let D be a category. A module M over P with codomain D is
given by
—a map M : C → D on the objects of the categories involved and
—for all objects c, d of C a map
                                    ςc,d : C(c, P d) → C(M c, M d)
such that the following diagrams commute for all suitable morphisms f and g:
                                ς (f )
                       M cD             / Md           Mc
                             DD
                                DD                                   ς (ηc )
                                  DD
                                    D
                       ς (f ;σ (g)) DDD
                                            ς (g)
                                       D! 
                                                                        * 
                                                            id
                                          M e,                           M c.
A functoriality for such a module M is then defined similarly to that for monads
(mlift):
                              M (f ) := mliftM (f ) := ς (f ; η P ) .
  Example 3.20. (Ex. 3.11 cont.) Let R be a commutative ring. For any set X,
R(X) is a module over R in the classical, algebraic sense. Let M be any module
over R. We define a map
                             M : X 7→ M (X) := M ⊗R R(X) ,
where ⊗R denotes the tensor product of modules. We omit the index R of the
tensor product. This map is the object function of a module (in the sense of Def.
3.19) over the monad R (cf. Ex. 3.11). The module substitution is defined using
the fact that the tensor product is functorial in the second argument:
       ςX,Y : (X → R(Y )) → M ⊗ R(X) → M ⊗ R(Y ) ,                    f 7→ M ⊗ σX,Y (f ) .
     The implementation of modules resembles that of monads:
Class Module struct (M : C −> D) := {
  mkleisli: forall c d, (c −−−> P d) −> (M c −−−> M d);
  mkleisli oid :> forall c d,
      Proper (equiv ==> equiv) (mkleisli (c:=c)(d:=d));
  mkl weta: forall c, mkleisli (weta c) == id ;
  mkl mkl: forall c d e (f : c −−−> P d) (g : d −−−> P e),
      mkleisli f ;; mkleisli g == mkleisli (f ;; kleisli g) }.
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                          Initial Semantics in Coq   ·     47

 We anticipate several constructions on modules to give some further examples of
modules:
  Example 3.21. (Ex. 3.14 cont.) Any monad P on a category C can be considered
as a module over itself, the tautological module (cf. Sec. 3.5). In particular, the
untyped lambda calculus LC is a LC–module with codomain Set.
  Example 3.22. The map
                               LC∗ : V 7→ LC(V ∗ )
can be equipped with a structure as LC–module, the derived module of (the module)
LC (cf. Sec. 3.7). Also, the map
                         LC × LC : V 7→ LC(V ) × LC(V )
can be equipped with a structure as LC–module.
  Example 3.23. Consider the monad TLC : [T , Set] → [T , Set] of Ex. 3.15. Given
any object type t ∈ T , the map
                              TLCt : V 7→ TLC(V )t                                       (3.4)
can be equipped with the structure of a module over TLC with codomain category
Set (cf. Sec. 3.6). Similarly, for s ∈ T , the map
                             TLCs : V 7→ TLC(V ∗s )
can be equipped with a module structure over the monad TLC (cf. Sec. 3.7).
  Those two operations, fibre and derivation, can be combined, yielding a module
over TLC with carrier
                         V 7→ TLCst (V ) := TLC(V ∗s )t .
  The final example is that of products: the map
                 TLCs⇒t × TLCs : V 7→ TLC(V )s⇒t × TLC(V )s
can be equipped with the structure of a module (cf. Sec. 3.5).
   Those three constructions are our main examples of modules. From the last ex-
ample the reader may have guessed that we will consider the domain and codomain
of some constructor to be given as modules: here the domain of (an uncurried ver-
sion of) the constructor Apps,t (cf. Ex. 1.2) of the simply–typed lambda calculus
is a module over TLC with codomain Set. The constructors themselves then are
morphisms of modules:
  Definition 3.24. Let M and N be two modules over P with codomain D. A
morphism of P –modules from M to N is given by a collection of morphisms
ρc ∈ D(M c, N c) such that for any morphism f ∈ C(c, P d) the following diagram
commutes:
                                      ς M (f )
                                 Mc              / Md

                                ρc                   ρd

                                                   
                                 Nc              / N d.
                                        N
                                       ς (f )

                                        Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
48      ·     B. Ahrens and J. Zsidó

We omit the formal definition. A module morphism M → N also constitutes a
natural transformation between the functors M and N induced by the modules.
     Example 3.25. (Ex. 3.22 cont.) The map
                          V 7→ AppV : LC(V ) × LC(V ) → LC(V )
verifies the diagram of the preceding definition and is hence a morphism of LC–
modules from LC × LC to LC. The map
                               V 7→ AbsV : LC(V ∗ ) → LC(V )
is a morphism of LC–modules from LC∗ to LC.
     Example 3.26. (Ex. 3.23 cont.) Given s, t ∈ T , the map
            App(s, t) : V 7→ AppV (s, t) : TLC(V )s⇒t × TLC(V )s → TLC(V )t
verifies the diagram of the preceding definition and is hence a morphism of modules
from TLCs⇒t × TLCs to TLCt .
   In the same way the constructor Abs(s, t) is a morphism of modules from TLCst
to TLCs⇒t .
  The modules over a monad P and with codomain D and morphisms between them
form a category called ModP
                          D (in the library: MOD P D), similar to the category of
monads.
3.5    Constructions on modules
The following constructions on monads and modules play a central role in what
follows.
Tautological Module (Taut Mod): Every monad P over C can be viewed as a
module (also denoted by P ) over itself, i.e. as an object in the category ModP
                                                                              C:

Program Instance Taut Mod struct : Module struct P D P := {
  mkleisli c d f := kleisli (Monad struct:=P) f;
  mkleisli oid c d := kleisli oid (a:=c)(b:=d);
  mkl mkl c d e f g := dist f g;
  mkl weta c := kl eta (Monad struct := P) c }.
In this definition we have actually inserted the section parameters P and D of
Module struct compared to the original code. The second argument P does not
denote the monad P but rather – by coercion – its underlying map on objects
P : C → C. The fact that we call P the monad as well as its tautological module is
reflected formally in the coercion
Coercion Taut Mod : Monad >−> obj.

Constant and terminal module (Const Mod, MOD Terminal): For any object
d ∈ D the constant map Td : C → D, c 7→ d for all c ∈ C can be provided with the
structure of a P –module for any monad P . In particular, if D has a terminal object
1D , then the constant module c 7→ 1D is terminal in ModP  D.
Pullback module (PbMod): Given a morphism of monads h : P → Q and a
Q-module M with codomain D, we define a P -module h∗ M with same object map
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                          Initial Semantics in Coq       ·     49

M : C → D with substitution map
                                ∗
                              ςh    M
                                        (f ) := ς M (f ; hd ).
This module is called the pullback module of M along h.
Program Instance PbMod struct (M : MOD Q D) : Module struct P (D:=D) M := {
  mkleisli c d f := mkleisli (f ;; h d) }.
The pullback extends to module morphisms (PbMod Hom) and is functorial.
  Remark 3.27. Note that pulling back the Q–module M does not change the
underlying functor. Similarly, pulling back a Q–module morphism s : M → M 0
does not modify the underlying natural transformation. It merely changes the
substitution action: while the module substitution of M takes morphisms f : c →
Qd as arguments, the module h∗ M takes as arguments morphisms of the form
c → P d.

Induced module morphism (PbMod ind Hom): With the same notation as in
the previous example, the monad morphism h induces a morphism of P –modules
h : P → h∗ Q. Again, in Coq we can indeed declare a
Coercion PbMod ind Hom : Monad Hom >−> mor.
corresponding to above abuse of notation.
  Remark 3.28. The module morphism h induced by the monad morphism h really
consists of the same data, namely, for any object c ∈ C, the morphism hc : P c → Qc
in C. In Sec. 4.3 we need to define the composite of a monad morphism with a
module morphism. This is done by considering, instead of the monad morphism,
the module morphism it induces.

Products (Prod Mod): Suppose the category D is equipped with a binary product.
Let M and N be P –modules with codomain D. We extend the map
                             C → D,          c 7→ M c × N c
to a module called the product of M and N :
Program Instance Prod Mod struct : Module struct (fun a => M a x N a) := {
   mkleisli c d f := (mkleisli f) X (mkleisli f) }.
This construction extends to a product on ModP  D . For the implementation of binary
product Cat Prod on a category, we refer to the library files.
  Our basic category of interest [T, Set] (in the library: ITYPE T) is formalized as
a category where objects are collections of Coq types indexed by T .
  The following two constructions – fibre and derivation – apply to monads and
modules over the category of (families of) sets.
3.6   Fibres
For a module M ∈ ModP                                            P
                    [T,Set] and u ∈ T , the fibre module Mu ∈ ModSet is defined
by
                                Mu V := (M V )(u)
                                              Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
50     ·     B. Ahrens and J. Zsidó

and
                                     ς Mu (f ) := ς M (f )(u) ,
that is, by forgetting all but one component of the indexed family of sets:
Program Instance ITFibre Mod struct u : Module struct P (fun c => M c u) := {
  mkleisli a b f := mkleisli (Module struct := M) f u }.
The construction extends to a functor (ITFIB MOD u)
                                ( )u : ModP            P
                                          [T,Set] → ModSet .

3.7   Derivation
Roughly speaking, a binding constructor makes free variables disappear. Its inputs
are hence terms “with (one or more) additional free variables” compared to the
output.
  Let T be a discrete category (a set) and u ∈ T an element of T . Define D(u) to
be the object of [T, Set] such that
                     D(u)(u) = {∗}         and       D(u)(t) = ∅ for t 6= u .
We enrich the object V of [T, Set] with respect to u by setting
                                       V ∗u := V + D(u),
i.e. we add a fresh variable of type u. Formally, we use an inductive type to construct
this coproduct, in order to use pattern matching to define coproduct maps.
Inductive opt (u : T) (V : ITYPE T) : ITYPE T :=
  | some : forall t : T, V t −> opt u V t
  | none : opt u V u.
This yields a monad ( )∗u on [T, Set] (opt monad u).
  For a map f : V → W in [T, Set] and w ∈ W (u), we call
                                  defaultu (f, w) : V ∗u → W
the coproduct map defined by
                                                 (
                                                     w,      if x = ∗
                       defaultu (f, w)(x) :=
                                                     ft (v), if x = v ∈ Vt .
  Given a monad P over [T, Set] and a P –module M with codomain [T, Set], we
define the derived module w.r.t. u ∈ T by setting
                                      M u (V ) := M (V ∗u ).
For a morphism f ∈ Hom(V, P (W )) the module substitution for the derived module
is given by
                                           u
                                      ς M (f ) := ς M (u f ).
Here the “shifted” map
                                      uf   : V ∗u → P (W ∗u )

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                        Initial Semantics in Coq       ·     51

is defined as
                                                            
                             uf   := default (f ; P i), η(∗) ,
the map i : W → W ∗ being the inclusion map.
  Example 3.29. When P is a monad of terms over free variables, the map u f
sends the additional variable of V ∗u to η P (∗u), i.e. to the term consisting of just the
“freshest” free variable. When recursively substituting with a map f : V → P W ,
terms under a constructor which binds a variable of type u such as λu must be
substituted using the shifted map u f . Examples are given in Ex. 3.14 for the
untyped case and Ex. 3.15 for the typed case.
Derivation is an endofunctor on the category of P –modules with codomain [T, Set].
   A constructor can bind several variables at once. Given a list l over T, the
multiple addition of variables with (object language) types according to l to a set
of variables V is defined by recursion over l. For this enriched set of variables we
introduce the notation V ∗∗ l.
Fixpoint pow (l : [T]) (V : ITYPE T) : ITYPE T :=
  match l with
  | nil => V
  | b::bs => pow bs (opt b V)
  end.
Being a monad, opt is functorial, as is the multiple addition of variables pow. On
morphisms the pow operation is defined by recursively applying the functoriality of
opt, where for the latter we use a special notation with a prefixed hat.
Fixpoint pow map (l : [T]) V W (f : V −−−> W) :
          V ∗∗ l −−−> W ∗∗ l :=
  match l return V ∗∗ l −−−> W ∗∗ l with
  | nil => f
  | b::bs => pow map (ˆf)
  end.
In the same manner the multiple shifting
Fixpoint lshift (l : [T]) (V W: ITYPE T) (f : V −−−> P W) :
            V ∗∗ l −−−> P (W ∗∗ l) := ...
is defined.
  The pullback operation commutes with products, derivations and fibres:
  Lemma 3.30. Let C be a category and D be a category with products. Let P
and Q be monads over C and ρ : P → Q a monad morphism. Let M and N be
Q–modules with codomain D. Then the following P –modules are isomorphic:
                             ρ∗ (M × N ) ∼
                                         = ρ∗ M × ρ∗ N .
  Lemma 3.31. Consider the setting as in the preceding lemma, with C = [T, Set]
and D = Set. Let u be an element of T . The following P –modules are isomorphic:
                                   ρ∗ (M u ) ∼
                                             = (ρ∗ M )u
                                            Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
52      ·     B. Ahrens and J. Zsidó

and
                                      ρ∗ (Mu ) ∼
                                               = (ρ∗ M )u .
   The carriers of these isomorphisms are families of identity functions, respectively,
since the carriers of the source and target modules are convertible. As modules,
however, source and target are not convertible in Coq. In our formalization we will
have to insert these isomorphisms (called PROD PB, ITDER PB and ITFIB PB) in
order to make some compositions typecheck.

4.    SIGNATURES & REPRESENTATIONS
An arity entirely describes the type and binding behaviour of a constructor, and
a signature is a family of arities. A signature may be seen as an abstract way of
storing all relevant information about a syntax.
  Given a signature S, a representation of S is given by any monad P (on a specific
category) which is equipped with some additional structure depending on S. This
additional structure is analoguous to the operations Z : X and S : X → X that a
representation of the signature N (cf. Sec. 1.1) in a set X comes with.
  Representations of S and their morphisms form a category, which, according to
our main theorem, has an initial object.
4.1     Arities & Signatures
To any constructor of a syntax we associate an arity, which is intuitively an abstract
way of storing all necessary (binding and typing) information about the constructor.
A signature is a family of arities.
  To any syntax Σ we can associate its signature, which is simply the family of
arities associated to the constructors of Σ.
  We start with an example before giving the general definition:
  Example 4.1. Consider Ex. 1.2 of the simply–typed lambda calculus. Given two
types s, t ∈ T , the arity associated to the constructor App(s, t) is
                               app(s, t) := [](s ⇒ t), []s −→ t ,
meaning that App(s, t) takes two arguments, a term of type s ⇒ t and one of type
s, yielding a term of type t. The empty lists signify that in both arguments no
variables will be bound.
   The arity associated to the constructor Abs(s, t) is
                                abs(s, t) := [s]t −→ (s ⇒ t) ,
where in the argument one variable of type s is bound by the constructor, yielding
a term of arrow type.
   Example 4.2. Untyped syntax may be considered as simply–typed over the sin-
gleton set of types, hence falling into the class of languages we consider. In that
case the only information an arity needs to give about a constructor is its number
of arguments and the number of variables bound in each argument. The example
of the untyped lambda calculus (cf. Ex. 1.1) shows such simplified arities.
     For the formal definitions let us fix a set T of object language types.

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                               Initial Semantics in Coq     ·     53

  Definition 4.3. A T –arity is a family of types consisting of ti ∈ T for i = 0, . . . , n
and ti,j ∈ T for all j = 1, . . . , mi and all i = 1, . . . , n, written
                      [t1,1 . . . t1,m1 ]t1 , . . . , [tn,1 . . . tn,mn ]tn → t0                (4.1)
or shorter
                                   (~s1 )t1 , . . . , (~sn )tn → t0
where ~sk denotes the list of types tk,1 . . . tk,mk . A T –signature is a family of T –
arities.
   A signature could be implemented as a pair consisting of a type sig index – which
is used for indexing the arities – and a map from the indexing type to the actual
arity type, which is simply built using lists – using a Haskell–like notation – and
products.
Record Signature : Type := {
  sig index : Type;
  sig : sig index −> [[T] ∗ T] ∗ T }.
   A slight modification however turns out to be useful. During the construction of
the initial representation a universal quantification over arities with a given target
type is needed. We choose to define a signature to be a function which maps each
t : T to the set of arities whose output type is the given t. In other words, the
parameter t of Signature t replaces the second component of the arities.
Record Signature t (t : T) : Type := {
  sig index : Type ;
  sig : sig index −> [[T] ∗ T] }.

Definition Signature := forall t, Signature t t.

  Example 4.4. (Impl. of Ex. 4.1) As an example we discuss the signature of the
simply typed lambda calculus. At first we define an indexing type TLC index t for
each object type t : T. After that, we build an indexed signature TLC sig mapping
each index to its collection of arities.
Inductive TLC index : T −> Type :=
   | TLC abs : forall s t : T, TLC index (s −−> t)
   | TLC app : forall s t : T, TLC index t.

Definition TLC arguments : forall t, TLC index t −> [[T] ∗ T] :=
    fun t r => match r with
       | TLC abs u v => (u::nil,v)::nil
       | TLC app u v => (nil,u −−> v)::(nil,u)::nil
       end.

Definition TLC sig t := Build Signature t t
       (@TLC arguments t).

The example signature of PCF is given in the Coq source files.
                                                 Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
54      ·    B. Ahrens and J. Zsidó

4.2    Representations
We summarize the preceding sections using the example of LC:
—The map V 7→ LC(V ) can be given the structure of a monad LC : Set → Set.
—The constructor App : LC × LC → LC is a morphism of LC–modules, and so is
 Abs : LC∗ → LC.
—The syntax of LC, i.e. the arguments and binding behaviour of its constructors,
 is stored entirely in the signature LC of LC.
Representations of LC are obtained by abstracting from the monad LC:
     Example 4.5. A representation R of the untyped lambda calculus is given by
—a monad P over the category Set of sets and
—two morphisms of modules
                          AppR : P × P → P ,           AbsR : P ∗ → P .
   The simply–typed lambda calculus as an example of a typed syntax is treated in
Ex. 4.9, after the general definitions.
   In the general case, given a set T of object types, a T –arity α associates to any
monad R over the category [T, Set] two R–modules: a target module cod(α, R),
which is of the form Rt for some t ∈ T , and a more complex source module
dom(α, R). The latter module is built from products (when the constructor in
question takes more than one argument) and derivations (for binding of variables)
of fibre modules of the form Rs .
   A representation of the arity α in the monad R is given by a morphism of R–
modules dom(α, R) → cod(α, R):
  Definition 4.6. Let α := (~s1 )t1 , . . . , (~sn )tn → t0 be a T –arity and R be a monad
on [T, Set]. A representation of the arity α in the monad R is an R–module mor-
phism
                            rαR : (R~s1 )t1 × . . . × (R~sn )tn → Rt0 ,
where R~s is the derivation of R associated to the list (~s) of object types obtained
by iterating
     Q       the derivation endofunctor. We write α = ` → t0 for the above arity
and ` R for the domain module.
  Definition 4.7. A representation R of a T –signature S is given by a monad
P : [T, Set] → [T, Set] and a representation of each arity α of S in P , that is, a
family of P –module morphisms
                                αR : dom(α, R) → cod(α, R) .
  Remark 4.8. Given a representation R, we will denote by R also its underlying
monad, i.e. we will omit the projection to its first component. However, it is possible
to define two different representations R and R0 of a signature in one and the same
monad P .
  Example 4.9. A representation R of TLC is any tuple of a monad P over [T , Set]
together with two families of P –module morphisms
               App(s, t)R : Ps⇒t × Ps → Pt ,           Abs(s, t)R : Pts → Ps⇒t ,
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                     Initial Semantics in Coq       ·     55

where s and t range over T . The reader might want to switch back to Ex. 4.1 and
compare how the source and target modules of those morphisms of modules are
determined by the arities app(s, t) and abs(s, t).

4.3   Morphisms of Representations
In the introductory example, a representation of the signature N is a set X together
with some “representation” data Z and S. A morphism of representations from
(X, Z, S) to (X 0 , Z 0 , S 0 ) is defined to be a map f : X → X 0 between the sets
underlying the representations that is compatible with the representation data in
the sense of Display (1.1).
  Another example of initial algebra, which illustrates a constructor with 2 argu-
ments, is the signature defining the types of TLC from Ex. 1.2,
                           T := {(∗) 7→ 0 ,      (⇒) 7→ 2} .
A morphism of representations from (X, ∗, ⇒) to (X 0 , ∗0 , ⇒0 ) is given by a map
f : X → X 0 such that

                     f (∗) = ∗0   and     X ×X
                                                       ⇒       /X                       (4.2)
                                              f ×f                 f
                                                                 
                                        X0 × X0                / X 0.
                                                       ⇒0

   Transferring this definition to the representations defined in Def. 4.7 yields that
a morphism P → Q of such representations is given by a monad morphism f :
P → Q of the underlying monads such that f is compatible in some sense with the
representation data.
   However, the map f is a monad morphism, while the representation data is given
by module morphisms. How can we plug them together in a way similar to what is
done in Diagram (4.2) ?
   From Sec. 3.5 we recall that f can be considered as a P –module morphism
f : P → f ∗ Q. We may then apply to f the functors fibre, derivation and products
of the category of P –modules to obtain a P –module morphism that is adapted to
the domain and codomain of some arity.
   Furthermore, the pullback functor f ∗ — which impacts the substitution struc-
ture, but not the underlying functor and natural transformation, as explained in
Remark 3.27 — can be used to obtain a P –module morphism from a Q–module
morphism. This will be used to turn the representation module morphisms of Q
into P –module morphisms.
  Definition 4.10. Let P and Q be representations of a T –signature S. A mor-
phism of representations f : P → Q is a morphism of monads f : P → Q (on
the underlying monads) such that the following diagram commutes for any arity




                                         Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
56     ·      B. Ahrens and J. Zsidó

α = (~s1 )t1 , . . . , (~sn )tn → t0 of S:
                                                                n
                                                                    (P ~si )ti         αP            / Pt 0
                                                                Q
                                                            i=1


                                                         Q ~s
                                                          (f i )ti                                         ft0
                                                            i


                                                                          
                                                                n                                         
                                                        ∗              ~
                                                                       si                           / f ∗ Qt0
                                                                Q
                                           f                        (Q )ti            ∗    Q
                                                            i=1                      f (α )

To make sense of this diagram it is necessary to recall the constructions on modules
of section 3.5. The diagram lives in the category ModP Set . The vertices are obtained
from the tautological modules P resp. Q over the monads P resp. Q by applying
the derivation, fibre and pullback functors as well as by the use of the product in
the category ModP  Set . The vertical morphisms are module morphisms induced by
the monad morphism f , to which functoriality of derivation, fibre and products
are applied. Furthermore instances of lemmas 3.30 and 3.31 are hidden in the
lower left corner. The lower horizontal morphism makes use of the functoriality of
the pullback operation, and in the lower right corner we again use the fact that
pullback commutes with fibres. Diagram (4.3) (on page 56) shows an expanded
version where the mentioned isomorphisms are explicitly inserted.

                               n
                               Q
                                    (P ~si )ti
                                                                                      αP
                                                                                                                   / Pt0       (4.3)
                               i=1


                    Q          ~
                               si
                        i (f      )t   i



                     Qn
                                               
                                                       ∗ Q)~
                                                           si )
                          i=1 ((f                              ti



                               ∼
                     Q
                          i (=)ti


                                           
                     Qn         ∗  ~
                                   si                                                                                   f t0
                          i=1 (f (Q ))ti


                                   ∼
                               Q
                                   i=



                     Qn
                                                   
                          i=1      f ∗ ((Q~si )ti )


                                   ∼
                                   =


                                                                                                                       
                        f∗
                               Qn        ~
                                         si
                                   i=1 (Q )ti
                                                                                     / f ∗ (Qt0 )                / (f ∗ Q)t0
                                                                                                       ∼
                                                                         f ∗ (αQ )                     =

                           Expanded diagram for morphisms of representations


Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                                    Initial Semantics in Coq                        ·   57

   Example 4.11. (Ex. 4.5 cont.) Given representations R and S of LC, a morphism
of representations from R to S is given by a monad morphism f : R → S such that
the following diagrams commute:
                                   AppR
                   R×R                           /R                R∗
                                                                                   AbsR        /R

                    f ×f                                    f     f∗                                   f
                                                                                                
               f ∗ (S × S)                      / f ∗S           f ∗S∗                        / f ∗S
                                f ∗ (AppS )                                     f ∗ (AbsS )

   Example 4.12. (Ex. 4.9 cont.) Given representations R and S of the simply–
typed lambda calculus, a morphism of representations from R to S is given by
a monad morphism f : R → S such that for any two object types s, t ∈ T the
following diagrams commute:
                               App(s,t)R                                          Abs(s,t)R
            Rs⇒t × Rs                            / Rt               Rts                                / Rs⇒t

              fs⇒t ×fs                                      ft    fts                                      fs⇒t
                                                                                                       
        f ∗ (Ss⇒t × Ss )                        / f ∗ St         f ∗ Sts                               / f ∗ Ss⇒t
                             f ∗ (App(s,t)S )                                   f ∗ (Abs(s,t)S )

   In the formalization, the aforementioned isomorphisms would have to be inserted
in order for the commutative diagram to typecheck, since the isomorphic modules
are not convertible. This would result in quite a cumbersome formalization with
decreased readability.
   Instead we implement the left vertical morphism from scratch, that is, we define
the data of the map first and prove afterwards that it is indeed a morphism of
modules. This decision entails another design decision: in Coq it is much more
convenient to define a map on an inductive data type than on a recursively defined
one. It is hence advantageous to also build the domain module from scratch, instead
of by applying recursively the categorical product of modules.         Q Given an arity
α = ` → t and a monad R, we define at first the map V 7→ ( ` P )(V ) and later
equip this map with a module substitution verifying the necessary properties.
                                         )tn → t0 (or shorter
   Given an arity (~s1 )t1 , . . . , (~snQ                    ` → t0 ) and a monad P , we
                                           n
have to construct the module i=1 (P ~si )ti = ` P . Its carrier, being a kind of
                                                        Q
heterogeneous list, is given as an inductive type parametrized by a set of variables
V and dependent on an arity (resp. its domain component). For the definition of
the carrier, we actually do not need all the information of a monad P , but just
its underlying map on objects of the category [T, Set] – in the code given by the
section variable M:
Variable M : (ITYPE T) −> (ITYPE T).
Inductive prod mod c (V : ITYPE T) : [[T] ∗ T] −> Type :=
  | TTT : prod mod c V nil
  | CONSTR : forall b bs,
        M (V ∗∗ (fst b)) (snd b) −> prod mod c V bs −> prod mod c V (b::bs).
Given now a module M over some monad P, the module substitution mkleisli:=
pm mkl for the module carrier prod mod c M is defined by recursion on this list–
                                                  Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
58     ·     B. Ahrens and J. Zsidó

like structure, applying the module substitution mkleisli of the module M in each
component:
Fixpoint pm mkl l V W (f : V −−−> P W)
       (X : prod mod c M V l) : prod mod c M W l :=
  match X in prod mod c      l return prod mod c M W l with
  | TTT => TTT M W
  | CONSTR b bs elem elems =>
          CONSTR (mkleisli (Module struct := M) (lshift f) (snd b) elem)
                   (pm mkl f elems)
  end.
Here the (multiple) shifting lshift is applied to accommodate the derivations in the
respective component.
  After having proved its module properties (by induction on the list–like structure)
and hence having defined a module prod mod l for each l : [[T] ∗ T], a type of module
morphisms is associated to each arity:
Definition modhom from arity (ar : [[T] ∗ T] ∗ T) : Type :=
 Module Hom (prod mod M (fst ar)) (M [(snd ar)]).
where M[(s)] denotes the fibre of the module M over s.
  Finally a representation of a signature S over a monad P is given by a module
morphism for each arity. Since the set of arities is indexed by the target of the
arities, the representation structure is indexed as well:
Variable P : Monad (ITYPE T).
Definition Repr t (t : T) :=
   forall i : sig index (S t), modhom from arity P ((sig i), t).
Definition Repr := forall t, Repr t t.
Here the monad P is actually seen as a module over itself via the coercion Taut Mod
mentioned earlier. After abstracting over the monad P, we bundle the data and
define a representation as a monad together with a representation structure over
this monad 10 :
Record Representation := {
  rep monad :> Monad (ITYPE T);
  repr : Repr rep monad }.
  As already mentioned, the carrier of the upper left product module is defined
as an inductive type. This suggests the use of structural recursion for defining
the left vertical morphism of the commutative diagram.
                                              Q        Given a monad morphism
f : P → Q, we apply f to every component of ` P :
Fixpoint Prod mor c (l : [[T] ∗ T]) (V : ITYPE T) (X : prod mod P l V) :
                  f∗ (prod mod Q l) V :=

10 Here an example of coercion occurs. The special notation :> allows us to omit the projection

rep monad when accessing the monad which underlies a given representation R. We can hence
also write R x for the value of the monad of R on an object x of the underlying category. This
coercion is the formal counterpart to the abuse of notation announced in Remark 4.8.
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                          Initial Semantics in Coq       ·     59

  match X in prod mod c    l return f∗ (prod mod Q l) V with
  | TTT => TTT
  | CONSTR b bs elem elems =>
    CONSTR (f     elem) (Prod mor c elems)
  end.
This function is easily proved to be a morphism of P –modules
                                      Y         Y
                           Prod mor :    P → f∗     Q .
                                          `               `

  The isomorphism in the lower right corner however remains in the formalization,
appearing as ITPB FIB. Its underlying family of morphisms, however, is simply
a family of identity functions. For an arity a and module morphisms RepP and
RepQ representing this arity in monads P and Q respectively, the definition of the
commutative diagram reads as follows.
Definition commute f RepP RepQ : Prop :=
   RepP ;; f [(snd a)] ==
   Prod mor (fst a) ;; f∗ RepQ ;; ITPB FIB f
A morphism of representations P and Q of the signature S is just a monad morphism
from P to Q together with the commutativity property for each t : T and each arity
(index) i in the indexing set of S t:
Variables P Q : Representation S.
Class Representation Hom struct (f : Monad Hom P Q) :=
  repr hom s : forall t (i : sig index (S t)), commute f (repr P i) (repr Q i).
Record Representation Hom : Type := {
  repr hom c :> Monad Hom P Q ;
  repr hom :> Representation Hom struct repr hom c }.
Morphisms of representations can be composed: the composition of the underlying
monad morphisms as defined in Lst. 5 makes the necessary diagram commute and
hence gives a morphism of representations. Similarly the identity morphism of
monads is a morphism of representations. Two morphisms of representations are
said to be equal if their underlying morphism of monads are equal. With these
definitions the collection of representations of the signature S and their morphisms
form a category:
Program Instance REPRESENTATION struct :
               Cat struct (@Representation Hom           S) := {
  mor oid a c := eq Rep oid a c ;
  id a := Rep Id a ;
  comp P Q R f g := Rep Comp f g }.
  The following theorem is the main result of our work:
  Theorem 4.13. Let S be a T –signature. Then the category Rep(S) of represen-
tations of S has an initial object Σ(S).
The formal counterpart of this theorem is the instance declaration for the Initial
type class of Lst. 6.
                                              Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
60     ·     B. Ahrens and J. Zsidó

   Remark 4.14. The monad underlying the initial representation associates to any
V ∈ [T, Set] the set of terms of the syntax associated to S with free variables in V .
The module morphisms of the initial representation are given by the constructors
of this syntax.
  A set–theoretic construction of the syntax as well as a proof of the theorem can
be found in Zsidó’s PhD thesis [Zsi10]. In a type–theoretic setting such as Coq the
syntax can be defined as an inductive type. The next section is devoted to the
proof of the theorem, i.e. the construction of the initial representation.

5.    THE INITIAL OBJECT
The initial object of the category of representations of the signature S is constructed
in several steps:
—the syntax associated to S as an inductive data type STS,
—definition of a monad structure STS Monad on said data type,
—construction of the representation structure STSRepr on STS Monad,
—for any representation R, construction of a morphism init R from STSRepr to R,
—unicity of init R for any representation R.
5.1   The Syntax associated to a Signature
The first step is to define a map STS : ITYPE T −−−> ITYPE T – the monad
carrier – mapping each type family V of variables to the type family of terms
with free variables in V . Since objects of ITYPE T really are just dependent Coq
types (cf. Sec. 3.1.4), this map can be implemented as a Coq inductive data type,
parametrized by a set of variables and dependent on object types. Apart from the
use of dependent types, the “data” parts of this section could indeed be done in
any programming language featuring inductive types.
   Mutual induction is used, defining at the same time a type STS list of heteroge-
neous lists of terms, yielding the arguments to the constructors of S. This list type
is indexed by arities, such that the constructors can be fed with precisely the right
kind of arguments.
Inductive STS (V : ITYPE T) : ITYPE T :=
  | Var : forall t, V t −> STS V t
  | Build : forall t (i : sig index (S t)), STS list V (sig i) −> STS V t
with
 STS list (V : ITYPE T) : [[T] ∗ T] −> Type :=
  | TT : STS list V nil
  | constr : forall b bs,
      STS (V ∗∗ (fst b)) (snd b) −> STS list V bs −> STS list V (b::bs).

Scheme STSind := Induction for STS Sort Prop with
      STSlistind := Induction for STS list Sort Prop.
The constructor Build takes 3 arguments:
—an object type t indicating its output type,
—an arity i (resp. its index) from the set of indices with output type t and
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                      Initial Semantics in Coq       ·     61

—a term of type STS list V (sig i) carrying the subterms of the term to construct.
Note that Coq typing ensures the correct typing of all constructible terms of STS,
a techique called intrinsic typing.
   The Scheme command generates a mutual induction scheme for the defined pair
of types.
   The latter type, STS list, is actually isomorphic to the type prod mod c STS.
This duplication of data could hence have been avoided by defining STS as a nested
inductive type as follows, instead of using mutual induction.
Inductive STS (V : ITYPE T) : ITYPE T :=
  | Var : forall t, V t −> STS V t
  | Build : forall t (i : sig index (S t)), prod mod c STS V (sig i) −> STS V t.
However, we use the mutual inductive version because it allows us to define func-
tions on those types by mutual recursion rather than nested recursion. We found
nested recursive functions to be difficult to reason about, whereas the mutual in-
duction principle produced by the Scheme command makes reasoning about mutual
recursive functions as easy as one could wish, compensating for any inconvenience
caused by the duplication of data (cf. Sec. 5.3).
5.2   Monad Structure on Syntax
We continue by defining a monad structure on the map STS. Again, due to our
choice of implementing sets as Coq types (cf. Sec. 3.1.4), the maps we need are
really just Coq functions. As in the special case of LC (cf. Ex. 3.14) and TLC
(cf. Ex. 3.15), the term–as–variable constructor Var serves as monadic map η. The
substitution map subst is defined using two helper functions rename (providing
functoriality) and shift (serving the same purpose as in Ex. 3.14). Renaming and
substitution, being recursive functions on the inductive data types, are implemented
using mutual recursion:
Fixpoint rename V W (f : V −−−> W) t (v : STS V t):=
     match v in STS t return STS W t with
     | Var t v => Var (f t v)
     | Build t i l => Build (l //−− f)
     end
with
  list rename V t (l : STS list V t) W (f : V −−−> W) : STS list W t :=
       match l in STS list t return STS list W t with
       | TT => TT W
       | constr b bs elem elems =>
                constr (elem //− ( f ˆˆ (fst b)))
                                  (elems //−− f)
       end
where ”x //− f” := (rename f x)
and ”x //−− f” := (list rename x f).

(* ... *)


                                          Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
62     ·     B. Ahrens and J. Zsidó

Fixpoint subst (V W : ITYPE T) (f : V −−−> STS W) t (v : STS V t) :
  STS W t := match v in STS t return STS W t with
     | Var t v => f t v
     | Build t i l => Build (l >>== f)
     end
with
  list subst V W t (l : STS list V t) (f : V −−−> STS W) : STS list W t :=
       match l in STS list t return STS list W t with
       | TT => TT W
       | constr b bs elem elems =>
          constr (elem >== ( lshift f)) (elems >>== f)
       end
where ”x >== f” := (subst f x)
and ”x >>== f” := (list subst x f).
The monadic properties that the substitution should verify, resemble the lemmas
one would prove in order to establish “program correctness”. As an example, the
third monad law reads as
Lemma subst subst V t (v : STS V t) W X (f : V −−−> STS W)
                (g : W −−−> STS X) :
      v >== f >== g = v >== f;; subst g.
Proof.
  apply (@STSind
    (fun (V : T −> Type) (t : T) (v : STS V t) => forall (W X : T −> Type)
           (f : V −−−> STS W) (g : W −−−> STS X),
         v >== f >== g = v >== (f;; subst g))
   (fun (V : T −> Type) l (v : STS list V l) =>
        forall (W X : T −> Type)
           (f : V −−−> STS W) (g : W −−−> STS X),
         v >>== f >>== g = v >>== (f;; subst g) ));
  t5.
Qed.
Its proof script is a typical example; most of those lemmas are proved using the
induction scheme STSind – instantiated with suitable properties – followed by a
single custom tactic which finishes off the resulting subgoals, mainly by rewriting
with previously proved equalities.
   After a quite lengthy series of lemmas we obtain that the function subst and the
variable–as–term constructor Var turn STS into a monad:
Program Instance STS monad : Monad struct STS := {
  weta := Var ;
  kleisli := subst }.

5.3   A representation in the Syntax
The representational structure on STS is defined using the Build constructor. For
each arity i in the index set sig index (S t) we must give a morphism of modules from
prod mod STS (sig i) to STS [(t)]. Since the constructor Build takes its argument
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                      Initial Semantics in Coq       ·     63

from STS list and not from the isomorphic prod mod STS, we precompose with one
of the isomorphisms between those two types:
Program Instance STS arity rep (t : T) (i : sig index (S t)) : Module Hom struct
       (S := prod mod STS (sig i)) (T := STS [(t)])
   (fun V X => Build (STSl f pm X)).
The only property to verify is the compatibility of this map with the module sub-
stitution, which we happily leave to Coq.
   The result is the object STSRepr of the category REPRESENTATION S:
Record STSRepr : REPRESENTATION S := Build Representation (@STSrepr).

5.4   Weak Initiality
In the introduction we gave the equations that a morphism of representations of the
natural numbers should verify. Reading those equations as a rewrite system from
left to right yields a way to define iterative functions on the natural numbers. This
idea is also used in order to define a morphism from STSRepr to any representation
R of the signature S: a term of STS, whose root is a constructor Build t i for some
object type t and an arity i, is mapped recursively to the image – of the recursively
computed argument – under the corresponding representation repr R i of R. This
definition for a morphism of representations will turn out to be the only one possible,
leading to initiality.
   Formally, the carrier init of what will be the initial morphism from STSRepr to
R is defined as a mutually recursive Coq function:
Fixpoint init V t (v : STS V t) : R V t :=
    match v in STS t return R V t with
    | Var t v => weta (Monad struct := R) V t v
    | Build t i X => repr R i V (init list X)
    end
with
 init list l (V : ITYPE T) (s : STS list V l) : prod mod R l V :=
    match s in STS list l return prod mod R l V with
    | TT => TTT
    | constr b bs elem elems =>
           CONSTR (init elem) (init list elems)
    end.
where the function init list applies init to (heterogeneous) lists of arguments. We
have to show that this function is (a) a morphism of monads and (b) a morphism
of representations.
   Several lemmas show that init commutes with renaming/lifting (init lift), shifting
(init shift) and substitution (init kleisli):
Lemma init lift V t x W (f : V −−−> W) : init (x //− f) = lift f t (init x).
Lemma init shift a V W (f : V −−−> STS W) : forall (t : T) (x : opt a V t),
     init (x >>− f) = x >>− (f ;; @init ).
Lemma init kleisli V t (v : STS V t) W (f : V −−−> STS W) :
  init (v >== f) = kleisli (f ;; @init ) t (init v).
                                          Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
64     ·     B. Ahrens and J. Zsidó

   The latter property is precisely one of the axioms of morphisms of monads (cf.
Def. 3.17, rectangular diagram). The second monad morphism axiom which states
compatibility with the ηs of the monads involved is fulfilled by definition of init –
it is exactly the first branch of the pattern matching. We hence have established
that init is (the carrier of) a morphism of monads:
Program Instance init monadic : Monad Hom struct (P:=STSM) init.
Record init mon := Build Monad Hom init monadic.
  Very much less work is then needed to show that init also is a morphism of
representations:
Program Instance init representic : Representation Hom struct init mon.

5.5   Uniqueness & Initiality
Its uniqueness is expressed by the following lemma:
Lemma init unique : forall f : STSRepr −−−> R , f == init rep.
Instead of directly proving the lemma, we prove at first an unfolded version which
allows to directly apply the mutual induction scheme STSind:
Variable f : Representation Hom STSRepr R.
Hint Rewrite one way : fin.
Ltac ttt := tt;
 (try match goal with [t:T, s : STS list    |− ] => rewrite <− (one way s);
               let H:=fresh in assert (H:=repr hom f (t:=t));
               unfold commute in H; simpl in H end);
               repeat (app (mh weta f) || tinv || tt).

Lemma init unique prepa V t (v : STS V t) : f V t v = init v.
Proof.
  apply (@STSind
      (fun V t v => f V t v = init v)
      (fun V l v => Prod mor f l V (pm f STSl v) = init list v));
  ttt.
Qed.
  Finally we declare an instance of the Initial type class for the category of rep-
resentations REPRESENTATION S with STSRepr as initial object and init rep R as
the initial morphism towards any other representation R.
Program Instance STS initial : Initial (REPRESENTATION S) := {
  Init := STSRepr ;
  InitMor R := init rep R }.

             Listing 6.    Instance of Initial for category of representations
The proof field InitMorUnique is filled automatically using the preceding lemma
init unique.

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                            Initial Semantics in Coq       ·     65

6.   CONCLUSIONS & FUTURE WORK
We have presented the formalization of a recently proved theorem of representations
of typed binding signatures in monads over (families of) sets. The theorem features
the relatively new notion of module over a monad and exhibits the structure of
constructors as morphisms of modules.
   The nature of the theorem made it convenient for computer theorem proving:
the proofs are straightforward, carrying no surprises. Moreover, they are highly
technical using (mutual) induction, something our favourite tool Coq offers good
support for.
   Some aspects remain unsatisfactory: using type classes and records simultane-
ously is at least confusing for the reader, even if there are good reasons from the
implementor’s point of view to do so. The weak support for nested induction in
Coq obliged us to use mutual induction instead, leading to some duplication of data
and hence another unnecessary source of confusion.
   Other aspects, such as the implementation of syntax in an efficient way, i.e.
without any extrinsic typing device, could be solved due to Coq’s good support for
dependent types.
   The formalization is split into a general library of category theoretic concepts and
a theory–specific part comprising the formalization of sections 4 and 5. According
to coqwc11 the latter consists of approx. 400 lines of specification and 600 lines of
proof. The proofs are mostly done in a semi–automated way, employing a proof style
promoted by Chlipala in his online book [Chl], as well as in a published user tutorial
[Chl10]. An earlier version using a more standard proof style included about 900
lines of proof. This reduction is mainly due to the fact that proof automation also
stimulates reuse of code – here reuse of proof code – similarly to how polymorphism
does for data structures and functions. However, we do not claim to be experts in
proof automation, nor do we have “one tactic to rule them all”.
   The first author is working on extending the presented result by adding different
features. A first generalization [Ahr11a] is to enlarge the category of representations
to allow for representations of a T -signature in a monad over [U, Set] for a given
“translation of object types” f : T → U . In this way translations from one pro-
gramming language to another — over different object types — can be considered
as initial morphisms in the category of representations of the source language.
   This extension yields a difficulty when one attempts to formalize the theorem in
Coq: for such translations of types, say, f , g and h, (propositional) equalities of the
form h(t) = g(f (t)) arise, as well as equations such as f (s ⇒ t) = f (s) ⇒ f (t) for
a hypothetical type constructor (⇒). Intrinsic typing expresses typing judgements
of some language L by type dependency. However, even in the presence of a proof
of equality t = s of two object types s and t, the types L(V )(s) and L(V )(t) (for
a type family of variables V ) are not convertible. In order to consider a term
p ∈ L(V )(s) to have type t instead, one would need explicit type casts and, later,
their elimination. This would introduce, in the formalization, a difficulty which
does not arise in the informal mathematics. Our Coq library contains two different
translations from PCF to LC which illustrate the heavy use of casts.

11 The tool coqwc, part of the standard Coq tools, counts the number of lines in a Coq source file,
classified into the 3 categories specification, proof and comment.
                                                Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
66     ·     B. Ahrens and J. Zsidó

   Secondly, syntax usually comes with a reduction relation, which we model by con-
sidering sets equipped with a preorder [Ahr11b]. This change is reflected by passing
from monads over (families of) sets to relative monads from sets to preorders. We
introduce inequations for the specification of reduction relations. A language with
reductions is given by a signature S, which specifies the terms of the syntax, as
well as of a set of inequations A for that syntax. The category of representations
of (S, A) is defined to be the full subcategory of representations of S that verify
all the inequations of A. We prove that this category has an initial object. The
implementation of this theorem is available on the first author’s web page 12 .

ACKNOWLEDGMENTS
The theorem was implemented in Coq by the first author during a stay at Università
degli Studi di Firenze, Italy, financially supported by the Conseil Général des Alpes–
Maritimes CG06.
   We wish to thank André Hirschowitz and Marco Maggesi for many discussions
on the subject and help with Coq.
   Furthermore, we are grateful to Assia Mahboubi for letting us use her Coq syntax
file for the listings package.
   Last but not least we thank the reviewers and the handling editor of JFR for
their valuable comments and careful proofreading.

References
[ABF+ 05]Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan
         Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Ge-
         offrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mecha-
         nized metatheory for the masses: The POPLmark challenge. In In-
         ternational Conference on Theorem Proving in Higher Order Logics
         (TPHOLs), August 2005.
[Acz93]  Peter Aczel. Galois: A Theory Development Project. Technical Report
         for the 1993 Turin meeting on the Representation of Mathematics in
         Logical Frameworks., 1993.
[Ahr11a] Benedikt Ahrens. Extended Initiality for Typed Abstract Syntax.
         ArXiv e-prints, jul 2011. arXiv:1107.4751.
[Ahr11b] Benedikt Ahrens. Modules over relative monads for syntax and se-
         mantics. ArXiv e-prints, jul 2011. arXiv:1107.5252.
[AR99]   Thorsten Altenkirch and Bernhard Reus. Monadic presentations of
         lambda terms using generalized inductive types. In Computer Science
         Logic, 13th International Workshop, CSL ’99, pages 453–468, 1999.
[BC04]   Yves Bertot and Pierre Castéran. Interactive Theorem Proving and
         Program Development. Coq’Art: The Calculus of Inductive Construc-
         tions. Texts in Theoretical Computer Science. Springer Verlag, 2004.
[BHKM11] Nick Benton, Chung-Kil Hur, Andrew Kennedy, and Conor McBride.
         Strongly Typed Term Representations in Coq. Journal of Automated
         Reasoning, pages 1–19, 2011. 10.1007/s10817-011-9219-0.

12 http://math.unice.fr/∼ahrens

Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                  Initial Semantics in Coq       ·     67

[BM98]   Richard S. Bird and Lambert Meertens. Nested datatypes. In Johan
         Jeuring, editor, LNCS 1422: Proceedings of Mathematics of Program
         Construction, pages 52–67, Marstrand, Sweden, June 1998. Springer-
         Verlag.
      +
[CAA 86] Robert L. Constable, Stuart F. Allen, S. F. Allen, H. M. Bromley,
         W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B.
         Knoblock, N. P. Mendler, P. Panangaden, Scott F. Smith, James T.
         Sasaki, and S. F. Smith. Implementing mathematics with the Nuprl
         proof development system. Prentice-Hall, Inc., Upper Saddle River,
         NJ, USA, 1986.
[CF09]   Venanzio Capretta and Amy Felty. Higher-order abstract syntax in
         type theory. In S. Barry Cooper, Herman Geuvers, Anand Pillay, and
         Jouko Väänänen, editors, Logic Colloquium 2006, volume 32 of Lecture
         Notes in Logic, pages 65–90. Cambridge University Press, 2009.
[Chl]    Adam Chlipala. Certified Programming with Dependent Types. http:
         //adam.chlipala.net/cpdt/.
[Chl10]  Adam Chlipala. An Introduction to Programming and Proving with
         Dependent Types in Coq. Journal of Formalized Reasoning, 3(2):1–93,
         December 2010.
[Coq]    Coq. The Coq Proof Assistant. http://coq.inria.fr.
[FH07]   Marcelo P. Fiore and Chung-Kil Hur. Equational systems and free
         constructions (extended abstract). In Lars Arge, Christian Cachin,
         Tomasz Jurdzinski, and Andrzej Tarlecki, editors, ICALP, volume
         4596 of Lecture Notes in Computer Science, pages 607–618. Springer,
         2007.
[Fio02]  Marcelo Fiore. Semantic analysis of normalisation by evaluation for
         typed lambda calculus. In Proceedings of the 4th ACM SIGPLAN
         international conference on Principles and practice of declarative pro-
         gramming, PPDP ’02, pages 26–37, New York, NY, USA, 2002. ACM.
[FPT99]  Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax
         and variable binding (extended abstract). In In Proc. 14 th LICS,
         pages 193–202. IEEE Computer Science Press, 1999.
[GGMR09] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence
         Rideau. Packaging Mathematical Structures. In Proceedings of the
         22nd International Conference on Theorem Proving in Higher Or-
         der Logics, TPHOLs ’09, pages 327–342, Berlin, Heidelberg, 2009.
         Springer-Verlag.
[GP99]   Murdoch J. Gabbay and Andrew M. Pitts. A new approach to ab-
         stract syntax involving binders. In 14th Annual Symposium on Logic
         in Computer Science, pages 214–224, Washington, DC, USA, 1999.
         IEEE Computer Society Press.
[GTWW77] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Ini-
         tial algebra semantics and continuous algebras. J. ACM, 24:68–95,
         January 1977.


                                      Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
68     ·     B. Ahrens and J. Zsidó

[HM07]         André Hirschowitz and Marco Maggesi. Modules over monads and
               linearity. In Daniel Leivant and Ruy J. G. B. de Queiroz, editors,
               WoLLIC, volume 4576 of Lecture Notes in Computer Science, pages
               218–237. Springer, 2007.
[HM10a]        André Hirschowitz and Marco Maggesi. Modules over monads and
               initial semantics. Inf. Comput., 208(5):545–564, 2010.
[HM10b]        André Hirschowitz and Marco Maggesi.          Nested Abstract Syn-
               tax in Coq. Journal of Automated Reasoning, pages 1–18, 2010.
               10.1007/s10817-010-9207-9.
[Hof99]        Martin Hofmann. Semantical analysis of higher-order syntax. In In
               14th Annual Symposium on Logic in Computer Science, pages 204–
               213. IEEE Computer Society Press, 1999.
[HS00]         Gérard P. Huet and Amokrane Saı̈bi. Constructive category theory.
               In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof,
               Language, and Interaction, pages 239–276. The MIT Press, 2000.
[Hur10]        Chung-Kil Hur. Categorical equational systems: algebraic models and
               equational reasoning. PhD thesis, University of Cambridge, UK, 2010.
[Man76]        Ernest Manes. Algebraic Theories, volume 26 of Graduate Texts in
               Mathematics. Springer, 1976.
[ML98]         Saunders Mac Lane. Categories for the working mathematician, vol-
               ume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York,
               second edition, 1998.
[MS03]         Marino Miculan and Ivan Scagnetto. A framework for typed HOAS
               and semantics. In PPDP, pages 184–194. ACM, 2003.
[O’K04]        Greg O’Keefe. Towards a Readable Formalisation of Category The-
               ory. Electronic Notes in Theoretical Computer Science, 91:212 – 228,
               2004. Proceedings of Computing: The Australasian Theory Sympo-
               sium (CATS) 2004.
[Sim06]        Carlos Simpson. Explaining Gabriel-Zisman Localization to the Com-
               puter. J. Autom. Reason., 36:259–285, April 2006.
[SO08]         Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. In
               César Muñoz Otmane Ait Mohamed and Sofiène Tahar, editors, The-
               orem Proving in Higher Order Logics, 21th International Conference,
               volume 5170 of Lecture Notes in Computer Science, pages 278–293.
               Springer, August 2008.
[SvdW11]       Bas Spitters and Eelis van der Weegen. Type classes for mathemat-
               ics in type theory. Mathematical Structures in Computer Science,
               21(4):795–825, 2011.
[The10]        The Coq Development Team. The Coq Proof Assistant Reference Man-
               ual – Version V8.3, 2010. http://coq.inria.fr.
[Ven00]        Varmo Vene. Categorical programming with inductive and coinductive
               types. PhD thesis, University of Tartu, 2000.
[Wad95]        Philip Wadler. Monads for functional programming. In Johan Jeuring
               and Erik Meijer, editors, Advanced Functional Programming, volume
               925 of Lecture Notes in Computer Science, pages 24–52. Springer, 1995.
Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
                                                 Initial Semantics in Coq       ·     69

[Wie08]   Freek Wiedijk. Formal proof—getting started. Notices Amer. Math.
          Soc., 55(11):1408–1417, 2008.
[Zsi10]   Julianna Zsidó. Typed Abstract Syntax. PhD thesis, University of Nice,
          France, 2010. http://tel.archives-ouvertes.fr/tel-00535944/.




                                     Journal of Formalized Reasoning Vol. 4, No. 1, 2011.
