# Term Rewriting vs Unification

How is term rewriting different from unification, and what's the difference between term rewriting languages and logic programming, like Prolog?

Term rewriting is a rewriting formalism. Starting with a term we rewrite the term according to the term rewriting rules until a normal form is found. Unification is finding a solution (substitution with specific properties) to a problem (a pair of terms).

Term rewriting uses a notion called "pattern matching". What you probably meant is: what is the difference between matching and unification?

Let two terms $t_1$ and $t_2$ be given.

If we want to unify $t_1$ and $t_2$, we search for a substitution $\sigma$ such that $t_1\sigma = t_2\sigma$. On the other hand, if we want to match $t_1$ into $t_2$, we are looking for a substitution such that $t_1\sigma = t_2$. That is, we apply the substitution only on $t_1$.

Logic programming is a programming paradigm which is based on resolution, which is a proof method for logics. In logic programming unification plays an important role.

• I was also thinking about differences between matching and unification. nice answer.
– alim
Nov 25, 2016 at 14:33
• So, matching is a special case of unification, right?
– alim
Nov 25, 2016 at 14:43
• could it be said that unification and term rewriting are two sides of the same coin/cycle? in Prolog, term rewriting needs to find terms to rewrite, which relies on unification, and once a term is rewritten, it continues in the unification process again. Feb 26, 2022 at 7:10
• @alim most languages do pattern matching without unification, see for example: stackoverflow.com/questions/4442314/… Feb 26, 2022 at 7:17