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]
Example[edit]
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 .[citation needed] Given the rule
and the term
- ,
attempting to find a matching substitution of the rule's left-hand side, , within will fail, since cannot match . However, if the rule is replaced by a fresh copy[lower-alpha 1]
before, matching will succeed with the answer substitution .
Notes[edit]
- ↑ that is, a copy with each variable consistently replaced by a fresh variable
References[edit]
- ↑ 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.
This logic-related article is a stub. You can help EverybodyWiki by expanding it. |
This article "Fresh variable" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Fresh variable. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.