De Bruijn notation
ریاضیاتی منطق میں، ڈی بروجن نوٹیشن ڈچ ریاضی دان نیکولاس گوورٹ ڈی بروجن کے ایجاد کردہ λ کیلکولس میں اصطلاحات کے لیے ایک نحو ہے۔ اسے λ کیلکولس کے لیے معمول کے نحو کے الٹ پلٹ کے طور پر دیکھا جا سکتا ہے جہاں کسی ایپلیکیشن میں دلیل کو فنکشن میں اس کے متعلقہ بائنڈر کے ساتھ رکھا جاتا ہے بجائے اس کے کہ مؤخر الذکر کے باڈی کے۔ رسمی تعریف ڈی بروجن نوٹیشن میں شرائط () یا تو متغیر () ہیں، یا دو ویگن سابقہ میں سے ایک ہے۔ تجریدی ویگن، لکھا ہوا، λ کیلکولس کے معمول λ-بائنڈر سے مطابقت رکھتا ہے، اور درخواست دہندہ ویگن، لکھا ہوا، λ کیلکولس میں ایک درخواست میں دلیل سے مطابقت رکھتا ہے۔ روایتی نحو میں اصطلاحات کو ایک انڈکٹو فنکشن کی وضاحت کرکے ڈی بروجن نوٹیشن میں تبدیل کیا جا سکتا ہے جس کے لیے: ترجمہ کے حوالے سے λ-اصطلاحات پر تمام کارروائیاں منتقل ہوتی ہیں۔ مثال کے طور پر، ڈی بروجن نوٹیشن میں معمول کی β-کمی، پیش گوئی کے مطابق، اس نوٹیشن کی ایک خصوصیت یہ ہے کہ β-ریڈکس کے تجریدی اور درخواست دینے والے ویگن کو قوسین کی طرح جوڑا جاتا ہے۔ مثال کے طور پر، اصطلاح کے β-کمی کے مراحل پر غور کریں، جہاں ریڈیکس کو واضح کیا گیا ہے: اس طرح، اگر کوئی درخواست دہندہ کو اوپن پیرنٹ ('(') اور تجریدی کو قریبی بریکٹ (']') کے طور پر دیکھتا ہے، تو مندرجہ بالا اصطلاح میں نمونہ '((] (])' ہے۔ ڈی بروجن نے اس تشریح کے شراکت داروں میں ایک درخواست دہندہ اور اس کے متعلقہ تجریدی کو، اور شراکت داروں کے بغیر ویگنوں کو بیچلر کہا۔ ویگنوں کا ایک سلسلہ، جسے انہوں نے ایک طبقہ کہا، اچھی طرح سے متوازن ہے اگر اس کے تمام ویگن شراکت دار ہوں۔ ڈی بروجن نوٹیشن کے فوائد ایک متوازن حصے میں، شراکت دار ویگنوں کو من مانی طور پر منتقل کیا جا سکتا ہے اور جب تک برابری ختم نہیں ہوتی، اس اصطلاح کا معنی وہی رہتا ہے۔ مثال کے طور پر، مندرجہ بالا مثال میں، درخواست دہندہ کو اس کے تجریدی، یا تجریدی کو درخواست دہندہ کے پاس لایا جا سکتا ہے۔ در حقیقت، لیمبڈا کی شرائط پر تمام نقل و حمل اور تغیر پذیر تبادلوں کو صرف شراکت دار ویگنوں کی برابری کے تحفظ کے دوبارہ ترتیب کے لحاظ سے بیان کیا جا سکتا ہے۔ اس طرح ڈی بروجن نوٹیشن میں λ-اصطلاحات کے لیے ایک عمومی تبدیلی حاصل ہوتی ہے۔ λ اصطلاحات کی کئی خصوصیات جو روایتی اشارے کا استعمال کرتے ہوئے بیان کرنا اور ثابت کرنا مشکل ہے، ڈی بروجن اشارے میں آسانی سے ظاہر کی جاتی ہیں۔ مثال کے طور پر، ٹائپ تھیوریٹک ترتیب میں، کوئی بھی ٹائپنگ کے سیاق و سباق میں کسی اصطلاح کے لیے اقسام کی کینونکل کلاس کا آسانی سے حساب لگا سکتا ہے، اور ٹائپ چیکنگ کے مسئلے کو اس بات کی تصدیق کرنے کے لیے دوبارہ بیان کر سکتا ہے کہ چیک شدہ قسم اس کلاس کا رکن ہے۔ ڈی بروجن نوٹیشن خالص قسم کے نظاموں میں واضح متبادل کے لیے کیلکولی میں بھی مفید ثابت ہوا ہے۔ ریاضیاتی نوٹیشن حوالہ جات لیمبڈا کیلکولس بھی دیکھیں۔