डी ब्रुइन संकेतन: Difference between revisions

Revision as of 19:49, 14 July 2023

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

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

शर्तें ( $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$ , जहां रिडेक्स को रेखांकित किया गया है:^[2] <ब्लॉककोट> ${\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]$ , या एप्लिकेटर का सार। वास्तव में, लैम्ब्डा शर्तों पर सभी क्रमविनिमेय रूपांतरण और क्रमविनिमेय रूपांतरणों को केवल भागीदारी वाले वैगनों की समता-संरक्षण पुनर्व्यवस्था के संदर्भ में वर्णित किया जा सकता है। इस प्रकार डी ब्रुइज़न संकेतन में λ-शब्दों के लिए सामान्यीकृत रूपांतरण आदिम प्राप्त होता है।

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

यह भी देखें

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

संदर्भ

↑ De Bruijn, Nicolaas Govert (1980). "A survey of the project AUTOMATH". In Hindley J. R. and Seldin J. P. (ed.). To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press. pp. 29–61. ISBN 978-0-12-349050-6. OCLC 6305265.
↑ Kamareddine, Fairouz (2001). "Reviewing the classical and the De Bruijn notation for λ-calculus and pure type systems". Logic and Computation. 11 (3): 363–394. CiteSeerX 10.1.1.29.3756. doi:10.1093/logcom/11.3.363. ISSN 0955-792X. The example is from page 384.
↑ Kamareddine, Fairouz; Nederpelt, Rob (1996). "A useful λ-notation". Theoretical Computer Science. 155: 85–109. doi:10.1016/0304-3975(95)00101-8. ISSN 0304-3975.
↑ De Leuw, B.-J. (1995). "Generalisations in the λ-calculus and its type theory". Masters Thesis, University of Glasgow. {{cite journal}}: Cite journal requires |journal= (help).

[de_bruijn_80-1] De Bruijn, Nicolaas Govert (1980). "A survey of the project AUTOMATH". In Hindley J. R. and Seldin J. P. (ed.). To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press. pp. 29–61. ISBN 978-0-12-349050-6. OCLC 6305265.

[kamaredding_2003-2] Kamareddine, Fairouz (2001). "Reviewing the classical and the De Bruijn notation for λ-calculus and pure type systems". Logic and Computation. 11 (3): 363–394. CiteSeerX 10.1.1.29.3756. doi:10.1093/logcom/11.3.363. ISSN 0955-792X. The example is from page 384.

[kamareddine_nederpelt_96-3] Kamareddine, Fairouz; Nederpelt, Rob (1996). "A useful λ-notation". Theoretical Computer Science. 155: 85–109. doi:10.1016/0304-3975(95)00101-8. ISSN 0304-3975.

[leuw_95-4] De Leuw, B.-J. (1995). "Generalisations in the λ-calculus and its type theory". Masters Thesis, University of Glasgow. {{cite journal}}: Cite journal requires |journal= (help).

[1]

[2]

[3]

[4]

@@ Line 1: / Line 1: @@
-{{for|the representation of variables with natural numbers|De Bruijn index}}
+{{for|प्राकृतिक संख्याओं के साथ चरों का प्रतिनिधित्व|डी ब्रुइज़न सूचकांक}}
-[[गणितीय तर्क]] में, डी ब्रुइज़न नोटेशन [[नीदरलैंड]] के [[गणितज्ञ]] [[निकोलस गोवर्ट डी ब्रुइज़न]] द्वारा आविष्कार किए गए λ कैलकुलस में शब्दों के लिए एक [[वाक्यविन्यास (तर्क)]] है।<ref name="de bruijn 80">{{cite book|author=De Bruijn, Nicolaas Govert|chapter=A survey of the project AUTOMATH|title=To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism|editor=Hindley J. R. and Seldin J. P.|pages=29&ndash;61|publisher=[[Academic Press]]|year=1980|isbn=978-0-12-349050-6|oclc=6305265}}</ref> इसे λ कैलकुलस के लिए सामान्य सिंटैक्स के उलट के रूप में देखा जा सकता है जहां किसी एप्लिकेशन में [[तर्क (कंप्यूटर विज्ञान)]] को बाद के मुख्य भाग के बजाय [[फ़ंक्शन (गणित)]] में उसके संबंधित बाइंडर के बगल में रखा जाता है।
+[[गणितीय तर्क]] में, '''डी ब्रुइज़न संकेतन''' [[नीदरलैंड]] के [[गणितज्ञ]] [[निकोलस गोवर्ट डी ब्रुइज़न]] द्वारा आविष्कार किए गए λ कैलकुलस में शब्दों के लिए [[वाक्यविन्यास (तर्क)]] है।<ref name="de bruijn 80">{{cite book|author=De Bruijn, Nicolaas Govert|chapter=A survey of the project AUTOMATH|title=To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism|editor=Hindley J. R. and Seldin J. P.|pages=29&ndash;61|publisher=[[Academic Press]]|year=1980|isbn=978-0-12-349050-6|oclc=6305265}}</ref> इसे λ कैलकुलस के लिए सामान्य सिंटैक्स के उलट के रूप में देखा जा सकता है, जहां किसी एप्लिकेशन में [[तर्क (कंप्यूटर विज्ञान)]] को बाद के मुख्य भाग के अतिरिक्त [[फ़ंक्शन (गणित)]] में उसके संबंधित बाइंडर के बगल में रखा जाता है।
 == औपचारिक परिभाषा ==
-शर्तें (<math>M, N, \ldots</math>) डी ब्रुइज़न नोटेशन में या तो चर हैं (<math>v</math>), या दो वैगन उपसर्गों में से एक है। अमूर्त वैगन, लिखा हुआ <math>[v]</math>, λ कैलकुलस के सामान्य λ-बाइंडर और लिखित एप्लिकेटर वैगन से मेल खाता है <math>(M)</math>, λ कैलकुलस में एक एप्लिकेशन में तर्क से मेल खाता है।
+शर्तें (<math>M, N, \ldots</math>) डी ब्रुइज़न संकेतन में या तो चर हैं (<math>v</math>), या दो वैगन उपसर्गों में से है। अमूर्त वैगन, लिखा हुआ <math>[v]</math>, λ कैलकुलस के सामान्य λ-बाइंडर और लिखित एप्लिकेटर वैगन से मेल खाता है <math>(M)</math>, λ कैलकुलस में एप्लिकेशन में तर्क से मेल खाता है।
 :<math>M,N,... ::=\ v\ |\ [v]\;M\ |\ (M)\;N</math>
-पारंपरिक वाक्यविन्यास में शब्दों को आगमनात्मक फ़ंक्शन को परिभाषित करके डी ब्रुइज़न नोटेशन में परिवर्तित किया जा सकता है <math>\mathcal{I}</math> जिसके लिए:
+पारंपरिक वाक्यविन्यास में शब्दों को आगमनात्मक फ़ंक्शन को परिभाषित करके डी ब्रुइज़न संकेतन में परिवर्तित किया जा सकता है <math>\mathcal{I}</math> जिसके लिए:
 <ब्लॉककोट><math>
 \begin{align}
@@ Line 18: / Line 18: @@
 λ-शर्तों पर सभी परिचालन इसके संबंध में चलते हैं <math>\mathcal{I}</math> अनुवाद. उदाहरण के लिए, सामान्य β-कमी,
 :<math>(\lambda v.\ M)\;N\ \ \longrightarrow_\beta\ \ M[v := N]</math>
-डी ब्रुइज़ नोटेशन में, अनुमानतः,
+डी ब्रुइज़ संकेतन में, अनुमानतः,
 :<math>(N)\;[v]\;M\ \ \longrightarrow_\beta\ \ M[v := N].</math>
-इस नोटेशन की एक विशेषता यह है कि β-रिडेक्स के एब्सट्रैक्टर और एप्लिकेटर वैगनों को कोष्ठक की तरह जोड़ा जाता है। उदाहरण के लिए, पद के β-कमी के चरणों पर विचार करें <math>(M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z</math>, जहां रिडेक्स को रेखांकित किया गया है:<ref name="kamaredding 2003">{{cite journal|author=Kamareddine, Fairouz|title=Reviewing the classical and the De Bruijn notation for λ-calculus and pure type systems|journal=[[Logic and Computation]]|volume=11|issue=3|pages=363&ndash;394|year=2001|issn=0955-792X|doi=10.1093/logcom/11.3.363|citeseerx=10.1.1.29.3756}} The example is from page 384.</ref>
+इस संकेतन की विशेषता यह है कि β-रिडेक्स के एब्सट्रैक्टर और एप्लिकेटर वैगनों को कोष्ठक की तरह जोड़ा जाता है। उदाहरण के लिए, पद के β-कमी के चरणों पर विचार करें <math>(M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z</math>, जहां रिडेक्स को रेखांकित किया गया है:<ref name="kamaredding 2003">{{cite journal|author=Kamareddine, Fairouz|title=Reviewing the classical and the De Bruijn notation for λ-calculus and pure type systems|journal=[[Logic and Computation]]|volume=11|issue=3|pages=363&ndash;394|year=2001|issn=0955-792X|doi=10.1093/logcom/11.3.363|citeseerx=10.1.1.29.3756}} The example is from page 384.</ref>
 <ब्लॉककोट><math>
 \begin{align}
@@ Line 33: / Line 33: @@
 </math></ब्लॉककोट>
-इस प्रकार, यदि कोई एप्लिकेटर को एक खुले माता-पिता के रूप में देखता है ('<code>(</code>') और अमूर्त को निकट कोष्ठक के रूप में ('<code>]</code>'), तो उपरोक्त पद में पैटर्न 'है<code>((](]]</code>'. डी ब्रुइज़न ने इस व्याख्या में एक एप्लिकेटर और उसके संबंधित अमूर्त को साझेदार कहा है, और वैगनों को बिना साझेदारों के स्नातक कहा है। वैगनों का एक क्रम, जिसे उन्होंने एक खंड कहा है, अच्छी तरह से संतुलित होता है यदि उसके सभी वैगनों की भागीदारी हो।
+इस प्रकार, यदि कोई एप्लिकेटर को खुले माता-पिता के रूप में देखता है ('<code>(</code>') और अमूर्त को निकट कोष्ठक के रूप में ('<code>]</code>'), तो उपरोक्त पद में पैटर्न 'है<code>((](]]</code>'. डी ब्रुइज़न ने इस व्याख्या में एप्लिकेटर और उसके संबंधित अमूर्त को साझेदार कहा है, और वैगनों को बिना साझेदारों के स्नातक कहा है। वैगनों का क्रम, जिसे उन्होंने खंड कहा है, अच्छी तरह से संतुलित होता है यदि उसके सभी वैगनों की भागीदारी हो।
-== डी ब्रुइज़न नोटेशन के लाभ ==
+== डी ब्रुइज़न संकेतन के लाभ ==
-एक अच्छी तरह से संतुलित खंड में, भागीदारी वाले वैगनों को मनमाने ढंग से इधर-उधर ले जाया जा सकता है और, जब तक समता नष्ट नहीं होती है, तब तक शब्द का अर्थ वही रहता है। उदाहरण के लिए, उपरोक्त उदाहरण में, एप्लिकेटर <math>(M)</math> इसके अमूर्तक में लाया जा सकता है <math>[w]</math>, या एप्लिकेटर का सार। वास्तव में, लैम्ब्डा शर्तों पर सभी [[क्रमविनिमेय रूपांतरण]]ों और क्रमविनिमेय रूपांतरणों को केवल भागीदारी वाले वैगनों की समता-संरक्षण पुनर्व्यवस्था के संदर्भ में वर्णित किया जा सकता है। इस प्रकार डी ब्रुइज़न नोटेशन में λ-शब्दों के लिए एक सामान्यीकृत रूपांतरण आदिम प्राप्त होता है।
+अच्छी तरह से संतुलित खंड में, भागीदारी वाले वैगनों को इच्छानुसार से इधर-उधर ले जाया जा सकता है और, जब तक समता नष्ट नहीं होती है, तब तक शब्द का अर्थ वही रहता है। उदाहरण के लिए, उपरोक्त उदाहरण में, एप्लिकेटर <math>(M)</math> इसके अमूर्तक में लाया जा सकता है <math>[w]</math>, या एप्लिकेटर का सार। वास्तव में, लैम्ब्डा शर्तों पर सभी [[क्रमविनिमेय रूपांतरण]] और क्रमविनिमेय रूपांतरणों को केवल भागीदारी वाले वैगनों की समता-संरक्षण पुनर्व्यवस्था के संदर्भ में वर्णित किया जा सकता है। इस प्रकार डी ब्रुइज़न संकेतन में λ-शब्दों के लिए सामान्यीकृत रूपांतरण आदिम प्राप्त होता है।
-λ-शब्दों के कई गुण जिन्हें पारंपरिक नोटेशन का उपयोग करके बताना और साबित करना मुश्किल है, डी ब्रुइज़न नोटेशन में आसानी से व्यक्त किए जाते हैं। उदाहरण के लिए, [[ प्रकार सिद्धांत ]]|टाइप-थियोरेटिक सेटिंग में, कोई टाइपिंग संदर्भ में किसी शब्द के लिए प्रकारों के विहित वर्ग की आसानी से गणना कर सकता है, और [[टाइप चेकिंग]] समस्या को यह सत्यापित करने के लिए पुन: स्थापित कर सकता है कि चेक किया गया प्रकार इस वर्ग का सदस्य है। .<ref name="kamareddine nederpelt 96">{{cite journal|author=Kamareddine, Fairouz|author2=Nederpelt, Rob|title=A useful λ-notation|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=155|year=1996|pages=85&ndash;109|issn=0304-3975|doi=10.1016/0304-3975(95)00101-8|doi-access=free}}</ref> शुद्ध प्रकार की प्रणालियों में [[स्पष्ट प्रतिस्थापन]] के लिए कैलकुली में डी ब्रुइज़न नोटेशन को भी उपयोगी दिखाया गया है।<ref name="leuw 95">{{Cite journal|last=De Leuw|first=B.-J.|title=Generalisations in the λ-calculus and its type theory|year=1995|place=Masters Thesis, [[University of Glasgow]]}}.</ref>
+λ-शब्दों के कई गुण जिन्हें पारंपरिक संकेतन का उपयोग करके बताना और सिद्ध करना जटिल है, डी ब्रुइज़न संकेतन में आसानी से व्यक्त किए जाते हैं। उदाहरण के लिए, [[ प्रकार सिद्धांत |प्रकार सिद्धांत]] | टाइप-थियोरेटिक सेटिंग में, कोई टाइपिंग संदर्भ में किसी शब्द के लिए प्रकारों के विहित वर्ग की आसानी से गणना कर सकता है, और [[टाइप चेकिंग]] समस्या को यह सत्यापित करने के लिए पुन: स्थापित कर सकता है कि चेक किया गया प्रकार इस वर्ग का सदस्य है। <ref name="kamareddine nederpelt 96">{{cite journal|author=Kamareddine, Fairouz|author2=Nederpelt, Rob|title=A useful λ-notation|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=155|year=1996|pages=85&ndash;109|issn=0304-3975|doi=10.1016/0304-3975(95)00101-8|doi-access=free}}</ref> शुद्ध प्रकार की प्रणालियों में [[स्पष्ट प्रतिस्थापन]] के लिए कैलकुली में डी ब्रुइज़न संकेतन को भी उपयोगी दिखाया गया है।<ref name="leuw 95">{{Cite journal|last=De Leuw|first=B.-J.|title=Generalisations in the λ-calculus and its type theory|year=1995|place=Masters Thesis, [[University of Glasgow]]}}.</ref>

Anonymous

Search

डी ब्रुइन संकेतन: Difference between revisions

Namespaces

More

Page actions

Revision as of 19:49, 14 July 2023

Contents

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

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

यह भी देखें

संदर्भ

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

डी ब्रुइन संकेतन: Difference between revisions

Revision as of 19:49, 14 July 2023

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

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

यह भी देखें

संदर्भ

Navigation

Wiki tools

Page tools

Other projects

Categories