Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:unification [2008/04/02 20:29] vkuncak |
sav08:unification [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 9: | Line 9: | ||
* equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$ ++| is contradictory++ | * equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$ ++| is contradictory++ | ||
- | ===== Unification Examples ===== | + | ===== Examples ===== |
First-order language: | First-order language: | ||
Line 19: | Line 19: | ||
**Example 1** | **Example 1** | ||
- | \[ | + | \begin{equation*} |
R(x,f(x,y)) \doteq R(f(a,v),f(f(u,b),f(u,u))) | R(x,f(x,y)) \doteq R(f(a,v),f(f(u,b),f(u,u))) | ||
- | \] | + | \end{equation*} |
**Example 2** | **Example 2** | ||
- | \[ | + | \begin{equation*} |
R(x,f(x,x)) \doteq R(f(a,v),f(f(u,b),f(u,u))) | R(x,f(x,x)) \doteq R(f(a,v),f(f(u,b),f(u,u))) | ||
- | \] | + | \end{equation*} |
**Example 3** | **Example 3** | ||
- | \[ | + | \begin{equation*} |
R(x,f(x,y)) \doteq R(f(u,v),v) | R(x,f(x,y)) \doteq R(f(u,v),v) | ||
- | \] | + | \end{equation*} |
**Definition:** Unifier of a set $E$ of syntactic equations is a substitution that makes all equations true. | **Definition:** Unifier of a set $E$ of syntactic equations is a substitution that makes all equations true. | ||
Line 52: | Line 52: | ||
A set of equations is in //solved form// if it is of the form $\{ x_1 \doteq t_1,\ldots, x_n \doteq t_n \}$ iff variables $x_i$ do not appear in terms $t_j$, that is | A set of equations is in //solved form// if it is of the form $\{ x_1 \doteq t_1,\ldots, x_n \doteq t_n \}$ iff variables $x_i$ do not appear in terms $t_j$, that is | ||
- | \[ | + | \begin{equation*} |
\{x_1,\ldots,x_n \} \cap (FV(t_1) \cup \ldots FV(t_n)) = \emptyset | \{x_1,\ldots,x_n \} \cap (FV(t_1) \cup \ldots FV(t_n)) = \emptyset | ||
- | \] | + | \end{equation*} |
We obtain a solved form in finite time using the non-deterministic algorithm that applies the following rules as long as no clash is reported and as long as the equations are not in solved form. | We obtain a solved form in finite time using the non-deterministic algorithm that applies the following rules as long as no clash is reported and as long as the equations are not in solved form. | ||
Line 84: | Line 84: | ||
===== References ===== | ===== References ===== | ||
- | * [[http://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf|Unification Theory Chapter in Handbook of Automated Reasoning]] (also {{sav08:unification-handbook.pdf|pdf file}}) | + | * [[http://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf|Unification Theory Chapter in Handbook of Automated Reasoning]] (also {{sav08:unification-handbook.pdf|pdf file}}, see pdf page 10, Rule based approach) |
* [[http://doi.acm.org/10.1145/357162.357169|An Efficient Unification Algorithm]] (also {{sav08:unification-p258-martelli.pdf|pdf file}}) | * [[http://doi.acm.org/10.1145/357162.357169|An Efficient Unification Algorithm]] (also {{sav08:unification-p258-martelli.pdf|pdf file}}) | ||
* [[http://www.mpi-inf.mpg.de/~uwe/lehre/eqlogic/v5.pdf|Course at MPI]] | * [[http://www.mpi-inf.mpg.de/~uwe/lehre/eqlogic/v5.pdf|Course at MPI]] | ||