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.

- Introduction
- Signatures and Sigma-Algebras
- Algebra Homomorphism
- Initial Algebra
- Syntax and Semantics
- Algebraic Data Types
- Free Algebra
- Equalities (identities), equational laws, equational theories
- Context-Free Grammars: the epitome of many-sorted algebras

- 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).
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.

**References**- 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 <http://www.math.uwaterloo.ca/~snburris/htdocs/UALG/univ-algebra2012.pdf>

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

<http://math.hawaii.edu/~ralph/Classes/619/birkhoff1935.pdf>

The foundational paper of the field of Universal Algebraalgebra.ml [6K]

The complete OCaml code accompanying the article: the executable specification

- 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 end

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 mappingzero \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 end

Since`NAT`

has only one sort, the`NatUL`

algebra has only one carrier set, which is the set`{[], [()], [();()], ...}`

of`unit list`

s. 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 *) end

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.

- 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: M1.sk -> M2.sk end

The functions`h_si`

(`i=1..k`

) are non necessarily injective or `onto' -- but have to be total:`h_si : M1.si -> M2.si`

should be able to handle any value from the set`M1.si`

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 M1.sn`

.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) end

The operation preservation conditionsh NatUL.zero = NatBool.zero h (NatUL.succ x) = NatBool.succ (h x) h (NatUL.plus (x,y)) = NatBool.plus (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 ^ ")" end

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.

- 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 functormodule TFzero(N:NAT) = struct let e = N.zero end

is in`TFc`

. If a functor`T1`

is in`TFc`

, so ismodule TS(N:NAT) = struct let e = let module M1 = T1(N) in N.succ M1.e end

To lighten the notation, we shall write the above asmodule 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 ismodule TP(N:NAT) = struct let e = N.plus (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)) end

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 end)) let plus ((module T1:TF), (module T2:TF)) : nat = (module (functor (N:NAT) -> struct let e = N.plus (T1(N).e, T2(N).e) end)) end

The sample element`TFN`

shown earlier can now be written asmodule 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 end

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 TFC.zero = N.zero h (TFC.succ x) = N.succ (h x) h (TFC.plus (x,y)) = N.plus (h x, h y)

for every`x`

and`y`

in`TFc`

. Indeed, unrolling the definitionsh TFC.zero = h (module TFzero) = TFzero(N).e = N.zero 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 TFC.zero = N.zero = g TFC.zero

That is,`h`

and`g`

coincide on`TFC.zero`

. If`h`

and`g`

map some`t`

of`TFc`

to the same element of`NAT.nat`

, thenh (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`TFC.plus`

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.

- 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.*

- 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) end

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 (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 end

(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" end

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 : CM.np 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) end module TFcm_chase(CM:CATMOUSE) = struct open CM let e = prod1(prod2(the,cat), prod3( prod4(chased, prod5(and_, prod4(chased, prod5(and_, caught)))), prod2 (the,mouse))) end

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) aslet 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.''