λ-पथरी। भाग एक: इतिहास और सिद्धांत

इस लेख के लिए मुख्य स्रोतों से विचार, एक छोटी योजना और लिंक z6Dabrata habrayuzer द्वारा मुझे सौंपे गए , जिसके लिए उन्हें बहुत धन्यवाद ।

UPD: इसे और अधिक समझने के लिए पाठ में कुछ बदलाव किए गए हैं। शब्दार्थ घटक एक ही रहा है।

प्रविष्टि

शायद इस प्रणाली में न केवल आवेदन होंगे
तार्किक गणना की भूमिका में। ( अलोंजो चर्च, 1932 )

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


हम इतिहास में एक पारंपरिक (लेकिन संक्षिप्त) भ्रमण के साथ शुरू करते हैं। पिछली शताब्दी के 30 के दशक में, गणितज्ञों ने डेविड हिल्बर्ट द्वारा तैयार तथाकथित रिज़ॉल्यूशन प्रॉब्लम ( Entscheidungsproblem ) का सामना किया। इसका सार यह है कि हमारे पास एक निश्चित औपचारिक भाषा है जिसमें आप कोई भी बयान लिख सकते हैं। क्या एक एल्गोरिथ्म है जो चरणों की एक सीमित संख्या में इसकी सच्चाई या झूठ को निर्धारित करता है? उत्तर अलोंजो चर्च और एलन ट्यूरिंग के समय के दो महान वैज्ञानिकों द्वारा पाया गया था। उन्होंने दिखाया (पहला - उनके द्वारा आविष्कार किए गए λ-पथरी की मदद से, और दूसरा - ट्यूरिंग मशीन के सिद्धांत के साथ) कि अंकगणित के लिए यह एल्गोरिथ्म सिद्धांत रूप में मौजूद नहीं है, अर्थात्। एंत्सिडींगस्प्रोब्लेम आमतौर पर अघुलनशील होता है।

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

λ-कलन: मूल अवधारणाएं

वाक्य-विन्यास

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

हम इसके सबसे सरल रूप पर विचार करेंगे: एक शुद्ध अनडिम्ड लैम्ब्डा कैलकुलस, और यह वही है जो हमारे निपटान में होगा।

शर्तें :

चर:	x
लैम्ब्डा अमूर्त (अनाम फ़ंक्शन):	λx.t , जहां x फ़ंक्शन का तर्क है, t इसका शरीर है।
समारोह के आवेदन (आवेदन):	fx , जहाँ f एक फ़ंक्शन है, x इसमें दिए गए तर्क का मान है

परिचालन प्राथमिकता समझौते :

• फ़ंक्शन का उपयोग बाएं-सहयोगी है। यानी stu (st) u
  
• एप्लिकेशन (एप्लिकेशन या फ़ंक्शन कॉल दिए गए मूल्य के संबंध में) वह सब कुछ लेता है जो वह पहुंचता है। यानी λx. λy. xyx λx. λy. xyx अर्थ λx. (λy. ((xy) x)) के समान है λx. (λy. ((xy) x)) λx. (λy. ((xy) x))
  
• ब्रैकेट स्पष्ट रूप से क्रियाओं के समूहीकरण का संकेत देते हैं।

ऐसा लग सकता है कि हमें कई तर्कों के साथ कार्यों के लिए कुछ विशेष तंत्रों की आवश्यकता है, लेकिन वास्तव में ऐसा नहीं है। दरअसल, शुद्ध लैम्ब्डा कैलकुलस की दुनिया में, एक फ़ंक्शन द्वारा लौटाया गया मान भी एक फ़ंक्शन हो सकता है। इसलिए, हम मूल फ़ंक्शन को इसके केवल एक तर्क पर लागू कर सकते हैं, दूसरों को "ठंड"। नतीजतन, हम तर्कों के "पूंछ" से एक नया कार्य प्राप्त करते हैं, जिसमें पिछले तर्क लागू होते हैं। इस तरह के एक ऑपरेशन को करींग (उस हास्केल करी के सम्मान में) कहा जाता है। यह कुछ इस तरह दिखेगा:

f = λx.λy.t	दो तर्कों के साथ कार्य x और y और बॉडी t
fvw	v वत v व w f v
(fv) w	यह प्रविष्टि पिछले एक के समान है, लेकिन कोष्ठक स्पष्ट रूप से प्रतिस्थापन अनुक्रम का संकेत देते हैं
((λy.[x → v]t) w)	x बजाय सब्स्टिट्यूट v । [x → v]t अर्थ है "शरीर t जिसमें x की सभी घटनाएं v द्वारा प्रतिस्थापित की जाती हैं"
[y → w][x → v]t	y बजाय स्थानापन्न w । रूपांतरण पूरा हो गया है।

और अंत में, गुंजाइश के बारे में कुछ शब्द। एक चर x को बाध्य किया जाता है यदि यह t λ-abstraction λx.t के शरीर t यदि x किसी अतिव्यापी अमूर्त द्वारा जुड़ा नहीं है, तो इसे मुक्त कहा जाता है। उदाहरण के लिए, xy और λy.xy में x λy.xy स्वतंत्र हैं, और λx.x और λz.λx.λy.x(yz) में x की λx.x जुड़ी हुई हैं। (λx.x)x पहली घटना जुड़ा हुआ है, और दूसरा स्वतंत्र है। यदि शब्द के सभी चर जुड़े हुए हैं, तो इसे बंद , या संयोजन कहा जाता है। हम निम्नलिखित सरल संयोजक ( पहचान समारोह ) का उपयोग करेंगे: id = λx.x यह कोई कार्रवाई नहीं करता है, लेकिन बिना बदलाव के बस अपना तर्क देता है।

गणना प्रक्रिया

निम्नलिखित आवेदन पर विचार करें:

(λx.t) y

इसका बाईं ओर - (λx.t) - एक तर्क x और बॉडी t साथ एक फ़ंक्शन t । गणना के प्रत्येक चरण में y साथ t अंदर वैरिएबल x की सभी घटनाओं को प्रतिस्थापित करने में शामिल होगा। इस प्रकार के शब्द-अनुप्रयोग को रीडेक्स कहा जाता है ( रिड्यूसियल एक्सप्रेशन से , रिडेक्स - "संक्षिप्त अभिव्यक्ति"), और निर्दिष्ट नियम के अनुसार रीराइट राइटिंग ऑपरेशन को बीटा रिडक्शन कहा जाता है।

अगले गणना चरण के लिए रीडेक्स चुनने के लिए कई रणनीतियाँ हैं। हम उदाहरण के रूप में निम्नलिखित शब्द का उपयोग करके उन पर विचार करेंगे:

(λx.x) ((λx.x) (λz. (λx.x) z)) ,

जो सादगी के लिए फिर से लिखा जा सकता है

id (id (λz. id z))

(याद रखें कि id फॉर्म λx.x का एक पहचान कार्य है)

इस शब्द में तीन रीडेक्स हैं:

1. पूरा reduction-कटौती । इस स्थिति में, प्रत्येक बार परिकलित शब्द के अंदर पुनर्भरण को मनमाने ढंग से चुना जाता है। यानी हमारे उदाहरण की गणना आंतरिक रेडेक्स से बाहरी में की जा सकती है:
   
   
2. गणना का सामान्य क्रम । पहला हमेशा सबसे बाहरी, सबसे बाहरी रेडेक्स होता है।
   
   
3. नाम से पुकारते हैं । इस रणनीति में गणना प्रक्रिया पिछले एक के समान है, लेकिन अमूर्त के अंदर संक्षिप्तीकरण पर प्रतिबंध इसमें जोड़ा गया है। यानी हमारे उदाहरण में, हम कदम पर रुकते हैं:
   
   इस तरह की रणनीति का एक अनुकूलित संस्करण ( आवश्यकतानुसार कॉल ) हास्केल द्वारा उपयोग किया जाता है। ये तथाकथित "आलसी" गणना हैं।
   
4. मूल्य से बुलाओ । यहां, कटौती सबसे बाईं ओर (बाहरी) रिडेक्स से शुरू होती है, जिसका दाएं हाथ में मूल्य है - एक बंद शब्द जिसे आगे गणना नहीं की जा सकती है।
   
   शुद्ध लैम्ब्डा कैलकुलस के लिए, ऐसा शब्द एक λ-एब्स्ट्रैक्शन (फंक्शन) है, और समृद्ध कैलकी में यह स्थिरांक, तार, सूची इत्यादि हो सकता है। इस रणनीति का उपयोग अधिकांश प्रोग्रामिंग भाषाओं में किया जाता है, जब सभी तर्कों की गणना पहले की जाती है, और फिर सभी को एक साथ फ़ंक्शन में प्रतिस्थापित किया जाता है।

यदि शब्द में अब कोई नया शब्द नहीं है, तो वे कहते हैं कि यह गणना की गई है , या सामान्य रूप में है । प्रत्येक पद का सामान्य रूप नहीं होता है, उदाहरण के लिए (λx.xx)(λx.xx) गणना के प्रत्येक चरण में यह स्वयं उत्पन्न होगा (यहां पहला ब्रैकेट एक अनाम फ़ंक्शन है, दूसरा x में इसके स्थान पर प्रतिस्थापित मान है)।

मूल्य-आधारित कॉल रणनीति का नुकसान यह है कि यह लूप हो सकता है और शब्द के मौजूदा सामान्य मूल्य को नहीं पा सकता है। उदाहरण के लिए, अभिव्यक्ति पर विचार करें

(λx.λy. x) z ((λx.xx)(λx.xx))

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

एक और सूक्ष्मता चरों के नामकरण से संबंधित है। उदाहरण के लिए, प्रतिस्थापन (λx.λy.x)y प्रतिस्थापन के बाद λy.y में गणना की λy.y यानी चर नामों के संयोग के कारण, हमें एक पहचान फ़ंक्शन मिलता है जहां यह मूल रूप से इरादा नहीं था। दरअसल, हम स्थानीय वैरिएबल को y नहीं कहेंगे, लेकिन z - मूल शब्द का रूप होगा (λx.λz.x)y और, कमी के बाद, λz.y जैसा λz.y इस तरह की अस्पष्टताओं को खत्म करने के लिए, यह स्पष्ट रूप से निगरानी रखना आवश्यक है कि प्रारंभिक शब्द से सभी मुक्त चर प्रतिस्थापन के बाद मुक्त रहते हैं। इस उद्देश्य के लिए, α- रूपांतरण का उपयोग करें - नाम संघर्ष से बचने के लिए अमूर्त में एक चर का नाम बदलना।

ऐसा भी होता है कि हमारे पास एक एब्स्ट्रैक्शन λx.tx , और x में बॉडी t में मुफ्त प्रविष्टियां नहीं हैं। इस मामले में, यह अभिव्यक्ति सिर्फ t बराबर होगी। ऐसे परिवर्तन को an-रूपांतरण कहा जाता है।

यह लैम्ब्डा कैलकुलस से परिचय का निष्कर्ष निकालता है। अगले लेख में, हम इस पर ध्यान केंद्रित करेंगे कि यह क्या था: λ-पथरी पर प्रोग्रामिंग।

सूत्रों की सूची

1. "लैम्ब्डा कैलकुलस क्या है और आपको ध्यान रखना चाहिए?", एर्की लिंडपेरे
2. प्रकार और प्रोग्रामिंग भाषाएँ, बेंजामिन पियर्स
3. विकी संग्रह "लैंबडा कैलकुलस"
4. "हास्केल ट्यूटोरियल", एंटोन खोलोमीव
5. कार्यात्मक प्रोग्रामिंग पर व्याख्यान