nLab free monoid

Finite lists and free monoids

Context

Algebra

Induction

Monoid theory

Finite lists and free monoids

Idea

Given a set SS, the free monoid on SS is the set S *S^* of all lists (finite sequences) of elements of SS, made into a monoid via concatenation.

The free functor from Set to Mon takes SS to S *S^*. Combined with its right adjoint forgetful functor this is the list monad whose modules are monoids.

Definitions

We will give three definitions, which can all be shown equivalent.

As functions

An element of S *S^* consists of a natural number nn (possibly n=0n = 0) and function from [n][n] to SS, where [n][n] is the subset {i:N|i<n}\{i\colon \mathbf{N} \;|\; i \lt n\} of N={0,1,2,}\mathbf{N} = \{0, 1, 2, \ldots\}. Such an element is called a list or (to specify nn) nn-tuple of elements of SS. The number nn is called the length of the list.

The empty list is the unique list of length 00. It may be written ()(), **, or ϵ\epsilon, perhaps with a subscript SS if desired.

If n>0n \gt 0, then the list which assigns 0,,n10, \ldots, n - 1 to a 0,a 1,,a n1a_0, a_1, \ldots, a_{n-1} may be written (a 0,a 1,,a n1)(a_0, a_1, \ldots, a_{n-1}). For example, if a,b,ca,b,c are elements of SS, then (a,b,c)(a,b,c) is an element of S *S^*.

Given two lists xx and yy, the former of length mm and the latter of length nn, their concatenation x*yx * y is a list of length m+nm + n, given as follows:

i{x i ifi<m y im ifim i \mapsto \left\{ \array { x_i & if\; i \lt m \\ y_{i-m} & if\; i \geq m } \right.

One can now show that concatenation is associative with the empty list as identity; hence S *S^* is a monoid.

Recursively

The (underlying) set S *S^* may be defined as an inductive type as follows. There are two basic constructors, one with no arguments, and one with two arguments, of which one is an element of SS and the other is an element of S *S^*. By the yoga of inductive types, that is a complete definition, but we spell it out in more detail while also giving terminology and notation.

So, a list is either the empty list or the cons (short for ‘constructor’ and deriving from Lisp) of an element aa of SS and a (previously constructed) list xx. The empty list may may be written ()(), **, or nilnil, perhaps with a subscript SS if desired; the cons of aa and xx may be written a:xa : x, (a)*x(a) * x, or cons(a,x)cons(a,x). We interpret the definition recursively, so we can list the elements of S *S^* in the order in which they appear:

  • ()(),
  • a:()a : (),
  • a:b:()a : b : (),
  • a:b:c:()a : b : c : (),
  • etc.

Here, a,b,c,a, b, c, \ldots are elements of SS. We may continue the ‘etc’ as far as we like, but no farther; while there are lists of arbitrarily long finite length, there are no lists of infinite length. (We would get such lists, however, if we interpreted the definition corecursively, known in computer science as a stream.) We normally abbreviate the lists above as follows:

  • ()(),
  • (a)(a),
  • (a,b)(a,b),
  • (a,b,c)(a,b,c),
  • etc.

We still must define the monoidal structure on S *S^*; we define the concatenation x*yx * y of xx and yy recursively in xx. To be explicit:

  • ()*y=y() * y = y;
  • (a:x)*y=a:(x*y)(a : x) * y = a : (x * y) (with parentheses for grouping, but the parentheses can be dropped now that have this definition).

One can now show that concatenation is associative with the empty list as identity; hence S *S^* is a monoid.

By general abstract nonsense

To prove that the category Mon of monoids is a complete category, one normally shows that the forgetful functor UU (from MonMon to the category Set of sets) preserves all limits. Then, the adjoint functor theorem defines a left adjoint to UU if a size condition is met; this adjoint is the functor ** that takes a set to its free monoid S *S^*.

To be sure, meeting the solution set condition basically requires starting the constructions in one of the other definitions above; but the proofs may all be thrown onto the adjoint functor theorem.

Another abstract approach is given in the following general theorem, which applies to more general monoids in a monoidal category:

Theorem

Suppose CC is a monoidal category with countable coproducts for which the tensor product distributes over countable coproducts (for example, a cocomplete monoidal biclosed category). Then a left adjoint to the forgetful functor Mon(C)CMon(C) \to C exists, taking an object cc to

n0c n,\sum_{n \geq 0} c^{\otimes n},

which thereby becomes the free monoid on cc.

This applies immediately to C=SetC = Set, as this is a cocomplete cartesian closed category.

In dependent type theory

In a general dependent type theory where we do not assume uniqueness of identity proofs, the free monoid on a type AA is the 0-truncation of the type of lists of AA, FreeMonoid(A)[List(A)] 0\mathrm{FreeMonoid}(A) \coloneqq [\mathrm{List}(A)]_0. This is because in any dependent type theory with uniqueness of identity proofs, where every type is 0-truncated, the type of lists of AA is the free monoid of AA.

Alternatively, the free monoid on AA can be constructed via the James construction type of AA.

Examples

  • If SS is the empty set, then S *S^* consists only of the empty list; it is the trivial monoid, one manifestation of the point.

  • If SS is the point, then S *S^* is N\mathbf{N}; the only information in a list of indistinguishable points is the length of the list. The monoid operation on N\mathbf{N} is addition.

  • If SS is N\mathbf{N}, then N *\mathbf{N}^* is still a denumerable set. But note that NN *\mathbf{N} \cong \mathbf{N}^* only as sets (that is, |N *|=|N|= 0{|\mathbf{N}^*|} = {|\mathbf{N}|} = \aleph_0 as cardinal numbers); they are quite different as monoids.

  • Generalising the above, |S *|=|S|{|S^*|} = {|S|} if SS is an infinite set, or more generally |S *|=max( 0,S){|S^*|} = max(\aleph_0,S) if SS is an inhabited set. (These theorems probably require the axiom of choice, but I haven't checked thoroughly.)

In computer science, the free monoid on a given alphabet is the categorical semantics for the data typeString” with characters in that alphabet.

The free monoid monad

If the free monoid functor F:SetMonF\colon Set \to Mon is followed by the forgetful functor U:MonSetU\colon Mon \to Set, then we get a monad on SetSet. This monad is very important as a monad in computer science, where it is known as the list monad.

The list monad bears the same relation to multicategories as the identity monad on SetSet bears to ordinary categories. This relation should be explained at generalized multicategory.

Foundational relevance

Every definition of free monoid makes use of some form of axiom of infinity, either N\mathbf{N} directly or the ability to form general inductive types. Indeed, as N=pt *\mathbf{N} = pt^*, the axiom of infinity follows from the existence of free monoids.

In topos theory the equivalent of the above theorem is due to C. J. Mikkelsen:

Proposition

Let 𝒮\mathcal{S} be a topos and mon(𝒮)\mathbf{mon}(\mathcal{S}) its category of internal monoids. Then 𝒮\mathcal{S} has a NNO precisely if the forgetful functor U:mon(𝒮)𝒮U:\mathbf{mon}(\mathcal{S})\to \mathcal{S} has a left adjoint.

For a proof see Johnstone (1977,p.190).

Furthermore then it is a theorem due to Andreas Blass (1989) that 𝒮\mathcal{S} has a NNO precisely if 𝒮\mathcal{S} has an object classifier 𝒮[𝕆]\mathcal{S}[\mathbb{O}].

A consequence of this, discussed in sec. B4.2 of (Johnstone 2002,I p.431), is that classifying toposes for geometric theories over 𝒮\mathcal{S} exist precisely if 𝒮\mathcal{S} has a NNO.

From a different perspective then, in a topos the existence of free objects over various gadgets like e.g. algebraic theories or geometric theories often hinge on the existence of free monoids, the intuition being that the free monoids permit to construct a free model syntactically by providing for the (syntactic) building blocks needed for this process.

Notice that algebraic theories can nevertheless have free algebras even if the ambient topos lacks a NNO. This may happen for algebraic theories that have the property that the free algebra on a finite set of generators has a finite carrier e.g. in the topos FinSetFinSet of finite sets free graphic monoids exist, and free Boolean algebras exist.

Stacks and queues

In computer science, lists often appear as stacks (not to be confused with the stacks from higher sheaf theory) and queues.

Fix a monoidal category that has coproducts with the unit object II. Given an object AA, an object of stacks on AA is an object S AS_A equipped with morphisms push A:S AAS Apush_A\colon S_A \otimes A \to S_A and pop A:S AS AA+Ipop_A\colon S_A \to S_A \otimes A + I such that these diagrams commute:

S AA ι S AA,I S AA+I push A pop A push A+id I S A ι S AA,I S A+I \array { S_A \otimes A & & \overset{\iota_{S_A \otimes A,I}}\to & & S_A \otimes A + I \\ & {}_{push_A}\searrow & & \nearrow_{pop_A} & & \searrow^{push_A + id_I} \\ & & S_A & & \underset{\iota_{S_A \otimes A,I}}\to & & S_A + I }

The idea is that push Apush_A and pop Apop_A are as close to inverses as reasonably possible, but pop Apop_A takes us to S AA+IS_A \otimes A + I rather than to S AAS_A \otimes A, because of the empty stack.

Queues are a little more complicated. An object of queues on AA is an object Q AQ_A equipped with morphisms ins A:AQ AQ Ains_A\colon A \otimes Q_A \to Q_A (‘insert’) and rem A:Q AQ AA+Irem_A\colon Q_A \to Q_A \otimes A + I (‘remove’). These operations are far from inverses; whereas popping a stack returns the last item to be pushed onto it, removing an item from a queue returns the first item to have been inserted into it.

What are the diagrams for this? I seem to recall that we need a distributive category; in particular, we need a cartesian monoidal category, so that \otimes is ×\times. But perhaps a 2-rig will be sufficient?

References

  • Jean Bénabou, Some Remarks on Free Monoids in a Topos , pp.20-29 in LNM 1488 Springer Heidelberg 1991.

  • Andreas Blass, Classifying topoi and the axiom of infinity , Algebra Universalis 26 (1989) pp.341-345.

  • Peter Johnstone, Topos Theory, Academic Press New York 1977. (Dover reprint Minneola 2014, chap. 6)

The list monad as a monad in computer science:

Last revised on December 23, 2023 at 18:48:10. See the history of this page for a list of all contributions to it.