Universal algebra is an area of mathematics that is important to programming languages for many reasons.
Universal algebra provides the mathematical environment to talk about
Universal algebra provides the easiest examples for important ideas in the semantics of programming languages such as types, homomorphisms, free constructions, syntax, semantics, soundness, completeness, term rewriting, normal forms and many more
Universal algebra has many ramifications in computer science (we will hear more about abstract data types in this lecture and maybe more about process algebras in a later lecture):
The aim of this lecture is to introduce some mathematical notions that provide useful tools for what is to follow later in the course.
If we look at what we have done so far, we find that our mathematical tools are not powerful enough to go further. I point out two areas of limitations.
The example language we studied
exp ::= 1 | exp + exp | exp * exp
is not even the full language o arithmetic. Most importantly, variables are missing.
So far the methods we developed for "rewriting as a model of computation" only deal with abstract reduction systems min
, max
, sort
, insert
) and variables.
We therefore should be interested in the area of mathematics that deals with variables, terms, and equations. It is called Universal Algebra.
Later we will consider directed equations, leading us from Universal Algebra to Term Rewriting. After this, we will then add functions as first-class citizens, which gives us
Universal Algebra is the area of mathematics that studies, from a general point of view, sets with operations.
There are many reasons why universal algebra is interesting, even foundational, for computer science and we discussed some of them. Most important for this lecture are the following.
Universal algebra
We already know many algebras.
Notation: For brevity, we write the above algebras as
What do they all have in common?
From a general point of view (and universal algebra is indeed called general algebra by many authors), we say that an algebra is any set equipped with a number of operations.
Above, all operations are either constants (which take 0 arguments) or binary operations (which take 2 arguments).
But in general, we want to allow operations with any number
Universal algebra does not study particular algebras, such as the integers with addition and multiplication, but classes of algebras. To get a handle of this one starts with the notion of signature.
Def: A signature is a set
Example: In most of the examples above the signature consists of one constant (= 0-ary operation symbol) and one binary operation symbol. In some cases, there are two constants and/or two binary operation symbols. But in general a signature can contain any number of operation symbols of any arity.
Each signature gives rise to a class of algebras that "implement" the operation symbols specified by the signature.
Def: An algebra for a signature
Notation: Conceptually, it is important to distinguish syntax from semantics and to distinguish the operation symbols of the signature form the operations of the algebra. In more detail, if
Example: The algebras
So what makes these two algebras different?
Certainly that the symbols
The interesting difference is that they satisfy different equations. For example,
So could we say that the meaning of the operations is defined by the equations they satisfy?
This is certainly the point of view taken by universal algebra.
Actually, this is not a new idea for us, we encountered it already in the lectures on syntax and semantics, see here for the first, second and third.
And this connection is one reason why are interested in universal algebra.
But what are equations?
As we know from high-school algebra equations contain variables. So we first must answer
What are variables?
But before we come to that I want to present the idea of
For a mathematician, algebras are sets with operations. To a computer scientist, algebras are abstract data types. We first present an example of a data type as a set and then argue that this set only becomes a proper data type after we "upgraded" it to an algebra.
First we need a set of data. Let us assume that we have a set
Such data is then called an
What is a short way of writing down the set of all tuples?
First note that
where
So the set of all tuples is the union (or sum) of all
Remark: You know a similar notation from high-school algebra. For example, the geometric series is written as
To summarise, we presented an example of a data type, the type of tuples of arbitrary length, as a set and took some time to introduce standard notation from set theory/type theory to describe it in succinct notation.
Next we explain why data types are more than sets, why it is useful to think about them as algebras.
The set
may not look much like a data type to you. But this is why I have chosen this notation. We will see that there are many different data types that are based on this same set of elements.
Let us think about datatypes you know that are based on
and there must be many more.
So what distinguishes these datatypes if they all have the same set of data?
One answer could be that, for example, linked lists and arrays are implemented in very different ways. In class we discussed this in some detail and here is a video I found on the internet which roughly covers the same points.
But in a course on "Programming Langauges" it is interesting to find ways of distinguishing lists and arrays, or other data types, in a way that is indpendent of particular implementations and languages.
Our first answer, then, is that we can distinguish different data types on the same underlying set of data by the different operations they provide to the programmer.
Let us run through some examples.
Lists have basic operations
nil: List
cons: Elem x List -> List
and then everything that can be defined by induction on nil
and cons
such as
isempty: List -> Bool
append: List x List -> List
and much more.
Arrays have basic operations
get: Array x Nat -> Elem
put: Array x Nat x Elem -> Array
Stacks have basic operations [2]
pop: Stack -> Stack
top: Stack -> Elem
and more that can be defined from them such as [3]
nil: Stack
push: Stack x Elem -> Stack
As these examples show, many different datatypes can have the same underlying set, but are distinguished by the operations they support, or, in algebraic terms, by their signature.
The above signature for stacks could also be used for fifo-queues. The fact that we might want to name the operations then differently is not important. Let us agree that, when talking about queues, fifo or lifo, we name the operations
nil: Queue
enqueue: Queue x Elem -> Queue
dequeue: Queue -> Queue
head: Stack -> Elem
The operation head
may also be called front
(for fifo) or end
(for lifo), but here we want to emphasize that both lifo and fifo are based on the same set and the same signature.
Nevertheless, their difference does show up in an implementation-independent, purely algebraic way, namely in the equations that hold for them.
For example, for lifo we have
dequeue(enqueue(s,e)) = s
head(enqueue(s,e)) = e
which do not hold for fifo.
To summarise, we see that the notions of signature, algebras and equations all make sense for data types.
One benefit we get from this is that we can distinguish different data types abstractly without having to consider any particular programming language or implementation.
This approach to data structures is called abstract data types.
The only, very small, modification we need to make to our definitions of signature and algebra to accommodate abstract data types is to allow, instead of just one set, a family of sets. For example, the type array was based on sets Array
, Nat
, Elem
.
This leads to many-sorted universal algebra, but many-sorted universal algebra is both conceptually and technically so similar to (one-sorted) universal algebra that it is not worth to elaborate this point in this course.
After this excursion on abstract data types, let us go back to the main thread of thought. We said that we first have to understand variables.
To see how to implement abstract data types as Java classes, the following book contains all the details about arrays, vectors, hash tables, lists, stacks, queues, and various forms of trees:
Jenkins: Abstract Data Types in Java (1998)
We will later learn about algebraic data types, see for an interesting
discussion about algebraic data types at stackexchange.
This seems all quite complicated compared to the simplicity of algebraic data types in languages such as Haskell, so it is no surprise that there are extensions of Java with algebraic data types, for example Pizza. The following page also contains a tutorial of how to implement algebraic data types in Java.
Pizza is not developed any more, but the generics introduced by Pizza, and then Generic Java are part of Java 5 since 2004, see the official Java tutorial on generics:
Generics in Java (Recommended reading for Java programmers.)
A further tutorial with examples of generics in Java.
This analogy is not a coincidence but at the heart of a deep connection between combinatorics and set theory (via category theory). Let me know if you are interested to hear more about this … ↩︎
Actually, taking a closer look, we find that pop
and top
are not functions, but only partial functions as they are not defined if the stack is empty. There are various ways, to extend the universal algebra we present by allowing for partial functions, but we will ignore this for our treatment. But there is no principled reason why one couldn't account for partiality. ↩︎
While both List
and Stack
can be considered as supporting the four operations of nil
, cons
, pop
, top
one can argue that they differ in the sense that lists have basic operations nil
and cons
with pop
and top
defined inductively, while stacks have basic operations pop
and top
with nil
and cons
define co-inductively. Unfortunately, we will probably not have time to explain the difference of induction and co-induction. ↩︎