De Bruijn index
ریاضیاتی منطق میں، ڈی بروجن انڈیکس ایک ایسا آلہ ہے جسے ڈچ ریاضی دان نیکولاس گوورٹ ڈی بروجن نے باؤنڈ متغیرات کا نام لیے بغیر لیمبڈا کیلکولس کی اصطلاحات کی نمائندگی کے لیے ایجاد کیا تھا۔ ان اشاریوں کا استعمال کرتے ہوئے لکھی گئی اصطلاحات α-تبدیلی کے حوالے سے غیر متغیر ہیں، لہذا α-مساوات کے لیے چیک وہی ہے جو نحو مساوات کے لیے ہے۔ ہر ڈی بروجن انڈیکس ایک قدرتی نمبر ہے جو λ-اصطلاح میں متغیر کی موجودگی کی نمائندگی کرتا ہے، اور بائنڈرز کی تعداد کی نشاندہی کرتا ہے جو اس واقعہ اور اس کے متعلقہ بائنڈر کے درمیان دائرہ کار میں ہیں۔ مندرجہ ذیل کچھ مثالیں ہیں: اصطلاح λx۔ λy۔ x، جسے بعض اوقات K کمبینٹر کہا جاتا ہے، ڈی بروجن انڈیکس کے ساتھ λλ2 کے طور پر لکھا جاتا ہے۔ واقعہ x کے لیے بائنڈر دائرہ کار میں دوسرا λ ہے۔ اصطلاح λx۔ λy۔ λz. ایکس زیڈ (وائی زیڈ) (ایس کمبینٹر)، ڈی بروجن انڈیکس کے ساتھ، λλλ31 (211) ہے۔ اصطلاح λz۔ (λy۔ y (λx. x)) (λx۔ zx) λ (λ1 (λ1)) (λ21) ہے۔ مندرجہ ذیل مثال دیکھیں، جہاں بائنڈر رنگین ہیں اور حوالہ جات تیروں کے ساتھ دکھائے گئے ہیں۔ ڈی بروجن انڈیکس عام طور پر اعلی درجے کے استدلال کے نظاموں جیسے خودکار تھیوریم پروورز اور منطق پروگرامنگ سسٹم میں استعمال ہوتے ہیں۔ رسمی تعریف رسمی طور پر، ڈی بروجن انڈیکس کا استعمال کرتے ہوئے لکھے گئے λ-اصطلاحات (M، N،.) میں درج ذیل نحو ہوتی ہے (قوسین کو آزادانہ طور پر اجازت دی جاتی ہے): M، N،:: = n | M N | λ M جہاں n-قدرتی اعداد جو 0 سے زیادہ ہیں-متغیر ہیں۔ ایک متغیر n پابند ہے اگر یہ کم از کم n بائنڈر (λ) کے دائرہ کار میں ہو ؛ بصورت دیگر یہ آزاد ہے۔ متغیر n کے لیے بائنڈنگ سائٹ n واں بائنڈر ہے جو اس کے دائرہ کار میں ہے، جو اندرونی بائنڈر سے شروع ہوتا ہے۔ λ اصطلاحات پر سب سے قدیم عمل متبادل ہے: کسی اصطلاح میں آزاد متغیرات کو دوسری اصطلاحات سے تبدیل کرنا۔ مثال کے طور پر، β-کمی (λ M) N میں، ہمیں متغیر n1، n2،.، m میں nk کی مثالیں تلاش کرنی چاہئیں جو λ M میں λ سے جڑے ہوئے ہیں، بیرونی λ-بائنڈر کو ہٹانے سے ملنے کے لیے M کے آزاد متغیرات کو کم کریں، اور n1، n2،.، nk کو N سے تبدیل کریں، ہر بار N میں پائے جانے والے آزاد متغیرات کو مناسب طریقے سے بڑھاتے ہوئے، λ-بائنڈرز کی تعداد سے ملنے کے لیے، جس کے تحت متعلقہ متغیر اس وقت ہوتا ہے جب N کسی ایک ni کے لیے متبادل ہوتا ہے۔ مثال کے طور پر، درخواست (λλ42 (λ13)) (λ51) پر غور کریں جو معمول کے اشارے (λx) میں لکھی گئی مندرجہ ذیل اصطلاح سے مطابقت رکھتی ہے۔ λy۔ z x (λu. u x)) (λx۔ ڈبلیو ایکس)۔ مرحلہ 1 کے بعد، ہم اصطلاح λ4· (λ1·) حاصل کرتے ہیں، جہاں متغیرات جو متبادل کے لیے مقرر کیے گئے ہیں انہیں خانوں سے تبدیل کر دیا جاتا ہے۔ مرحلہ 2 آزاد متغیرات کو کم کرتا ہے، جس سے λ3⁄2 (λ1⁄2) ملتا ہے۔ آخر میں، مرحلہ 3 میں، ہم بکسوں کو دلیل کے ساتھ تبدیل کرتے ہیں، یعنی λ51 ؛ پہلا باکس ایک بائنڈر کے نیچے ہے، لہذا ہم اسے λ61 سے تبدیل کرتے ہیں (جو کہ λ51 ہے جس میں فری متغیرات میں 1 کا اضافہ ہوتا ہے) ؛ دوسرا دو بائنڈر کے نیچے ہے، لہذا ہم اسے λ71 سے تبدیل کرتے ہیں۔ حتمی نتیجہ λ3 (λ61) (λ1 (λ71)) ہے۔ رسمی طور پر، متبادل اصطلاحات کی ایک لامحدود فہرست ہے، جو M1.M2 لکھی جاتی ہے، جہاں ایم آئی ith فری متغیر کا متبادل ہے۔ مرحلہ 3 میں بڑھتے ہوئے عمل کو بعض اوقات شفٹ اور تحریری k کہا جاتا ہے جہاں k ایک قدرتی نمبر ہے جو متغیرات کو بڑھانے کی رقم کی نشاندہی کرتا ہے، اور اس کی تعریف اس طرح کی جاتی ہے۔ مثال کے طور پر، 0 شناخت کا متبادل ہے، جس سے اصطلاح میں کوئی تبدیلی نہیں ہوتی ہے۔ اصطلاحات کی ایک محدود فہرست M1.M2.Mn متبادل M1.M2.Mn. (n + 1). (n + 2) کو مختصر کرتی ہے۔ n سے بڑے تمام متغیرات کو بغیر کسی تبدیلی کے چھوڑنا۔ اصطلاح M کے متبادل s کا اطلاق M [s] لکھا جاتا ہے۔ دو متبادلات s1 اور s2 کی ساخت s1s2 لکھی گئی ہے اور اس کی تعریف (M1.M2) s = M1 [s]. M2 [s]. خاصیت M [s1s2] = (M [s1]) [s2] کو مطمئن کرتی ہے، اور متبادل کی تعریف مندرجہ ذیل شرائط پر کی گئی ہے: اوپر β-کمی کے لیے بیان کردہ اقدامات اس طرح زیادہ مختصر طور پر ظاہر کیے گئے ہیں: (λM) N → βM [N]۔ ڈی بروجن انڈیکس کے متبادل λ-اصطلاحات کی معیاری "نامزد" نمائندگی کا استعمال کرتے وقت، جہاں متغیرات کو لیبل یا سٹرنگ کے طور پر سمجھا جاتا ہے، شرائط پر کسی بھی آپریشن کی وضاحت کرتے وقت کسی کو واضح طور پر α-تبدیلی کو سنبھالنا چاہیے۔ عملی طور پر یہ بوجھل، غیر موثر اور اکثر غلطی کا شکار ہوتا ہے۔ اس وجہ سے اس طرح کی اصطلاحات کی مختلف نمائندگی کی تلاش کا باعث بنی ہے۔ دوسری طرف، λ-اصطلاحات کی نامزد نمائندگی زیادہ وسیع ہے اور دوسروں کے ذریعہ زیادہ فوری طور پر قابل فہم ہوسکتی ہے کیونکہ متغیرات کو وضاحتی نام دیے جا سکتے ہیں۔ اس طرح، یہاں تک کہ اگر کوئی نظام اندرونی طور پر ڈی بروجن انڈیکس کا استعمال کرتا ہے، تو یہ ناموں کے ساتھ ایک یوزر انٹرفیس پیش کرے گا۔ ڈی بروجن انڈیکس کو دیکھنے کا ایک متبادل طریقہ ڈی بروجن لیولز کے طور پر ہے، جو اوپر کی بجائے اسٹیک کے نیچے سے متغیرات کو انڈیکس کرتا ہے۔ یہ ری انڈیکس فری متغیرات کی ضرورت کو ختم کرتا ہے، مثال کے طور پر سیاق و سباق کو کمزور کرتے وقت، جبکہ ڈی بروجن انڈیکس ری انڈیکس باؤنڈ متغیرات کی ضرورت کو ختم کرتے ہیں، مثال کے طور پر جب کسی دوسرے سیاق و سباق میں بند اظہار کو تبدیل کرتے ہیں۔ ڈی بروجن انڈیکس λ-اصطلاحات کی واحد نمائندگی نہیں ہیں جو α-تبدیلی کے مسئلے کو ختم کرتی ہیں۔ نامزد نمائندوں میں، پٹس اور گابی کی برائے نام تکنیک ایک نقطہ نظر ہے، جہاں λ-اصطلاح کی نمائندگی کو متغیر ترتیبات کا استعمال کرتے ہوئے اس کے لیے دوبارہ لکھنے کے قابل تمام اصطلاحات کے مساوی طبقے کے طور پر سمجھا جاتا ہے۔ یہ نقطہ نظر اسابیل/ایچ او ایل کے برائے نام ڈیٹا ٹائپ پیکیج کے ذریعے لیا جاتا ہے۔ ایک اور عام متبادل اعلی درجے کی نمائندگی کے لیے اپیل ہے جہاں λ-بائنڈر کو ایک حقیقی فنکشن کے طور پر سمجھا جاتا ہے۔ اس طرح کی نمائندگی میں، α-مساوات، متبادل وغیرہ کے مسائل۔ میٹا لاجک میں ایک ہی کارروائیوں کے ساتھ شناخت کی جاتی ہے۔ پروف اسسٹنٹ میں کٹوتی کے نظام کی میٹا تھیوریٹک خصوصیات کے بارے میں استدلال کرتے وقت، بعض اوقات اپنے آپ کو فرسٹ آرڈر کی نمائندگی تک محدود رکھنا اور مفروضوں کو نام دینے یا ان کا نام تبدیل کرنے کی صلاحیت رکھنا مطلوب ہوتا ہے۔ مقامی طور پر بے نام نقطہ نظر متغیرات کی مخلوط نمائندگی کا استعمال کرتا ہے-باؤنڈ متغیرات کے لیے ڈی بروجن انڈیکس اور مفت متغیرات کے نام-جو مناسب ہونے پر ڈی بروجن انڈیکس شدہ اصطلاحات کی α-canonical شکل سے فائدہ اٹھانے کے قابل ہے۔ بیرینڈریگٹ کا متغیر کنونشن بیرینڈریگٹ کا متغیر کنونشن ایک ایسا کنونشن ہے جو عام طور پر ثبوتوں اور تعریفوں میں استعمال ہوتا ہے جہاں یہ فرض کیا جاتا ہے کہ: باؤنڈ متغیر آزاد متغیرات سے الگ ہیں، اور تمام بائنڈر ایسے متغیرات کو باندھتے ہیں جو پہلے سے دائرہ کار میں نہیں ہیں۔ انڈکٹو تعریف کے عمومی تناظر میں، کنونشن کا استعمال کرتے ہوئے ایک انڈکٹو تعریف کو اس میں تبدیل کرنے کے لیے α-تبدیلی کا اطلاق کرنا ممکن نہیں ہے جہاں کنونشن استعمال نہیں کیا جاتا ہے، کیونکہ ایک متغیر بائنڈنگ پوزیشن اور اصول میں غیر بائنڈنگ پوزیشن دونوں میں ظاہر ہو سکتا ہے۔ اگر ہر قاعدہ مندرجہ ذیل دو شرائط کو پورا کرتا ہے تو انڈکشن اصول برقرار رہتا ہے: قاعدہ برائے نام منطق کے معنی میں مساوی ہے، یعنی یہ کہ اس کی صداقت قاعدے کے احاطے کو فرض کرتے ہوئے متغیرات کا نام بدلنے سے تبدیل نہیں ہوتی ہے، قاعدے میں بائنڈنگ پوزیشنوں میں متغیرات الگ ہیں اور نتیجے میں آزاد ہیں۔ λ-اصطلاحات کے لیے ڈی بروجن نوٹیشن بھی دیکھیں۔ متغیر ناموں کو ختم کرنے کا ایک زیادہ ضروری طریقہ، مشترکہ منطق۔ حوالہ جات لیمبڈا کیلکولس