Fresh variable

In formal reasoning, in particular in mathematical logic, computer algebra, and automated theorem proving, a fresh variable is a variable that did not occur in the context considered so far. The concept is often used without explanation.

Example

For example, in term rewriting, before applying a rule $l\to r$ to a given term $t$, each variable in $l\to r$ should be replaced by a fresh one to avoid clashes with variables occurring in $t$. Given the rule

$append(cons(x,y),z)\to cons(x,append(y,z))$

and the term

$append(cons(x,cons(y,nil)),cons(3,nil))$,

attempting to find a matching substitution of the rule's left-hand side, $append(cons(x,y),z)$, within $append(cons(x,cons(y,nil)),cons(3,nil))$ will fail, since $y$ cannot match $cons(y,nil)$. However, if the rule is replaced by a fresh copy

$append(cons(v_{1},v_{2}),v_{3})\to cons(v_{1},append(v_{2},v_{3}))$

before, matching will succeed with the answer substitution $\{v_{2}\mapsto x,\;v_{2}\mapsto cons(y,nil),\;v_{3}\mapsto cons(3,nil)\}$.

References

This article "Fresh variable" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Fresh variable. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.

---