Fresh variable: Difference between revisions

Revision as of 02:58, 5 February 2024

Revision as of 08:23, 7 November 2024

Line 42:

However, if the rule is replaced by a ''fresh copy''{{efn|name=copy|that is, a copy with each variable consistently replaced by a fresh variable}}

:<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_2v_1 \mapsto x, \; v_2 \mapsto cons(y,nil), \; v_3 \mapsto cons(3,nil) \}</math>.

== Notes ==