Fresh variable

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 more citations. 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, 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 ${\displaystyle l\to r}$ to a given term ${\displaystyle t}$, each variable in ${\displaystyle l\to r}$ should be replaced by a fresh one to avoid clashes with variables occurring in ${\displaystyle t}$.^{[citation needed]} Given the rule $${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)\to \operatorname {cons} (x,\operatorname {append} (y,z))}$$ and the term $${\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, ${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)}$, within ${\displaystyle \operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} ))}$ will fail, since ${\displaystyle y}$ cannot match ${\displaystyle \operatorname {cons} (y,\mathrm {nil} )}$. However, if the rule is replaced by a fresh copy^[a] $${\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 $${\displaystyle \{v_{1}\mapsto x,\;v_{2}\mapsto \operatorname {cons} (y,\mathrm {nil} ),\;v_{3}\mapsto \operatorname {cons} (3,\mathrm {nil} )\}.}$$

Notes

References

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

• v
• t
• e