Fresh variable

<p>In formal reasoning, in particular in <a href="/facts/Mathematical_logic/SaI7Y3wN">mathematical logic</a>, <a href="/facts/Computer_algebra/hjun1KAX">computer algebra</a>, and <a href="/facts/Automated_theorem_proving/vKGvuKFI">automated theorem proving</a>, a fresh variable is a variable that did not occur in the context considered so far.
The concept is often used without explanation.
</p><p>Fresh variables may be used to replace other variables, to eliminate <a href="/facts/Variable_shadowing/MkxEt5Tz">variable shadowing</a> or capture. For instance, in <a href="/facts/Alpha-conversion/DaD3RuQ4">alpha-conversion</a>, the processing of terms in the <a href="/facts/Lambda_calculus/DaD3RuQ4">lambda calculus</a> 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 <a href="/facts/Free_variable/ndWnXXYs">free</a>. Another use for fresh variables involves the development of <a href="/facts/Loop_invariant/fIbNgcsI">loop invariants</a> in <a href="/facts/Formal_verification/BYD4GnJR">formal program verification</a>, where it is sometimes useful to replace constants by newly introduced fresh variables.
</p>

Fresh variable open-in-new

Fresh variable