تدوين دي بروين

في المنطق الرياضي ، تُعدّ صيغة دي بروين طريقةً لتمثيل المصطلحات في حساب لامدا، وقد ابتكرها عالم الرياضيات الهولندي نيكولاس جوفيرت دي بروين . ^{[ 1 ]} ويمكن اعتبارها عكسًا للصيغة المعتادة لحساب لامدا، حيث يُوضع الوسيط في التطبيق بجوار الرابط المقابل له في الدالة بدلًا من وضعه بعد جسم الدالة.

شروط (${\displaystyle M,N,\ldots }$) في تدوين De Bruijn إما متغيرات (${\displaystyle v}$أو أن يكون لها أحد بادئتين للعربة . العربة المجردة ، مكتوبة${\displaystyle [v]}$، يتوافق مع رابط λ المعتاد في حساب λ ، وعربة التطبيق ، مكتوبة${\displaystyle (M)}$، يتوافق مع الحجة في تطبيق في حساب التفاضل والتكامل λ.

${\displaystyle M,N,...::=\ v\ |\ [v]\;M\ |\ (M)\;N}$

يمكن تحويل المصطلحات في الصيغة التقليدية إلى تدوين دي بروين عن طريق تعريف دالة استقرائية${\displaystyle {\mathcal {I}}}$والتي من أجلها:

${\displaystyle {\begin{aligned}{\mathcal {I}}(v)&=v\\{\mathcal {I}}(\lambda v.\ M)&=[v]\;{\mathcal {I}}(M)\\{\mathcal {I}}(M\;N)&=({\mathcal {I}}(N)){\mathcal {I}}(M).\end{aligned}}}$

جميع العمليات على الحدود λ تتبادل بالنسبة إلى${\displaystyle {\mathcal {I}}}$الترجمة. على سبيل المثال، عملية الاختزال بيتا المعتادة،

${\displaystyle (\lambda v.\ M)\;N\ \ \longrightarrow _{\beta }\ \ M[v:=N]}$

في تدوين De Bruijn هو، كما هو متوقع،

${\displaystyle (N)\;[v]\;M\ \ \longrightarrow _{\beta }\ \ M[v:=N].}$

من سمات هذه الصيغة أن عربات التجريد والتطبيق في اختزالات بيتا تُقرن كأقواس. على سبيل المثال، لننظر إلى مراحل اختزال بيتا للمصطلح${\displaystyle (M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z}$، حيث يتم وضع خط تحت الاختصارات: ^{[ 2 ]}

${\displaystyle {\begin{aligned}(M)\;{\underline {(N)\;[u]}}\;(P)\;[v]\;[w]\;(Q)\;z&{\ \longrightarrow _{\beta }\ }(M)\;{\underline {(P[u:=N])\;[v]}}\;[w]\;(Q[u:=N])\;z\\&{\ \longrightarrow _{\beta }\ }{\underline {(M)\;[w]}}\;(Q[u:=N,v:=P[u:=N]])\;z\\&{\ \longrightarrow _{\beta }\ }(Q[u:=N,v:=P[u:=N],w:=M])\;z.\end{aligned}}}$

وبالتالي، إذا اعتبرنا المُطبِّق قوسًا مفتوحًا (' (') والمُجرِّد قوسًا مغلقًا (' ]')، فإن النمط في المصطلح أعلاه هو ' ((](]]'. أطلق دي بروين على المُطبِّق ومُجرِّده المُقابل في هذا التفسير اسم "الشركاء "، وعلى العربات التي لا شركاء لها اسم "العُزَّاب" . وتكون سلسلة العربات، التي أطلق عليها اسم "القطاع" ، متوازنة جيدًا إذا كانت جميع عرباتها مُرتبطة بشركاء.

في قطاع متوازن جيدًا، يمكن تحريك العربات المترافقة بشكل عشوائي، وطالما لم يختل التوازن، يبقى معنى المصطلح كما هو. على سبيل المثال، في المثال أعلاه، أداة التطبيق${\displaystyle (M)}$يمكن إرجاعها إلى مُستخلصها${\displaystyle [w]}$أو المُجرِّد للمُطبِّق. في الواقع، يمكن وصف جميع التحويلات التبادلية والتبديلية على حدود لامدا ببساطة من حيث إعادة ترتيب العربات المترافقة مع الحفاظ على التكافؤ. وبالتالي، نحصل على عنصر تحويل أولي مُعمَّم لحدود لامدا في تدوين دي بروين.

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

• الترميز الرياضي