डी ब्रुइन संकेतन

For प्राकृतिक संख्याओं के साथ चरों का प्रतिनिधित्व, see डी ब्रुइज़न सूचकांक.

गणितीय तर्क में, डी ब्रुइज़न संकेतन नीदरलैंड के गणितज्ञ निकोलस गोवर्ट डी ब्रुइज़न द्वारा आविष्कार किए गए λ कैलकुलस में शब्दों के लिए वाक्यविन्यास (तर्क) है। इसे λ कैलकुलस के लिए सामान्य सिंटैक्स के उलट के रूप में देखा जा सकता है, जहां किसी एप्लिकेशन में तर्क (कंप्यूटर विज्ञान) को बाद के मुख्य भाग के अतिरिक्त फ़ंक्शन (गणित) में उसके संबंधित बाइंडर के बगल में रखा जाता है।

औपचारिक परिभाषा

शर्तें ($M,N,\ldots$) डी ब्रुइज़न संकेतन में या तो चर हैं ($v$), या दो वैगन उपसर्गों में से है। अमूर्त वैगन, लिखा हुआ $[v]$, λ कैलकुलस के सामान्य λ-बाइंडर और लिखित एप्लिकेटर वैगन से मेल खाता है $(M)$, λ कैलकुलस में एप्लिकेशन में तर्क से मेल खाता है।

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

पारंपरिक वाक्यविन्यास में शब्दों को आगमनात्मक फ़ंक्शन को परिभाषित करके डी ब्रुइज़न संकेतन में परिवर्तित किया जा सकता है ${\mathcal {I}}$ जिसके लिए: <ब्लॉककोट>${\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}}$</ब्लॉककोट>

λ-शर्तों पर सभी परिचालन इसके संबंध में चलते हैं ${\mathcal {I}}$ अनुवाद. उदाहरण के लिए, सामान्य β-कमी,

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

डी ब्रुइज़ संकेतन में, अनुमानतः,

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

इस संकेतन की विशेषता यह है कि β-रिडेक्स के एब्सट्रैक्टर और एप्लिकेटर वैगनों को कोष्ठक की तरह जोड़ा जाता है। उदाहरण के लिए, पद के β-कमी के चरणों पर विचार करें $(M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z$, जहां रिडेक्स को रेखांकित किया गया है: <ब्लॉककोट>${\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}}$</ब्लॉककोट>

इस प्रकार, यदि कोई एप्लिकेटर को खुले माता-पिता के रूप में देखता है ('(') और अमूर्त को निकट कोष्ठक के रूप में (']'), तो उपरोक्त पद में पैटर्न 'है((](]]'. डी ब्रुइज़न ने इस व्याख्या में एप्लिकेटर और उसके संबंधित अमूर्त को साझेदार कहा है, और वैगनों को बिना साझेदारों के स्नातक कहा है। वैगनों का क्रम, जिसे उन्होंने खंड कहा है, अच्छी तरह से संतुलित होता है यदि उसके सभी वैगनों की भागीदारी हो।

डी ब्रुइज़न संकेतन के लाभ

अच्छी तरह से संतुलित खंड में, भागीदारी वाले वैगनों को इच्छानुसार से इधर-उधर ले जाया जा सकता है और, जब तक समता नष्ट नहीं होती है, तब तक शब्द का अर्थ वही रहता है। उदाहरण के लिए, उपरोक्त उदाहरण में, एप्लिकेटर $(M)$ इसके अमूर्तक में लाया जा सकता है $[w]$, या एप्लिकेटर का सार। वास्तव में, लैम्ब्डा शर्तों पर सभी क्रमविनिमेय रूपांतरण और क्रमविनिमेय रूपांतरणों को केवल भागीदारी वाले वैगनों की समता-संरक्षण पुनर्व्यवस्था के संदर्भ में वर्णित किया जा सकता है। इस प्रकार डी ब्रुइज़न संकेतन में λ-शब्दों के लिए सामान्यीकृत रूपांतरण आदिम प्राप्त होता है।

λ-शब्दों के कई गुण जिन्हें पारंपरिक संकेतन का उपयोग करके बताना और सिद्ध करना जटिल है, डी ब्रुइज़न संकेतन में आसानी से व्यक्त किए जाते हैं। उदाहरण के लिए, प्रकार सिद्धांत | टाइप-थियोरेटिक सेटिंग में, कोई टाइपिंग संदर्भ में किसी शब्द के लिए प्रकारों के विहित वर्ग की आसानी से गणना कर सकता है, और टाइप चेकिंग समस्या को यह सत्यापित करने के लिए पुन: स्थापित कर सकता है कि चेक किया गया प्रकार इस वर्ग का सदस्य है। शुद्ध प्रकार की प्रणालियों में स्पष्ट प्रतिस्थापन के लिए कैलकुली में डी ब्रुइज़न संकेतन को भी उपयोगी दिखाया गया है।

यह भी देखें

• गणितीय संकेतन