क्रिवाइन मशीन: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
Line 1: Line 1:
{{Short description|Abstract machine}}
[[सैद्धांतिक कंप्यूटर विज्ञान]] में, '''मशीन वक्र''' एक ''[[अमूर्त मशीन]]'' है (कभी-कभी इसे ''[[ आभासी मशीन |आभासी मशीन]]'' भी कहा जाता है)। एक अमूर्त मशीन के रूप में, यह [[ट्यूरिंग मशीन]] और [[एसईसीडी मशीन]] के साथ सुविधाएँ साझा करती है। वक्र मशीन बताती है कि पुनरावर्ती समारोह की गणना कैसे करें। अधिक विशेष रूप से इसका उद्देश्य [[नाम से बुलाओ]] कमी का उपयोग करके [[लैम्ब्डा कैलकुलस|लैम्ब्डा गणना]] के सामान्य रूप में कमी को सख्ती से परिभाषित करना है। इसकी औपचारिकता के लिए धन्यवाद, यह विवरण में बताता है कि एक प्रकार की कमी कैसे काम करती है और [<nowiki/>[[कार्यात्मक प्रोग्रामिंग]]] भाषाओं के [[परिचालन शब्दार्थ]] की सैद्धांतिक नींव निर्धारित करती है। दूसरी ओर, वक्र मशीन कॉल-बाय-नाम लागू करती है क्योंकि यह समारोह शरीर को उसके पैरामीटर पर लागू करने से पहले β-[[ कम करने योग्य अभिव्यक्ति ]] के शरीर का मूल्यांकन करती है। दूसरे शब्दों में, एक अभिव्यक्ति (''λ'' ''x''. ''t'') ''u'' में यह पहले ''λ'' ''x'' का मूल्यांकन करता है। इसे ''यू'' पर लागू करने से पहले ''टी'' कार्यात्मक प्रोग्रामिंग में, इसका मतलब यह होगा कि किसी पैरामीटर पर लागू समारोह का मूल्यांकन करने के लिए, यह पैरामीटर पर लागू करने से पहले समारोह का मूल्यांकन करता है।
[[File:Machine de Krivine.jpg|thumb|क्रिवाइन मशीन का एक चित्र दृश्य]][[सैद्धांतिक कंप्यूटर विज्ञान]] में, क्रिवाइन मशीन एक ''[[अमूर्त मशीन]]'' है (कभी-कभी इसे ''[[ आभासी मशीन ]]'' भी कहा जाता है)। एक अमूर्त मशीन के रूप में, यह [[ट्यूरिंग मशीन]]ों और [[एसईसीडी मशीन]] के साथ सुविधाएँ साझा करती है। क्रिवाइन मशीन बताती है कि पुनरावर्ती फ़ंक्शन की गणना कैसे करें। अधिक विशेष रूप से इसका उद्देश्य [[नाम से बुलाओ]] रिडक्शन का उपयोग करके [[लैम्ब्डा कैलकुलस]] के सामान्य रूप में कमी को सख्ती से परिभाषित करना है। इसकी औपचारिकता के लिए धन्यवाद, यह विवरण में बताता है कि एक प्रकार की कमी कैसे काम करती है और [[[[कार्यात्मक प्रोग्रामिंग]] भाषा]]ओं के [[परिचालन शब्दार्थ]] की सैद्धांतिक नींव निर्धारित करती है। दूसरी ओर, क्रिवाइन मशीन कॉल-बाय-नाम लागू करती है क्योंकि यह फ़ंक्शन बॉडी को उसके पैरामीटर पर लागू करने से पहले β-[[ कम करने योग्य अभिव्यक्ति ]] के बॉडी का मूल्यांकन करती है। दूसरे शब्दों में, एक अभिव्यक्ति (''λ'' ''x''. ''t'') ''u'' में यह पहले ''λ'' ''x'' का मूल्यांकन करता है। इसे ''यू'' पर लागू करने से पहले ''टी''कार्यात्मक प्रोग्रामिंग में, इसका मतलब यह होगा कि किसी पैरामीटर पर लागू फ़ंक्शन का मूल्यांकन करने के लिए, यह पैरामीटर पर लागू करने से पहले फ़ंक्शन का मूल्यांकन करता है।


क्रिवाइन मशीन को 1980 के दशक की शुरुआत में फ्रांसीसी तर्कशास्त्री :fr:जीन-लुई क्रिवाइन|जीन-लुई क्रिवाइन द्वारा डिजाइन किया गया था।
वक्र मशीन को 1980 के दशक की प्रारंभिक में फ्रांसीसी तर्कशास्त्री :fr:जीन-लुई वक्र जीन-लुई वक्र द्वारा डिजाइन किया गया था।


== नाम और सिर से बुलाएं सामान्य रूप में कमी ==
== नाम और सिर से बुलाएं सामान्य रूप में कमी ==
{{more|Lambda calculus}}
{{more|लैम्ब्डा कैलकुलस}}


क्रिवाइन मशीन लैम्ब्डा कैलकुलस से संबंधित दो अवधारणाओं पर आधारित है, अर्थात् हेड रिडक्शन और नाम से कॉल।
वक्र मशीन लैम्ब्डा गणना से संबंधित दो अवधारणाओं पर आधारित है, अर्थात् सिर में कमी और नाम से कॉल पर आधारित है|


=== सिर सामान्य रूप में कमी ===
=== सिर सामान्य रूप में कमी ===


एक लैम्ब्डा कैलकुलस#कमी<ref>{{Citation
एक लैम्ब्डा गणना कमी<ref>{{Citation
  |last=Barendregt  
  |last=Barendregt  
  |first=Hendrik Pieter  
  |first=Hendrik Pieter  
Line 26: Line 25:
  |archivedate=2004-08-23  
  |archivedate=2004-08-23  
}}  [ftp://ftp.cs.ru.nl/pub/CompMath.Found/ErrataLCalculus.pdf Corrections].
}}  [ftp://ftp.cs.ru.nl/pub/CompMath.Found/ErrataLCalculus.pdf Corrections].
</ref> (एक यह भी कहता है कि β-redex) फॉर्म (λ x. t) u के लैम्ब्डा कैलकुलस का एक शब्द है। यदि किसी पद का आकार (λ x. t) u है<sub>1</sub> ... में<sub>''n''</sub> इसे हेड रिडेक्स कहा जाता है। [[बीटा सामान्य रूप]] लैम्ब्डा कैलकुलस का एक शब्द है जो हेड रिडेक्स नहीं है।{{efn|If one only deals with closed terms, these terms take the form ''λ'' ''x''. ''t''.}} हेड रिडक्शन एक शब्द के संकुचन का एक (गैर-खाली) अनुक्रम है जो हेड रिडेक्स को अनुबंधित करता है। किसी टर्म टी का हेड रिडक्शन (जिसे हेड नॉर्मल फॉर्म में नहीं माना जाता है) एक हेड रिडक्शन है जो टर्म टी से शुरू होता है और हेड नॉर्मल फॉर्म पर खत्म होता है। एक अमूर्त दृष्टिकोण से, हेड रिडक्शन वह तरीका है जिससे एक प्रोग्राम गणना करता है जब वह एक पुनरावर्ती उप-प्रोग्राम का मूल्यांकन करता है। यह समझना महत्वपूर्ण है कि ऐसी कटौती कैसे लागू की जा सकती है। क्रिवाइन मशीन का एक उद्देश्य किसी शब्द को सामान्य रूप में कम करने और इस प्रक्रिया का औपचारिक रूप से वर्णन करने के लिए एक प्रक्रिया का प्रस्ताव करना है। जैसे [[एलन ट्यूरिंग]] ने एल्गोरिदम की धारणा का औपचारिक रूप से वर्णन करने के लिए एक अमूर्त मशीन का उपयोग किया, :fr: जीन-लुई क्रिविन ने सिर के सामान्य रूप में कमी की धारणा का औपचारिक रूप से वर्णन करने के लिए एक अमूर्त मशीन का उपयोग किया।
</ref> (एक यह भी कहता है कि β-रीडेक्स) फॉर्म (λ x. t) u के लैम्ब्डा गणना का एक शब्द है। यदि किसी पद का आकार (λ x. t) u है<sub>1</sub> ... में<sub>''n''</sub> इसे हेड रिडेक्स कहा जाता है। [[बीटा सामान्य रूप]] लैम्ब्डा गणना का एक शब्द है जो हेड रिडेक्स नहीं है।{{efn|If one only deals with closed terms, these terms take the form ''λ'' ''x''. ''t''.}} सिर में कमी एक शब्द के संकुचन का एक (गैर-खाली) अनुक्रम है जो हेड रिडेक्स को अनुबंधित करता है। किसी अवधि टी का सिर में कमी (जिसे सिर सामान्य रूप में नहीं माना जाता है) एक सिर में कमी है जो अवधि टी से शुरू होता है और सिर सामान्य रूप पर खत्म होता है। एक अमूर्त दृष्टिकोण से, सिर में कमी वह विधि है जिससे एक प्रोग्राम गणना करता है जब वह एक पुनरावर्ती उप-प्रोग्राम का मूल्यांकन करता है। यह समझना महत्वपूर्ण है कि ऐसी कटौती कैसे लागू की जा सकती है। वक्र मशीन का एक उद्देश्य किसी शब्द को सामान्य रूप में कम करने और इस प्रक्रिया का औपचारिक रूप से वर्णन करने के लिए एक प्रक्रिया का प्रस्ताव करना है। जैसे [[एलन ट्यूरिंग]] ने कलन विधि की धारणा का औपचारिक रूप से वर्णन करने के लिए एक अमूर्त मशीन का उपयोग किया, :fr: जीन-लुई क्रिविन ने सिर के सामान्य रूप में कमी की धारणा का औपचारिक रूप से वर्णन करने के लिए एक अमूर्त मशीन का उपयोग किया जाता है।


==== उदाहरण ====
==== '''उदाहरण''' ====
शब्द ((λ 0) (λ 0)) (λ 0) (जो अस्पष्ट चरों का उपयोग करता है, उसे टर्म (λx.x) (λy.y) (λz.z) के लिए कहा जाता है) हेड नॉर्मल फॉर्म में नहीं है क्योंकि (λ 0) (λ 0) को (λ 0) में संक्षेपित करता है, जिससे हेड रेडेक्स (λ 0) (λ 0) उत्पन्न होता है, जो (λ 0) में संक्षेपित होता है और जो कि इसलिए ((λ 0) (λ 0)) (λ 0) का हेड नॉर्मल फॉर्म है। दूसरे शब्दों में कहा जाए, हेड नॉर्मल फॉर्म संक्षेपण है:
शब्द ((λ 0) (λ 0)) (λ 0) (जो अस्पष्ट चरों का उपयोग करता है, उसे अवधि (λx.x) (λy.y) (λz.z) के लिए कहा जाता है) सिर सामान्य रूप में नहीं है क्योंकि (λ 0) (λ 0) को (λ 0) में संक्षेपित करता है, जिससे हेड रेडेक्स (λ 0) (λ 0) उत्पन्न होता है, जो (λ 0) में संक्षेपित होता है और जो कि इसलिए ((λ 0) (λ 0)) (λ 0) का सिर सामान्य रूप है। दूसरे शब्दों में कहा जाए, सिर सामान्य रूप संक्षेपण है:
: ((λ 0) (λ 0)) (λ 0) ➝ (λ 0) (λ 0) ➝ λ 0,
: ((λ 0) (λ 0)) (λ 0) ➝ (λ 0) (λ 0) ➝ λ 0,
जो इसके लिए है:
जो इसके लिए है:
: (λx.x) (λy.y) (λz.z) ➝ (λy.y) (λz.z) ➝ λz.z.
: (λx.x) (λy.y) (λz.z) ➝ (λy.y) (λz.z) ➝ λz.z.
आगे चलकर हम देखेंगे कि क्रिवाइन मशीन कैसे टर्म ((λ 0) (λ 0)) (λ 0) को संक्षेपित करती है।
आगे चलकर हम देखेंगे कि वक्र मशीन कैसे अवधि ((λ 0) (λ 0)) (λ 0) को संक्षेपित करती है।


=== नाम से पुकारें ===
=== नाम से पुकारें ===
टर्म u v की हेड रेडक्शन को कार्यान्वित करने के लिए, जो एक एप्लिकेशन है, लेकिन जो रेडेक्स नहीं है, हमें पहले टर्म u को संक्षेपित करके एक अव्यवहार्यता दिखाने के लिए u को संक्षेपित करना होगा, और इस तरह v के साथ एक रेडेक्स बनाना होगा। जब एक रेडेक्स प्रकट होता है, तो हम उसे संक्षेपित करते हैं। एक एप्लिकेशन के बॉडी को हमेशा पहले संक्षेपित करना, कॉल बाय नाम कहलाता है। क्रिवाइन मशीन कॉल बाय नाम को कार्यान्वित करती है।
अवधि u v की हेड रेडक्शन को कार्यान्वित करने के लिए, जो एक आवेदन है, लेकिन जो रेडेक्स नहीं है, हमें पहले अवधि u को संक्षेपित करके एक अव्यवहार्यता दिखाने के लिए u को संक्षेपित करना होगा, और इस तरह v के साथ एक रेडेक्स बनाना होगा। जब एक रेडेक्स प्रकट होता है, तो हम उसे संक्षेपित करते हैं। एक आवेदन के शरीर को सदैव पहले संक्षेपित करना, कॉल बाय नाम कहलाता है। वक्र मशीन कॉल बाय नाम को कार्यान्वित करती है।


== विवरण ==
== विवरण ==


यहां दी गई क्रिवाइन मशीन की प्रस्तुति लैम्ब्डा शब्दों के नोटेशन पर आधारित है जो डी ब्रूजन सूचकांकों का उपयोग करती है और मानती है कि जिन शर्तों से यह सिर के सामान्य रूपों की गणना करती है वे लैम्ब्डा कैलकुलस परिभाषा#मुक्त और बाध्य चर हैं।<ref name="Curien">{{cite book | first1 = Pierre-Louis  
यहां दी गई वक्र मशीन की प्रस्तुति लैम्ब्डा शब्दों के नोटेशन पर आधारित है जो डी ब्रूजन सूचकांकों का उपयोग करती है और मानती है कि जिन शर्तों से यह सिर के सामान्य रूपों की गणना करती है वे लैम्ब्डा गणना परिभाषा#मुक्त और बाध्य चर हैं।<ref name="Curien">{{cite book | first1 = Pierre-Louis  
| last1 = Curien
| last1 = Curien
| title = Categorical Combinators, Sequential Algorithms and Functional
| title = Categorical Combinators, Sequential Algorithms and Functional
| publisher = Birkhaüser
| publisher = Birkhaüser
| year = 1993
| year = 1993
| edition =  2nd}}</ref> यह वर्तमान स्थिति को तब तक संशोधित करता है जब तक कि वह ऐसा नहीं कर सकता, जिस स्थिति में इसे एक सामान्य सामान्य रूप प्राप्त होता है। यह शीर्ष सामान्य रूप गणना के परिणाम को दर्शाता है या त्रुटि उत्पन्न करता है, जिसका अर्थ है कि जिस शब्द से इसकी शुरुआत हुई है वह सही नहीं है। हालाँकि, यह संक्रमणों के एक अनंत अनुक्रम में प्रवेश कर सकता है, जिसका अर्थ है कि यह जिस शब्द को कम करने का प्रयास करता है उसका कोई सामान्य रूप नहीं है और यह एक गैर-समाप्ति गणना से मेल खाता है।
| edition =  2nd}}</ref> यह वर्तमान स्थिति को तब तक संशोधित करता है जब तक कि वह ऐसा नहीं कर सकता, जिस स्थिति में इसे एक सामान्य रूप प्राप्त होता है। यह शीर्ष सामान्य रूप गणना के परिणाम को दर्शाता है या त्रुटि उत्पन्न करता है, जिसका अर्थ है कि जिस शब्द से इसकी प्रारंभिक हुई है वह सही नहीं है। हालाँकि, यह संक्रमणों के एक अनंत अनुक्रम में प्रवेश कर सकता है, जिसका अर्थ है कि यह जिस शब्द को कम करने का प्रयास करता है उसका कोई सामान्य रूप नहीं है और यह एक गैर-समाप्ति गणना से मेल खाता है।


यह साबित हो चुका है कि क्रिवाइन मशीन लैम्ब्डा-कैलकुलस में नेम हेड नॉर्मल फॉर्म रिडक्शन द्वारा कॉल को सही ढंग से लागू करती है। इसके अलावा, क्रिवाइन मशीन नियतात्मक संकलन है, क्योंकि स्थिति का प्रत्येक पैटर्न अधिकतम एक मशीन संक्रमण से मेल खाता है।
यह सिद्ध हो चुका है कि वक्र मशीन लैम्ब्डा-गणना में नेम सिर सामान्य रूप रिडक्शन द्वारा कॉल को सही ढंग से लागू करती है। इसके अतिरिक्त, वक्र मशीन नियतात्मक संकलन है, क्योंकि स्थिति का प्रत्येक नमूना अधिकतम एक मशीन संक्रमण से मेल खाता है।


=== स्थिति ===
=== स्थिति ===
स्थिति के तीन घटक हैं<ref name="Curien" />:# अवधी,
स्थिति के तीन घटक हैं<ref name="Curien" />:# अवध
:# ढेर,
:# ढेर,
:# पर्यावरण।
:# पर्यावरण।


यह शब्द डी ब्रुइज़न सूचकांकों वाला एक λ-शब्द है। स्टैक और पर्यावरण एक ही पुनरावर्ती डेटा संरचना से संबंधित हैं। अधिक सटीक रूप से, पर्यावरण और स्टैक ''<term, environment>'' जोड़ियों की सूचियाँ हैं, जिन्हें ''क्लोज़र'' कहा जाता है। निम्नलिखित में, किसी तत्व ''ए'' की सूची ℓ (स्टैक या पर्यावरण) के प्रमुख के रूप में प्रविष्टि ''ए:ℓ'' लिखी जाती है, जबकि खाली सूची □ लिखी जाती है। स्टैक वह स्थान है जहां मशीन क्लोजर को संग्रहीत करती है जिसका मूल्यांकन किया जाना चाहिए, जबकि पर्यावरण मूल्यांकन के दौरान एक निश्चित समय पर सूचकांक और क्लोजर के बीच संबंध है। पर्यावरण का पहला तत्व इंडेक्स ''0'' से जुड़ा क्लोजर है, दूसरा तत्व इंडेक्स ''1'' आदि से जुड़े क्लोजर से मेल खाता है। यदि मशीन को किसी इंडेक्स का मूल्यांकन करना है, तो वह वहां जोड़ी लाती है। ''<अवधि, पर्यावरण>'' वह समापन जो मूल्यांकन किए जाने वाले शब्द को उत्पन्न करता है और वह वातावरण जिसमें इस शब्द का मूल्यांकन किया जाना चाहिए।{{efn|Using the concept of closure, one may replace the triple ''<term,stack, environment>'', which defines the state, by a couple ''<closure,stack>'', but this change is cosmetic.}} यह सहज स्पष्टीकरण मशीन के संचालन नियमों को समझने की अनुमति देता है। यदि कोई पद के लिए t, स्टैक के लिए p लिखता है,{{efn|p is for ''pile'', the French word for stack, which we do not want to mix up with ''s'', for state.}} और पर्यावरण के लिए ई, इन तीन संस्थाओं से जुड़े स्थितिों को टी, पी, ई लिखा जाएगा। नियम बताते हैं कि कैसे मशीन स्थितिों के बीच पैटर्न की पहचान करने के बाद एक स्थिति को दूसरे स्थिति में बदल देती है।
यह शब्द डी ब्रुइज़न सूचकांकों वाला एक λ-शब्द है। स्टैक और पर्यावरण एक ही पुनरावर्ती डेटा संरचना से संबंधित हैं। अधिक सटीक रूप से, पर्यावरण और स्टैक ''<term, environment>'' जोड़ियों की सूचियाँ हैं, जिन्हें ''क्लोज़र'' कहा जाता है। निम्नलिखित में, किसी तत्व ''ए'' की सूची ℓ (स्टैक या पर्यावरण) के प्रमुख के रूप में प्रविष्टि ''ए:ℓ'' लिखी जाती है, जबकि खाली सूची □ लिखी जाती है। स्टैक वह स्थान है जहां मशीन क्लोजर को संग्रहीत करती है जिसका मूल्यांकन किया जाना चाहिए, जबकि पर्यावरण मूल्यांकन के दौरान एक निश्चित समय पर सूचकांक और क्लोजर के बीच संबंध है। पर्यावरण का पहला तत्व इंडेक्स ''0'' से जुड़ा क्लोजर है, दूसरा तत्व इंडेक्स ''1'' आदि से जुड़े क्लोजर से मेल खाता है। यदि मशीन को किसी इंडेक्स का मूल्यांकन करना है, तो वह वहां जोड़ी लाती है। ''<अवधि, पर्यावरण>'' वह समापन जो मूल्यांकन किए जाने वाले शब्द को उत्पन्न करता है और वह वातावरण जिसमें इस शब्द का मूल्यांकन किया जाना चाहिए।{{efn|Using the concept of closure, one may replace the triple ''<term,stack, environment>'', which defines the state, by a couple ''<closure,stack>'', but this change is cosmetic.}} यह सहज स्पष्टीकरण मशीन के संचालन नियमों को समझने की अनुमति देता है। यदि कोई पद के लिए t, स्टैक के लिए p लिखता है,{{efn|p is for ''pile'', the French word for stack, which we do not want to mix up with ''s'', for state.}} और पर्यावरण के लिए ई, इन तीन संस्थाओं से जुड़े स्थितिों को टी, पी, ई लिखा जाएगा। नियम बताते हैं कि कैसे मशीन स्थितिों के बीच नमूना की पहचान करने के बाद एक स्थिति को दूसरे स्थिति में बदल देती है।


प्रारंभिक अवस्था का लक्ष्य किसी पद t का मूल्यांकन करना है, यह अवस्था t,□,□ है, जिसमें पद t है और स्टैक और वातावरण खाली हैं। अंतिम स्थिति (त्रुटि के अभाव में) λ t, □, e के रूप में होती है, दूसरे शब्दों में, परिणामी शब्द अपने पर्यावरण और एक खाली स्टैक के साथ एक अमूर्त है।
प्रारंभिक अवस्था का लक्ष्य किसी पद t का मूल्यांकन करना है, यह अवस्था t,□,□ है, जिसमें पद t है और स्टैक और वातावरण खाली हैं। अंतिम स्थिति (त्रुटि के अभाव में) λ t, □, e के रूप में होती है, दूसरे शब्दों में, परिणामी शब्द अपने पर्यावरण और एक खाली स्टैक के साथ एक अमूर्त है।


=== परिवर्तन ===
=== परिवर्तन ===
क्रिविन मशीन<ref name="Curien" />इसमें चार ट्रांज़िशन हैं: ''ऐप'', ''एब्स'', ''ज़ीरो'', ''सक्स''।
क्रिविन मशीन<ref name="Curien" />इसमें चार संक्रमण हैं: ''ऐप'', ''एब्स'', ''शून्य'', ''सक्स''।
{| class="wikitable center" style = "width:50%"
{| class="wikitable center" style = "width:50%"
|+ Transitions of the Krivine machine
|+ क्रिवाइन मशीन का परिवर्तन
|-
|-
! scope=col | Name
! scope=col | Name
Line 95: Line 94:
n, p, e
n, p, e
|}
|}
ट्रांज़िशन ''ऐप'' किसी एप्लिकेशन के पैरामीटर को हटा देता है और इसे आगे के मूल्यांकन के लिए स्टैक पर रख देता है। परिवर्तन ''एबीएस'' शब्द के λ को हटा देता है और स्टैक के शीर्ष से क्लोजर को पॉप अप करता है और इसे पर्यावरण के शीर्ष पर रख देता है। यह समापन नए परिवेश में डी ब्रुइज़न सूचकांक ''0'' से मेल खाता है। संक्रमण ''शून्य'' पर्यावरण का पहला समापन लेता है। इस समापन की अवधि वर्तमान अवधि बन जाती है और इस समापन का वातावरण वर्तमान परिवेश बन जाता है। संक्रमण ''सक्स'' पर्यावरण सूची के पहले समापन को हटा देता है और सूचकांक के मूल्य को कम कर देता है।
संक्रमण ''ऐप'' किसी आवेदन के पैरामीटर को हटा देता है और इसे आगे के मूल्यांकन के लिए स्टैक पर रख देता है। परिवर्तन ''एबीएस'' शब्द के λ को हटा देता है और स्टैक के शीर्ष से क्लोजर को पॉप अप करता है और इसे पर्यावरण के शीर्ष पर रख देता है। यह समापन नए परिवेश में डी ब्रुइज़न सूचकांक ''0'' से मेल खाता है। संक्रमण ''शून्य'' पर्यावरण का पहला समापन लेता है। इस समापन की अवधि वर्तमान अवधि बन जाती है और इस समापन का वातावरण वर्तमान परिवेश बन जाता है। संक्रमण ''सक्स'' पर्यावरण सूची के पहले समापन को हटा देता है और सूचकांक के मूल्य को कम कर देता है।


=== दो उदाहरण ===
=== दो उदाहरण ===
Line 101: Line 100:


{|class="wikitable center" style= "width:30%"
{|class="wikitable center" style= "width:30%"
|+ Evaluation of the  term ''(λ 0 0) (λ 0)''
|+ पद का मूल्यांकन ''(λ 0 0) (λ 0)''
|-
|-
|
|
Line 133: Line 132:


{|class="wikitable center" style="width:35%"
{|class="wikitable center" style="width:35%"
|+ Evaluation of ((λ 0) (λ 0)) (λ 0)
|+ ((λ 0) (λ 0)) (λ 0) का मूल्यांकन
|-
|-
| ((''λ'' 0) (''λ'' 0)) (''λ'' 0), □, □
| ((''λ'' 0) (''λ'' 0)) (''λ'' 0), □, □
Line 153: Line 152:


== अंतर-व्युत्पत्तियाँ ==
== अंतर-व्युत्पत्तियाँ ==
क्रिवाइन मशीन, CEK मशीन की तरह, न केवल कार्यात्मक रूप से [[मेटा-सर्कुलर मूल्यांकनकर्ता]] के अनुरूप है,
वक्र मशीन, CEK मशीन की तरह, न केवल कार्यात्मक रूप से [[मेटा-सर्कुलर मूल्यांकनकर्ता]] के अनुरूप है,
<ref name="schmidt 80">
<ref name="schmidt 80">
{{cite conference
{{cite conference
Line 201: Line 200:
|doi=10.7146/brics.v10i13.21783}}
|doi=10.7146/brics.v10i13.21783}}
</ref>
</ref>
यह वाक्यविन्यास की दृष्टि से भी मेल खाता है <math>\lambda\widehat{\rho}</math> कैलकुलस - पियरे-लुई क्यूरियन का एक संस्करण <math>\lambda\widehat{\rho}</math> [[स्पष्ट प्रतिस्थापन]] की गणना जो कमी के तहत बंद होती है - एक सामान्य-क्रम कटौती रणनीति के साथ।
यह वाक्यविन्यास की दृष्टि से भी मेल खाता है <math>\lambda\widehat{\rho}</math> गणना - पियरे-लुई क्यूरियन का एक संस्करण <math>\lambda\widehat{\rho}</math> [[स्पष्ट प्रतिस्थापन]] की गणना जो कमी के तहत बंद होती है - एक सामान्य-क्रम कटौती रणनीति के साथ।
<ref name="curien 91">
 
यदि <math>\lambda\widehat{\rho}</math> गणना में सामान्यीकृत सम्मलित है <math>\beta</math> कमी (यानी, नेस्टेड <math>\beta</math> रेडेक्स <math>(\lambda x_1.\lambda x_2.e_0)\;e_1\;e_2</math> दो के अतिरिक्त एक चरण में अनुबंधित किया जाता है), तो वाक्यात्मक रूप से संबंधित मशीन जीन-लुई क्रिविन की मूल मशीन के साथ मेल खाती है।<ref name="Krivine 07">
{{cite journal
{{cite journal
|last1=Curien
|last1=Krivine
|first1=Pierre-Louis
|first1=Jean-Louis
|date=1991
|date=2007
|title=An Abstract Framework for Environment Machines
|title=A call-by-name lambda-calculus machine
|journal=Theoretical Computer Science
|journal=Higher-Order and Symbolic Computation
|volume=82
|volume=20
|issue=2
|issue=3
|pages=389–402
|pages=199–207
|doi=10.1016/0304-3975(91)90230-Y}}
|doi=10.1007/s10990-007-9018-9|s2cid=18158499
}}
</ref>
</ref>
<ref name="1biernacka danvy brics-07">
<ref name="1biernacka danvy brics-07">
Line 229: Line 230:
|pages=1–30
|pages=1–30
|doi=10.7146/brics.v13i3.21909}}
|doi=10.7146/brics.v13i3.21909}}
</ref>
</ref>(इसके अतिरिक्त, यदि कटौती की रणनीति मूल्य के आधार पर दाएं से बाएं कॉल है और इसमें सामान्यीकृत सम्मलित है <math>\beta</math> कमी, तो वाक्यात्मक रूप से संगत मशीन [[जेवियर लेरॉय]] की ZINC अमूर्त मशीन है, जो [[OCaml]] का आधार है।)<ref name="Leroy 90">
<ref name="swierstra msfp-12">
{{cite journal
|last1=Swierstra
|first1=Wouter
|date=2012
|title=From mathematics to abstract machine: A formal derivation of an executable Krivine machine
|journal=Electronic Proceedings in Theoretical Computer Science
|volume=76
|institution=Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012)
|pages=163–177
|doi=10.4204/EPTCS.76.10
|url=https://doi.org/10.4204/EPTCS.76.10}}
</ref>
यदि <math>\lambda\widehat{\rho}</math> कैलकुलस में सामान्यीकृत शामिल है <math>\beta</math> कमी (यानी, नेस्टेड <math>\beta</math> redex <math>(\lambda x_1.\lambda x_2.e_0)\;e_1\;e_2</math> दो के बजाय एक चरण में अनुबंधित किया जाता है), तो वाक्यात्मक रूप से संबंधित मशीन जीन-लुई क्रिविन की मूल मशीन के साथ मेल खाती है।<ref name="Krivine 07">
{{cite journal
|last1=Krivine
|first1=Jean-Louis
|date=2007
|title=A call-by-name lambda-calculus machine
|journal=Higher-Order and Symbolic Computation
|volume=20
|issue=3
|pages=199–207
|doi=10.1007/s10990-007-9018-9|s2cid=18158499
}}
</ref>
<ref name="1biernacka danvy brics-07"/>(इसके अलावा, यदि कटौती की रणनीति मूल्य के आधार पर दाएं से बाएं कॉल है और इसमें सामान्यीकृत शामिल है <math>\beta</math> कमी, तो वाक्यात्मक रूप से संगत मशीन [[जेवियर लेरॉय]] की ZINC अमूर्त मशीन है, जो [[OCaml]] का आधार है।)<ref name="Leroy 90">
{{cite techreport
{{cite techreport
|last1=[[Xavier Leroy|Leroy]]
|last1=[[Xavier Leroy|Leroy]]
Line 266: Line 240:
|url=https://hal.inria.fr/inria-00070049/document}}
|url=https://hal.inria.fr/inria-00070049/document}}
</ref>
</ref>
<ref name="1biernacka danvy brics-07"/>
<ref name="1biernacka danvy brics-07" />
 





Revision as of 23:55, 14 July 2023

सैद्धांतिक कंप्यूटर विज्ञान में, मशीन वक्र एक अमूर्त मशीन है (कभी-कभी इसे आभासी मशीन भी कहा जाता है)। एक अमूर्त मशीन के रूप में, यह ट्यूरिंग मशीन और एसईसीडी मशीन के साथ सुविधाएँ साझा करती है। वक्र मशीन बताती है कि पुनरावर्ती समारोह की गणना कैसे करें। अधिक विशेष रूप से इसका उद्देश्य नाम से बुलाओ कमी का उपयोग करके लैम्ब्डा गणना के सामान्य रूप में कमी को सख्ती से परिभाषित करना है। इसकी औपचारिकता के लिए धन्यवाद, यह विवरण में बताता है कि एक प्रकार की कमी कैसे काम करती है और [कार्यात्मक प्रोग्रामिंग] भाषाओं के परिचालन शब्दार्थ की सैद्धांतिक नींव निर्धारित करती है। दूसरी ओर, वक्र मशीन कॉल-बाय-नाम लागू करती है क्योंकि यह समारोह शरीर को उसके पैरामीटर पर लागू करने से पहले β-कम करने योग्य अभिव्यक्ति के शरीर का मूल्यांकन करती है। दूसरे शब्दों में, एक अभिव्यक्ति (λ x. t) u में यह पहले λ x का मूल्यांकन करता है। इसे यू पर लागू करने से पहले टी कार्यात्मक प्रोग्रामिंग में, इसका मतलब यह होगा कि किसी पैरामीटर पर लागू समारोह का मूल्यांकन करने के लिए, यह पैरामीटर पर लागू करने से पहले समारोह का मूल्यांकन करता है।

वक्र मशीन को 1980 के दशक की प्रारंभिक में फ्रांसीसी तर्कशास्त्री :fr:जीन-लुई वक्र जीन-लुई वक्र द्वारा डिजाइन किया गया था।

नाम और सिर से बुलाएं सामान्य रूप में कमी

वक्र मशीन लैम्ब्डा गणना से संबंधित दो अवधारणाओं पर आधारित है, अर्थात् सिर में कमी और नाम से कॉल पर आधारित है|

सिर सामान्य रूप में कमी

एक लैम्ब्डा गणना कमी[1] (एक यह भी कहता है कि β-रीडेक्स) फॉर्म (λ x. t) u के लैम्ब्डा गणना का एक शब्द है। यदि किसी पद का आकार (λ x. t) u है1 ... मेंn इसे हेड रिडेक्स कहा जाता है। बीटा सामान्य रूप लैम्ब्डा गणना का एक शब्द है जो हेड रिडेक्स नहीं है।[lower-alpha 1] सिर में कमी एक शब्द के संकुचन का एक (गैर-खाली) अनुक्रम है जो हेड रिडेक्स को अनुबंधित करता है। किसी अवधि टी का सिर में कमी (जिसे सिर सामान्य रूप में नहीं माना जाता है) एक सिर में कमी है जो अवधि टी से शुरू होता है और सिर सामान्य रूप पर खत्म होता है। एक अमूर्त दृष्टिकोण से, सिर में कमी वह विधि है जिससे एक प्रोग्राम गणना करता है जब वह एक पुनरावर्ती उप-प्रोग्राम का मूल्यांकन करता है। यह समझना महत्वपूर्ण है कि ऐसी कटौती कैसे लागू की जा सकती है। वक्र मशीन का एक उद्देश्य किसी शब्द को सामान्य रूप में कम करने और इस प्रक्रिया का औपचारिक रूप से वर्णन करने के लिए एक प्रक्रिया का प्रस्ताव करना है। जैसे एलन ट्यूरिंग ने कलन विधि की धारणा का औपचारिक रूप से वर्णन करने के लिए एक अमूर्त मशीन का उपयोग किया, :fr: जीन-लुई क्रिविन ने सिर के सामान्य रूप में कमी की धारणा का औपचारिक रूप से वर्णन करने के लिए एक अमूर्त मशीन का उपयोग किया जाता है।

उदाहरण

शब्द ((λ 0) (λ 0)) (λ 0) (जो अस्पष्ट चरों का उपयोग करता है, उसे अवधि (λx.x) (λy.y) (λz.z) के लिए कहा जाता है) सिर सामान्य रूप में नहीं है क्योंकि (λ 0) (λ 0) को (λ 0) में संक्षेपित करता है, जिससे हेड रेडेक्स (λ 0) (λ 0) उत्पन्न होता है, जो (λ 0) में संक्षेपित होता है और जो कि इसलिए ((λ 0) (λ 0)) (λ 0) का सिर सामान्य रूप है। दूसरे शब्दों में कहा जाए, सिर सामान्य रूप संक्षेपण है:

((λ 0) (λ 0)) (λ 0) ➝ (λ 0) (λ 0) ➝ λ 0,

जो इसके लिए है:

(λx.x) (λy.y) (λz.z) ➝ (λy.y) (λz.z) ➝ λz.z.

आगे चलकर हम देखेंगे कि वक्र मशीन कैसे अवधि ((λ 0) (λ 0)) (λ 0) को संक्षेपित करती है।

नाम से पुकारें

अवधि u v की हेड रेडक्शन को कार्यान्वित करने के लिए, जो एक आवेदन है, लेकिन जो रेडेक्स नहीं है, हमें पहले अवधि u को संक्षेपित करके एक अव्यवहार्यता दिखाने के लिए u को संक्षेपित करना होगा, और इस तरह v के साथ एक रेडेक्स बनाना होगा। जब एक रेडेक्स प्रकट होता है, तो हम उसे संक्षेपित करते हैं। एक आवेदन के शरीर को सदैव पहले संक्षेपित करना, कॉल बाय नाम कहलाता है। वक्र मशीन कॉल बाय नाम को कार्यान्वित करती है।

विवरण

यहां दी गई वक्र मशीन की प्रस्तुति लैम्ब्डा शब्दों के नोटेशन पर आधारित है जो डी ब्रूजन सूचकांकों का उपयोग करती है और मानती है कि जिन शर्तों से यह सिर के सामान्य रूपों की गणना करती है वे लैम्ब्डा गणना परिभाषा#मुक्त और बाध्य चर हैं।[2] यह वर्तमान स्थिति को तब तक संशोधित करता है जब तक कि वह ऐसा नहीं कर सकता, जिस स्थिति में इसे एक सामान्य रूप प्राप्त होता है। यह शीर्ष सामान्य रूप गणना के परिणाम को दर्शाता है या त्रुटि उत्पन्न करता है, जिसका अर्थ है कि जिस शब्द से इसकी प्रारंभिक हुई है वह सही नहीं है। हालाँकि, यह संक्रमणों के एक अनंत अनुक्रम में प्रवेश कर सकता है, जिसका अर्थ है कि यह जिस शब्द को कम करने का प्रयास करता है उसका कोई सामान्य रूप नहीं है और यह एक गैर-समाप्ति गणना से मेल खाता है।

यह सिद्ध हो चुका है कि वक्र मशीन लैम्ब्डा-गणना में नेम सिर सामान्य रूप रिडक्शन द्वारा कॉल को सही ढंग से लागू करती है। इसके अतिरिक्त, वक्र मशीन नियतात्मक संकलन है, क्योंकि स्थिति का प्रत्येक नमूना अधिकतम एक मशीन संक्रमण से मेल खाता है।

स्थिति

स्थिति के तीन घटक हैं[2]:# अवध

  1. ढेर,
  2. पर्यावरण।

यह शब्द डी ब्रुइज़न सूचकांकों वाला एक λ-शब्द है। स्टैक और पर्यावरण एक ही पुनरावर्ती डेटा संरचना से संबंधित हैं। अधिक सटीक रूप से, पर्यावरण और स्टैक <term, environment> जोड़ियों की सूचियाँ हैं, जिन्हें क्लोज़र कहा जाता है। निम्नलिखित में, किसी तत्व की सूची ℓ (स्टैक या पर्यावरण) के प्रमुख के रूप में प्रविष्टि ए:ℓ लिखी जाती है, जबकि खाली सूची □ लिखी जाती है। स्टैक वह स्थान है जहां मशीन क्लोजर को संग्रहीत करती है जिसका मूल्यांकन किया जाना चाहिए, जबकि पर्यावरण मूल्यांकन के दौरान एक निश्चित समय पर सूचकांक और क्लोजर के बीच संबंध है। पर्यावरण का पहला तत्व इंडेक्स 0 से जुड़ा क्लोजर है, दूसरा तत्व इंडेक्स 1 आदि से जुड़े क्लोजर से मेल खाता है। यदि मशीन को किसी इंडेक्स का मूल्यांकन करना है, तो वह वहां जोड़ी लाती है। <अवधि, पर्यावरण> वह समापन जो मूल्यांकन किए जाने वाले शब्द को उत्पन्न करता है और वह वातावरण जिसमें इस शब्द का मूल्यांकन किया जाना चाहिए।[lower-alpha 2] यह सहज स्पष्टीकरण मशीन के संचालन नियमों को समझने की अनुमति देता है। यदि कोई पद के लिए t, स्टैक के लिए p लिखता है,[lower-alpha 3] और पर्यावरण के लिए ई, इन तीन संस्थाओं से जुड़े स्थितिों को टी, पी, ई लिखा जाएगा। नियम बताते हैं कि कैसे मशीन स्थितिों के बीच नमूना की पहचान करने के बाद एक स्थिति को दूसरे स्थिति में बदल देती है।

प्रारंभिक अवस्था का लक्ष्य किसी पद t का मूल्यांकन करना है, यह अवस्था t,□,□ है, जिसमें पद t है और स्टैक और वातावरण खाली हैं। अंतिम स्थिति (त्रुटि के अभाव में) λ t, □, e के रूप में होती है, दूसरे शब्दों में, परिणामी शब्द अपने पर्यावरण और एक खाली स्टैक के साथ एक अमूर्त है।

परिवर्तन

क्रिविन मशीन[2]इसमें चार संक्रमण हैं: ऐप, एब्स, शून्य, सक्स

क्रिवाइन मशीन का परिवर्तन
Name Before After

App

t u, p, e

t, <u,e>:p, e

Abs

λ t, <u,e'>:p, e

t, p, <u,e'>:e

Zero

0, p, <t, e'>:e

t, p, e'

Succ

n+1, p, <t,e'>:e

n, p, e

संक्रमण ऐप किसी आवेदन के पैरामीटर को हटा देता है और इसे आगे के मूल्यांकन के लिए स्टैक पर रख देता है। परिवर्तन एबीएस शब्द के λ को हटा देता है और स्टैक के शीर्ष से क्लोजर को पॉप अप करता है और इसे पर्यावरण के शीर्ष पर रख देता है। यह समापन नए परिवेश में डी ब्रुइज़न सूचकांक 0 से मेल खाता है। संक्रमण शून्य पर्यावरण का पहला समापन लेता है। इस समापन की अवधि वर्तमान अवधि बन जाती है और इस समापन का वातावरण वर्तमान परिवेश बन जाता है। संक्रमण सक्स पर्यावरण सूची के पहले समापन को हटा देता है और सूचकांक के मूल्य को कम कर देता है।

दो उदाहरण

आइए हम पद (λ 0 0) (λ 0) का मूल्यांकन करें जो पद (λ x. x x) (λ x. x) से संगत है। आइए स्थिति (λ 0 0) (λ 0), □, □ से शुरू करें।

पद का मूल्यांकन (λ 0 0) (λ 0)

(λ 0 0) (λ 0), □, □

λ 0 0, [<λ 0, □>], □

0 0, □, [<λ 0, □>]

0, [<0, <λ 0, □>>], [<λ 0, □>]

λ 0, [<0, <λ 0, □>>], □

0, □, [<0, <λ 0, □>>]

0, □, [<λ 0, □>]

λ 0, □, □

निष्कर्ष यह है कि पद (λ 0 0) (λ 0) का शीर्ष सामान्य रूप λ 0 है। यह चर के साथ अनुवाद करता है: पद का शीर्ष सामान्य रूप (λ x. x x) (λ x. x) है λ एक्स. एक्स।

आइए हम पद ((λ 0) (λ 0)) (λ 0) का मूल्यांकन करें जैसा कि नीचे दिखाया गया है:

((λ 0) (λ 0)) (λ 0) का मूल्यांकन
((λ 0) (λ 0)) (λ 0), □, □
(λ 0) (λ 0), [<(λ 0), □>], □
(λ 0), [<(λ 0), □>,<(λ 0), □>], □
0, [<(λ 0), □>], [<(λ 0), □>]
λ 0, [<(λ 0), □>], □
0, □, [<(λ 0), □>]
(λ 0), □, □

यह उपरोक्त तथ्य की पुष्टि करता है कि पद ((λ 0) (λ 0)) (λ 0) का सामान्य रूप (λ 0) है।

अंतर-व्युत्पत्तियाँ

वक्र मशीन, CEK मशीन की तरह, न केवल कार्यात्मक रूप से मेटा-सर्कुलर मूल्यांकनकर्ता के अनुरूप है, [3] [4] [5] यह वाक्यविन्यास की दृष्टि से भी मेल खाता है गणना - पियरे-लुई क्यूरियन का एक संस्करण स्पष्ट प्रतिस्थापन की गणना जो कमी के तहत बंद होती है - एक सामान्य-क्रम कटौती रणनीति के साथ।

यदि गणना में सामान्यीकृत सम्मलित है कमी (यानी, नेस्टेड रेडेक्स दो के अतिरिक्त एक चरण में अनुबंधित किया जाता है), तो वाक्यात्मक रूप से संबंधित मशीन जीन-लुई क्रिविन की मूल मशीन के साथ मेल खाती है।[6] [7](इसके अतिरिक्त, यदि कटौती की रणनीति मूल्य के आधार पर दाएं से बाएं कॉल है और इसमें सामान्यीकृत सम्मलित है कमी, तो वाक्यात्मक रूप से संगत मशीन जेवियर लेरॉय की ZINC अमूर्त मशीन है, जो OCaml का आधार है।)[8] [7]


यह भी देखें

टिप्पणियाँ

  1. If one only deals with closed terms, these terms take the form λ x. t.
  2. Using the concept of closure, one may replace the triple <term,stack, environment>, which defines the state, by a couple <closure,stack>, but this change is cosmetic.
  3. p is for pile, the French word for stack, which we do not want to mix up with s, for state.

संदर्भ

  1. Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103 (Revised ed.), North Holland, Amsterdam, ISBN 0-444-87508-5, archived from the original on 2004-08-23 Corrections.
  2. 2.0 2.1 2.2 Curien, Pierre-Louis (1993). Categorical Combinators, Sequential Algorithms and Functional (2nd ed.). Birkhaüser.
  3. Schmidt, David A. (1980). "State transition machines for lambda-calculus expressions". State transition machines for lambda calculus expressions. Lecture Notes in Computer Science. Vol. 94. Semantics-Directed Compiler Generation, LNCS 94. pp. 415–440. doi:10.1007/3-540-10250-7_32. ISBN 978-3-540-10250-2.
  4. Schmidt, David A. (2007). "State-transition machines, revisited". Higher-Order and Symbolic Computation. 20 (3): 333–335. doi:10.1007/s10990-007-9017-x. S2CID 3012667.
  5. Ager, Mads Sig; Biernacki, Dariusz; Danvy, Olivier; Midtgaard, Jan (2003). "A Functional Correspondence between Evaluators and Abstract Machines". Brics Report Series. 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'03). 10 (13): 8–19. doi:10.7146/brics.v10i13.21783.
  6. Krivine, Jean-Louis (2007). "A call-by-name lambda-calculus machine". Higher-Order and Symbolic Computation. 20 (3): 199–207. doi:10.1007/s10990-007-9018-9. S2CID 18158499.
  7. 7.0 7.1 Biernacka, Małgorzata; Danvy, Olivier (2007). Article #6. "A Concrete Framework for Environment Machines". ACM Transactions on Computational Logic. 9 (1): 1–30. doi:10.7146/brics.v13i3.21909.
  8. Leroy, Xavier (1990). The ZINC experiment: an economical implementation of the ML language (Technical report). Inria. 117.

Content in this edit is translated from the existing French Wikipedia article at fr:Machine de Krivine; see its history for attribution.


ग्रन्थसूची

  • Jean-Louis Krivine: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3): 199-207 (2007) archive.
  • Curien, Pierre-Louis (1993). Categorical Combinators, Sequential Algorithms and Functional (2nd ed.). Birkhaüser.
  • Frédéric Lang: Explaining the lazy Krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation 20(3): 257-270 (2007) archive.
  • Olivier Danvy (Ed.): Editorial of special issue of Higher-Order and Symbolic Computation on the Krivine machine, vol. 20(3) (2007)


बाहरी संबंध