Algebras

 
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 mathematical notation.


 

Introduction

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.

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 Algebra

algebra.ml [5K]
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
    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 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
    end
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 *)
    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.

 

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: 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 conditions
    h 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.

 

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 = N.zero  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
    end
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 = 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 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
    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 definitions
    h 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 an 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, 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 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.

 

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