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

Latest revision as of 11:07, 2 August 2023

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

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

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

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

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

रेडेक्स^[1] (बीटा-रेडेक्स भी कहा जाता है) लैम्बडा गणना का पद होता है जिसकी रूप में (λ x. t) u होता है। यदि पद की आकृति (λ x. t) u₁ ... u_n होती है, तो उसे हेड रेडेक्स कहा जाता है। बीटा सामान्य रूप लैम्ब्डा गणना का पद है जो हेड रिडेक्स नहीं है।^{[lower-alpha 1]} हेड रीडक्शन पद के (गैर खाली) क्रमबद्ध श्रिंखला होती है जो पद के हेड रेडेक्स को श्रिंकलेट करती है। पद 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 के साथ रेडेक्स बनाना होगा। जब रेडेक्स प्रकट होता है, तो हम उसे संक्षेपित करते हैं। आवेदन के शरीर को सदैव पहले संक्षेपित करना, नाम से कॉल लागू करती है। क्रिवाइन मशीन नाम से कॉल लागू को कार्यान्वित करती है।

विवरण

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

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

स्थिति

स्थिति के तीन होते हैं^[2]:

शब्द,
स्टैक
वातावरण

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

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

परिवर्तन

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

क्रिवाइन मशीन के स्थानांतरण
नाम	पहले	बाद में
ऐप	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}$ दो के अतिरिक्त चरण में अनुबंधित किया जाता है), तो वाक्यात्मक रूप से संबंधित मशीन जीन-लुई क्रिविन की मूल मशीन के साथ मेल खाती है।^[3]^[4](इसके अतिरिक्त, यदि कटौती की रणनीति मूल्य के आधार पर दाएं से बाएं कॉल है और इसमें सामान्यीकृत सम्मलित है $\beta$ कमी, तो वाक्यात्मक रूप से संगत मशीन जेवियर लेरॉय की ज़िन्क अमूर्त मशीन है, जो ओसीमल का आधार में है।

यह भी देखें

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

यह भी देखें

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

↑ If one only deals with closed terms, these terms take the form λ x. t.
↑ 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.
↑ p is for pile, the French word for stack, which we do not want to mix up with s, for state.

संदर्भ

↑ 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.0 ^2.1 ^2.2 Curien, Pierre-Louis (1993). Categorical Combinators, Sequential Algorithms and Functional (2nd ed.). Birkhaüser.
↑ 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.
↑ 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.

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

[2] If one only deals with closed terms, these terms take the form λ x. t.

[4] 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.

[5] s 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.

[Curien-3] 2.0 ^2.1 ^2.2 Curien, Pierre-Louis (1993). Categorical Combinators, Sequential Algorithms and Functional (2nd ed.). Birkhaüser.

[Krivine_07-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.

[1biernacka_danvy_brics-07-7] 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.

[1]

[lower-alpha 1]

[2]

[lower-alpha 2]

[lower-alpha 3]

[3]

[4]

Anonymous

Search

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

Namespaces

More

Page actions

Latest revision as of 11:07, 2 August 2023

Contents

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

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

उदाहरण

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

विवरण

स्थिति

परिवर्तन

दो उदाहरण

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

यह भी देखें

यह भी देखें

टिप्पणियाँ

संदर्भ

ग्रन्थसूची

बाहरी संबंध

Navigation

Navigation

Wiki tools

Wiki tools

@@ Line 1: / Line 1: @@
-{{Short description|Abstract machine}}
+[[सैद्धांतिक कंप्यूटर विज्ञान]] में, '''क्रिवाइन मशीन''' ''[[अमूर्त मशीन]]'' है (कभी-कभी इसे ''[[ आभासी मशीन |आभासी मशीन]]'' भी कहा जाता है)। अमूर्त मशीन के रूप में, यह [[ट्यूरिंग मशीन]] और [[एसईसीडी मशीन]] के साथ सुविधाएँ साझा करती है। क्रिवाइन मशीन ऐसी प्रतिष्ठानिक मशीन है जो रिकर्सिव फ़ंक्शन को कैसे कंप्यूट करती है को परिभाषित करने का प्रयास करती है। अधिक विशेष रूप से इसका उद्देश्य [[नाम से बुलाओ]] कमी का उपयोग करके [[लैम्ब्डा कैलकुलस|लैम्ब्डा गणना]] के सामान्य रूप में कमी को सख्ती से परिभाषित करना है। इसकी औपचारिकता के कारण, यह विवरण में बताता है कि प्रकार की कमी कैसे काम करती है और [[कार्यात्मक प्रोग्रामिंग]]भाषाओं के [[परिचालन शब्दार्थ]] की सैद्धांतिक नींव निर्धारित करती है। दूसरी ओर, क्रिवाइन मशीन कॉल-बाय-नाम को लागू करती है इसमें β-[[ कम करने योग्य अभिव्यक्ति | कम करने योग्य अभिव्यक्ति]] को उसके पैरामीटर पर लागू करने से पहले उसे निर्धारित किया जाता है। अन्य शब्दों में, अभिव्यक्ति (''λ'' ''x''. ''t'') ''u'' में यह पहले ''λ'' ''x'' को निर्धारित किया जाता है और फिर उसे u पर लागू किया जाता है। फ़ंक्शनल प्रोग्रामिंग में, यह यह तात्पर्य होता है कि पैरामीटर पर लागू किए गए फ़ंक्शन को मूल्यांकित करने के लिए, इसे पहले फ़ंक्शन को मूल्यांकित किया जाता है।
-[[File:Machine de Krivine.jpg|thumb|क्रिवाइन मशीन का एक चित्र दृश्य]][[सैद्धांतिक कंप्यूटर विज्ञान]] में, क्रिवाइन मशीन एक ''[[अमूर्त मशीन]]'' है (कभी-कभी इसे ''[[ आभासी मशीन ]]'' भी कहा जाता है)। एक अमूर्त मशीन के रूप में, यह [[ट्यूरिंग मशीन]]ों और [[एसईसीडी मशीन]] के साथ सुविधाएँ साझा करती है। क्रिवाइन मशीन बताती है कि पुनरावर्ती फ़ंक्शन की गणना कैसे करें। अधिक विशेष रूप से इसका उद्देश्य [[नाम से बुलाओ]] रिडक्शन का उपयोग करके [[लैम्ब्डा कैलकुलस]] के सामान्य रूप में कमी को सख्ती से परिभाषित करना है। इसकी औपचारिकता के लिए धन्यवाद, यह विवरण में बताता है कि एक प्रकार की कमी कैसे काम करती है और [[[[कार्यात्मक प्रोग्रामिंग]] भाषा]]ओं के [[परिचालन शब्दार्थ]] की सैद्धांतिक नींव निर्धारित करती है। दूसरी ओर, क्रिवाइन मशीन कॉल-बाय-नाम लागू करती है क्योंकि यह फ़ंक्शन बॉडी को उसके पैरामीटर पर लागू करने से पहले β-[[ कम करने योग्य अभिव्यक्ति ]] के बॉडी का मूल्यांकन करती है। दूसरे शब्दों में, एक अभिव्यक्ति (''λ'' ''x''. ''t'') ''u'' में यह पहले ''λ'' ''x'' का मूल्यांकन करता है। इसे ''यू'' पर लागू करने से पहले ''टी''। कार्यात्मक प्रोग्रामिंग में, इसका मतलब यह होगा कि किसी पैरामीटर पर लागू फ़ंक्शन का मूल्यांकन करने के लिए, यह पैरामीटर पर लागू करने से पहले फ़ंक्शन का मूल्यांकन करता है।
-क्रिवाइन मशीन को 1980 के दशक की शुरुआत में फ्रांसीसी तर्कशास्त्री :fr:जीन-लुई क्रिवाइन|जीन-लुई क्रिवाइन द्वारा डिजाइन किया गया था।
+क्रिवाइन मशीन को फ्रांसीसी तार्किक विद्वान जीन-लुई क्रिवाइन ने 1980 के दशक की प्रारंभिक में डिज़ाइन किया था।
 == नाम और सिर से बुलाएं सामान्य रूप में कमी ==
-{{more|Lambda calculus}}
+{{more|लैम्ब्डा कैलकुलस}}
-क्रिवाइन मशीन लैम्ब्डा कैलकुलस से संबंधित दो अवधारणाओं पर आधारित है, अर्थात् हेड रिडक्शन और नाम से कॉल।
+क्रिवाइन मशीन लैम्ब्डा गणना से संबंधित दो अवधारणाओं पर आधारित है, अर्थात् हेड रिडक्शन और नाम से कॉल पर आधारित है|
 === सिर सामान्य रूप में कमी ===
-एक लैम्ब्डा कैलकुलस#कमी<ref>{{Citation
+रेडेक्स<ref>{{Citation
   |last=Barendregt
   |first=Hendrik Pieter
@@ Line 26: / Line 25: @@
   |archivedate=2004-08-23
 }}  [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> ... ''u<sub>n</sub>'' होती है, तो उसे हेड रेडेक्स कहा जाता है। [[बीटा सामान्य रूप]] लैम्ब्डा गणना का पद है जो हेड रिडेक्स नहीं है।{{efn|If one only deals with closed terms, these terms take the form ''λ'' ''x''. ''t''.}} हेड रीडक्शन पद के (गैर खाली) क्रमबद्ध श्रिंखला होती है जो पद के हेड रेडेक्स को श्रिंकलेट करती है। पद t की हेड रीडक्शन (जिसे हेड साधारण फ़ॉर्म में नहीं होने का समझा जाता है) हेड रीडक्शन है जो पद t से प्रारंभ होती है और हेड साधारण फ़ॉर्म पर समाप्त होती है। अभिकल्पिक दृष्टिकोण से, हेड रीडक्शन प्रोग्राम की प्रक्रिया है जब वह पुनरावृत्तिशील उप-प्रोग्राम का मूल्यांकन करता है। इस प्रकार की श्रिंकलन को कैसे कार्यान्वित किया जा सकता है, इसे समझना महत्वपूर्ण है। क्रिवाइन मशीन का उद्देश्य हेड साधारण फ़ॉर्म में पद को श्रिंकलने की प्रक्रिया प्रस्तावित करना है और इस प्रक्रिया को समय-समय पर वर्णित करना है। जैसे [[एलन ट्यूरिंग]] ने अवकाशी मशीन का उपयोग करके सामान्यता की नीति को समय-समय पर वर्णित किया, क्रिवाइन ने अवकाशी मशीन का उपयोग करके हेड साधारण फ़ॉर्म श्रिंकलन की नीति को समय-समय पर वर्णित किया जाता है।
-==== उदाहरण ====
+==== '''उदाहरण''' ====
-शब्द ((λ 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,
 जो इसके लिए है:
 : (λ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
 | title = Categorical Combinators, Sequential Algorithms and Functional
 | publisher = Birkhaüser
 | 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.}} और पर्यावरण के लिए ई, इन तीन संस्थाओं से जुड़े स्थितिों को टी, पी, ई लिखा जाएगा। नियम बताते हैं कि कैसे मशीन स्थितिों के बीच पैटर्न की पहचान करने के बाद एक स्थिति को दूसरे स्थिति में बदल देती है।
+शब्द डी ब्रुयन सूचकांकों के साथ लैम्बडा-शब्द होता है। स्टैक और वातावरण एक ही पुनरावृत्तिशील डेटा संरचना में होते हैं। अधिक सटीक रूप से, पर्यावरण और स्टैक को ''<अवधि, पर्यावरण>'' के जोड़ों की सूची के रूप में प्रस्तुत किया जाता है, जिन्हें ''क्लोज़र'' कहा जाता है। निम्नलिखित में, किसी तत्व a की सूची ℓ ( स्टैक या पर्यावरण) के प्रमुख के रूप में प्रविष्टि a'':ℓ'' लिखी जाती है, चूँकि खाली सूची □ लिखी जाती है। स्टैक वह स्थान है जहां मशीन क्लोजर को संग्रहीत करती है जिसका मूल्यांकन किया जाना चाहिए, चूँकि पर्यावरण मूल्यांकन के समय निश्चित समय पर सूचकांक और क्लोजर के बीच संबंध है। पर्यावरण का पहला तत्व अनुक्रमणिका ''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.}} और पर्यावरण के लिए e, इन तीन संस्थाओं से जुड़े स्थितियों को t, p, e लिखा जाएगा जाता है। नियम बताते हैं कि कैसे मशीन स्थितिों के बीच नमूना की पहचान करने के बाद स्थिति को दूसरे स्थिति में बदल देती है।
-प्रारंभिक अवस्था का लक्ष्य किसी पद t का मूल्यांकन करना है, यह अवस्था t,□,□ है, जिसमें पद t है और स्टैक और वातावरण खाली हैं। अंतिम स्थिति (त्रुटि के अभाव में) λ t, □, e के रूप में होती है, दूसरे शब्दों में, परिणामी शब्द अपने पर्यावरण और एक खाली स्टैक के साथ एक अमूर्त है।
+प्रारंभिक स्थिति एक शब्द t को मूल्यांकित करने का उद्देश्य रखती है, यह ''t'',□,□, की स्थिति है, जिसमें शब्द t है और स्टैक और वातावरण खाली हैं। अंतिम स्थिति (त्रुटि की अनुपस्थिति में) एक लैम्बडा''λ t'', □, e की आकृति होती है, अन्य शब्दों में, परिणामी शब्द एक विचारशक्ति के साथ होती है जिसका वातावरण होता है और एक खाली स्टैक होती है।
 === परिवर्तन ===
-क्रिविन मशीन<ref name="Curien" />इसमें चार ट्रांज़िशन हैं: ''ऐप'', ''एब्स'', ''ज़ीरो'', ''सक्स''।
+क्रिवाइन मशीन<ref name="Curien" /> में चार स्थानांतरण होते हैं: ''ऐप'', ''एब्स'', ''शून्य'', ''सुक्क'' ।
 {| class="wikitable center" style = "width:50%"
-|+ Transitions of the Krivine machine
+|+ क्रिवाइन मशीन के स्थानांतरण
 |-
-! scope=col | Name
+! scope=col |नाम
-! scope=col | Before
+! scope=col |पहले
-! scope=col | After
+! scope=col |बाद में
 |-
-| width="20%" |
+| width="20%" |''ऐप''
-'''''App'''''
 | width="40%" |
 ''t u'', p, e
@@ Line 74: / Line 73: @@
 ''t'', <''u'',e>:p, e
 |-
-|
+|''एब्स''
-'''''Abs'''''
 |
 ''λ t'', <''u'',e'>:p, e
@@ Line 81: / Line 79: @@
 ''t'', p, <''u'',e'>:e
 |-
-|
+|''शून्य''
-'''''Zero'''''
 |
 ''0'', p, <''t'', e'>:e
@@ Line 88: / Line 85: @@
 ''t'', p, e'
 |-
-|
+|''सक्स''
-'''''Succ'''''
 |
 ''n+1'', p, <''t'',e'>:e
@@ Line 95: / Line 91: @@
 n, p, e
 |}
-ट्रांज़िशन ''ऐप'' किसी एप्लिकेशन के पैरामीटर को हटा देता है और इसे आगे के मूल्यांकन के लिए स्टैक पर रख देता है। परिवर्तन ''एबीएस'' शब्द के λ को हटा देता है और स्टैक के शीर्ष से क्लोजर को पॉप अप करता है और इसे पर्यावरण के शीर्ष पर रख देता है। यह समापन नए परिवेश में डी ब्रुइज़न सूचकांक ''0'' से मेल खाता है। संक्रमण ''शून्य'' पर्यावरण का पहला समापन लेता है। इस समापन की अवधि वर्तमान अवधि बन जाती है और इस समापन का वातावरण वर्तमान परिवेश बन जाता है। संक्रमण ''सक्स'' पर्यावरण सूची के पहले समापन को हटा देता है और सूचकांक के मूल्य को कम कर देता है।
+संक्रमण ''ऐप'' किसी आवेदन के पैरामीटर को हटा देता है और इसे आगे के मूल्यांकन के लिए स्टैक पर रख देता है। परिवर्तन ''एबीएस'' पद के λ को हटा देता है और स्टैक के शीर्ष से क्लोजर को पॉप अप करता है और इसे पर्यावरण के शीर्ष पर रख देता है। यह समापन नए परिवेश में डी ब्रुइज़न सूचकांक ''0'' से मेल खाता है। संक्रमण ''शून्य'' पर्यावरण का पहला समापन लेता है। इस समापन की अवधि वर्तमान अवधि बन जाती है और इस समापन का वातावरण वर्तमान परिवेश बन जाता है। संक्रमण सुक्क पर्यावरण सूची के पहले समापन को हटा देता है और सूचकांक के मूल्य को कम कर देता है।
 === दो उदाहरण ===
-आइए हम पद (λ 0 0) (λ 0) का मूल्यांकन करें जो पद (λ x. x x) (λ x. x) से संगत है। आइए स्थिति (λ 0 0) (λ 0), □, □ से शुरू करें।
+हम (λ 0 0) (λ 0) पद का मूल्यांकन करें जो पद (λ x. x x) (λ x. x) के साथ होता है। नीचे दिए गए स्थिति से प्रारंभ करेंगे:
+(''λ'' 0 0) (''λ'' 0), □, □.
 {|class="wikitable center" style= "width:30%"
-|+ Evaluation of the  term ''(λ 0 0) (λ 0)''
+|+ पद का मूल्यांकन ''(λ 0 0) (λ 0)''
 |-
 |
@@ Line 128: / Line 126: @@
 |-
 |}
-निष्कर्ष यह है कि पद (λ 0 0) (λ 0) का शीर्ष सामान्य रूप λ 0 है। यह चर के साथ अनुवाद करता है: पद का शीर्ष सामान्य रूप (λ x. x x) (λ x. x) है λ एक्स. एक्स।
+निष्कर्ष यह है कि पद (λ 0 0) (λ 0) का शीर्ष सामान्य रूप λ 0 है। यह चर के साथ अनुवाद करता है: पद (λ x. x x) (λ x. x) का शीर्ष सामान्य रूप ''λ'' ''x''. ''x''. है।
-आइए हम पद ((λ 0) (λ 0)) (λ 0) का मूल्यांकन करें जैसा कि नीचे दिखाया गया है:
+अब हम पद ((λ 0) (λ 0)) (λ 0) का मूल्यांकन करें जैसा कि नीचे दिखाया गया है:
 {|class="wikitable center" style="width:35%"
-|+ Evaluation of ((λ 0) (λ 0)) (λ 0)
+|+ ((λ 0) (λ 0)) (λ 0) का मूल्यांकन
 |-
 | ((''λ'' 0) (''λ'' 0)) (''λ'' 0), □, □
@@ Line 143: / Line 141: @@
 | 0, [<(''λ'' 0), □>], [<(''λ'' 0), □>]
 |-
-| ''λ'' 0, [<(''λ'' 0), □>],  □
+| ''λ'' 0, [<(''λ'' 0), □>], □
 |-
 | 0, □, [<(''λ'' 0), □>]
@@ Line 153: / Line 151: @@
 == अंतर-व्युत्पत्तियाँ ==
-क्रिवाइन मशीन, CEK मशीन की तरह, न केवल कार्यात्मक रूप से [[मेटा-सर्कुलर मूल्यांकनकर्ता]] के अनुरूप है,
+क्रिवाइन मशीन, CEK मशीन की प्रकार, न केवल कार्यात्मक रूप से [[मेटा-सर्कुलर मूल्यांकनकर्ता]] के अनुरूप है,यह वाक्य विन्यास की दृष्टि से भी मेल खाता है <math>\lambda\widehat{\rho}</math> गणना - पियरे-लुई क्यूरियन का संस्करण <math>\lambda\widehat{\rho}</math> [[स्पष्ट प्रतिस्थापन]] की गणना जो कमी के अनुसार बंद होती है - सामान्य-क्रम कटौती रणनीति के साथ होता है।
-<ref name="schmidt 80">
-{{cite conference
+यदि <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">
-|last1=Schmidt
-|first1=David A.
-|date=1980
-|title=State transition machines for lambda calculus expressions
-|chapter=State transition machines for lambda-calculus expressions
-|series=Lecture Notes in Computer Science
-|volume=94
-|institution=Semantics-Directed Compiler Generation, LNCS 94
-|pages=415–440
-|doi=10.1007/3-540-10250-7_32|isbn=978-3-540-10250-2
-}}
-</ref>
-<ref name="schmidt 07">
 {{cite journal
-|last1=Schmidt
+|last1=Krivine
-|first1=David A.
+|first1=Jean-Louis
 |date=2007
-|title=State-transition machines, revisited
+|title=A call-by-name lambda-calculus machine
 |journal=Higher-Order and Symbolic Computation
 |volume=20
 |issue=3
-|pages=333–335
+|pages=199–207
-|doi=10.1007/s10990-007-9017-x|s2cid=3012667
+|doi=10.1007/s10990-007-9018-9|s2cid=18158499
 }}
-</ref>
+</ref><ref name="1biernacka danvy brics-07">
-<ref name="ager et al 03">
-{{cite journal
-|last1=Ager
-|first1=Mads Sig
-|last2=Biernacki
-|first2=Dariusz
-|author3-link=Olivier Danvy
-|last3=Danvy
-|first3=Olivier
-|last4=Midtgaard
-|first4=Jan
-|date=2003
-|title=A Functional Correspondence between Evaluators and Abstract Machines
-|journal=Brics Report Series
-|volume=10
-|issue=13
-|institution=5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'03)
-|pages=8–19
-|doi=10.7146/brics.v10i13.21783}}
-</ref>
-यह वाक्यविन्यास की दृष्टि से भी मेल खाता है <math>\lambda\widehat{\rho}</math> कैलकुलस - पियरे-लुई क्यूरियन का एक संस्करण <math>\lambda\widehat{\rho}</math> [[स्पष्ट प्रतिस्थापन]] की गणना जो कमी के तहत बंद होती है - एक सामान्य-क्रम कटौती रणनीति के साथ।
-<ref name="curien 91">
-{{cite journal
-|last1=Curien
-|first1=Pierre-Louis
-|date=1991
-|title=An Abstract Framework for Environment Machines
-|journal=Theoretical Computer Science
-|volume=82
-|issue=2
-|pages=389–402
-|doi=10.1016/0304-3975(91)90230-Y}}
-</ref>
-<ref name="1biernacka danvy brics-07">
 {{cite journal
 |last1=Biernacka
@@ Line 229: / Line 180: @@
 |pages=1–30
 |doi=10.7146/brics.v13i3.21909}}
-</ref>
+</ref>(इसके अतिरिक्त, यदि कटौती की रणनीति मूल्य के आधार पर दाएं से बाएं कॉल है और इसमें सामान्यीकृत सम्मलित है <math>\beta</math> कमी, तो वाक्यात्मक रूप से संगत मशीन [[जेवियर लेरॉय]] की ज़िन्क अमूर्त मशीन है, जो [[OCaml|ओसीमल]] का आधार में है।
-<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
-|last1=[[Xavier Leroy|Leroy]]
-|first1=Xavier
-|date=1990
-|title=The ZINC experiment: an economical implementation of the ML language
-|institution=Inria
-|number=117
-|url=https://hal.inria.fr/inria-00070049/document}}
-</ref>
-<ref name="1biernacka danvy brics-07"/>
 == यह भी देखें ==
@@ Line 274: / Line 187: @@
 * एसईसीडी मशीन
 * [[प्रोग्रामिंग भाषाओं का शब्दार्थ]]
+== यह भी देखें ==
+* स्पष्ट प्रतिस्थापन
+* परिचालन शब्दार्थ
+*
 ==टिप्पणियाँ==
@@ Line 282: / Line 200: @@
 Content in this edit is translated from the existing French Wikipedia article at [[:fr:Machine de Krivine]]; see its history for attribution.
 ==ग्रन्थसूची==
@@ Line 294: / Line 211: @@
 *Frédéric Lang: ''Explaining the lazy Krivine machine using explicit substitution and addresses''. Higher-Order and Symbolic Computation 20(3): 257-270 (2007) [https://hal.inria.fr/inria-00198756 archive].
 *[[Olivier Danvy]] (Ed.): Editorial of special issue of ''Higher-Order and Symbolic Computation'' on the Krivine machine, vol. 20(3) (2007)
 ==बाहरी संबंध==
 *{{Commonscatinline}}
-[[Category: लैम्ब्डा कैलकुलस]] [[Category: संचालनात्मक शब्दार्थ]] [[Category: शैक्षिक सार मशीनें]] [[Category: सैद्धांतिक कंप्यूटर विज्ञान]] [[Category: गणना के मॉडल]] [[Category: कम्प्यूटेबिलिटी सिद्धांत]] [[Category: सार मशीनें]] [[Category: प्रोग्रामिंग भाषा कार्यान्वयन]]
-[[Category: Machine Translated Page]]
 [[Category:Created On 08/07/2023]]
+[[Category:Machine Translated Page]]
+[[Category:Pages with script errors]]
+[[Category:Templates Vigyan Ready]]
+[[Category:कम्प्यूटेबिलिटी सिद्धांत]]
+[[Category:गणना के मॉडल]]
+[[Category:प्रोग्रामिंग भाषा कार्यान्वयन]]
+[[Category:लैम्ब्डा कैलकुलस]]
+[[Category:शैक्षिक सार मशीनें]]
+[[Category:संचालनात्मक शब्दार्थ]]
+[[Category:सार मशीनें]]
+[[Category:सैद्धांतिक कंप्यूटर विज्ञान]]

Anonymous

Search

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

Latest revision as of 11:07, 2 August 2023

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

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

उदाहरण

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

विवरण

स्थिति

परिवर्तन

दो उदाहरण

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

यह भी देखें

यह भी देखें

टिप्पणियाँ

संदर्भ

ग्रन्थसूची

बाहरी संबंध

Navigation

Wiki tools

Page tools

Other projects

Categories