# Fresh variable

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Fresh_variable
> Markdown URL: https://mediated.wiki/source/Fresh_variable.md
> Source: https://en.wikipedia.org/wiki/Fresh_variable
> Source revision: 1317542956
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages) This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Fresh variable" – news · newspapers · books · scholar · JSTOR (September 2023) (Learn how and when to remove this message) The topic of this article may not meet Wikipedia's general notability guideline. Please help to demonstrate the notability of the topic by citing reliable secondary sources that are independent of the topic and provide significant coverage of it beyond a mere trivial mention. If notability cannot be shown, the article is likely to be merged, redirected, or deleted. Find sources: "Fresh variable" – news · newspapers · books · scholar · JSTOR (September 2023) (Learn how and when to remove this message) (Learn how and when to remove this message)

In formal reasoning, in particular in [mathematical logic](/source/Mathematical_logic), [computer algebra](/source/Computer_algebra), and [automated theorem proving](/source/Automated_theorem_proving), a **fresh variable** is a variable that did not occur in the context considered so far.[1][*[citation needed](https://en.wikipedia.org/wiki/Wikipedia:Citation_needed)*] The concept is often used without explanation.[2][*[citation needed](https://en.wikipedia.org/wiki/Wikipedia:Citation_needed)*]

Fresh variables may be used to replace other variables, to eliminate [variable shadowing](/source/Variable_shadowing) or capture. For instance, in [alpha-conversion](/source/Alpha-conversion), the processing of terms in the [lambda calculus](/source/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](/source/Free_variable).[3] Another use for fresh variables involves the development of [loop invariants](/source/Loop_invariant) in [formal program verification](/source/Formal_verification), where it is sometimes useful to replace constants by newly introduced fresh variables.[4]

## Example

For example, in [term rewriting](/source/Term_rewriting), before applying a rule l → r {\displaystyle l\to r} to a given term t {\displaystyle t} , each variable in l → r {\displaystyle l\to r} should be replaced by a fresh one to avoid clashes with variables occurring in t {\displaystyle t} .[*[citation needed](https://en.wikipedia.org/wiki/Wikipedia:Citation_needed)*] Given the rule append ⁡ ( cons ⁡ ( x , y ) , z ) → cons ⁡ ( x , append ⁡ ( y , z ) ) {\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)\to \operatorname {cons} (x,\operatorname {append} (y,z))} and the term append ⁡ ( cons ⁡ ( x , cons ⁡ ( y , n i l ) ) , cons ⁡ ( 3 , n i l ) ) , {\displaystyle \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, append ⁡ ( cons ⁡ ( x , y ) , z ) {\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)} , within append ⁡ ( cons ⁡ ( x , cons ⁡ ( y , n i l ) ) , cons ⁡ ( 3 , n i l ) ) {\displaystyle \operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} ))} will fail, since y {\displaystyle y} cannot match cons ⁡ ( y , n i l ) {\displaystyle \operatorname {cons} (y,\mathrm {nil} )} . However, if the rule is replaced by a *fresh copy*[a] append ⁡ ( cons ⁡ ( v 1 , v 2 ) , v 3 ) → cons ⁡ ( v 1 , append ⁡ ( v 2 , v 3 ) ) {\displaystyle \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 ↦ x , v 2 ↦ cons ⁡ ( y , n i l ) , v 3 ↦ cons ⁡ ( 3 , n i l ) } . {\displaystyle \{v_{1}\mapsto x,\;v_{2}\mapsto \operatorname {cons} (y,\mathrm {nil} ),\;v_{3}\mapsto \operatorname {cons} (3,\mathrm {nil} )\}.}

## Notes

1. **[^](#cite_ref-copy_5-0)** that is, a copy with each variable consistently replaced by a fresh variable

## References

1. **[^](#cite_ref-1)** Carmen Bruni (2018). [Predicate Logic: Natural Deduction](https://cs.uwaterloo.ca/~cbruni/CS245Resources/lectures/2018_Fall/13_Predicate_Logic_Natural_Deduction_post.pdf) (PDF) (Lecture Slides). Univ. of Waterloo. Here: slide 13/26.

1. **[^](#cite_ref-2)** Michael Färber (Feb 2023). Denotational Semantics and a Fast Interpreter for jq (Technical Report). Univ. of Innsbruck. [arXiv](/source/ArXiv_(identifier)):[2302.10576](https://arxiv.org/abs/2302.10576). Here: p.4.

1. **[^](#cite_ref-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](/source/Doi_(identifier)):[10.1007/BFB0105404](https://doi.org/10.1007%2FBFB0105404). [ISBN](/source/ISBN_(identifier)) [978-3-540-61587-3](https://en.wikipedia.org/wiki/Special:BookSources/978-3-540-61587-3).

1. **[^](#cite_ref-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](/source/Doi_(identifier)):[10.1007/978-1-4613-9706-9](https://doi.org/10.1007%2F978-1-4613-9706-9). [ISBN](/source/ISBN_(identifier)) [9781461397069](https://en.wikipedia.org/wiki/Special:BookSources/9781461397069). [S2CID](/source/S2CID_(identifier)) [1509875](https://api.semanticscholar.org/CorpusID:1509875).

This logic-related article is a stub. You can help Wikipedia by adding missing information.

- [v](https://en.wikipedia.org/wiki/Template:Logic-stub)
- [t](/source/Template_talk%3ALogic-stub)
- [e](https://en.wikipedia.org/wiki/Special:EditPage/Template:Logic-stub)

---
Adapted from the Wikipedia article [Fresh variable](https://en.wikipedia.org/wiki/Fresh_variable) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Fresh_variable?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.