2
$\begingroup$

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!

$\endgroup$
1
  • 7
    $\begingroup$ There's a precise meaning: see the Wikipedia article on free objects as a starting point. The definition itself is a little abstract, but the intuitive idea is simple: it's the algebraic structure generated from a signature without any additional axioms imposed. $\endgroup$
    – varkor
    Commented Jan 24, 2021 at 2:20

1 Answer 1

2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.