Meaning of Free (Arbitrary Abstract Algebra Term)

Question

I'm currently learning abstract algebra and the word free appears (free monoid, free vector space) throughout different literatures. Is there a general (and simple) definition of the word (and possibly examples in functional programming) or is it merely a highly overloaded word? Many Thanks!

Answer 1

Yes, and in fact there is even a general notion of an algebraic theory, and thus algebraic object. An algebraic theory consists of:

• a sort
• constants and function symbols
• algebraic axioms, that is universally quantified sentences which may contain equality, but no other logical symbols (ie. $\exists,\vee,\to,\neg$)

It is worth noting that the theory of fields is not algebraic, thus there are no free fields.

So the theory of monoids $\mathcal M$ has a sort $M$, constant $e : M$, function symbol $\mu:G\times G\to G$, and axioms

• $\forall x.\mu(x,e)=x$
• $\forall x.\mu(e,x)=x$
• $\forall x,y,z.\mu(\mu(x,y),z)=\mu(x,\mu(y,z))$

In general, given an algebraic theory $T$ we may consider the set of terms in this theory. Categorically, a free algebra for $T$ is the initial object in the category of algebras for $T$. The standard way to construct the free algebra is to take the term model for $T$, that is the underlying set of the free algebra is the set of terms of $T$ modulo the equivalence relation generated by the axioms of $T$.

So what we mean by a free structure in the theory $T$ generated by the set $B$, is to consider a free algebra for the theory $T_B$ containing an additional constant symbol for each element of $B$.

This description is concrete but a bit complicated. There is a much simpler but more abstract construction using the theory of monads, because an algebraic theory corresponds precisely to a monad.

---

An example for monoids in a functional programming language could look as follows, by interpreting the theory of monoids as a monad:

type 'a mon =  
| Id
| Bin of 'a mon * 'a mon
| Var of 'a

let return (x : 'a) : 'a mon = Var x

let rec bind (x : 'a mon) (f : 'a -> 'b mon) : 'b mon =
match x with
| Id -> Id
| Bin (s,t) -> Bin (bind s f, bind t f)
| Var u -> f u

let rec eq (a_eq : 'a -> 'a -> bool) (s : 'a mon) (t : 'a mon) : bool =
match (s,t) with
| (Bin (Id,u), v) | (Bin (u,Id), v) | (u, Bin (Id,v)) | (u, Bin (v,Id)) -> eq u v
| (Bin (Bin (u1,u2),u3), v) -> eq (Bin u1, Bin (u2,u3)) v
| (u, Bin (Bin (v1,v2),v3)) -> eq u (Bin v1, Bin (v2,v3))
| (Id,Id) -> true
| (Bin (u1,v1), Bin (u2,v2)) -> (eq u1 u2) && (eq v1 v2)
| (Var x, Var y) -> a_eq x y
| _ -> false


type two = A | B

let two_eq x y : bool = 
match (x,y) with
| (A,A) | (B,B) -> true
| _ -> false

Then the type two mon with relation eq two_eq gives the free monoid on two elements.

The function return : two -> two mon gives us the two generators return A and return B.

The function bind : two mon -> (two -> 'b mon) -> 'b mon tells us that a map from the free monoid on two elements to another (in this case free) monoid is uniquely determined by what the elements of two are mapped to.