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.