क्रिवाइन मशीन
सैद्धांतिक कंप्यूटर विज्ञान में, मशीन वक्र अमूर्त मशीन है (कभी-कभी इसे आभासी मशीन भी कहा जाता है)। अमूर्त मशीन के रूप में, यह ट्यूरिंग मशीन और एसईसीडी मशीन के साथ सुविधाएँ साझा करती है। वक्र मशीन बताती है कि पुनरावर्ती समारोह की गणना कैसे करें। अधिक विशेष रूप से इसका उद्देश्य नाम से बुलाओ कमी का उपयोग करके लैम्ब्डा गणना के सामान्य रूप में कमी को सख्ती से परिभाषित करना है। इसकी औपचारिकता के लिए धन्यवाद, यह विवरण में बताता है कि प्रकार की कमी कैसे काम करती है और [कार्यात्मक प्रोग्रामिंग] भाषाओं के परिचालन शब्दार्थ की सैद्धांतिक नींव निर्धारित करती है। दूसरी ओर, वक्र मशीन कॉल-बाय-नाम लागू करती है क्योंकि यह समारोह शरीर को उसके पैरामीटर पर लागू करने से पहले β- कम करने योग्य अभिव्यक्ति के शरीर का मूल्यांकन करती है। दूसरे शब्दों में, अभिव्यक्ति (λ 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]:# अवध
- ढेर,
- पर्यावरण।
यह शब्द डी ब्रुइज़न सूचकांकों वाला λ-शब्द है। ढेर और पर्यावरण ही पुनरावर्ती डेटा संरचना से संबंधित हैं। अधिक सटीक रूप से, पर्यावरण और ढेर <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 है। यह चर के साथ अनुवाद करता है: पद का शीर्ष सामान्य रूप (λ 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) है।
अंतर-व्युत्पत्तियाँ
वक्र मशीन, CEK मशीन की तरह, न केवल कार्यात्मक रूप से मेटा-सर्कुलर मूल्यांकनकर्ता के अनुरूप है,
यह वाक्यविन्यास की दृष्टि से भी मेल खाता है गणना - पियरे-लुई क्यूरियन का संस्करण स्पष्ट प्रतिस्थापन की गणना जो कमी के तहत बंद होती है - सामान्य-क्रम कटौती रणनीति के साथ।
यदि गणना में सामान्यीकृत सम्मलित है कमी ( बरकरार, नेस्टेड रेडेक्स दो के अतिरिक्त चरण में अनुबंधित किया जाता है), तो वाक्यात्मक रूप से संबंधित मशीन जीन-लुई क्रिविन की मूल मशीन के साथ मेल खाती है।[3]
[4](इसके अतिरिक्त, यदि कटौती की रणनीति मूल्य के आधार पर दाएं से बाएं कॉल है और इसमें सामान्यीकृत सम्मलित है कमी, तो वाक्यात्मक रूप से संगत मशीन जेवियर लेरॉय की ZINC अमूर्त मशीन है, जो OCaml का आधार है।
यह भी देखें
- स्पष्ट प्रतिस्थापन
- परिचालन शब्दार्थ
- एसईसीडी मशीन
- प्रोग्रामिंग भाषाओं का शब्दार्थ
यह भी देखें
- स्पष्ट प्रतिस्थापन
- परिचालन शब्दार्थ
टिप्पणियाँ
- ↑ 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
