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

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

append(cons(x,y),z)\to cons(x,append(y,z))

and the term

append(cons(x,cons(y,nil)),cons(3,nil))

,

attempting to find a matching substitution of the rule's left-hand side, $append(cons(x,y),z)$ , within $append(cons(x,cons(y,nil)),cons(3,nil))$ will fail, since $y$ cannot match $cons(y,nil)$ . However, if the rule is replaced by a fresh copy^[a]

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

Notes

^ that is, a copy with each variable consistently replaced by a fresh variable

References

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

This logic-related article is a stub. You can help Wikipedia by expanding it.

[copy-5] that is, a copy with each variable consistently replaced by a fresh variable

[1] Carmen Bruni (2018). Predicate Logic: Natural Deduction (PDF) (Lecture Slides). Univ. of Waterloo. Here: slide 13/26.

[2] Michael Färber (Feb 2023). Denotational Semantics and a Fast Interpreter for jq (Technical Report). Univ. of Innsbruck. arXiv:2302.10576. Here: p.4.

[3] Gordon, Andrew D.; Melham, Thomas F. (1996). "Five axioms of alpha-conversion". In von Wright, Joakim; Grundy, Jim; Harrison, John (eds.). Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings. Lecture Notes in Computer Science. Vol. 1125. Springer. pp. 173–190. doi:10.1007/BFB0105404.

[4] Cohen, Edward (1990). "Loops B — On replacing constants by fresh variables". Programming in the 1990s. Monographs in Computer Science. New York: Springer. pp. 149–194. doi:10.1007/978-1-4613-9706-9. ISBN 9781461397069. S2CID 1509875.

[1]

[2]

[3]

[4]

[a]