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.Template:Cn The concept is often used without explanation.Template:Cn

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.

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$.Template:Cn Given the rule $$\mathrm{append}(\mathrm{cons}(x,y),z)\to \mathrm{cons}(x,\mathrm{append}(y,z))$$ and the term $$\mathrm{append}(\mathrm{cons}(x,\mathrm{cons}(y,\mathrm{n}\mathrm{i}\mathrm{l})),\mathrm{cons}(3,\mathrm{n}\mathrm{i}\mathrm{l})),$$ attempting to find a matching substitution of the rule's left-hand side, $\mathrm{append}(\mathrm{cons}(x,y),z)$, within $\mathrm{append}(\mathrm{cons}(x,\mathrm{cons}(y,\mathrm{n}\mathrm{i}\mathrm{l})),\mathrm{cons}(3,\mathrm{n}\mathrm{i}\mathrm{l}))$ will fail, since $y$ cannot match $\mathrm{cons}(y,\mathrm{n}\mathrm{i}\mathrm{l})$. However, if the rule is replaced by a fresh copyTemplate:Efn $$\mathrm{append}(\mathrm{cons}(v_1,v_2),v_3)\to \mathrm{cons}(v_1,\mathrm{append}(v_2,v_3))$$ before, matching will succeed with the answer substitution $$\{v_1\mapsto x,v_2\mapsto \mathrm{cons}(y,\mathrm{n}\mathrm{i}\mathrm{l}),v_3\mapsto \mathrm{cons}(3,\mathrm{n}\mathrm{i}\mathrm{l})\}.$$