# Trace monoid
A **trace monoid** (also called a free partially commutative monoid, or a Mazurkiewicz trace monoid after Antoni Mazurkiewicz who introduced them in 1977) is an algebraic structure that captures the notion of concurrent computation. The idea is simple: if two actions in a program do not share any data, the order in which you execute them should not matter. A trace monoid makes this precise by taking the set of all instruction sequences and declaring two sequences equivalent if one can be obtained from the other by repeatedly swapping adjacent independent actions.

## Monoids and why the trace construction gives one

A **monoid** is a triple $(S, \cdot, \varepsilon)$ where $S$ is a set, $\cdot$ is a binary operation on $S$, and $\varepsilon \in S$ is an identity element, satisfying three axioms:

- **Closure**: for all $a, b \in S$, $a \cdot b \in S$.
- **Associativity**: for all $a, b, c \in S$, $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
- **Identity**: for all $a \in S$, $\varepsilon \cdot a = a \cdot \varepsilon = a$.

Strings under concatenation form the simplest example: $(\Sigma^*, \cdot, \varepsilon)$ where $\Sigma^*$ is the set of all finite strings over alphabet $\Sigma$, $\cdot$ is concatenation, and $\varepsilon$ is the empty string. This is the **free monoid** on $\Sigma$.

To build a trace monoid you start with a **dependence alphabet** $(\Sigma, D)$, where $D \subseteq \Sigma \times \Sigma$ is a reflexive and symmetric relation — the dependence relation. Its complement $I = (\Sigma \times \Sigma) \setminus D$ is the **independence relation**: $(a, b) \in I$ means $a$ and $b$ do not interfere and can be executed in either order.

Define a congruence on $\Sigma^*$: two strings are equivalent if one can be transformed into the other by swapping adjacent letters $ab \to ba$ wherever $(a, b) \in I$. The **trace monoid** $\mathbb{M}(\Sigma, I)$ is the quotient:

$$\mathbb{M}(\Sigma, I) = \Sigma^* / \sim_I$$

Each element of $\mathbb{M}(\Sigma, I)$ is an equivalence class $[w]$, called a **trace**.

The three monoid axioms are satisfied:

- **Closure**: concatenating any two representatives $u \in [u]$ and $v \in [v]$ gives a string $uv$; its equivalence class $[uv]$ is well-defined (independent of which representatives you chose) and is again an element of $\mathbb{M}(\Sigma, I)$.
- **Associativity**: $([u] \cdot [v]) \cdot [w] = [uvw] = [u] \cdot ([v] \cdot [w])$, inherited directly from the associativity of concatenation in $\Sigma^*$.
- **Identity**: the trace $[\varepsilon]$ containing only the empty string is the identity — $[\varepsilon] \cdot [w] = [w] = [w] \cdot [\varepsilon]$ for all traces $[w]$.

What distinguishes the trace monoid from the free monoid is that it is not free: the generators do not all commute (only independent pairs do), and it is not a group (traces have no inverses). It sits between the free monoid (no commutativity) and the free commutative monoid (everything commutes).

## Traces of an assembly sequence

Consider four x86 instructions:

```asm
; description: two independent load-and-use chains; eax/ecx chain and ebx/edx chain

mov eax, 1    ; (a)  writes eax
mov ebx, 2    ; (b)  writes ebx
add ecx, eax  ; (c)  reads eax,  writes ecx
add edx, ebx  ; (d)  reads ebx,  writes edx
```

Two instructions are **dependent** if one writes a register that the other reads or writes. The dependence pairs here are $(a, c)$ (instruction $c$ reads `eax` which $a$ writes) and $(b, d)$ (instruction $d$ reads `ebx` which $b$ writes). Everything else is independent:

$$I = \{(a,b),\,(b,a),\,(a,d),\,(d,a),\,(b,c),\,(c,b),\,(c,d),\,(d,c)\}$$

The sequential program is the string $abcd$. Since $(a, b) \in I$, swapping $a$ and $b$ produces an equivalent string. Since $(c, d) \in I$, swapping $c$ and $d$ also produces an equivalent string. The full equivalence class — the trace $[abcd]$ — contains four sequences:

$$[abcd] = \{abcd,\; bacd,\; abdc,\; badc\}$$

Two of those orderings written out explicitly:

```asm
; trace member 1: original order
mov eax, 1
mov ebx, 2
add ecx, eax
add edx, ebx
```

```asm
; trace member 2: swap the two independent loads first
mov ebx, 2
mov eax, 1
add ecx, eax
add edx, ebx
```

Both produce identical register state afterwards. A compiler or out-of-order CPU is free to choose any member of the trace; the observable result is the same. The trace $[abcd]$ is not just a sequence but a partial order: $a$ must precede $c$, and $b$ must precede $d$, but there is no ordering constraint between the two chains.

The connection to concurrency is direct: if $a, b, c, d$ are actions of a concurrent program, any serialisation that respects the partial order encoded in the trace is a valid execution. Trace monoids are the algebraic foundation for Mazurkiewicz trace theory, which gives a precise language for talking about the semantics of concurrent systems without tying behaviour to a specific interleaving.