Fresh variable

In formal reasoning, in particular in mathematical logic, computer algebra, and automated theorem proving, a fresh variable is a variable that has not occurred in the context considered so far. The concept is often used without explanation.

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$. 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

$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)\}$.

References

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.

📰 Article(s) of the same category(ies)

• Interactive Theorem Proving (conference)
• Appeal to tradition
• Muhammad Wang fallacy
• Relation construction
• RegularChains
• Benz Patent dilemma

---