Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:unification [2008/04/02 20:27] vkuncak |
sav08:unification [2008/04/02 20:29] vkuncak |
||
|---|---|---|---|
| Line 39: | Line 39: | ||
| **Definition:** Composition $\circ$ of substitutions. | **Definition:** Composition $\circ$ of substitutions. | ||
| - | **Definition:** A //renaming// is substitution whose domain and codomain are variables, and which is injective. | + | **Definition:** A //renaming// is a substitution which 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. | **Lemma:** If $\sigma$ is a unifier for $E$ and $\tau$ is a substitution, then $\tau \circ \sigma$ is also a unifier. | ||