Abstract Reduction Systems

An Abstract Reduction System (ARS) is the simplest possible "things that
rewrite" model: a pair $\langle A, \to \rangle$ where:

• $A$ is a set (the things you can rewrite)
• $\to \subseteq A \times A$ is a binary relation (the one-step reduction)

The reflexive-transitive closure $\to^*$ captures "reduces in zero or more
steps". Sometimes we write $\to^1$ to be explicit about the one-step relation.

Difference from transition systems. A transition system has THREE
components (states, actions, transitions). An ARS has TWO (a set, a relation).
You can recover the actions by labelling the relation, but the ARS is purely
about reachability: given $a$, which $b$ can you reach? This is a useful
abstraction when the actions don't matter — only the structure of rewriting
does.

Examples of ARS:
- Arithmetic simplification: $2 + 2 \to 4$
- Lambda calculus: $(\lambda x. x) y \to y$
- Unification: a substitution $\sigma$ reduces a formula by applying it
- Term rewriting: $x + 0 \to x$
- Grammar derivation (from Ch7!): $S \Rightarrow aSb$

Observation. Every ARS $\langle A, \to \rangle$ is the same thing as a
directed graph with vertex set $A$ and edge set $\to$. The reverse is also
true: any directed graph can be viewed as an ARS.

The point of using ARS instead of "just a graph" is that ARS comes with
terminology and theorems (confluence, termination, Newman's lemma) that we
study next.