How is term rewriting different from unification, and what's the difference between term rewriting languages and logic programming, like Prolog?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
4
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$– alimNov 25, 2016 at 14:33
-
2$\begingroup$ So, matching is a special case of unification, right? $\endgroup$– alimNov 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$ Feb 26, 2022 at 7:10
-
$\begingroup$ @alim most languages do pattern matching without unification, see for example: stackoverflow.com/questions/4442314/… $\endgroup$ Feb 26, 2022 at 7:17