$$

Universal Algebra 2: Termalgebras, Homomorphisms, Universal Properties

"To a large extent it is true that the increase in power of programming languages has corresponded to the increase in the size and complexity of the right hand sides of their assignment commands for this is the situation in which expressions are most valuable."

Christopher Strachey in 1967 about the early history of programming languages, see Fundamental Concepts in Programming Languages

Introduction

The distinction between syntax and semantics, invented by philosophers, logicians and linguists over 100 years ago, is crucial to computer scientists.

Programs are syntactic objects and we use techniques such as context-free grammars and parsing in order to check whether programs are syntactically correct, whether they are legitimate, well-formed programs.

On the other hand, programs have to be intepreted, evaluated, compiles to be executed. This gives us the meaning or semantics of a program. In the worst case, the semantics of a programming languages is only given to use via a compiler together with a target architecture. In programming languages as an area of computer science, we study more abstract methods independen of any particular machine or language in order to explain the meaning of programs.

The methods covered so far in this course include abstract reduction systems, equivalence relations and normal forms.

In this lecture, we add term-algebras, homomorphisms and initiality.

The general idea is that we want to have syntax and semantics in the same "category". Looking back at the lecture on syntax and semantics and the definition of

$$\begin{array}{rl}\text{color}black[[-]]:\text{color}blue\mathcal{L}& \text{color}black\to \text{color}red\mathbb{N}\\ [[\text{color}blue1]]& =\text{color}red1\\ [[\text{color}bluet+t^{\prime }]]& =[[\text{color}bluet]]\text{color}red+[[\text{color}blue{t}^{\prime }]]\\ [[\text{color}bluet\ast t^{\prime }]]& =[[\text{color}bluet]]\text{color}red\cdot [[\text{color}blue{t}^{\prime }]]\end{array}$$

we will indentify in this lecture both the syntax

$\mathcal{L}$ and the semantics

$\mathbb{N}$ as algebras and the

$[[-]]$ as a homomorphism.

But syntax is special. While there can be many algebras to interpret

$1,+,\ast$, there is only one language of terms formed from

$1,+,\ast$. So if syntax is also an algebra, then what property characterises as the special algebra of syntax?

The answer will be initiality.

But before can come to this we need to explain how terms form an algebra and write down a formal definition of what a homomorphism is.

Termalgebras

In the section on Abstract Data Types we argued that data types are not just sets of data, but algebras of data.

Similarly, in this section we will learn that terms form not just sets but algebras. These algebras are called term-algebras. Or absolutely free algebras but this terminology will be explained only later.

For each choice of signature there is one term algebra.

For example, the language

$\mathcal{L}$ of expressions

​​​​    exp ::= 1 | exp + exp | exp * exp

is the term algebra for the signature

$\mathrm{\Sigma }=\{1,+,\ast \}$ (where again 1 is a constant and

$+.\ast$ are binary operation symbols).

Activity: Can you translate any signature

$\mathrm{\Sigma }$ into BNF notation as in the example above?

The answer is "yes".

So this can serve as the first definition of term algebra for a signature

$\mathrm{\Sigma }$: the language of terms as defined by the corresponding context-free grammar.

But, wait a moment, if

$\mathcal{L}$ is supposed to be an algebra, then we should find operations

$1^{\mathcal{L}},{+}^{\mathcal{L}},{\ast }^{\mathcal{L}}$ on terms, so that

$(\mathcal{L},1^{\mathcal{L}},{+}^{\mathcal{L}},{\ast }^{\mathcal{L}})$ becomes an algebra for the signature

$\mathrm{\Sigma }=\{1,+,\ast \}$. In more detail, if

$\mathcal{L}$ is to be an algebra, then then there must be operations

$$\begin{array}{rl}{1}^{\mathcal{L}}& \in \mathcal{L}\\ {+}^{\mathcal{L}}:\mathcal{L}\times \mathcal{L}& \to \mathcal{L}\\ {\ast }^{\mathcal{L}}:\mathcal{L}\times \mathcal{L}& \to \mathcal{L}\end{array}$$

But this is easy, so easy that it almost feels like cheating (but it isn't). We simply define:

$$\begin{array}{rl}{1}^{\mathcal{L}}& =1\\ t_1{+}^{\mathcal{L}}{t}_2& =t_1+t_2\\ t_1{\ast }^{\mathcal{L}}{t}_2& =t_1\ast t_2\end{array}$$

This is an inductive definition similar to others we have seen before (induction on the three cases that make up the definition of

$\mathcal{L}$). Nevertheless, this definition does look like a notational trick, just replacing

${+}^{\mathcal{L}}$ by

$+$, etc.

So what is going on here?

Activity: Imagine we want to implement a calculator in the C langauge. Terms are trees. Each node in such a tree consists of some data with pointers to the children ^[1]. Picture

$1+1$ as such a tree and also

$(1+1)+1$. What is

${\ast }^{\mathcal{L}}$ then? In our C-implementation,

${\ast }^{\mathcal{L}}$ is the function that takes as inputs, for example, the trees corresponding to

$1+1$ and

$(1+1)+1$ and constructs the tree corresponding to

$(1+1)\ast ((1+1)+1)$. Think about how to implement

${\ast }^{\mathcal{L}}$ in C and you will find that a lot is going on here. Actually implement

${\ast }^{\mathcal{L}}$ in C and you will find that it is not such an easy task. On the other hand, from our more abstract point of view, all of what

${\ast }^{\mathcal{L}}$ does, in this example, is summarised in the seemingly trivial equation

$$(1+1){\ast }^{\mathcal{L}}((1+1)+1)=(1+1)\ast ((1+1)+1)$$ or, more generally,

$$t_1{\ast }^{\mathcal{L}}{t}_2=t_1\ast t_2.$$ In a high-level language such as Haskell you can actually implement

${\ast }^{\mathcal{L}}$ by, essentially, just writing

$t_1{\ast }^{\mathcal{L}}{t}_2=t_1\ast t_2.$

Summary: We have seen that algebra is tightly related to induction.

• The term algebra is defined inductively via a context-free grammar.
• The operations of the term algebra are defined by induction over the rules of the grammar.
• The operations of the term algebra are the constructors that build terms (=trees) from symbols.

Homomorphisms

In a previous lecture we discussed structure preserving maps in detail.

Homomorphisms are the structure preserving maps of algebra.

But before coming to the formal definition of a homomorphism, I want to come back to one of the recurring topics of this course, namely how we can capture meaning in a computational way. This was the main topic of the lecture on meaning in syntax and then brought to a satisfying conclusion in the lecture on normalisation by evaluation.

I will now summarise the main insights of this story under the heading of

Meaning as homomorphism

In our example of a language

$\mathcal{L}$ given by the grammar

​​​​    exp ::= 1 | exp + exp | exp * exp

we defined the semantics as follows.

$$\begin{array}{rl}\text{color}black[[-]]:\text{color}blue\mathcal{L}& \text{color}black\to \text{color}red\mathbb{N}\\ [[\text{color}blue1]]& =\text{color}red1\\ [[\text{color}bluet+t^{\prime }]]& =[[\text{color}bluet]]\text{color}red+[[\text{color}blue{t}^{\prime }]]\\ [[\text{color}bluet\ast t^{\prime }]]& =[[\text{color}bluet]]\text{color}red\cdot [[\text{color}blue{t}^{\prime }]]\end{array}$$

Quotienting

$\mathcal{L}$ by the equations discussed in the lecture on normalisation by evaluation, the semantics

$[[-]]$ becomes a bijection between equivalence classes of terms and numbers.

This establishes that, up to notation, terms and numbers are the same.

Or does it?

In fact, all countably infinite sets are bijective. For example, the natural numbers

$\mathbb{N}$ are in bijection with the rationals

$\mathbb{Q}$. Surely, we cant say that natural numbers and rationals are the same? As discussed in the lecture on structure preserving maps the solution to the conundrum lies in the notion of what we now call a homomorphism.

Indeed, the semantics

$[[-]]$ is more than a bijection, it is a bijective homomorphism.

To see this in more detail, by definition,

$[[-]]$ preserves the relevant structure:

It maps

$\text{color}blue1$ to

$\text{color}red1$ and

$\text{color}blue+$ to

$\text{color}red+$ and

$\text{color}blue\ast$ to

$\text{color}red\cdot$.

Homomorphisms defined

The definition of homomorphism is, as the definition of algebra, given wrt a signature.

Definition: Let

$\mathrm{\Sigma }$ be a signature and let

$A$ and

$B$ be two

$\mathrm{\Sigma }$-algebras. Then a

$\mathrm{\Sigma }$-homomorphism

$h:A\to B$ is a function that satisfies in addition for each

$n$-ary operation symbol

$op$ of the signature that

$$h(\text{color}blueop(a_1,\dots a_n))=\text{color}redop(h(a_1),\dots h(a_n))$$

for all elements

$a_1,\dots a_n\in A$.

Remark: The colour code is meant to highlight that

$\text{color}blueop$ is the interpretation of

$op$ in

$A$ and

$\text{color}redop$ is the interpretation of

$op$ in

$B$. We could have written

$o{p}^A$ and

$o{p}^B$ instead. But I wanted to highlight the connection with the definition of

$[[-]]$ in …, repeated in the next example, where the colours are used in the same meaning.

Example: In first section we have seen that the language

$\mathcal{L}$ defined by

​​​​    exp ::= 1 | exp + exp | exp * exp 

is the term-algebra for the signature

$\mathrm{\Sigma }=\{1,+,\ast \}$. In the second section we argued that meaning is a homomorphism. We can make this precise now we formalised what we want to understand by a homomorphism. Copying in the definition of the semantics

$$\begin{array}{rl}\text{color}black[[-]]:\text{color}blue\mathcal{L}& \text{color}black\to \text{color}red\mathbb{N}\\ [[\text{color}blue1]]& =\text{color}red1\\ [[\text{color}bluet+t^{\prime }]]& =[[\text{color}bluet]]\text{color}red+[[\text{color}blue{t}^{\prime }]]\\ [[\text{color}bluet\ast t^{\prime }]]& =[[\text{color}bluet]]\text{color}red\cdot [[\text{color}blue{t}^{\prime }]]\end{array}$$

and comparing with the definition of homomorphism

$$h(\text{color}blueop(a_1,\dots a_n))=\text{color}redop(h(a_1),\dots h(a_n))$$

we see that they exactly agree after identifying

$h=[[-]]$ and letting

$op$ range over

$\{1,+,\ast \}$.

Remark: In other words, we turned our observation of

$[[-]]$ preserving the structure of

$1,+,\ast$ into a general definition of a homomorphism preserving the structure given by any number operation symbols of any arity.

Example: Modular Arithmetic

One of the most important and familiar examples of homomorphism is the clock. The signature is

$0,1,+,\ast$ and the two algebras in question are the integers

$\mathbb{Z}$ and the

$Clock=\{1,2,\dots 12\}$. The function

$$\mathbb{Z}\to Clock$$ which takes and integer

$n$ to the number

$m\in Clock$ such that there is an integer

$k$ with

$n=m+12k$ is the familiar map that takes as input "universal" time and outputs the time as shown on the clock.

Exercise: Show that

$\mathbb{Z}\to Clock$ is a homomorphism. (Hint: If you know modular arithmetic this follows from the laws of modular arithmetic you learned. In fact, the laws for computing with arithmetic modulo 12 are equivalent to saying that

$\mathbb{Z}\to Clock$ is a homomorphism.)

Activity: Convince yourself that the reason that the clock works so well is that the function

$\mathbb{Z}\to Clock$ is a homomorphism.

Isomorphisms

Let us come back to our previous discussion of when two structures are the same up to renaming of their elements. Certainly, we want that "being the same" implies that the elements of the structures can be mapped one-to-one, that is, that there is a bijection from one structure to the other. But as the example of the integers and the rationals showed this is not enough. So we will also ask that the bijection is structure preserving. This is then called a isomorphism.

Definition: An isomorphism of

$\mathrm{\Sigma }$-algebras is a bijective homomorphism.

There is a more elegant definition of isomorphism. It is based on the following observation. Recall that a function is bijective if it is injective (one-to-one) and surjective (onto). We write

$id$ to denote the identity function, that is, the function satisfying

$id(x)=x$.

Exercise: Let

$X,Y$ be sets. A function

$f:X\to Y$ is a bijection if and only if there is a function

$g:Y\to X$ such that

$f\circ g=id$ and

$g\circ f=id$.

The observation above emphasises that a bijection is a translation that gives you back what you started with if you translate back and forth (or forth and back).

This is the property that is taken to define isomorphism as it only requires that one has identity arrows and composition of arrows.

Definition:

$f:A\to B$ is an isomorphism if there is

$g:B\to A$ such that

$f\circ g=id$ and

$g\circ f=id$.

Intuitively, two structures are isomorphic, if they are the same up renaming of their elements.

This does not sound very exciting, but we have seen some interesting examples.

Example:

• In the section on normalisation by evaluation, and earlier in the section on meaning in syntax, we have seen how an isomorphism between syntax and semantics can be used to represent faithfully a semantic domain.
• In the section on structure preserving maps we have seen bijections that fail to be isomorphisms for interesting reasons.
• The integers modulo the equivalence relation
  $n\equiv m$ if congruent modulo 12 are isomorphic to the Clock.

Remark: It is important to understand that whether two structures are isomorphic depends on having agreed on what "structure" should consist of. In our current setting, universal algebra, structure is formalised by a signature, that is, the set of operation symbols and their arities.

The following example highlights how being isomorphic depends on the signature. (See the lecture on structure preserving maps for more details on the relationship of integers and rationals.)

Example: If the signature is empty ("no structure"), then

$\mathbb{N}$ and

$\mathbb{Q}$ are isomorphic. If the signature contains addition, then

$\mathbb{N}$ and

$\mathbb{Q}$ are not isomorphic. ^[2]

Universal Properties

In this section, we will see that the term algebra is characterised up to isomorphism by a so-called universal property, called initiality. In other words, the initial algebras are isomorphic to the term algebra, but are defined without reference to syntax.

The category of all

$\mathrm{\Sigma }$-algebras

We make a big step now. So far we only looked at particular algebras.

Now we look at all algebras for a given signature, or, as one says, the category of

$\mathrm{\Sigma }$-algebras. To be more precise, we fix a signature, for example,

$$\mathrm{\Sigma }=\{1,+,\ast \}$$

where, again, 1 is a constant and

$+,\ast$ are binary operation symbols.

We know at least two such algebras, namely

$\mathbb{N}$ and

$\mathbb{Q}$. But there are many more. In fact, there are infinitely many such algebras.

We also met a very special such algebra, namely the term-algebra.

Recall that the term-algebra interpretes

$+,\ast$ as term-constructors. In other words, in the term-algebra all terms are different,

$+,\ast$ do not behave like addition and multiplication. For example, in the term algebra

$1\ast 1$ is not equal to

$1$.

So what is the special property of the term-algbra? What makes the term-algebra interesting if it can't even do addition and multiplication?

The special property of the term-algebra

$\mathcal{L}$ is that the term-algebra is initial, that is, for any other algebra

$A$ of the signature there is one, and only one, homomorphism

$$\mathcal{L}\to A$$

Remark: The property quantifies over all

$\mathrm{\Sigma }$-algebras

$A$, which is why it is called a universal property. Another reason for the name universal property is that it is about an 'object' that has a unique 'arrow' to all other objects. Formulating it in this way, initiality is also universal in the sense that it is not specific to algebras but can be interpreted in any situation where it makes sense to talk about object and arrows. ^[3]

Fact: The term-algebra is, up to isomorphism, the only initial

$\mathrm{\Sigma }$-algebra. ^[4]

Note that the characterisation of the term-algebra as an initial algebra is completely syntax free.

Initial algebras defined

Intial algebras have a simple definition. It only relies on the notions of signature, algebra, and homomorphism.

Definition: Let

$\mathrm{\Sigma }$ be a signature. A

$\mathrm{\Sigma }$-algebra

$I$ is initial if for all

$\mathrm{\Sigma }$-algebras

$A$ there is a unique homomorphism

$I\to A$.

Remark: Universal properties are interesting because they abstract away from the implementation, no terms, or operations, or equations appear in its definition. But this advantage also comes at a price. Just from stating this definition, we do not even know whether an initial algebra exists, nor how they can be implemented. Fortunatley, we have seen in the section on term-algebras above that term-algebras are initial algebras.

Examples:

• If
  $\mathrm{\Sigma }$ is the empty signature, then the initial algebra is the empty set.
• If
  $\mathrm{\Sigma }=\{0,S\}$ and
  $0$ is a constant and
  $S$ is a unary operation symbol, then the natural numbers are the initial algebra.
• Given any signature
  $\mathrm{\Sigma }$ the term-algebra for
  $\mathrm{\Sigma }$ is the initial
  $\mathrm{\Sigma }$-algebra.

Exercise: Verify the statements made in the examples above.

We often talk about "the" initial algebra, even if the initial algebra is not uniquely determined. But all initial algebras are isomorphic.

Proposition: Let

$\mathrm{\Sigma }$ be a signature. Any two initial

$\mathrm{\Sigma }$-algebras are isomorphic.

Exercise: Prove the proposition. (Remark: The proof is short and based on an important idea … but maybe not easy to find if you have never seen it … anyway, give it a try!)

The universal characterisation of induction

We can think of the universal property of initial algebras as an abstract characterisation of induction.

In a nutshell:

• Functions defined by induction are unique homomorphisms from termalgebras.
• Termalgebras are, up to isomomporphism, initial algebras.
• Hence, inductively defined functions are the unique functions guaranteed to exist by initiality.

Let us try to understand this better.

Induction means, in the example of natural numbers, that if I have an element

$z\in \mathbb{N}$ and a function

$s:\mathbb{N}\to \mathbb{N}$, then this defines by induction a unique function

$$h:\mathbb{N}\to \mathbb{N}$$ such that

$h(0)=z$ and

$h(n+1)=s(h(n))$.

More generally, if

$(A,z,s)$ is any algebra with

$z\in A$ and

$s:A\to A$, then this again defines by induction a unique function

$$h:\mathbb{N}\to A$$ such that

$$\begin{array}{rl}h(0)& =z\\ h(n+1)& =s(h(n))\end{array}$$

But now look again at the two conditions

$h(0)=z$ and

$h(n+1)=s(h(n))$. They are exactly saying that

$h$ is an homomorphism for the signature that consists of one constant and one unary operation.

Exercise: Verify the statement that

$h(0)=z$ and

$h(n+1)=s(h(n))$ is exactly saying that

$h$ is a homomorphism for the signature that consists of one constant and one unary operation.

Exercise: Verify that the definition of

$[[-]]:\mathcal{L}\to \mathbb{N}$ is the unique homomorphism from the initial algebra

$\mathcal{L}$ to the algebra

$\mathbb{N}$.

Summary

We are now ready to summarise one of the most important ideas in the semantics of programming languages, namely that initiality "is" induction.

Instead of starting with inductively defined term-algebras, we take their universal property and use it as a definition of initial algebras. We then use induction to prove the existence of initial algebras, the prove revealing initial algebras as term-algebras.

What is the advantage of this shift of perspective from the point of view of programming languages?

In general terms, starting with term-algebras means starting with the implementation. Starting with universal properties such as initiality means starting with the specification. Initiality is the property we want, the term-algebra provides an implementation.

So the abstract formalism we have been learning so far lines up with important principles of good software engineering: Starting from the specification in a language that is close to the specific problem domain instead of committing too early to a particular implementation.

More specifically, in this course, we are currently using term-rewriting based on universal algebra as our model of computation. It has the advantage of being simple, yet powerful. But not all features of programming languages can be modelled in this framework.

The abstract view of induction as initiality has the advantage that it carries over to more complicated models of computation, which go beyond the realm of universal algebra.

So everything we learn here, can be applied later ("scales to more complicated situations"), because we take care of formulating it at the approriate level of abstraction.

---

1. More precisely nodes are either triples

   $(+,p,q)$ or
   $(\ast ,p,q)$ where
   $p,q$ are pointers to children nodes or triples
   $(1,p,q)$ where
   $p,q$ are the null pointer. ↩︎

2. There is a geometric proof that shows that there is no isomorphism preserving addition. Assume that there was such an isomorphism, lining up integers against rationals. Pick two integers/rationals and consider the interval of numbers between them. Start subdividing this interval and continue until you reach a contradiction. ↩︎

3. Technically, what one needs is a collection

   $\mathcal{A}$ of objects and for all objects
   $A,B$ a set
   $\mathcal{A}(A,B)$ of arrows. Moreover, for all
   $A$ there is an identity arrow and arrows can be composed. Such a structure
   $\mathcal{A}$ is known as a category, and category theory is the natural habitat for universal properties. ↩︎

4. We will return to this below. But if you want to prove the claim now, you need to show that any two initial algebras are isomorphic. ↩︎