Fresh variable: Difference between revisions

Revision as of 03:20, 3 September 2023

Revision as of 03:23, 3 September 2023

Line 13:

:<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>{{efn|name=copy|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>

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

== ReferencesNotes ==

{{reflistnotelist}}

{{logic-stub}}