Definition of linear and renaming substitution

74 Views Asked by At

Wikipedia's article on substitution defines linear substitution as follows:

A substitution $σ$ is called a linear substitution if $tσ$ is a linear term for some (and hence every) linear term $t$ containing precisely the variables of $σ$'s domain, i.e. with $vars(t) = dom(σ)$.

The same article provides the following definition of renaming substitutions:

A substitution $σ$ is called a renaming substitution if it is a permutation on the set of all variables.

It seems that both definitions come from Baader et Snyder, Unification Theory, pp. 439–526. Therefore, the substitution $\{x \mapsto a, y \mapsto b\}$ is flat and linear, but not renaming, since it maps both variables $x$ and $a$ to $a$ and both variables $y$ and $b$ to $b$. The renaming substitution, as the definition clearly states, must be a permutation on the set of all variables, for instance, the substitution $\{x \mapsto a, y \mapsto b, a \mapsto y, b \mapsto x\}$.

Reading other resources, I found alternative definitions for the renaming substitution. According to Burghardt et Heinz, Implementing Anti–Unification Modulo Equational Theory, p. 6, for example, renaming substitutions are bijective (flat and linear) mappings from variables to variables. According to Nienhuys-Cheng et de Wolf, Foundations of Inductive Logic Programming, p. 52, the substitution $\sigma$ is renaming for a formula $P$, if all $x_0\neq x_1$ in the domain of $\sigma$ occur in $P$ and the variables $x_0\sigma \neq x_1\sigma$ either are equal to some $x$ in the domain of $\sigma$ or do not occur in $P$.

As far as I understood, the two alternative definitions allow a substitution to be renaming for a given formula, but not for others. For example, the substitution $\{x \mapsto a, y \mapsto b\}$ is renaming for the formula $P(x,y)$, but it is not renaming for $P(x,y,a,b)$. The Wikipedia definition only considers the existence of, so to speak, "absolute" renaming substitutions, i.e. substitutions that are renaming for any formula.

In my opinion, it all comes down to the definition of linear substitution. According to Wikipedia, the substitution $\sigma=\{x \mapsto a, y \mapsto b\}$ is linear for the formula $P(x,y)$, since $P(a,b)$ is linear and $vars(P)=dom(\sigma)=\{x,y\}$, but it is not linear for $P(x,y,a,b)$, since $P(a,b,a,b)$ is not linear and $vars(P)\neq dom(\sigma)$. Since it is not both flat and linear for $P(x,y,a,b)$, the substitution is not renaming. In the very special case that the substitution is linear for all variables (and thus, for any formula), the substitution is also a permutation of variables.

Are these definitions really different or did I misinterpret something? And if they are, which one is considered standard in the literature?