De Bruijn index
गणितीय तर्क में, डी ब्रुइजन सूचकांक एक उपकरण है जिसका आविष्कार डच गणितशास्त्री निकोलास गोवर्ट डी ब्रुइजन ने बाउंड चर का नामकरण किए बिना लैम्ब्डा कलन के शब्दों का प्रतिनिधित्व करने के लिए किया था। इन सूचकांकों का उपयोग करके लिखे गए शब्द α-रूपांतरण के संबंध में अपरिवर्तनीय हैं, इसलिए α-समतुल्यता के लिए जाँच वाक्य रचना समानता के लिए समान है। प्रत्येक डी ब्रुइजन सूचकांक एक प्राकृतिक संख्या है जो एक λ-अवधि में एक चर की घटना का प्रतिनिधित्व करता है, और उन बाइंडरों की संख्या को दर्शाता है जो उस घटना और उसके संबंधित बाइंडर के बीच दायरे में हैं। निम्नलिखित कुछ उदाहरण हैंः λx शब्द। λy। x, जिसे कभी-कभी K संयोजक कहा जाता है, को डी ब्रुइजन सूचकांकों के साथ λλ2 के रूप में लिखा जाता है। घटना x के लिए बाइंडर दायरे में दूसरा λ है। शब्द λx। λy। λz। डी ब्रुइजन सूचकांकों के साथ xz (yz) (S संयोजक), λλλ31 (211) है। शब्द λz। (λy। y (λx। x)) (λx। z x) λ (λ1 (λ1)) (λ21) है। निम्नलिखित चित्रण देखें, जहाँ बांधने वाले रंगीन हैं और संदर्भ तीरों के साथ दिखाए गए हैं। डी ब्रुइजन सूचकांकों का उपयोग आमतौर पर उच्च-क्रम तर्क प्रणालियों जैसे स्वचालित प्रमेय प्रोवर्स और तर्क प्रोग्रामिंग प्रणालियों में किया जाता है। औपचारिक परिभाषा औपचारिक रूप से, डी ब्रुइजन सूचकांकों का उपयोग करके लिखे गए λ-शब्दों (M, N,.) में निम्नलिखित वाक्यविन्यास होता है (कोष्ठकों को स्वतंत्र रूप से अनुमति दी जाती है): M, N,:: = n। M N। λ M जहाँ n-0 से अधिक प्राकृतिक संख्याएँ-चर हैं। एक चर n बाध्य है यदि यह कम से कम n बाइंडर (λ) के दायरे में है; अन्यथा यह मुक्त है। एक चर n के लिए बंधन स्थल n वां बंधनक है जो इसके दायरे में है, जो सबसे भीतरी बंधनक से शुरू होता है। λ-शब्दों पर सबसे आदिम संचालन प्रतिस्थापन हैः एक शब्द में मुक्त चर को अन्य शब्दों के साथ बदलना। उदाहरण के लिए, β-रिडक्शन (λM) N में, हमें M में चर n1, n2,., 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 लिखा जाता है, जहाँ Mi, ith मुक्त चर के लिए प्रतिस्थापन है। चरण 3 में बढ़ते संचालन को कभी-कभी शिफ्ट कहा जाता है और लिखा जाता है जहाँ k एक प्राकृतिक संख्या है जो चर को बढ़ाने की राशि को दर्शाती है, और इसे इस प्रकार परिभाषित किया जाता है उदाहरण के लिए, 0 पहचान प्रतिस्थापन है, जिससे एक शब्द अपरिवर्तित रहता है। M1.M2.Mn शब्दों की एक सीमित सूची प्रतिस्थापन M1.M2.Mn. (n + 1). (n + 2) को संक्षिप्त करती है। सभी चरों को n से अधिक अपरिवर्तित छोड़ दें। एम शब्द के प्रतिस्थापन एस के अनुप्रयोग को एम [एस] लिखा जाता है। दो प्रतिस्थापन s1 और s2 की संरचना को s1s2 लिखा जाता है और इसे (M1.M2) s = M1 [s]. M2 [s] द्वारा परिभाषित किया जाता है. गुण M [s1s2] = (M [s1]) [s2] को संतुष्ट करता है, और प्रतिस्थापन को निम्न शब्दों पर परिभाषित किया जाता हैः उपरोक्त β-कटौती के लिए उल्लिखित चरणों को इस प्रकार अधिक संक्षिप्त रूप से व्यक्त किया जाता हैः (λM) N → βM [N]। डी ब्रुइजन सूचकांकों के विकल्प जब λ-शब्दों के मानक "नामित" प्रतिनिधित्व का उपयोग करते हैं, जहां चर को लेबल या स्ट्रिंग के रूप में माना जाता है, तो शब्दों पर किसी भी ऑपरेशन को परिभाषित करते समय स्पष्ट रूप से α-रूपांतरण को संभालना चाहिए। व्यवहार में यह बोझिल, अक्षम और अक्सर त्रुटि-प्रवण होता है। इसलिए इसने ऐसे शब्दों के विभिन्न प्रतिनिधित्वों की खोज की है। दूसरी ओर, λ-शब्दों का नामित प्रतिनिधित्व अधिक व्यापक है और दूसरों द्वारा अधिक तुरंत समझा जा सकता है क्योंकि चर को वर्णनात्मक नाम दिए जा सकते हैं। इस प्रकार, भले ही कोई प्रणाली आंतरिक रूप से डी ब्रुइजन सूचकांकों का उपयोग करती है, यह नामों के साथ एक उपयोगकर्ता इंटरफेस प्रस्तुत करेगी। डी ब्रुइजन सूचकांकों को देखने का एक वैकल्पिक तरीका डी ब्रुइजन स्तरों के रूप में है, जो ऊपर के बजाय स्टैक के नीचे से चर को अनुक्रमित करता है। यह रीइंडेक्स मुक्त चर की आवश्यकता को समाप्त करता है, उदाहरण के लिए जब संदर्भ कमजोर होता है, जबकि डी ब्रुइजन सूचकांक रीइंडेक्स बाध्य चर की आवश्यकता को समाप्त करते हैं, उदाहरण के लिए जब किसी अन्य संदर्भ में एक बंद अभिव्यक्ति को प्रतिस्थापित किया जाता है। डी ब्रुइजन सूचकांक λ-शब्दों का एकमात्र प्रतिनिधित्व नहीं है जो α-रूपांतरण की समस्या को दूर करता है। नामित अभ्यावेदनों में, पिट्स और गब्बे की नाममात्र तकनीक एक दृष्टिकोण है, जहां एक λ-शब्द के प्रतिनिधित्व को परिवर्तनीय क्रमपरिवर्तन का उपयोग करके फिर से लिखने योग्य सभी शब्दों के समतुल्य वर्ग के रूप में माना जाता है। यह दृष्टिकोण इसाबेल/एचओएल के नॉमिनल डेटाटाइप पैकेज द्वारा लिया जाता है। एक अन्य सामान्य विकल्प उच्च-क्रम प्रतिनिधित्वों के लिए एक अपील है जहां λ-बाइंडर को एक सही कार्य के रूप में माना जाता है। इस तरह के अभ्यावेदन में, α-समतुल्यता, प्रतिस्थापन आदि के मुद्दे। एक मेटा-लॉजिक में समान संचालन के साथ पहचाने जाते हैं। एक प्रमाण सहायक में एक अनुमानात्मक प्रणाली के मेटा-सैद्धांतिक गुणों के बारे में तर्क करते समय, कभी-कभी स्वयं को प्रथम-क्रम प्रतिनिधित्वों तक सीमित रखना और मान्यताओं को नाम देने या उनका नाम बदलने की क्षमता रखना वांछनीय होता है। स्थानीय रूप से अनाम दृष्टिकोण चर के मिश्रित प्रतिनिधित्व का उपयोग करता है-बाध्य चर के लिए डी ब्रुइजन सूचकांक और मुक्त चर के लिए नाम-जो उपयुक्त होने पर डी ब्रुइजन अनुक्रमित शब्दों के α-कैनॉनिकल रूप से लाभान्वित होने में सक्षम है। बरेनड्रेग्ट का चर परिपाटी बरेनड्रेग्ट का चर परिपाटी आमतौर पर प्रमाणों और परिभाषाओं में उपयोग किया जाने वाला एक परिपाटी है जहां यह माना जाता है किः बाध्य चर मुक्त चर से अलग हैं, और सभी बाइंडर उन चरों को बांधते हैं जो पहले से ही दायरे में नहीं हैं। एक प्रेरक परिभाषा के सामान्य संदर्भ में, परंपरा का उपयोग करके एक प्रेरक परिभाषा को परिवर्तित करने के लिए α-रूपांतरण को लागू करना संभव नहीं है, क्योंकि एक चर नियम में एक बाध्यकारी स्थिति और एक गैर-बाध्यकारी स्थिति दोनों में दिखाई दे सकता है। प्रेरण सिद्धांत तब लागू होता है जब प्रत्येक नियम निम्नलिखित दो शर्तों को संतुष्ट करता हैः नियम नाममात्र तर्क के अर्थ में समतुल्य है, अर्थात यह कहना कि इसकी वैधता नियम के परिसर को मानते हुए चर का नाम बदलने से अपरिवर्तित है, नियम में बाध्यकारी स्थितियों में चर अलग हैं और निष्कर्ष में स्वतंत्र हैं। संयोजी तर्क, चर नामों को समाप्त करने का एक अधिक आवश्यक तरीका है। संदर्भ लैम्ब्डा कैलकुलस