डी ब्रुइन संकेतन: Difference between revisions
No edit summary |
No edit summary |
||
| Line 7: | Line 7: | ||
:<math>M,N,... ::=\ v\ |\ [v]\;M\ |\ (M)\;N</math> | :<math>M,N,... ::=\ v\ |\ [v]\;M\ |\ (M)\;N</math> | ||
पारंपरिक वाक्यविन्यास में शब्दों को आगमनात्मक फ़ंक्शन को परिभाषित करके डी ब्रुइज़न संकेतन में परिवर्तित किया जा सकता है <math>\mathcal{I}</math> जिसके लिए: | पारंपरिक वाक्यविन्यास में शब्दों को आगमनात्मक फ़ंक्शन को परिभाषित करके डी ब्रुइज़न संकेतन में परिवर्तित किया जा सकता है <math>\mathcal{I}</math> जिसके लिए:<blockquote><math> | ||
< | |||
\begin{align} | \begin{align} | ||
\mathcal{I}(v) &= v \\ | \mathcal{I}(v) &= v \\ | ||
| Line 14: | Line 13: | ||
\mathcal{I}(M\;N) &= (\mathcal{I}(N))\mathcal{I}(M). | \mathcal{I}(M\;N) &= (\mathcal{I}(N))\mathcal{I}(M). | ||
\end{align} | \end{align} | ||
</math></ | </math></blockquote>λ-शर्तों पर सभी परिचालन इसके संबंध में चलते हैं <math>\mathcal{I}</math> अनुवाद. उदाहरण के लिए, सामान्य β-कमी, | ||
λ-शर्तों पर सभी परिचालन इसके संबंध में चलते हैं <math>\mathcal{I}</math> अनुवाद. उदाहरण के लिए, सामान्य β-कमी, | |||
:<math>(\lambda v.\ M)\;N\ \ \longrightarrow_\beta\ \ M[v := N]</math> | :<math>(\lambda v.\ M)\;N\ \ \longrightarrow_\beta\ \ M[v := N]</math> | ||
डी ब्रुइज़ संकेतन में, अनुमानतः, | डी ब्रुइज़ संकेतन में, अनुमानतः, | ||
:<math>(N)\;[v]\;M\ \ \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–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–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><blockquote><math> | ||
< | |||
\begin{align} | \begin{align} | ||
(M)\;\underline{(N)\;[u]}\;(P)\;[v]\;[w]\;(Q)\;z | (M)\;\underline{(N)\;[u]}\;(P)\;[v]\;[w]\;(Q)\;z | ||
| Line 31: | Line 27: | ||
(Q[u:=N,v:=P[u:=N],w:=M])\;z. | (Q[u:=N,v:=P[u:=N],w:=M])\;z. | ||
\end{align} | \end{align} | ||
</math></ | </math></blockquote>इस प्रकार, यदि कोई एप्लिकेटर को खुले माता-पिता के रूप में देखता है ('<code>(</code>') और अमूर्त को निकट कोष्ठक के रूप में ('<code>]</code>'), तो उपरोक्त पद में पैटर्न 'है<code>((](]]</code>'. डी ब्रुइज़न ने इस व्याख्या में एप्लिकेटर और उसके संबंधित अमूर्त को साझेदार कहा है, और वैगनों को बिना साझेदारों के स्नातक कहा है। वैगनों का क्रम, जिसे उन्होंने खंड कहा है, अच्छी तरह से संतुलित होता है यदि उसके सभी वैगनों की भागीदारी हो। | ||
इस प्रकार, यदि कोई एप्लिकेटर को खुले माता-पिता के रूप में देखता है ('<code>(</code>') और अमूर्त को निकट कोष्ठक के रूप में ('<code>]</code>'), तो उपरोक्त पद में पैटर्न 'है<code>((](]]</code>'. डी ब्रुइज़न ने इस व्याख्या में एप्लिकेटर और उसके संबंधित अमूर्त को साझेदार कहा है, और वैगनों को बिना साझेदारों के स्नातक कहा है। वैगनों का क्रम, जिसे उन्होंने खंड कहा है, अच्छी तरह से संतुलित होता है यदि उसके सभी वैगनों की भागीदारी हो। | |||
== डी ब्रुइज़न संकेतन के लाभ == | == डी ब्रुइज़न संकेतन के लाभ == | ||
| Line 40: | Line 34: | ||
λ-शब्दों के कई गुण जिन्हें पारंपरिक संकेतन का उपयोग करके बताना और सिद्ध करना जटिल है, डी ब्रुइज़न संकेतन में आसानी से व्यक्त किए जाते हैं। उदाहरण के लिए, [[ प्रकार सिद्धांत |प्रकार सिद्धांत]] | टाइप-थियोरेटिक सेटिंग में, कोई टाइपिंग संदर्भ में किसी शब्द के लिए प्रकारों के विहित वर्ग की आसानी से गणना कर सकता है, और [[टाइप चेकिंग]] समस्या को यह सत्यापित करने के लिए पुन: स्थापित कर सकता है कि चेक किया गया प्रकार इस वर्ग का सदस्य है। <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–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–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> | ||
== यह भी देखें == | == यह भी देखें == | ||
* [[गणितीय संकेतन]] | * [[गणितीय संकेतन]] | ||
Revision as of 19:51, 14 July 2023
गणितीय तर्क में, डी ब्रुइज़न संकेतन नीदरलैंड के गणितज्ञ निकोलस गोवर्ट डी ब्रुइज़न द्वारा आविष्कार किए गए λ कैलकुलस में शब्दों के लिए वाक्यविन्यास (तर्क) है।[1] इसे λ कैलकुलस के लिए सामान्य सिंटैक्स के उलट के रूप में देखा जा सकता है, जहां किसी एप्लिकेशन में तर्क (कंप्यूटर विज्ञान) को बाद के मुख्य भाग के अतिरिक्त फ़ंक्शन (गणित) में उसके संबंधित बाइंडर के बगल में रखा जाता है।
औपचारिक परिभाषा
शर्तें () डी ब्रुइज़न संकेतन में या तो चर हैं (), या दो वैगन उपसर्गों में से है। अमूर्त वैगन, लिखा हुआ , λ कैलकुलस के सामान्य λ-बाइंडर और लिखित एप्लिकेटर वैगन से मेल खाता है , λ कैलकुलस में एप्लिकेशन में तर्क से मेल खाता है।
पारंपरिक वाक्यविन्यास में शब्दों को आगमनात्मक फ़ंक्शन को परिभाषित करके डी ब्रुइज़न संकेतन में परिवर्तित किया जा सकता है जिसके लिए:
λ-शर्तों पर सभी परिचालन इसके संबंध में चलते हैं अनुवाद. उदाहरण के लिए, सामान्य β-कमी,
डी ब्रुइज़ संकेतन में, अनुमानतः,
इस संकेतन की विशेषता यह है कि β-रिडेक्स के एब्सट्रैक्टर और एप्लिकेटर वैगनों को कोष्ठक की तरह जोड़ा जाता है। उदाहरण के लिए, पद के β-कमी के चरणों पर विचार करें , जहां रिडेक्स को रेखांकित किया गया है:[2]
इस प्रकार, यदि कोई एप्लिकेटर को खुले माता-पिता के रूप में देखता है ('(') और अमूर्त को निकट कोष्ठक के रूप में (']'), तो उपरोक्त पद में पैटर्न 'है((](]]'. डी ब्रुइज़न ने इस व्याख्या में एप्लिकेटर और उसके संबंधित अमूर्त को साझेदार कहा है, और वैगनों को बिना साझेदारों के स्नातक कहा है। वैगनों का क्रम, जिसे उन्होंने खंड कहा है, अच्छी तरह से संतुलित होता है यदि उसके सभी वैगनों की भागीदारी हो।
डी ब्रुइज़न संकेतन के लाभ
अच्छी तरह से संतुलित खंड में, भागीदारी वाले वैगनों को इच्छानुसार से इधर-उधर ले जाया जा सकता है और, जब तक समता नष्ट नहीं होती है, तब तक शब्द का अर्थ वही रहता है। उदाहरण के लिए, उपरोक्त उदाहरण में, एप्लिकेटर इसके अमूर्तक में लाया जा सकता है , या एप्लिकेटर का सार। वास्तव में, लैम्ब्डा शर्तों पर सभी क्रमविनिमेय रूपांतरण और क्रमविनिमेय रूपांतरणों को केवल भागीदारी वाले वैगनों की समता-संरक्षण पुनर्व्यवस्था के संदर्भ में वर्णित किया जा सकता है। इस प्रकार डी ब्रुइज़न संकेतन में λ-शब्दों के लिए सामान्यीकृत रूपांतरण आदिम प्राप्त होता है।
λ-शब्दों के कई गुण जिन्हें पारंपरिक संकेतन का उपयोग करके बताना और सिद्ध करना जटिल है, डी ब्रुइज़न संकेतन में आसानी से व्यक्त किए जाते हैं। उदाहरण के लिए, प्रकार सिद्धांत | टाइप-थियोरेटिक सेटिंग में, कोई टाइपिंग संदर्भ में किसी शब्द के लिए प्रकारों के विहित वर्ग की आसानी से गणना कर सकता है, और टाइप चेकिंग समस्या को यह सत्यापित करने के लिए पुन: स्थापित कर सकता है कि चेक किया गया प्रकार इस वर्ग का सदस्य है। [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).
