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.^{[citation needed]}

Exampe

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}$ .^{[citation needed]} 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 ${\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^[1]

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

References

1. that is, a copy with each variable consistently replace by a fresh variable