Differences
This shows you the differences between two versions of the page.
sav08:unification [2008/04/02 20:29] vkuncak |
sav08:unification [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Unification ====== | ||
- | |||
- | |||
- | Unification is the process of solving equations in term algebra, which is the algebra of ground terms, with functions defined as in the [[Ground Terms]] section of proof of Herbrand theorem. | ||
- | |||
- | The solution process is essentially variable elimination, based on two main properties | ||
- | * equation $f(t_1,\ldots,t_n) \doteq f(s_1,\ldots,s_n)$ ++| is equivalent to system $t_1 \doteq s_1,\ldots,t_n \doteq s_n$++ | ||
- | * equation $f(t_1,\ldots,t_n) \doteq g(s_1,\ldots,s_m)$ where $f \neq g$ ++| is contradictory++ | ||
- | * equation $x \doteq t(x)$ where $t$ is a term containing $x$ but not identical to $x$ ++| is contradictory++ | ||
- | |||
- | ===== Unification Examples ===== | ||
- | |||
- | First-order language: | ||
- | * $R$ - binary relation symbol | ||
- | * $f$ - binary function symbol | ||
- | * $a,b,c$ - constants | ||
- | * $x,y,z,u,v,w$ - variables | ||
- | |||
- | **Example 1** | ||
- | |||
- | \[ | ||
- | R(x,f(x,y)) \doteq R(f(a,v),f(f(u,b),f(u,u))) | ||
- | \] | ||
- | |||
- | **Example 2** | ||
- | |||
- | \[ | ||
- | R(x,f(x,x)) \doteq R(f(a,v),f(f(u,b),f(u,u))) | ||
- | \] | ||
- | |||
- | **Example 3** | ||
- | |||
- | \[ | ||
- | R(x,f(x,y)) \doteq R(f(u,v),v) | ||
- | \] | ||
- | |||
- | **Definition:** Unifier of a set $E$ of syntactic equations is a substitution that makes all equations true. | ||
- | |||
- | **Definition:** Composition $\circ$ of substitutions. | ||
- | |||
- | **Definition:** A //renaming// is a substitution which, viewed as relation, is a total function and a bijection on the set of all variables. | ||
- | |||
- | **Lemma:** If $\sigma$ is a unifier for $E$ and $\tau$ is a substitution, then $\tau \circ \sigma$ is also a unifier. | ||
- | |||
- | A unifier is a solution of equations. mgu is the most general solution. | ||
- | |||
- | **Definition:** A most general unifier for $E$ is a unifier $\sigma$ such that if $\sigma'$ is another unifier, then there exists a substitution $\tau$ such that $\sigma' = \tau \circ \sigma$. | ||
- | |||
- | ===== Algorithm ===== | ||
- | |||
- | We next sketch an algorithm for computing mgu. | ||
- | |||
- | 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 | ||
- | \[ | ||
- | \{x_1,\ldots,x_n \} \cap (FV(t_1) \cup \ldots FV(t_n)) = \emptyset | ||
- | \] | ||
- | |||
- | 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. | ||
- | |||
- | === Orient === | ||
- | |||
- | Select $t \doteq x$ where t is not x, and replace it with $x \doteq t$. | ||
- | |||
- | === Delete === | ||
- | |||
- | Select $x \doteq x$, remove it. | ||
- | |||
- | === Eliminate === | ||
- | |||
- | Given $x \doteq t$ where $x$ does not occur in $t$, substitute $x$ with $t$ in all remaining equations. | ||
- | |||
- | === Occurs Check === | ||
- | |||
- | Given $x \doteq t$ where $x$ occurs in $t$, report clash. | ||
- | |||
- | === Decomposition === | ||
- | |||
- | Given $f(t_1,\ldots,t_n) \doteq f(s_1,\ldots,s_n)$, replace it with $t_1 \doteq s_1,\ldots,t_n \doteq s_n$. | ||
- | |||
- | === Decomposition Clash === | ||
- | |||
- | Given $f(t_1,\ldots,t_n) \doteq g(s_1,\ldots,s_m)$ for $f$ not $g$, report clash | ||
- | |||
- | ===== 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://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]] | ||