What exactly is algebraic about algebraic effects or algebraic data types? Which module/object signatures are actually algebraic? What is algebra anyway? Where is freedom in free algebra? What is the initial algebra, what good does it do, and how does one actually prove the initiality? Can we say something precise about the correctness of a tagless-final DSL embedding and its interpreters? How do we substantiate the correctness claims?

This web page, written in the form of lecture notes, is (being) built in response to such questions. It presents the standard introductory material from the field of Universal Algebra -- however, selected and arranged specifically for programmers, especially those interested in the tagless-final approach. We only use programming examples, and, as far as possible, a concrete programming language notation rather than the mathematical notation.



What is Algebra? Garett Birkhoff, the founder of the field now called Universal Algebra, said:
``By an `abstract algebra' is meant, loosely speaking, any system of elements and operations such as a ring, a field, a group, or a Boolean algebra'' (Birkhoff, 1935).
He then followed up with a `tentative formal definition', which is still in use (and which we recall later).

Universal Algebra is a field of Mathematics. A significant part of a Universal Algebra course and textbooks is devoted to lattices and combinatorics. There is not much connection, it seems, to common programming tasks. And yet it is. The automata theory (finite state machines, Kleene Algebra, regular expressions, etc.) was one of the first applications of algebras in Computer Science. According to Goguen et al. (1977), Burstall and Landin's ``Programs and their proofs: An algebraic approach'' (1969) was the first use of universal algebra and (implicitly) initiality in programming language semantics. F.L.Morris (``Correctness of translations of programming languages'', Ph.D. Thesis, Stanford, 1972) brought in many-sorted algebras, most commonly of interest in programming languages. The ADJ collaboration (J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright) was responsible for the all-out introduction of algebraic and categorical methods in Computer Science -- and the subsequent development of algebraic data types, module systems and algebraic specifications. In particular, Goguen et al. (1977) demonstrated how the initial algebra semantics unifies a great number of semantic formalisms, and elegantly answers the questions of what is syntax and what is semantics. Recently, algebraic effects put algebras into spotlight once again. The tagless-final approach is another application of algebras, very closely related to the initial algebra semantics.

The present web page in intended as a reference, to collect the definitions and standard results from universal algebra that are of most interest to computer scientists and especially tagless-final programmers. The overarching goal of being relevant to programming dictates the selection of the material and the choice of notation. We use only programming examples and a concrete programming language notation (namely, OCaml). The standard mathematical practice relies on a multitude of superscripts and subscripts and the extensive, sometimes confusing, overloading to avoid writing even more deeply nested subscripts. A programming-language notation is more regular, less ambiguous -- and can be `mechanically checked', by a compiler.

The fact that the OCaml module notation turns out adequate is not all surprising: Joseph Goguen has been a major influence in the design of the ML module system.

Martin Wirsing: Algebraic specifications
Handbook of Theoretical Computer Science B, 1990, J. van Leeuwen, Ed. Elsevier. pp 675-788
Comprehensive, but fairly mathematical and categorical. We borrow most definitions from it, changing the notation.

Stanley Burris and H. P. Sankappanavar: A Course in Universal Algebra
Graduate Texts in Mathematics, 1981, v. 78 10.1007/978-1-4613-8130-3
Available online <>
The standard, detailed graduate text, for Math graduate students. Initial algebra is mentioned only as a remark, as a special case of free algebra with the empty set of generators.

J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright: Initial Algebra Semantics and Continuous Algebras
Journal of the ACM, Vol 24, No 1, January 1977, pp 68-95
This is the paper that properly introduced initial algebras in Computer Science, see particularly Sections 1-4.

Bart Jacobs and Jan Rutten: A Tutorial on (Co)Algebras and (Co)Induction
EATCS Bulletin, 1997, 62, pp. 222--259
The tutorial, for computer scientists, explains algebras and initiality in detail and at a good slow pace. It demonstrates proofs by initiality as an alternative to inductive proofs -- often a simpler and clearer alternative. The tutorial uses a different presentation of Sigma-algebras: so-called F-algebras, relying on polynomial functors to represent signatures.

Garrett Birkhoff: On the structure of abstract algebras
Proceedings of the Cambridge Philosophical Society, 1935, v31, 433-454
The foundational paper of the field of Universal Algebra [6K]
The complete OCaml code accompanying the article: the executable specification


Signatures and Sigma-Algebras

Birkhoff formally defined an (abstract) algebra as a class A, now called the carrier set, with a class of operations on it: each operation is associated with a set of sequences of elements of A and maps each sequence from its associated set to some element of A. We shall see what it means in concrete, programming terms in a moment.

We will be working with so-called many-sorted algebras, with not one but several carrier sets. To tell them apart and conveniently refer to, each carrier set is associated with its own `sort'. One may think of the `sort' as a symbol that names a carrier set. For many-sorted algebras, it is customary to first define a signature -- the `type' of an algebra. Here is the formal definition, to be illustrated below. ``Formally, a (many-sorted algebraic) signature Sigma is a pair <S,F> where S is a set (of sorts) and F is a set (of function symbols) such that F is equipped with the mapping F \mapsto S^n \times S for some n >=0. The mapping, for a particular f of F is often denoted as f: s_1 ... s_n -> s where {s,s_1,...,s_n} \subset S'' (Wirsing, 1990). The number n is called the arity of f. The operations of zero arity are called constants.

Wirsing's definition is the straightforward generalization of Birkhoff's original definition to the many-sorted case. (It is also a restriction: Birkhoff's definition admitted operations of infinite arity, and algebras whose carriers and operations are not just infinite sets but proper classes).

In programming terms, a many-sorted algebraic signature is a module signature. For example,

    module type NAT = sig
      type nat
      val zero : nat
      val succ : nat -> nat
      val plus : nat * nat -> nat
Here, the set of sorts S is the singleton set {nat}. The set F has three elements: {zero, succ, plus} and is equipped with the mapping
    zero \mapsto                         nat
    succ \mapsto nat              \times nat
    plus \mapsto (nat \times nat) \times nat
That mapping is (more perspicuously) represented by the OCaml declarations:
    val zero : nat
    val succ : nat -> nat
    val plus : nat * nat -> nat
Thus `sort' is what in programming may be called `type'. (Joseph Goguen has remarked that `type' is too ambiguous a word and so `sort' has been chosen instead.) We shall continue to use the term `sort', however odd it may sound to an (OCaml) programmer.

Exercise: give several examples of OCaml module signatures that are not algebraic signatures.

With the signature Sigma thus defined, ``A Sigma-Algebra consists of an S-sorted family of non-empty (carrier) sets {A_s}_{s\in S} and a total function f^A: A_{s_1},\ldots,A_{s_n} -> A_s for each f: s_1,\ldots,s_n -> s in F.'' (Wirsing, 1990).

Here is an example of a NAT-algebra:

    module NatUL = struct
      type nat = unit list
      let zero = []
      let succ x = () :: x
      let plus (x,y) = x @ y
Since NAT has only one sort, the NatUL algebra has only one carrier set, which is the set {[], [()], [();()], ...} of unit lists. The constant zero is the empty list, succ maps a list to a longer, by one (), list; and plus maps a pair of lists to the concatenated list. All these operations are total as required: succ and plus can handle any lists supplied as arguments, with no exceptions.

Here is another NAT algebra:

    module NatBool : (NAT with type nat = bool) = struct
      type nat = bool
      let zero = false
      let succ x = not x
      let plus (x,y) = not (x = y)          (* exclusive or *)
Its carrier is the set of Booleans. We added the signature ascription to the NatBool module so that the OCaml compiler could check that all operations required by the Nat signature are defined. We have exposed the particular type of the carrier set (that is, the association between the abstract sort nat and the concrete carrier type).

From now on, we shall use the OCaml notation: OCaml signatures for Sigma signatures, and OCaml modules implementing the signature for the corresponding algebra.


Algebra Homomorphism

An algebra homomorphism is a mapping between two algebras of the same signature: specifically, a mapping of the carriers of one algebra to the corresponding carriers of the other algebra that is said to `preserve operations'. Here what it means formally: let S be an algebraic signature (with sorts s1, s2, ... sk and the operations f1, f2, ... fm). Let M1: S and M2: S be two S-algebras: two OCaml modules of that signature. A homomorphism H12 from M1 to M2 (notated as H12: M1 ~> M2) is a collection of functions h_s1,...,h_sk, one for each sort, which can be represented by the following OCaml signature:
    module H12 : sig 
      val h_s1: M1.s1 -> M2.s1
      val h_s2: M1.s2 -> M2.s2
      val h_sk: ->
The functions h_si (i=1..k) are non necessarily injective or `onto' -- but have to be total: h_si : -> should be able to handle any value from the set received as the argument. The functions h_si must also `preserve the operations': that is, for every operation f : s_1 ... s_n -> s of arity n,
    h_s (M1.f (a_1, ..., a_n)) = M2.f (h_s1 a_1, ..., h_sn a_n)
for every a_1 \in M1.s1, ... a_n \in

There is always a homomorphism from any algebra to itself: the identity homomorphism, to be written as Id. It is the identity mapping on the carriers (which clearly preserves the operations).

A bit more interesting is the homomorphism from NatUL to NatBool:

    module HULtoBool : sig val h : NatUL.nat -> NatBool.nat end = struct
      let rec h = function 
        | []   -> false
        | _::t -> not (h t)
The operation preservation conditions
    h         =
    h (NatUL.succ x)     = NatBool.succ (h x)
    h ( (x,y)) = (h x,h y)
are clearly satisfied, for any unit list values x and y, as one can easily see by unrolling the definitions of h and the operations. The reader may want to see it for themself.

Exercise: show that there is no homomorphism from NatBool to NatUL.

Exercise: Consider yet another NAT-algebra:

    module NatStr : (NAT with type nat = string) = struct
      type nat = string
      let zero = "Z"
      let succ x = "S" ^ x
      let plus (x,y) = "(" ^ x ^ "+" ^ y ^ ")"
Are there any homomorphisms involving NatStr and the earlier introduced algebras? Note that NatStr's carrier is the set of all OCaml strings (which includes not only "SZ" but also "foo"). Is there any way to adjust NatStr so that there is a homomorphism to NatUL?

Homomorphism is just a collection of functions mapping carriers of one algebra to the corresponding carriers of the other algebra. As functions, they may be composed. We use the symbol \cdot of functional composition also for the composition of homomorphisms.

Theorem: if H1: M1 ~> M2 and H2: M2 ~> M3 are two homomorphisms, then their composition H2 \cdot H1 is also a homomorphism, from M1 to M3.
Proof: clearly, H2 \cdot H1 maps the carriers of M1 to the carriers of M3. As for operation preservation, for any f : s_1,...,s_n -> s,

    (H2.hs \cdot H1.hs) M1.f(x_1,...,x_n)
    = H2.hs (H1.hs (M1.f(x_1,...,x_n)))
    = H2.hs (M2.f(H1.hs1 x_1,...,H1.hsn x_n))
    = M3.f(H2.hs1 (H1.hs1 x_1),...,H2.hsn (H1.hsn x_n))
    = M3.f((H2.hs1 \cdot H1.hs1) x_1,...,(H2.hsn \cdot H1.hsn) x_n)
If a homomorphism H: M1~>M2 is `onto' -- that is, every element of every carrier set of M2 is an image by H of some element of an M1 carrier -- the algebra M2 is called a homomorphic image of M1. For example, the homomorphism HULtoBool is onto and NatBool is hence a homomorphic image of NatUL.

If all carrier-mapping functions in a homomorphism H: M1 ~> M2 are one-to-one (that is, injective and onto), the homomorphism is called isomorphism, and M1 and M2 isomorphic. The identity homomorphism Id is in fact the isomorphism.

Theorem: A homomorphism H: M1 ~> M2 is isomorphism if and only if there is also a homomorphism H': M2 ~> M1 such that H \cdot H' = Id and H' \cdot H = Id. (H' is also isomorphism). The proof is left as an exercise.


Initial Algebra

We have seen that an algebra homomorphism does not always exist. We now construct an algebra from which there is always a homomorphism to any other algebra of the same signature. Moreover, the homomorphism is unique. We show the construction on the running example of the NAT signature. Let TFc be the set of OCaml functors:
    module type TF = functor(N:NAT) -> sig val e : N.nat end
constructed as follows. The functor
    module TFzero(N:NAT) = struct  let e =  end
is in TFc. If a functor T1 is in TFc, so is
    module TS(N:NAT) = struct
      let e = let module M1 = T1(N) in
              N.succ M1.e
To lighten the notation, we shall write the above as
    module TS(N:NAT) = struct  let e = N.succ T1(N).e  end
(In the current version of OCaml, it is necessary to code T(N).e as let module M = T(N) in M.e; see the accompanying code for details.) If functors T1 and T2 are in TFc, so is
    module TP(N:NAT) = struct  let e = (T1(N).e, T2(N).e)  end
Finally, nothing else is in TFc.

A different way to write an element of TFc is illustrated by the following sample:

    module TFN(N:NAT) = struct
      open N
      (* A term constructed using only the operations succ, zero and plus *)  
      let e = plus (succ zero, succ (succ zero))
which should look very familiar to the readers who have encountered the tagless-final style.

We turn TFc into a NAT algebra by adding the operations in the obvious way:

    module TFC : (NAT with type nat = (module TF)) = struct
      type nat = (module TF)
      let zero = (module TFzero : TF)
      let succ (module T1:TF) : nat =
        (module (functor (N:NAT) -> struct
          let e = N.succ T1(N).e
      let plus ((module T1:TF), (module T2:TF)) : nat =
        (module (functor (N:NAT) -> struct
          let e = (T1(N).e, T2(N).e)
The sample element TFN shown earlier can now be written as
    module TFCsample : TF =
      (val let open TFC in plus (succ zero, succ (succ zero)))
For any NAT algebra N there exists a homomorphism from TFC to that algebra:
    module HTFC(N:NAT) = struct
      let h : TFC.nat -> N.nat = fun (module T:TF) -> T(N).e
In the following demonstration, let N be an arbitrary NAT algebra and let h be HTFC(N).h, that is, fun (module T:TF) -> T(N).e. Clearly h maps every element of the carrier TFc (that is, every functor TF) to some element of N.nat. For example, the result of mapping TFN is TFN(N).e, which is the N.nat value computed as follows, using the operations zero, succ and plus of N:
    let open N in let e = plus (succ zero, succ (succ zero))
Now that we have seen that h is the total mapping, we verify that it preserves the operations:
    h         =
    h (TFC.succ x)     = N.succ (h x)
    h ( (x,y)) = (h x, h y)
for every x and y in TFc. Indeed, unrolling the definitions
    h = h (module TFzero) = TFzero(N).e =
    h (TFC.succ x) = 
       let (module T1:TF) = x in
       h (module (functor (N:NAT) -> struct let e = N.succ T1(N).e end))
    =  let (module T1:TF) = x in N.succ T1(N).e
    =  N.succ (h x)
(the verification of the plus preservation is left to the reader.) The banality of the proof is the indication that TFC preserves the operations by its very construction.

We now demonstrate that h is a unique homomorphism from TFC to N. Suppose there is another mapping, called g, from TFc to N.nat that preserves operations. Since both h and g must preserve the zero operation,

    h = = g
That is, h and g coincide on If h and g map some t of TFc to the same element of NAT.nat, then
    h (TFC.succ t) = N.succ (h t) = N.succ (g t) = g (TFC.succ t)
That is, they also have to agree on TFC.succ t. The case of is similar. By structural induction h and g coincide on all elements of TFc. Thus, h is unique.

A Sigma-algebra with a unique homomorphism to any other algebra of the same signature is called initial algebra.

The TFc construction is standard, used already by Birkhoff to show the existence of initial algebras (actually, he talked about free algebras, of which initial algebras are a particular case.) The carrier constructed like TFc is called `Herbrand universe' for the signature Sigma (cf. Herbrand universe and Herbrand basis in Logic Programming). The TFC algebra itself is called word-algebra or ground-term algebra. The construction easily generalizes to the many-sorted case, giving:

Theorem: For any signature Sigma whose Herbrand universe has a term of every sort, there exists an initial Sigma-algebra

Exercise: NatBool is not an initial NAT-algebra (why?). Show that NatUL is not an initial NAT-algebra either. (Hint: show that there is no homomorphism from NatUL to TFC).

Exercise: (not entirely straightforward): Although NatUL fails to be an initial NAT-algebra, there is still an initial NAT-algebra with the same carrier set, viz. unit list. Construct it.

Exercise: Carry out the initial NAT algebra construction using functions instead of functors (the functions may take modules as arguments)

Theorem: two initial algebras of the same signature are isomorphic
Proof: Let M1 and M2 be two initial algebras. Then there exist (the unique) homomorphisms H12: M1 ~> M2 and H21: M2 ~> M1. Their composition H21 \cdot H12: M1 ~> M1 must be a homomorphism too. There is also the identity homomorphism Id: M1 ~> M1. Since M1 is initial, there is only one homomorphism from it to another algebra, including itself. Therefore, the two previously mentioned homomorphisms from M1 to itself must be the same: H21 \cdot H12 = Id. Likewise, we find that H12 \cdot H21 = Id. Hence H12 (and H21) are in fact isomorphisms. The proof relies on the uniqueness of homomorphisms from an initial algebra -- the so-called `universality property'. The tutorial by Jacobs and Rutten shows more proofs by initiality, which, they argue, are often more perspicuous than the corresponding proofs by induction.

Theorem: An algebra isomorphic to an initial algebra is initial as well
Proof: a simple application of the homomorphism composition theorem.


Syntax and Semantics

The word-algebra construction feels like a mindless shuffling of function symbols, very `syntactic' -- which is exactly the point, according to Goguen et al. (1977). They invited to think of a signature Sigma as the grammar of a language, an initial Sigma-algebra S as the abstract syntax, and the other Sigma algebras A as semantics of the language. ``The semantic function is the uniquely determined homomorphism hA : S ~> A, assigning a meaning hA(s) in A to each syntactic structure s in S'' -- that is, to each term in the language. That initial algebras of the same signature are isomorphic strengthens their claim to be the `abstract syntax': there may be multiple presentations of abstract syntax, but they are `essentially the same'.

In our running example, NAT is the grammar of the tiny language for adding natural numbers; TFc is the set of its terms (TFN or TFCsample being sample terms); the other NAT algebras provide interpretations, or semantics: NatUL is the unary number semantics, NatBool is the parity semantics.

``From this viewpoint it becomes clear that a major aspect of formal semantics (both practical and theoretical) is constructing intended semantic algebras for particular programming languages.'' (Goguen et al., (1977))

Tagless-final takes this to heart, and to the letter. Once the signature is decided, one can write sample terms like TFN right away. Implementations of the signature provide interpreters: semantics. Applying the TFN functor to, say, the NatUL module, amounts to interpreting the TFN term, or computing its NatUL-semantics.

In fact, the very module that defines a NAT algebra (its carrier and operations), such as NatUL, is also the module that implements an interpreter of tagless-final terms like TFN -- that is, implements the homomorphism from TFC. An algebra is hence literally defined by its homomorphism from the word-algebra. Writing a tagless-final interpreter is defining an algebra, and vice versa.


Algebraic Data Types

Consider yet another algebra
    module ADT = struct
      type nat = Z | S of nat | P of nat * nat
      let zero       = Z
      let succ x     = S x
      let plus (x,y) = P (x,y)
As we saw in the tagless-final approach, ADT is the homomorphism from TFC. Moreover, its mapping from the TFc to the data type ADT.nat is injective and onto. Hence it is an isomorphism and ADT is also an initial algebra.

Exercise: show the homomorphism from ADT to TFC, which must exist.

Although TFC and ADT are isomorphic and hence `essentially the same', there may still be useful presentation differences between them. After all, two programs that produce the same outputs for all the same inputs are also `essentially the same'. Yet there may be many reasons to prefer one over the other: one program may be faster, smaller, written in a familiar language, easier to maintain and extend, etc.


Context-Free Grammars: the epitome of many-sorted algebras

Context-free grammars (CFG) are the exemplar of many-sorted algebras, described as such already in Goguen et al. (1977, Sec 3.1). Unlike the general exposition in Goguen et al., we explain CFG as algebras on a concrete example and in the programming language notation.

Consider the following CFG for a small subset of English:

    S   -> NP VP           DET -> the
    NP  -> DET N           N   -> cat
    VP  -> TV NP           N   -> mouse
    TV  -> TV CTV          TV  -> chased
    CTV -> CRD TV          TV  -> caught
                           CRD -> and
The non-terminals are in upper case and the terminals are in lower case. The grammar happens to be in the Chomsky Normal Form (CNF): each production has the form NONTERM -> NONTERM NONTERM or NONTERM -> term. (The Chomsky Normal form will later help us relate CFG to AB grammars. It also makes the algebraic presentation perspicuous.) In this form, the grammar productions fall into two classes: the (proper) `rules' (the left column of the above figure) and the `lexicon' (the right column). Incidentally, every CFG can be converted to the equivalent (in the sense of recognizing/generating the same language) CNF grammar.

A context-free grammars may be viewed as a set of rules for generating a language, i.e., a set of `strings' where each string is a sequence of terminal symbols of the grammar. In fact, each non-terminal generates its own language. For example, the non-terminal NP of our grammar generates only two strings: ``the cat'' and ``the mouse''. (We write the strings with spaces to delimit the terminals for readability.) On the other hand, the language of S is infinite, with the strings like ``the cat chased the mouse'' or ``the cat chased and chased and caught the mouse'', etc. Each grammar production can be interpreted as generating a string of the corresponding language: N -> cat produces the string ``cat'' of the N language, NP -> DET N forms a string of the NP language from an arbitrary string of the DET language and an arbitrary string of the N language. Looked this way, we see the sets of objects (strings of the language) and the operations defined on those sets -- quite like the algebra in Birkhoff's original definition. However, instead of a single carrier set there are several sets, one for each `sort', that is, non-terminal of the grammar. We thus have a many-sorted algebra.

The algebraic signature in our example is as follows, written in the form of the OCaml module signature:

    module type CATMOUSE = sig
      type s          type vp
      type np         type tv
      type n          type ctv
      type det        type crd
      val prod1 : np * vp -> s        val the    : det
      val prod2 : det * n -> np       val cat    : n
      val prod3 : tv * np -> vp       val mouse  : n
      val prod4 : tv * ctv -> tv      val chased : tv
      val prod5 : crd * tv -> ctv     val caught : tv
                                      val and_   : crd
(Since and is reserved in OCaml, we write and_.) Unlike the NAT signature in the earlier examples, we clearly see many sorts -- eight, as a matter of fact, corresponding to the non-terminals of our grammar. The signature looks strikingly similar to the grammar, modulo switching the sides of the productions. Such close correspondence is the particular advantage of the Chomsky Normal Form. The only notable change is attaching the names such as prod1 to the rules of the grammar. Naming of the rules is often useful. However, the conventional CFG notation does not have the conventional way of doing that. In the algebraic presentation of CFG, the naming is inescapable. Also worth pointing out is that each terminal symbol of the grammar is treated as an operator symbol of zero arity in the algebra.

One algebra of the CATMOUSE signature is the string algebra:

    module CMString = struct
      type s   = string       type vp  = string
      type np  = string       type tv  = string
      type n   = string       type ctv = string
      type det = string       type crd = string
      let ccat : string * string -> string = fun (x,y) -> x ^ " " ^ y
      let prod1 = ccat        let the    = "the"
      let prod2 = ccat        let cat    = "cat"
      let prod3 = ccat        let mouse  = "mouse"
      let prod4 = ccat        let chased = "chased"
      let prod5 = ccat        let caught = "caught"
                              let and_   = "and"
Each non-terminal denotes a set of strings, i.e., a language. In other words, a carrier of the sort, say, vp, is a language generated by the grammar with the start symbol VP.

Exercise: Is CMString an initial algebra?

Exercise: One may say that the CMString algebra realizes the view of a context-free grammar as a set of rules for generating languages. However, CMString only shows how to produce one string of a language. For example, prod1 tells how to generate a string of the S language from a string of NP and VP languages. Using CMString, write a program that produces all strings of the NP, VP, S, etc. languages.

One may wonder what would be the analogue of TFC (see Initial Algebra) for the CATMOUSE signature. It should be a many-sorted algebra -- call it TFCATMOUSE -- with sorts s, np, vp, etc., whose carrier set of the sort, say, np is a set of OCaml functors of the type TFCM_np:

    module type TFCM_np = functor(CM:CATMOUSE) -> sig val e : end
    module type TFCM_s  = functor(CM:CATMOUSE) -> sig val e : CM.s end
Likewise, the carrier set of the sort s contains the functors of the type TFCM_s. Here are a couple of typical elements of these carrier sets:
    module TFcm_thecat(CM:CATMOUSE) = struct
      open CM
      let e = prod2 (the,cat)
    module TFcm_chase(CM:CATMOUSE) = struct
      open CM
      let e = 
              prod3( prod4(chased, prod5(and_, prod4(chased, prod5(and_, caught)))),
                     prod2 (the,mouse)))
built in the manner of TFN of the earlier section.

Exercise: Taking TFC as an example, write TFCATMOUSE explicitly as an OCaml module.

Exercise: Again, with TFC as an example, show that TFCATMOUSE is an initial algebra. As a pre-condition, show that all carrier sets of TFCATMOUSE are populated.

Let's look closer at the elements of the TFCATMOUSE carriers, such as TFcm_chase. The term TFcm_chase.e is a term built using only the constants and operations of the algebra. In CFG terms, it shows a particular application of CFG productions. That is, TFcm_chase.e denotes a parse tree (a derivation tree) of the CATMOUSE grammar. If we enter the TFcm_chase module into OCaml, we see it is accepted by the type checker. It means TFcm_chase.e is well-typed -- that is, it represents a valid application of CFG productions, or, it represents a valid parse tree.

Thus, we have reached the conclusion stated in Goguen et al. (1977), that an initial algebra of the signature representing a CFG has carriers that are parsed trees for derivations in the grammar from each non-terminal.

Furthermore, if we write the initial algebra or its carrier elements in the manner of TFcm_chase, the validity of the derivations (of parsed trees) can be mechanically checked by the OCaml type checker.

Since TFCATMOUSE is an initial algebra, there is a unique homomorphism to any other algebra of the same signature, say, CMString. It maps a TFCATMOUSE carrier element to a CMString carrier element (i.e., a string) as

    let module M = TFcm_chase(CMString) in M.e
        - : string = "the cat chased and chased and caught the mouse"
(The indented line shows the evaluation result.) In other words, the homomorphism from TFCATMOUSE to CMString computes the yield of the corresponding parse tree -- that is, the string which the parse tree is the derivation of.

Exercise: Is the homomorphism from TFCATMOUSE to CMString injective? Is it onto? How does the injectivity of this homomorphism relate to the ambiguity of the grammar?

Goguen et al. (1977) write that in general, if G is a CFG grammar and TG is the initial algebra for the signature of the grammar, that any other algebra S of the same signature provides the semantics for the context-free language generated by G. ``TG, being initial, gives the unique homomorphism hs : TG ~> S which assigns "meanings" in S to all syntactically well-formed phrases of the language.''

Exercise: As a further example, Goguen et al. (1977) outline how Knuth's attribute grammars may be thought as algebras giving meaning to CFG derivations (``but Knuth's definitions and notation seem more complex than is necessary''). The carriers of those algebras are sets of tuples: synthesized attributes. (Inherited attributes require a bit more elaboration). Think of an attribute grammar for CATMOUSE and implement it as a CATMOUSE algebra.

Finally, the classical denotational semantics is but another example of the initial algebra semantics for CFG. Goguen et al. note that Scott's ``Data types as lattices'' begins with the motto ``Extend BNF to semantics''. Scott and Strachey in ``Towards a mathematical semantics for computer languages'' write: ``The semantical definition is syntax directed in that it follows the same order of clauses and transforms each language construct into the intended operations on the meanings of the parts.'' Goguen et al.: ``This essentially says that syntax is context-free and semantics is a homomorphism.''