متغير جديد

في الاستدلال الصوري، ولا سيما في المنطق الرياضي ، والجبر الحاسوبي ، وإثبات النظريات الآلي ، يُعرَّف المتغير الجديد بأنه متغير لم يظهر في السياق المدروس حتى الآن. ^{[ 1 ]} وكثيراً ما يُستخدم هذا المفهوم دون شرح. ^{[ 2 ]}

يمكن استخدام المتغيرات الجديدة لاستبدال متغيرات أخرى، وذلك لتجنب تداخل المتغيرات أو التقاطها. على سبيل المثال، في تحويل ألفا ، أي معالجة الحدود في حساب لامدا إلى حدود مكافئة بمتغيرات مُعاد تسميتها، يُعد استبدال المتغيرات بمتغيرات جديدة مفيدًا لتجنب التقاط متغيرات كان ينبغي أن تكون حرة عن طريق الخطأ . ^{[ 3 ]} يُستخدم أيضًا إنشاء ثوابت الحلقات في التحقق الرسمي من البرامج ، حيث يكون من المفيد أحيانًا استبدال الثوابت بمتغيرات جديدة مُضافة حديثًا. ^{[ 4 ]}

على سبيل المثال، في إعادة صياغة المصطلحات ، قبل تطبيق قاعدة${\displaystyle l\to r}$لمصطلح معين${\displaystyle t}$، كل متغير في${\displaystyle l\to r}$ينبغي استبدالها بنسخة جديدة لتجنب التعارضات مع المتغيرات التي تحدث في${\displaystyle t}$بالنظر إلى القاعدة $${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)\to \operatorname {cons} (x,\operatorname {append} (y,z))}$$ والمصطلح $${\displaystyle \operatorname {append} (\operatorname {cons} (x،\operatorname {cons} (y،\mathrm {nil} ))،\operatorname {cons} (3،\mathrm {nil} ))،}$$ محاولة إيجاد بديل مطابق للجانب الأيسر من القاعدة،${\displaystyle \operatorname {append} (\operatorname {cons} (x,y),z)}$، داخل${\displaystyle \operatorname {append} (\operatorname {cons} (x,\operatorname {cons} (y,\mathrm {nil} )),\operatorname {cons} (3,\mathrm {nil} ))}$سوف تفشل، لأن${\displaystyle y}$لا يمكن المطابقة${\displaystyle \operatorname {cons} (y,\mathrm {nil} )}$ومع ذلك، إذا تم استبدال القاعدة بنسخة جديدة ^{[ أ ]}$${\displaystyle \operatorname {append} (\operatorname {cons} (v_{1},v_{2}),v_{3})\to \operatorname {cons} (v_{1},\operatorname {append} (v_{2},v_{3}))}$$ في السابق، ستنجح عملية المطابقة مع استبدال الإجابة $${\displaystyle \{v_{1}\mapsto x,\;v_{2}\mapsto \operatorname {cons} (y,\mathrm {nil} ),\;v_{3}\mapsto \operatorname {cons} (3,\mathrm {nil} )\}.}$$