Content deleted Content added
No edit summary |
→Exampe: ce |
||
Line 1:
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.{{cn}}
==
For example, in [[term rewriting]], before applying a rule <math>l \to r</math> to a given term <math>t</math>, each variable in <math>l \to r</math> should be replaced by a fresh one to avoid clashes with variables occurring in <math>t</math>.{{cn}}
Given the rule
Line 7:
and the term
:<math>append(cons(x,cons(y,nil)),cons(3,nil))</math>,
attempting to find a matching substitution of the rule's left-hand side, <math>append(cons(x,y),z)</math>, within <math>append(cons(x,cons(y,nil)),cons(3,nil))</math> will fail, since <math>y</math> cannot match <math>cons(y,nil)</math>.
However, if the rule is replaced by a ''fresh copy''<ref>that is, a copy with each variable consistently replaced by a fresh variable</ref>
:<math>append(cons(v_1,v_2),v_3) \to cons(v_1,append(v_2,v_3))</math>
|