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 о = {x1 ^ s1,...,xm ^ sm}. SF,X denotes the set of all substitutions. The application of the substitution о to a term t, denoted , is defined by induction on the structure of terms

The substitution e = {} with te = t for all terms t in TF,X is called the identity. A substitution о = {x1 ^ s1,...,xm ^ sm} has the finite 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 о ={x1 ^ s1; x2 ^ s2,..., x ^ sm}, is often rewritten into “triangle form” [8]:

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 RV, and defined as aRVт xaRxt for all x in V. Two substitutions a and в are equal, denoted a = в iff xa = xв for every variable x, they are equal restricted to V xa =Vxe, iff xa = xв for all variables x in V.

< Prev   CONTENTS   Source   Next >