क्रिवाइन मशीन

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

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

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

Further information: लैम्ब्डा कैलकुलस

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

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

रेडेक्स (बीटा-रेडेक्स भी कहा जाता है) लैम्बडा गणना का पद होता है जिसकी रूप में (λ x. t) u होता है। यदि पद की आकृति (λ x. t) u₁ ... u_n होती है, तो उसे हेड रेडेक्स कहा जाता है। बीटा सामान्य रूप लैम्ब्डा गणना का पद है जो हेड रिडेक्स नहीं है। हेड रीडक्शन पद के (गैर खाली) क्रमबद्ध श्रिंखला होती है जो पद के हेड रेडेक्स को श्रिंकलेट करती है। पद t की हेड रीडक्शन (जिसे हेड साधारण फ़ॉर्म में नहीं होने का समझा जाता है) हेड रीडक्शन है जो पद t से प्रारंभ होती है और हेड साधारण फ़ॉर्म पर समाप्त होती है। अभिकल्पिक दृष्टिकोण से, हेड रीडक्शन प्रोग्राम की प्रक्रिया है जब वह पुनरावृत्तिशील उप-प्रोग्राम का मूल्यांकन करता है। इस प्रकार की श्रिंकलन को कैसे कार्यान्वित किया जा सकता है, इसे समझना महत्वपूर्ण है। क्रिवाइन मशीन का उद्देश्य हेड साधारण फ़ॉर्म में पद को श्रिंकलने की प्रक्रिया प्रस्तावित करना है और इस प्रक्रिया को समय-समय पर वर्णित करना है। जैसे एलन ट्यूरिंग ने अवकाशी मशीन का उपयोग करके सामान्यता की नीति को समय-समय पर वर्णित किया, क्रिवाइन ने अवकाशी मशीन का उपयोग करके हेड साधारण फ़ॉर्म श्रिंकलन की नीति को समय-समय पर वर्णित किया जाता है।

उदाहरण

पद ((λ 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 के साथ रेडेक्स बनाना होगा। जब रेडेक्स प्रकट होता है, तो हम उसे संक्षेपित करते हैं। आवेदन के शरीर को सदैव पहले संक्षेपित करना, नाम से कॉल लागू करती है। क्रिवाइन मशीन नाम से कॉल लागू को कार्यान्वित करती है।

विवरण

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

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

स्थिति

स्थिति के तीन होते हैं:

1. शब्द,
2. स्टैक
3. वातावरण

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

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

परिवर्तन

क्रिवाइन मशीन में चार स्थानांतरण होते हैं: ऐप, एब्स, शून्य, सुक्क ।

क्रिवाइन मशीन के स्थानांतरण

नाम	पहले	बाद में
ऐप	t u, p, e	t, <u,e>:p, e
एब्स	λ t, <u,e'>:p, e	t, p, <u,e'>:e
शून्य	0, p, <t, e'>:e	t, p, e'
सक्स	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) का शीर्ष सामान्य रूप λ 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 मशीन की प्रकार, न केवल कार्यात्मक रूप से मेटा-सर्कुलर मूल्यांकनकर्ता के अनुरूप है,यह वाक्य विन्यास की दृष्टि से भी मेल खाता है $\lambda {\widehat {\rho }}$ गणना - पियरे-लुई क्यूरियन का संस्करण $\lambda {\widehat {\rho }}$ स्पष्ट प्रतिस्थापन की गणना जो कमी के अनुसार बंद होती है - सामान्य-क्रम कटौती रणनीति के साथ होता है।

यदि $\lambda {\widehat {\rho }}$ गणना में सामान्यीकृत सम्मलित है $\beta$ कमी ( बरकरार, नेस्टेड $\beta$ रेडेक्स $(\lambda x_{1}.\lambda x_{2}.e_{0})\;e_{1}\;e_{2}$ दो के अतिरिक्त चरण में अनुबंधित किया जाता है), तो वाक्यात्मक रूप से संबंधित मशीन जीन-लुई क्रिविन की मूल मशीन के साथ मेल खाती है।(इसके अतिरिक्त, यदि कटौती की रणनीति मूल्य के आधार पर दाएं से बाएं कॉल है और इसमें सामान्यीकृत सम्मलित है $\beta$ कमी, तो वाक्यात्मक रूप से संगत मशीन जेवियर लेरॉय की ज़िन्क अमूर्त मशीन है, जो ओसीमल का आधार में है।

यह भी देखें

• स्पष्ट प्रतिस्थापन
• परिचालन शब्दार्थ
• एसईसीडी मशीन
• प्रोग्रामिंग भाषाओं का शब्दार्थ

यह भी देखें

• स्पष्ट प्रतिस्थापन
• परिचालन शब्दार्थ

संदर्भ

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)

बाहरी संबंध

• Media related to क्रिवाइन मशीन at Wikimedia Commons