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


1 Answer 1


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.

  • $\begingroup$ I was also thinking about differences between matching and unification. nice answer. $\endgroup$
    – alim
    Commented Nov 25, 2016 at 14:33
  • 2
    $\begingroup$ So, matching is a special case of unification, right? $\endgroup$
    – alim
    Commented Nov 25, 2016 at 14:43
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Feb 26, 2022 at 7:10
  • $\begingroup$ @alim most languages do pattern matching without unification, see for example: stackoverflow.com/questions/4442314/… $\endgroup$ Commented Feb 26, 2022 at 7:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.