# Substitutions

A *substitution* is a (unique) homomorphism in the term algebra generated by a mapping *о : X* —> *T(F, X)* from a finite set of variables to terms. Substitutions are generally denoted by small Greek letters *а, в, у, о* etc. and they are represented explicitly as a function by a set of variable bindings *о = {x** _{1}* ^

*s*

_{1}*,...,x*^

_{m}*s*}.

_{m}*S*denotes the set of all substitutions. The application of the substitution

_{F},_{X}*о*to a term

*t*, denoted

*tо*, is defined by induction on the structure of terms

The substitution *e* = {} with *te = t* for all terms *t* in *T _{F},_{X}* is called the

*identity.*A substitution

*о = {x*

*^*

_{1}*s*

_{1}*,...,x*^

_{m}*s*has the finite

_{m}}*domain:*

The *range* is the set of terms

The set of variables occurring in the range is УКап(о) := Var(Кап(о)) and Var*(о) =* Бош(о) U УКап(о). The *restriction* of a substitution *о* to a set of variables *Y* с *X*, denoted by *о _{Y}*, is the substitution which is equal to the identity everywhere except over

*Y*П Бош(о), where it is equal to

*о*. The

*composition*of two substitutions

*о*and

*в*is written

*о о в*(to emphasize the composition) or just as

*об*and its application is defined by

*tов = (tо)в.*This is fine if

*ов*has no contradictory variable bindings, otherwise if

*xо = xб*for some variable x, this binding in

*б*is applied to

*о*and eliminated in

*об,*(see [8] p. 451, for details). A substitution

*о*is

*idempotent*if

*оо = о*and this is true iff

*Dom(о)*П

*VRan(о) =*0. The application of a substitution to a term can be tricky, if it is not idempotent, for example if it contains infinite cycles or contradictory bindings, and there are several solutions proposed for this problem in the literature. In the area of automated reasoning there is the convention that the variables in

*si*are always renamed into new variables and contradictory bindings are removed. If

*о*is not idempotent, then the set representation of a substitution is inadequate, as the application order of the individual bindings matters. In that case

*о ={x*

*^ s*

_{1}_{1;}x

_{2}^

*s*

_{2}*,..., x*^

*s*}, is often rewritten into “triangle form” [8]:

_{m}and then applied sequentially and component wise, sometimes called dag solvent form.

Relations such as =, A — between substitutions sometimes hold only if they are restricted to a certain set of variables *V*. A relation *R* which is restricted to *V* is denoted as *R ^{V}*, and defined as

*aR*Rxt for all x in V. Two substitutions

^{V}т xa*a*and

*в*are

*equal,*denoted

*a = в*iff

*xa = xв*for every variable

*x*, they are

*equal restricted to V xa*=

^{V}xe, iff

*xa = xв*for all variables x in V.