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.

  • $\begingroup$ I was also thinking about differences between matching and unification. nice answer. $\endgroup$ – alim Nov 25 '16 at 14:33
  • 1
    $\begingroup$ So, matching is a special case of unification, right? $\endgroup$ – alim Nov 25 '16 at 14:43
  • $\begingroup$ Can it be said that unification is sort of like matching in both directions? $\endgroup$ – Erik Kaplun Feb 2 at 11:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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