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.

Fresh variables may be used to replace other variables, to eliminate variable shadowing or capture. For instance, in alpha-conversion, the processing of terms in the lambda calculus into equivalent terms with renamed variables, replacing variables with fresh variables can be helpful as a way to avoid accidentally capturing variables that should be free. Another use for fresh variables involves the development of loop invariants in formal program verification, where it is sometimes useful to replace constants by newly introduced fresh variables.

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

${\displaystyle append(cons(x,y),z)\to cons(x,append(y,z))}$

and the term

${\displaystyle append(cons(x,cons(y,nil)),cons(3,nil))}$,

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

${\displaystyle 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 ${\displaystyle \{v_{1}\mapsto x,\;v_{2}\mapsto cons(y,nil),\;v_{3}\mapsto cons(3,nil)\}}$.