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]

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

• Logic stubs
• Rewriting systems
• Automated theorem proving
• Computer algebra
• Variables (mathematics)

• Articles needing additional references from September 2023
• All articles needing additional references
• Articles with topics of unclear notability from September 2023
• All articles with topics of unclear notability
• Articles with multiple maintenance issues
• All articles with unsourced statements
• Articles with unsourced statements from September 2023
• Articles with unsourced statements from June 2023
• All stub articles