Encyclopedia

Fresh variable

Wikipedia contributorsAdapted for Fathomly · View authors

1 min read
Source updated October 18, 2025

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.

01Example

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 $\operatorname {append} (\operatorname {cons} (x,y),z)\to \operatorname {cons} (x,\operatorname {append} (y,z))$ and the term $\operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} )),$ attempting to find a matching substitution of the rule's left-hand side, $\operatorname {append} (\operatorname {cons} (x,y),z)$ , within $\operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} ))$ will fail, since $y$ cannot match $\operatorname {cons} (y,\mathrm {nil} )$ . However, if the rule is replaced by a fresh copy $\operatorname {append} (\operatorname {cons} (v_{1},v_{2}),v_{3})\to \operatorname {cons} (v_{1},\operatorname {append} (v_{2},v_{3}))$ before, matching will succeed with the answer substitution $\{v_{1}\mapsto x,\;v_{2}\mapsto \operatorname {cons} (y,\mathrm {nil} ),\;v_{3}\mapsto \operatorname {cons} (3,\mathrm {nil} )\}.$

Watch videos about Fresh variableExplainers and documentaries on YouTube (opens in a new tab)

Sources and credits

This article is adapted from the Wikipedia article “Fresh variable”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.

Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.