A *Term Rewriting System* (TRS) is a very powerful yet simple math tool used, for instance, for the creation of computational models. Given a set of function symbols **S**, and an (uncountable) set of variables **V**, I will define *rewriting rule* by example.

Suppose we have the "constant" function (function without parameters) **0** (representing a 0 in the natural numbers), the unary function **S** (as the successor of a number), and the binary function **+** (as the add operation). Let **x** and **y** be in **V**.** **These are rewriting rules to compute the add of two numbers:

0 + x → x

S(x) + y → x + S(y)

The arrow can be seen as a "rewrite as" relation. For example, S(S(0)) + S(0) rewrites by the second rule to S(0) + S(S(0)), then to 0 + S(S(S(0))), to achieve the final computation with the first rule: S(S(S(0))). And this is exacty what we expected: 2+1 = 3. Yeah, I know that it doesn't look like a very big science discovery, but we will soon see that with more complex rules we are going to be able to compute anything.