مؤشر دي بروين

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

• يُكتب المصطلح λ x . λ y . x ، والذي يُسمى أحيانًا مُركِّب K ، على الصورة λ λ 2 باستخدام مؤشرات دي بروين. الرابط الخاص بالظهور x هو λ الثاني في النطاق.
• المصطلح λ x . λ y . λ z . x z ( y z ) ( المركب S )، مع مؤشرات دي بروين، هو λ λ λ 3 1 (2 1).
• المصطلح λ z . (λ y . y (λ x . x )) (λ x . z x ) هو λ (λ 1 (λ 1)) (λ 2 1). انظر الرسم التوضيحي التالي، حيث تم تلوين المجلدات والإشارة إلى المراجع بالأسهم.

تُستخدم مؤشرات دي بروين بشكل شائع في أنظمة الاستدلال من الرتبة العليا مثل برامج إثبات النظريات الآلية وأنظمة البرمجة المنطقية . ^{[ 2 ]}

بشكل رسمي، فإن المصطلحات λ ( M ، N ، ...) المكتوبة باستخدام مؤشرات دي بروين لها الصيغة التالية (الأقواس مسموح بها بحرية):

M ، N ، ...  ::= n | M N | λ M

حيث n - أعداد طبيعية أكبر من صفر - هي المتغيرات. يكون المتغير n مرتبطًا إذا كان ضمن نطاق n رابطًا على الأقل (λ)؛ وإلا فهو حر . موقع ارتباط المتغير n هو الرابط رقم n الذي يقع ضمن نطاقه ، بدءًا من الرابط الأقرب.

أبسط عملية على حدود λ هي الاستبدال : استبدال المتغيرات الحرة في حد ما بحدود أخرى. في اختزال β (λ M ) N ، على سبيل المثال، يجب علينا

1. أوجد حالات المتغيرات n1 _، n2 _، ...، nk في _M التي تكون مقيدة بـ λ في λM ،
2. قم بتقليل المتغيرات الحرة لـ M لتتوافق مع إزالة الرابط الخارجي λ، و
3. استبدل n ₁ ، n ₂ ، ... ، n _k بـ N ، مع زيادة المتغيرات الحرة التي تظهر في N في كل مرة بشكل مناسب ، لمطابقة عدد روابط λ ، والتي يظهر المتغير المقابل عند استبدال N بأحد n _i .

ولتوضيح ذلك، انظر إلى التطبيق

(λ λ 4 2 (λ 1 3)) (λ 5 1)

والذي قد يتوافق مع المصطلح التالي المكتوب بالترميز المعتاد

(λ x . λ y . z x (λ u . u x )) (λ x . w x ).

بعد الخطوة الأولى، نحصل على الحد λ₄□(λ₁□)، حيث تُستبدل مواضع المتغير المُستبدل بمربعات. في الخطوة الثانية، يتم إنقاص المتغيرات الحرة، فنحصل على λ₃□(λ₁□). أخيرًا، في الخطوة الثالثة، نستبدل المربعات بالوسيط، أي λ₅□؛ المربع الأول يقع تحت رابط واحد، لذا نستبدله بـ λ₆□ (وهو λ₅□ مع زيادة المتغيرات الحرة بمقدار 1)؛ أما المربع الثاني فيقع تحت رابطين، لذا نستبدله بـ λ₇□. والنتيجة النهائية هي λ₃□(λ₆□)(λ₁□(λ₇□)).

بصورة رسمية، يُعرَّف الاستبدال بأنه قائمة غير محدودة من الحدود، تُكتب M1، M2 _، ... _، حيث يُمثل Mi بديلًا للمتغير الحر رقم i . تُسمى عملية الزيادة في الخطوة 3 أحيانًا بالإزاحة ، وتُكتب ↑ ^k _، حيث k عدد طبيعي يُشير إلى مقدار الزيادة في المتغيرات، ويُعرَّف كما يلي:

${\displaystyle \uparrow ^{k}=(k+1).(k+2)....}$

على سبيل المثال، ↑ 0 هو استبدال محايد، حيث يبقى الحد دون تغيير. تُختصر قائمة محدودة من الحدود M1، ^M2 ، ... _، Mn _إلى الاستبدال _M1 ، M2 ، _... ، Mn ، ... _، مع بقاء جميع المتغيرات الأكبر من n دون تغيير. يُكتب تطبيق الاستبدال s على الحد M على النحو التالي _: M [ s ]. يُكتب تركيب استبدالين s1 و s2 على النحو _{التالي :} s1 s2 _، ويُعرّف كما يلي _:

( M1.M2 _... ) s = M1 [ s ] .M2 [ _s ] ..._​​_​​

استيفاء الخاصية

M [ s ₁ s ₂ ] = ( M [ s ₁ ]) [ s ₂ ],

ويتم تعريف الاستبدال وفقًا للشروط التالية:

${\displaystyle {\begin{aligned}n[N_{1}\ldots N_{n}\ldots ]=&N_{n}\\(M_{1}\;M_{2})[s]=&(M_{1}[s])(M_{2}[s])\\(\lambda \;M)[s]=&\lambda \;(M[1.s'])\\&{\text{حيث ​​}}s'=s\uparrow ^{1}\end{aligned}}}$

وبالتالي، يمكن التعبير عن الخطوات الموضحة أعلاه لاختزال بيتا بشكل أكثر إيجازًا على النحو التالي:

( M ) N → _β M [ N .1.2.3...].

عند استخدام التمثيل القياسي "المُسمى" لمصطلحات لامدا، حيث تُعامل المتغيرات كعلامات أو سلاسل نصية، يجب التعامل صراحةً مع تحويل ألفا عند تعريف أي عملية على هذه المصطلحات. عمليًا، يُعدّ هذا الأمر مُرهقًا وغير فعّال، وغالبًا ما يكون عُرضةً للأخطاء. لذلك، أدّى هذا إلى البحث عن تمثيلات مختلفة لهذه المصطلحات. من ناحية أخرى، يُعدّ التمثيل المُسمى لمصطلحات لامدا أكثر انتشارًا وأسهل فهمًا للآخرين، لأنّ المتغيرات يُمكن إعطاؤها أسماءً وصفية. وبالتالي، حتى لو كان النظام يستخدم مؤشرات دي بروين داخليًا، فإنه عادةً ما يُقدّم واجهة مستخدم بأسماء.

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

لا تُعدّ مؤشرات دي بروين التمثيل الوحيد لمصطلحات λ الذي يُغني عن مشكلة التحويل إلى α. من بين التمثيلات المُسمّاة، تُعتبر تقنيات بيتس وغاباي الاسمية أحد الأساليب، حيث يُعامل تمثيل مصطلح λ كفئة تكافؤ لجميع المصطلحات القابلة لإعادة الكتابة إليه باستخدام تباديل المتغيرات. ^{[ 4 ]} يتبنى حزمة أنواع البيانات الاسمية في Isabelle/HOL هذا الأسلوب . ^{[ 5 ]}

ثمة بديل شائع آخر يتمثل في اللجوء إلى تمثيلات من الرتبة العليا حيث يُعامل الرابط λ كدالة حقيقية. في هذه التمثيلات، تُعرَّف مسائل التكافؤ α، والاستبدال، وما إلى ذلك، بالعمليات نفسها في منطق فوقي .

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

• تدوين de Bruijn لمصطلحات lect.
• المنطق التوافقي ، وهو طريقة أكثر أهمية للتخلص من أسماء المتغيرات.