λ-पथरी। भाग दो: अभ्यास

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

पहले भाग ने हमें एक सैद्धांतिक विचार दिया कि लैम्ब्डा कैलकुलस क्या है। इस लेख में, हम अनौपचारिक अभ्यास-अभ्यास-अभ्यास योग आज्ञा का पालन करेंगे और इसे कार्रवाई में देखेंगे।

चर्च बुलियन कॉन्स्टेंट

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

हम सबसे सरल से शुरू करते हैं: True और False । इन स्थिरांक के व्यवहार को अपनाने वाले दो शब्द इस प्रकार हैं:

tru = λt.λf.t	एक दो-तर्क फ़ंक्शन जो हमेशा पहला तर्क देता है
fls = λt.λf.f	एक दो-तर्क फ़ंक्शन जो हमेशा दूसरा तर्क लौटाता है

if इस तरह के बूलियन स्थिरांक के लिए if तरह दिखेगा:
if = λb. λx. λy.bxy
यहाँ b tru या fls , x then , then y है।

आइए देखें कि यह कैसे काम करेगा:
if fls te

चूंकि if स्थिति झूठी है ( fls ), तो else शाखा से अभिव्यक्ति (हमारे मामले में e ) को लौटाया जाना चाहिए।

(λb. λx. λy. bxy) fls te	परिभाषा से if
(λx. λy. fls xy) te	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
(λy. fls ty) e	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
fls te	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
(λt.λf. f) t e	परिभाषा fls द्वारा
(λf. f) e	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
e	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी

बुनियादी बूलियन ऑपरेटरों को परिभाषित करना भी जटिल नहीं है। उदाहरण के लिए, एक संयोजन (एक तार्किक "और") इस तरह दिखेगा:
and = λx. λy. xy fls

and दो बूलियन मान प्राप्त करता है x और y । पहला x (करी) है। यदि यह tru (कटौती के बाद tru y fls ) है, तो y को वापस कर दिया जाएगा, जिसे तब सत्य के लिए भी जांचा जाएगा। इस प्रकार, हम अंतिम tru केवल तभी प्राप्त करेंगे जब x और y दोनों "सत्य" हों। अन्य सभी विकल्पों में, जवाब fls ।

चर्च नंबर

हम केवल प्राकृतिक संख्याओं को एनकोड करेंगे, जिसके लिए हम पीनो के स्वयंसिद्धों को याद करते हैं जो उनके सेट को परिभाषित करते हैं। कार्यान्वयन उन कार्यों पर आधारित होगा जो एक इकाई, दो, आदि जैसे संदर्भ में व्यवहार करते हैं। दरअसल, यह लैम्ब्डा कैलकुलस की विशेषताओं में से एक है: इसकी शर्तों में लिखी गई संस्थाओं में आत्मनिर्भरता नहीं होती है, क्योंकि वे किसी वस्तु के व्यवहार को अपनाती हैं।

तो, हमें एक फ़ंक्शन की आवश्यकता है जो दो तर्क लेता है: एक निश्चित प्रारंभिक मूल्य और अगले तत्व ( एक फॉलो-अप फ़ंक्शन ) को निर्धारित करने के लिए एक फ़ंक्शन । प्रारंभिक मान पर अनुवर्ती फ़ंक्शन के अनुप्रयोगों की संख्या में संख्या को इनकोड किया जाएगा:

0 ≡ λs.λz. z	फ़ंक्शन s को प्रारंभिक मान z शून्य समय पर लागू किया जाता है
1 ≡ λs.λz. sz	फ़ंक्शन s को z के प्रारंभिक मान पर एक बार लागू किया जाता है
2 ≡ λs.λz. s (sz)	फ़ंक्शन s को z के प्रारंभिक मान पर दो बार लागू किया जाता है
...	और इसी तरह

यह नोटिस करना आसान है कि शून्य तार्किक फाल्स के समान है। फिर भी, किसी को इससे दूरगामी निष्कर्ष नहीं निकालना चाहिए: यह सिर्फ एक संयोग है।

फॉलो फंक्शन का काम किसी दिए गए नंबर में एक जोड़ना है। यानी एक तर्क के रूप में, यह वह मूल्य लेगा जिसे आप बढ़ाना चाहते हैं, और जो दो तर्कों का कार्य भी है। इस प्रकार, कुल में, फ़ंक्शन (+1) में तीन तर्क हैं: पिछले चर्च नंबर n , प्रारंभिक मान के लिए n+1 बार लागू होने वाला फ़ंक्शन और प्रारंभिक मूल्य स्वयं। यह इस तरह दिखता है:
scc = λn. λs. λz. s (nsz)
यहाँ nsz z समय के लिए लागू फ़ंक्शन है। लेकिन हमें इसे n+1 बार लागू करने की आवश्यकता है, जहां से स्पष्ट s (nsz) लिया गया है।

मान लें कि हमें "यूनिट" से one = λs.λz. sz प्राप्त करने की आवश्यकता है one = λs.λz. sz one = λs.λz. sz "दो" two = λs.λz. s (sz) two = λs.λz. s (sz) । यह इस तरह होगा:

scc one s' z'	s' और z' - चर नाम के साथ प्रतिस्थापित मूल्यों को भ्रमित करने के लिए नहीं
(λn. λs. λz. s (nsz)) one s' z'	परिभाषा के अनुसार
(λs. λz. s (one sz)) s' z'	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
(λz. s' (one s' z)) z'	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
s' (one s' z')	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
s' ( (λs.λz। sz) s' z ')	परिभाषा के अनुसार
s' ( (λz. s' z) z' )	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
s' (s' z')	पिछली पंक्ति से रेखांकित अभिव्यक्ति की कमी
two s' z'	परिभाषा two

अंकगणित संचालन

इसके अलावा

दो चर्च संख्याओं को जोड़ने वाले फ़ंक्शन में दो शब्द होंगे: x और y , जिसके बदले में दो तर्क भी हैं - s (अनुवर्ती कार्य) और z (प्रारंभिक मूल्य)। जोड़ पहले से लागू करने के लिए z x समय में लागू होगा, और फिर एक और y समय।

plus = λx. λy. λs. λz. xs (ysz)

एक उदाहरण के रूप में, one = λs.λz. sz जोड़ें। one = λs.λz. sz और two = λs.λz. s (sz) two = λs.λz. s (sz) । जवाब इस तरह दिखना चाहिए: three = λs.λz. s (s (sz)) three = λs.λz. s (s (sz)) ।

plus one two s' z'	s' और z' - चर नाम के साथ प्रतिस्थापित मूल्यों को भ्रमित करने के लिए नहीं
(λx. λy. λs. λz. xs (ysz)) one two s' z'	परिभाषा से plus
one s' (two s' z')	कमी के बाद
(λs.λz. sz) s' (two s' z')	परिभाषा के अनुसार
s' (two s' z')	कमी के बाद
s' (( λs.λz. s (sz) s' z')	परिभाषा two
s' (s' (s' z'))	कमी के बाद
three s' z'	परिभाषा three

गुणन

गुणन के लिए फ़ंक्शन को अतिरिक्त फ़ंक्शन के माध्यम से परिभाषित किया जा सकता है। अंत में, x को y गुणा करने का अर्थ है y x प्रतियां जोड़ना।

times = λx. λy. x (plus y) z

plus का उपयोग किए बिना, चर्च की संख्या से गुणा का निर्धारण करने का एक और तरीका है। उनका विचार है कि उत्पाद x और y प्राप्त करने के लिए y आपको x को प्रारंभिक मान x लागू फंक्शन के लिए लेने की आवश्यकता है:

times' = λx.λy.λs.λz. x (ys) z

उदाहरण के लिए, हम two = λs.λz. s (sz) गुणा two = λs.λz. s (sz) two = λs.λz. s (sz) द्वारा three = λs.λz. s (s (sz)) three = λs.λz. s (s (sz)) । परिणाम में फॉर्म होना चाहिए: six = λs.λz. s (s (s (s (s (sz))))) six = λs.λz. s (s (s (s (s (sz))))) ।

times' two three s' z'	s' और z' - चर नाम के साथ प्रतिस्थापित मूल्यों को भ्रमित करने के लिए नहीं
(λx.λy.λs.λz. x (ys) z) two three s' z'	परिभाषा के अनुसार times'
two (three s') z'	कमी के बाद
(λs.λz. s (sz)) (three s') z'	परिभाषा two
three s' ((three s') z')	कमी के बाद
(λs.λz. s (s (sz))) s' ((three s') z')	परिभाषा three
s' (s' (s' ((three s') z')))	कमी के बाद
s' (s' (s' (((λs.λz. s (s (sz))) s') z')))	परिभाषा three
s' (s' (s' (( (λz. s' (s' (s' z))) z' )))	कमी के बाद
s' (s' (s' (s' (s' (s' z')))))	अभिव्यक्ति में कमी को रेखांकित करें
six s' z'	परिभाषा six

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

निष्कर्ष

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

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

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