Fresh variable explained

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.^[1] The concept is often used without explanation.^[2]

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.^[3] 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.^[4]

Example

For example, in term rewriting, before applying a rule

to a given term , each variable in should be replaced by a fresh one to avoid clashes with variables occurring in .Given the rule$$\backslash operatorname(\backslash operatorname(x,y),z)\; \backslash to\; \backslash operatorname(x,\backslash operatorname(y,z))$$and the term $$\backslash operatorname(\backslash operatorname(x,\backslash operatorname(y,\backslash mathrm)),\backslash operatorname(3,\backslash mathrm)),$$attempting to find a matching substitution of the rule's left-hand side, , within $\backslash operatorname(\backslash operatorname(x,\backslash operatorname(y,\backslash mathrm)),\backslash operatorname(3,\backslash mathrm))$ will fail, since cannot match .However, if the rule is replaced by a fresh copy$$\backslash operatorname(\backslash operatorname(v\_1,v\_2),v\_3)\; \backslash to\; \backslash operatorname(v\_1,\backslash operatorname(v\_2,v\_3))$$ before, matching will succeed with the answer substitution$$\backslash .$$

Notes and References

1. Predicate Logic: Natural Deduction . Carmen Bruni . Univ. of Waterloo . Lecture Slides . CS245 / 13 . 2018 . Here: slide 13/26.
2. 2302.10576 . Michael Färber . Denotational Semantics and a Fast Interpreter for jq . Univ. of Innsbruck . Technical Report . Feb 2023 . Here: p.4.
3. Book: Gordon . Andrew D. . Melham . Thomas F. . von Wright . Joakim . Grundy . Jim . Harrison . John . Five axioms of alpha-conversion . 10.1007/BFB0105404 . 173–190 . Springer . Lecture Notes in Computer Science . Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings . 1125 . 1996. 978-3-540-61587-3 .
4. Book: Cohen, Edward . Loops B — On replacing constants by fresh variables . 10.1007/978-1-4613-9706-9 . 9781461397069 . New York . 149–194 . Springer . Monographs in Computer Science . Programming in the 1990s . 1990. 1509875 .