Fresh variable: Difference between revisions

Revision as of 18:28, 28 June 2023

Revision as of 18:29, 28 June 2023

Line 8:

:<math>append(cons(x,cons(y,nil)),cons(3,nil))</math>,

attempting to find a matching substitution of <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 replacereplaced by a fresh variable</ref>

:<math>append(cons(v_1,v_2),v_3) \to cons(v_1,append(v_2,v_3))</math>

before, matching will succeed with the answer substitution <math>\{ v_2 \mapsto x, \; v_2 \mapsto cons(y,nil), \; v_3 \mapsto cons(3,nil) \}</math>.