De Bruijn notation
गणितीय तर्क में, डी ब्रुइजन संकेतन डच गणितशास्त्री निकोलास गोवर्ट डी ब्रुइजन द्वारा आविष्कार किए गए λ कलन में शब्दों के लिए एक वाक्यविन्यास है। इसे λ कलन के लिए सामान्य वाक्यविन्यास के उलट के रूप में देखा जा सकता है जहां एक अनुप्रयोग में तर्क को बाद के मुख्य भाग के बजाय कार्य में इसके संबंधित बाइंडर के बगल में रखा जाता है। औपचारिक परिभाषा डी ब्रुइजन संकेतन में शर्तें () या तो चर () हैं, या दो वैगन उपसर्गों में से एक है। अमूर्त वैगन, लिखित, λ कलन के सामान्य λ-बाइंडर से मेल खाता है, और आवेदक वैगन, लिखित, λ कलन में एक अनुप्रयोग में तर्क से मेल खाता है। पारंपरिक वाक्यविन्यास में शब्दों को एक प्रेरक कार्य को परिभाषित करके डी ब्रुइजन संकेतन में परिवर्तित किया जा सकता है जिसके लिएः अनुवाद के संबंध में λ-शब्दों पर सभी संचालन संचारित होते हैं। उदाहरण के लिए, डी ब्रुइजन संकेतन में सामान्य β-रिडक्शन, अनुमानित रूप से, इस संकेतन की एक विशेषता यह है कि β-रिडेक्स के एब्स्ट्रैक्टर और एप्लीकेटर वैगन को कोष्ठक की तरह जोड़ा जाता है। उदाहरण के लिए, शब्द के β-रिडक्शन के चरणों पर विचार करें, जहां रिडेक्स को रेखांकित किया गया हैः इस प्रकार, यदि कोई आवेदक को एक खुले पैरेंट ('(') और एब्स्ट्रैक्टर को एक करीबी ब्रैकेट (']') के रूप में देखता है, तो उपरोक्त शब्द में पैटर्न '((] (])' है। डी ब्रुइजन ने इस व्याख्या भागीदारों में एक आवेदक और उसके संबंधित अमूर्त को बुलाया, और भागीदारों के बिना वैगनों को अविवाहित कहा। वैगनों का एक क्रम, जिसे उन्होंने एक खंड कहा, अच्छी तरह से संतुलित है यदि इसके सभी वैगन भागीदार हैं। डी ब्रुइजन संकेतन के लाभ एक अच्छी तरह से संतुलित खंड में, भागीदार वैगनों को मनमाने ढंग से इधर-उधर ले जाया जा सकता है और जब तक समानता नष्ट नहीं होती है, तब तक शब्द का अर्थ वही रहता है। उदाहरण के लिए, उपरोक्त उदाहरण में, आवेदक को उसके अमूर्तकर्ता, या अमूर्तकर्ता को आवेदक के पास लाया जा सकता है। वास्तव में, लैम्ब्डा शब्दों पर सभी कम्यूटेटिव और क्रमपरिवर्तन रूपांतरणों को केवल भागीदार वैगनों के समानता-संरक्षण पुनर्व्यवस्था के संदर्भ में वर्णित किया जा सकता है। इस प्रकार डी ब्रुइजन संकेतन में λ-शब्दों के लिए एक सामान्यीकृत रूपांतरण प्राप्त होता है। λ-शब्दों के कई गुण जिन्हें पारंपरिक संकेतन का उपयोग करके बताना और साबित करना मुश्किल है, डी ब्रुइजन संकेतन में आसानी से व्यक्त किए जाते हैं। उदाहरण के लिए, एक प्रकार-सैद्धांतिक सेटिंग में, कोई भी आसानी से टाइपिंग संदर्भ में एक शब्द के लिए प्रकारों के विहित वर्ग की गणना कर सकता है, और प्रकार जाँच समस्या को यह सत्यापित करने के लिए दोहराता है कि जाँच किया गया प्रकार इस वर्ग का सदस्य है। डी ब्रुइजन संकेतन को शुद्ध प्रकार प्रणालियों में स्पष्ट प्रतिस्थापन के लिए गणना में भी उपयोगी दिखाया गया है। गणितीय संकेतन संदर्भ लैम्ब्डा कलन भी देखें।