यदि आप कोई प्रोग्राम नहीं लिख रहे हैं, तो प्रोग्रामिंग भाषा का उपयोग न करें

लेस्ली लैम्पपोर्ट वितरित कंप्यूटिंग में मौलिक काम के लेखक हैं, और आप उन्हें ला टेक्स में पत्रों द्वारा भी जान सकते हैं - "लैम्पपोर्ट टीएक्स"। यह पहली बार था जब उन्होंने 1979 में लगातार सुसंगतता की अवधारणा शुरू की, और उनका लेख "मल्टीप्रोसेसर कंप्यूटर कैसे बनाया जाए, जो सही ढंग से मल्टीप्रोसेस प्रोग्राम को सही करता है" ने दिक्जस्ट्रा पुरस्कार जीता (अधिक सटीक रूप से, 2000 में पुरस्कार पुराने तरीके से कहा गया था: "PODC Influential Paper Award ")। उसके बारे में विकिपीडिया पर एक लेख है जहाँ आप कुछ और दिलचस्प लिंक प्राप्त कर सकते हैं। यदि आप बीजान्टिन जनरलों (बीएफटी) की समस्याओं से पहले या समस्याओं को हल करने से प्रसन्न हैं, तो आपको समझना चाहिए कि लैमपोर्ट इस सब के पीछे है।

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

एक बार टोनी होर ने लिखा था: "हर बड़े कार्यक्रम में एक छोटा कार्यक्रम होता है जो बाहर निकलने की कोशिश करता है।" मैं इसे इस तरह से दोहराऊंगा: "हर बड़े कार्यक्रम में, एक एल्गोरिथ्म होता है जो बाहर निकलने की कोशिश करता है।" हालाँकि, मैं नहीं जानता कि क्या टोनी इस तरह की व्याख्या से सहमत होंगे।

एक उदाहरण के रूप में, दो सकारात्मक पूर्णांकों के सबसे बड़े सामान्य भाजक को खोजने के लिए यूक्लिडियन एल्गोरिथ्म पर विचार करें $$$(एम, एन)$ । इस एल्गोरिथ्म में हम असाइन करते हैं $$$x$ अर्थ $$$एम$ । $$$एन$ - मूल्य $$$य$ , और फिर इनमें से सबसे छोटे मूल्यों को सबसे बड़े से घटाते हैं, जब तक कि वे समान न हों। इन का अर्थ $$$x$ और $$$य$ और सबसे बड़ा सामान्य कारक होगा। इस एल्गोरिथ्म और इसे लागू करने वाले कार्यक्रम के बीच आवश्यक अंतर क्या है? इस तरह के कार्यक्रम में कई निम्न-स्तरीय चीजें होंगी: $$$एम$ और $$$एन$ एक निश्चित प्रकार, BigInteger या ऐसा कुछ होगा; यदि कार्यक्रम का व्यवहार निर्धारित करना आवश्यक होगा $$$एम$ और $$$एन$ गैर सकारात्मक; और इतने पर और आगे। एल्गोरिदम और कार्यक्रमों के बीच कोई स्पष्ट अंतर नहीं है, लेकिन सहज स्तर पर हम अंतर को महसूस करते हैं - एल्गोरिदम अधिक सार, उच्च-स्तर हैं। और, जैसा कि मैंने कहा, प्रत्येक कार्यक्रम के अंदर एक एल्गोरिथ्म रहता है जो बाहर निकलने की कोशिश करता है। आमतौर पर ये वो एल्गोरिदम नहीं होते हैं जिनके बारे में हमें एल्गोरिदम कोर्स में बताया गया था। एक नियम के रूप में, यह एक एल्गोरिथ्म है जो केवल इस विशेष कार्यक्रम के लिए उपयोगी है। सबसे अधिक बार, यह किताबों में वर्णित की तुलना में बहुत अधिक जटिल होगा। इस तरह के एल्गोरिदम को अक्सर विनिर्देशों कहा जाता है। और ज्यादातर मामलों में, यह एल्गोरिथ्म बाहर निकलने में विफल रहता है, क्योंकि प्रोग्रामर को इसके अस्तित्व पर संदेह नहीं है। तथ्य यह है कि यदि आपकी सोच कोड, प्रकारों, अपवादों पर केंद्रित है, while छोरों, और अधिक, और संख्याओं के गणितीय गुणों पर नहीं, तो यह एल्गोरिथम नहीं देखा जा सकता है। इस तरह लिखा गया एक प्रोग्राम डिबग करना कठिन है, इसलिए कोड स्तर पर एक एल्गोरिथ्म को डीबग करने का क्या मतलब है। डिबगिंग टूल कोड में त्रुटियों को खोजने के लिए डिज़ाइन किए गए हैं, और एल्गोरिथ्म में नहीं। इसके अलावा, ऐसा कार्यक्रम अप्रभावी होगा, क्योंकि, फिर से, आप कोड स्तर पर एल्गोरिथ्म का अनुकूलन करेंगे।

विज्ञान और प्रौद्योगिकी के लगभग किसी भी अन्य क्षेत्र की तरह, इन समस्याओं को गणितीय रूप से वर्णित करके हल किया जा सकता है। ऐसा करने के कई तरीके हैं, हम उनमें से सबसे उपयोगी पर विचार करेंगे। यह अनुक्रमिक और समानांतर (वितरित) एल्गोरिदम दोनों के साथ काम करता है। इस पद्धति में एल्गोरिदम के निष्पादन को राज्यों के अनुक्रम के रूप में वर्णित किया गया है, और प्रत्येक राज्य को चर के गुणों के असाइनमेंट के रूप में वर्णित किया गया है। उदाहरण के लिए, यूक्लिडियन एल्गोरिथ्म को निम्नलिखित राज्यों के अनुक्रम के रूप में वर्णित किया गया है: पहला, x को मूल्य M (संख्या 12) सौंपा गया है, और y मान N (संख्या 18) है। तब हम बड़े से छोटे मूल्य को घटाते हैं ( $$$x$ से $$$य$ ), जो हमें उस अगली स्थिति में ले जाता है जिसमें हम पहले से ही दूर हैं $$$य$ से $$$x$ , और एल्गोरिथ्म का निष्पादन इस पर रुक जाता है: $$$[x \ leftarrow 12, \ leftarrow 18], [x \ leftarrow 12, \ leftarrow 6], [x \ leftarrow ६, \ leftarrow 6]$ ।

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

कई व्यवहारों का वर्णन किया गया है, सबसे पहले, राज्यों के लिए एक प्रारंभिक विधेय द्वारा (एक विधेय एक बूलियन मूल्य के साथ एक फ़ंक्शन है); और, दूसरी बात, राज्यों के जोड़े के लिए अगले राज्य का एक विधेय। कुछ व्यवहार $$$s_1, s_2, s_3 ...$ कई व्यवहार में प्रवेश करता है केवल अगर प्रारंभिक विधेय सच है $$$s_1$ , और अगले चरण की भविष्यवाणी प्रत्येक चरण के लिए सही है $$$(s_i, s_ {i + 1})$ । आइए हम इस तरह से यूक्लिडियन एल्गोरिथ्म का वर्णन करने का प्रयास करें। यहाँ प्रारंभिक विधेय है: $$$(x = M) \ भूमि (y = N)$ । और राज्यों के जोड़े के लिए अगले राज्य की भविष्यवाणी निम्नलिखित सूत्र द्वारा वर्णित है:

कृपया चिंतित न हों - इसमें केवल छह लाइनें हैं; यदि आप ऐसा करते हैं तो यह पता लगाना बहुत आसान है। इस सूत्र में, स्ट्रोक के बिना चर पहले राज्य को संदर्भित करते हैं, और स्ट्रोक वाले चर दूसरे राज्य में समान चर होते हैं।

जैसा कि आप देख सकते हैं, पहली पंक्ति कहती है कि पहले मामले में x पहले राज्य में y से अधिक है। एक तार्किक और के बाद, यह कहा गया है कि दूसरे राज्य में x का मान पहले राज्य में x के मान के बराबर है और पहले राज्य में y का मान है। एक और तार्किक और के बाद, यह कहा गया है कि दूसरे राज्य में y का मूल्य पहले राज्य में y के मूल्य के बराबर है। इसका मतलब यह है कि जब x, y से अधिक होता है, तो प्रोग्राम x से y को घटाएगा और y को अपरिवर्तित छोड़ देगा। अंतिम तीन पंक्तियाँ मामले का वर्णन करती हैं जब y x से अधिक होता है। ध्यान दें कि यदि x के बराबर y है तो यह सूत्र गलत है। इस स्थिति में, कोई अगली स्थिति नहीं है, और व्यवहार बंद हो जाता है।

इसलिए, हमने यूक्लिडियन एल्गोरिथ्म को केवल दो गणितीय सूत्रों में वर्णित किया है - और हमें किसी भी प्रोग्रामिंग भाषा के साथ गड़बड़ नहीं करना है। इन दोनों फॉर्मूलों से ज्यादा खूबसूरत और क्या हो सकता है? उन्हें एक सूत्र से बदलें। व्यवहार $$$s_1, s_2, s_3 ...$ यूक्लिडियन एल्गोरिथ्म का निष्पादन केवल तभी होता है:

• $$$Init_E$ के लिए सच है $$$s_1$ ।
• $$$Next_E$ हर कदम के लिए सच है $$$(s_i, s_ {i + 1})$ ।

यह व्यवहार के लिए एक विधेय के रूप में लिखा जा सकता है (हम इसे एक संपत्ति कहेंगे)। पहली स्थिति को बस के रूप में व्यक्त किया जा सकता है $$$Init_E$ । इसका मतलब यह है कि हम एक राज्य की व्याख्या व्यवहार के लिए सही के रूप में करते हैं यदि यह पहले राज्य के लिए सच है। दूसरी शर्त इस प्रकार लिखी गई है: $$$\ square Next_E$ । एक वर्ग का अर्थ है राज्य के जोड़े की भविष्यवाणी और व्यवहार की भविष्यवाणी के बीच पत्राचार, अर्थात्। $$$Next_E$ व्यवहार में हर कदम के लिए सच है। परिणामस्वरूप, सूत्र इस तरह दिखता है: $$$Init_E \ land \ square Next_E$ ।

इसलिए, हमने यूक्लिडियन एल्गोरिथम को गणितीय रूप से लिखा। संक्षेप में, ये केवल परिभाषाएँ हैं, या संक्षिप्त रूप हैं $$$Init_E$ और $$$Next_E$ । यह पूरा सूत्र इस तरह दिखेगा:

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

हमने जो संपत्ति लिखी है वह कुछ व्यवहार के लिए सही है यदि केवल दो स्थितियां जो हम वर्णित हैं, वे संतुष्ट हैं। पर $$$M = 12$ और $$$N = 18$ वे निम्नलिखित व्यवहार के लिए सही हैं: $$$[x \ leftarrow 12, \ leftarrow 18], [x \ leftarrow 12, \ leftarrow 6], [x \ leftarrow ६, \ leftarrow 6]$ । लेकिन ये स्थितियाँ समान व्यवहार के छोटे संस्करणों के लिए भी संतुष्ट हैं: $$$[x \ leftarrow 12, \ leftarrow 18], [x \ leftarrow 12, \ leftarrow 6]$ । और हमें उन्हें ध्यान में नहीं रखना चाहिए, क्योंकि ये हमारे द्वारा पहले से ही उठाए गए व्यवहार के अलग-अलग चरण हैं। उनसे छुटकारा पाने का एक स्पष्ट तरीका है: बस उन व्यवहारों को अनदेखा करें जो एक राज्य में समाप्त होते हैं जिसके लिए कम से कम एक अगला कदम संभव है। लेकिन यह सही दृष्टिकोण नहीं है, हमें और अधिक सामान्य समाधान की आवश्यकता है। इसके अलावा, यह स्थिति हमेशा काम नहीं करती है।

इस समस्या की चर्चा हमें सुरक्षा और गतिविधि की अवधारणाओं की ओर ले जाती है। सुरक्षा संपत्ति इंगित करती है कि कौन सी घटनाएं वैध हैं। उदाहरण के लिए, एल्गोरिथ्म को सही मान वापस करने की अनुमति है। गतिविधि संपत्ति इंगित करती है कि कौन सी घटनाएं जल्द या बाद में होनी चाहिए। उदाहरण के लिए, एक एल्गोरिथ्म को जल्द या बाद में कुछ मूल्य वापस करना चाहिए। यूक्लिडियन एल्गोरिथ्म के लिए, सुरक्षा संपत्ति निम्नानुसार है: $$$Init_E \ land \ square Next_E$ । समय से पहले रुकने से रोकने के लिए इसमें एक गतिविधि गुण जोड़ा जाना चाहिए: $$$Init_E \ भूमि \ वर्ग Next_E \ भूमि L$ । प्रोग्रामिंग भाषाओं में, सबसे अच्छी तरह से, गतिविधि की कुछ आदिम परिभाषा है। सबसे अधिक बार, गतिविधि का उल्लेख भी नहीं किया जाता है, बस यह निहित है कि कार्यक्रम में अगला कदम होना चाहिए। और इस संपत्ति को जोड़ने के लिए, आपको एक जटिल कोड की आवश्यकता है। गणितीय रूप से, गतिविधि को व्यक्त करना बहुत आसान है (बस इसके लिए वर्ग की आवश्यकता है), लेकिन, दुर्भाग्य से, मेरे पास इसके लिए समय नहीं है - हमें अपनी चर्चा को सुरक्षा तक सीमित करना होगा।

केवल गणितज्ञों के लिए एक छोटा विषयांतर: प्रत्येक गुण व्यवहार का एक समूह है जिसके लिए यह गुण सत्य है। अनुक्रम के प्रत्येक सेट के लिए, एक प्राकृतिक टोपोलॉजी है जो निम्नलिखित दूरी फ़ंक्शन बनाता है:

$$$s = 17, \ sqrt {2}, -2, \ pi, 10, 1/2 \\ t = 17, \ sqrt {2}, -2, e, 10, 1/$

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

आंशिक शुद्धता का अर्थ है कि कार्यक्रम तभी रुक सकता है जब वह सही उत्तर दे। यूक्लिडियन एल्गोरिथ्म की आंशिक शुद्धता कहती है कि यदि यह निष्पादन पूरा करता है, तो $$$x = जीसीडी (एम, एन)$ । और हमारा एल्गोरिथ्म निष्पादन को पूरा करता है यदि $$$x = y$ । दूसरे शब्दों में, $$$(x = y) \ Rightarrow (x = GCD (M, N))$ । इस एल्गोरिथ्म की आंशिक शुद्धता का मतलब है कि यह सूत्र व्यवहार के सभी राज्यों के लिए सही है। इसकी शुरुआत में एक प्रतीक जोड़ें $$$\ वर्ग$ जिसका अर्थ है "सभी चरणों के लिए।" जैसा कि आप देख सकते हैं, सूत्र में स्ट्रोक के साथ कोई चर नहीं हैं, इसलिए इसकी सच्चाई प्रत्येक चरण पर पहली स्थिति पर निर्भर करती है। और अगर प्रत्येक चरण के पहले राज्य के लिए कुछ सच है, तो यह कथन सभी राज्यों के लिए सही है। यूक्लिडियन एल्गोरिथ्म की आंशिक शुद्धता एल्गोरिदम के लिए स्वीकार्य किसी भी व्यवहार से संतुष्ट है। जैसा कि हमने देखा है, अगर फॉर्मूला सही है तो व्यवहार स्वीकार्य है। जब हम कहते हैं कि एक संपत्ति संतुष्ट है, तो इसका सीधा सा मतलब है कि यह संपत्ति किसी सूत्र से है। यह अद्भुत नहीं है? यहाँ यह है:

$$$Init_E \ land \ square अगला_E \ Rightarrow \ square ((x = y) \ Rightarrow (x = GCD (M, N))$

हम आक्रमण का रुख करते हैं। कोष्ठक के साथ वर्ग को इसके बाद की संपत्ति कहा जाता है:

$$$Init_E \ भूमि \ वर्ग Next_E \ Rightarrow \ color {लाल} {\ square ((x = y) \ Rightarrow (x = GCD (M, N))}$

वर्ग के बाद कोष्ठक में संलग्न मान को अपरिवर्तनीय कहा जाता है:

$$$Init_E \ land \ square अगला_E \ Rightarrow \ Square (रंग {लाल}} {(x = y) \ Rightarrow (x = GCD (M, N))})$

आक्रमणकारी कैसे साबित हों? साबित करने के लिए $$$Init_E \ land \ square Next_E \ Rightarrow \ square I_E$ , आपको किसी भी व्यवहार के लिए यह साबित करने की आवश्यकता है $$$s_1, s_2, s_3 ...$ परिणाम $$$Init_E \ land \ square Next_E$ सत्य है $$$I_e$ किसी भी हालत के लिए $$$s_j$ । हम इसे प्रेरण द्वारा सिद्ध कर सकते हैं, इसके लिए हमें निम्नलिखित सिद्ध करने की आवश्यकता है:

1. से $$$Init_E \ land \ square Next_E$ यह इस प्रकार है $$$I_e$ राज्य के लिए सच है $$$s_1$ ;
2. से $$$Init_E \ land \ square Next_E$ यह इस प्रकार है कि अगर $$$I_e$ राज्य के लिए सच है $$$s_j$ फिर यह भी
   राज्य के लिए सच है $$$s_ {j + 1}$ ।

पहले हमें यह साबित करने की जरूरत है $$$Init_E$ माध्यम $$$I_e$ । क्योंकि सूत्र दावा करता है कि $$$Init_E$ पहले राज्य के लिए सच है, इसका मतलब है कि $$$I_e$ पहले राज्य के लिए सच है। आगे, जब $$$Next_E$ किसी भी कदम के लिए सच है, और $$$I_e$ सच है $$$s_j$ । $$$I_e$ के लिए सच है $$$s_ {j + 1}$ क्योंकि $$$\ square Next_E$ इसका मतलब है कि $$$Next_E$ राज्यों के किसी भी जोड़े के लिए सच है। यह इस तरह लिखा गया है: $$$Next_E \ Land I_E \ Rightarrow मैं_E $ हू$ जहाँ $$$I'_E$ क्या वह $$$I_e$ एक स्ट्रोक के साथ सभी चर के लिए।

एक अपरिवर्तनीयता जो दो स्थितियों को पूरा करती है, जिन्हें हमने अभी साबित किया है, एक प्रेरक अपरिवर्तनीय कहा जाता है । आंशिक शुद्धता आगमनात्मक नहीं है। इसके अदर्शन को सिद्ध करने के लिए, आपको आगमनात्मक आवेश को खोजने की आवश्यकता है जो इसका तात्पर्य करता है। हमारे मामले में, आगमनात्मक आवेश इस प्रकार होगा: $$$GCD (x, y) = GCD (M, N)$ ।

एल्गोरिथ्म की प्रत्येक बाद की कार्रवाई इसकी वर्तमान स्थिति पर निर्भर करती है, और पिछले कार्यों पर नहीं। एल्गोरिथ्म सुरक्षा संपत्ति को संतुष्ट करता है, क्योंकि इसमें प्रेरक अपरिवर्तनीय संरक्षित है। यूक्लिडियन एल्गोरिथ्म सबसे बड़े सामान्य भाजक की गणना कर सकता है (यानी, यह तब तक बंद नहीं होता है जब तक कि यह पहुंच न जाए) इस तथ्य के कारण कि इसमें एक अपरिवर्तनीयता है $$$GCD (x, y) = GCD (M, N)$ । एल्गोरिथ्म को समझने के लिए, आपको इसके प्रेरक अपरिवर्तक को जानना होगा। यदि आपने कार्यक्रम सत्यापन का अध्ययन किया है, तो आप जानते हैं कि एक अपरिवर्तनीय का सिर्फ दिया गया प्रमाण अनुक्रमिक फ्लोयड-होरे कार्यक्रमों के आंशिक शुद्धता को साबित करने के तरीके से ज्यादा कुछ नहीं है। आपने होवीकी - ग्रिस विधि के बारे में भी सुना होगा, जो कि फ्लोयड-होर पद्धति के समानांतर कार्यक्रमों का विस्तार है। दोनों ही मामलों में, प्रोग्राम एनोटेशन का उपयोग करते हुए आगमनात्मक अपरिवर्तनीय लिखा जाता है। और अगर आप गणित की मदद से ऐसा करते हैं, और प्रोग्रामिंग भाषा के साथ नहीं, तो यह बहुत सरलता से किया जाता है। यह वही है जो Oviki-Gris पद्धति के केंद्र में स्थित है। गणित समझने के लिए जटिल घटनाओं को बहुत अधिक सुलभ बनाता है, हालांकि घटना स्वयं, निश्चित रूप से, कोई सरल नहीं मिलेगी।

सूत्र पर एक करीब से नज़र डालें। अगर गणित में हमने चर के साथ एक सूत्र लिखा है $$$x$ और $$$य$ , इसका मतलब यह नहीं है कि अन्य चर मौजूद नहीं हैं। आप एक और समीकरण जोड़ सकते हैं जिसमें $$$य$ के संबंध में रखा गया $$$z$ , यह कुछ भी नहीं बदलेगा। बस सूत्र किसी अन्य चर के बारे में कुछ नहीं कहता है। मैंने पहले ही कहा था कि एक राज्य चर के मानों का एक असाइनमेंट है, अब आप इसे जोड़ सकते हैं: सभी संभव चर के साथ, शुरू करना $$$x$ और $$$य$ और ईरान की जनसंख्या के साथ समाप्त हो रहा है। मुझे कबूल करना चाहिए: जब मैंने कहा कि सूत्र $$$Init_E \ land \ square Next_E$ यूक्लिडियन एल्गोरिथ्म का वर्णन करता है, मैंने झूठ बोला था। यह वास्तव में एक ब्रह्मांड का वर्णन करता है जिसमें अर्थ है $$$x$ और $$$य$ यूक्लिडियन एल्गोरिथ्म के निष्पादन का प्रतिनिधित्व करते हैं। सूत्र का दूसरा भाग ( $$$\ square Next_E$ ) का दावा है कि प्रत्येक चरण में परिवर्तन होता है $$$x$ या $$$य$ । दूसरे शब्दों में, यह एक ब्रह्मांड का वर्णन करता है जिसमें ईरान की आबादी केवल तभी बदल सकती है जब अर्थ बदल गया हो $$$x$ या $$$य$ । यह इस प्रकार है कि यूक्लिडियन एल्गोरिथ्म के निष्पादन के बाद ईरान में किसी का जन्म नहीं हो सकता है। जाहिर है, ऐसा नहीं है। यदि हमारे पास वैध कदम हैं, तो इस त्रुटि को ठीक किया जा सकता है $$$x$ और $$$य$ अपरिवर्तित रहें। इसलिए, हमें अपने सूत्र में एक और भाग जोड़ने की आवश्यकता है: $$$Init_E \ भूमि \ वर्ग (Next_E \ lor (x '= x) \ भूमि (y' = y))$ । संक्षिप्तता के लिए, हम इसे इस तरह लिखते हैं: $$$Init_E \ भूमि \ वर्ग [Next_E] _ {<x, y>}$ । यह सूत्र एक ब्रह्मांड का वर्णन करता है जिसमें यूक्लिडियन एल्गोरिथ्म है। उसी परिवर्तन को अपरिवर्तनीय के प्रमाण में किया जाना चाहिए:

• हम साबित करते हैं: $$$Init_E \ land \ color {red} {\ square [Next_E] _ {<x, y>}} \ Rightarrow \ square I_E$
• की मदद से:
  
  1. $$$Init_E \ Rightarrow I_E$
  2. $$$\ रंग {लाल} {\ वर्ग [Next_E] _ {<x, y>}} \ भूमि I_E \ Rightarrow I'm_E$

यह परिवर्तन यूक्लिडियन एल्गोरिथ्म की सुरक्षा के लिए जिम्मेदार है, क्योंकि अब व्यवहार किन मूल्यों में संभव है $$$x$ और $$$य$ मत बदलो। गतिविधि संपत्ति का उपयोग करके इन व्यवहारों को समाप्त किया जाना चाहिए। यह काफी सरल है, लेकिन मैंने अभी इसके बारे में बात नहीं की है।

कार्यान्वयन के बारे में बात करें। मान लीजिए हमारे पास किसी प्रकार की मशीन है जो कंप्यूटर की तरह यूक्लिडियन एल्गोरिथ्म को लागू करती है। यह 32-बिट शब्दों के सरणियों के रूप में संख्याओं का प्रतिनिधित्व करता है। जोड़ और घटाव के सरल संचालन के लिए, उसे कंप्यूटर की तरह कई चरणों की आवश्यकता होती है। यदि आप अभी तक गतिविधि को स्पर्श नहीं करते हैं, तो हम सूत्र द्वारा ऐसी मशीन की कल्पना भी कर सकते हैं $$$Init_ {ME} \ भूमि \ वर्ग [Next_ {ME}] _ {<...>}$ । जब हम कहते हैं कि यूक्लिडियन मशीन यूक्लिडियन एल्गोरिथ्म को लागू करती है तो हमारा क्या मतलब है? इसका मतलब है कि निम्न सूत्र सही है:

चिंता मत करो, अब हम क्रम में इसकी जांच करेंगे। यह कहता है कि हमारी मशीन कुछ संपत्ति को संतुष्ट करती है ( $$$\ Rightarrow$ )। यह संपत्ति यूक्लिडियन फार्मूला है। $$$(Init_E \ land \ Square [Next_E] _ {<x, y>}$ , डॉट्स ऐसे व्यंजक हैं जिनमें यूक्लिडियन मशीन चर हैं, और $$$के साथ$ एक प्रतिस्थापन है। दूसरे शब्दों में, दूसरी पंक्ति यूक्लिडियन सूत्र है जिसमें $$$x$ और $$$य$ डॉट्स द्वारा प्रतिस्थापित। गणित में, प्रतिस्थापन के लिए कोई सार्वभौमिक रूप से स्वीकृत संकेतन नहीं है, इसलिए मुझे स्वयं इसके साथ आना पड़ा। अनिवार्य रूप से, यूक्लिडियन सूत्र ( $$$Init_E \ भूमि \ वर्ग [Next_E] _ {<x, y>}$ ) सूत्र के लिए एक संक्षिप्त नाम है:

सूत्र को लाल हाइलाइट किया गया भाग, अनुमति देता है $$$x$ और $$$य$ में $$$(Init_E \ land \ Square [Next_E] _ {\ color {लाल} {<x, y>}}$ वैसे ही रहो।

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

इसे साबित करने के लिए, एक उपयुक्त अपरिवर्तनीय खोजना आवश्यक है $$$I_ {ME}$ यूक्लिडियन कारें। ऐसा करने के लिए, निम्नलिखित शर्तों को पूरा करना होगा:

1. $$$Init_ {ME} \ Rightarrow (Init_E, with \ thinspace x \ leftarrow ..., y \ leftarrow ...)$
2. $$$I_ {ME} \ भूमि [Next_ {ME}] _ {<...> \ Rightarrow ([Next_E] _ {<x, y>}, के साथ \ thinspace x \ leftarrow ..., y \ leftrrow। ..)$

हम अब उन पर ध्यान नहीं देंगे, बस इस तथ्य पर ध्यान दें कि ये साधारण गणितीय सूत्र हैं, हालांकि सबसे सरल नहीं हैं। अचल $$$I_ {ME}$ बताते हैं कि यूक्लिडियन मशीन यूक्लिडियन एल्गोरिथ्म को क्यों लागू करती है। कार्यान्वयन का अर्थ है चर के लिए भावों का प्रतिस्थापन। यह एक बहुत ही सामान्य गणितीय ऑपरेशन है। लेकिन कार्यक्रम में, इस तरह के एक प्रतिस्थापन प्रदर्शन नहीं किया जा सकता है। आप असाइनमेंट एक्सप्रेशन x = … में x के स्थान पर a + b स्थानापन्न नहीं कर सकते हैं x = … , ऐसे रिकॉर्ड का कोई मतलब नहीं होगा। फिर यह कैसे निर्धारित किया जाए कि एक कार्यक्रम दूसरे को लागू करता है? यदि आप केवल प्रोग्रामिंग के संदर्भ में सोचते हैं, तो यह संभव नहीं है। सबसे अच्छे मामले में, आप कुछ मुश्किल परिभाषा पा सकते हैं, लेकिन एक बेहतर तरीका यह है कि कार्यक्रमों को गणितीय सूत्रों में अनुवाद किया जाए और जो परिभाषा मैंने ऊपर दी है उसका उपयोग करें। एक कार्यक्रम को गणितीय सूत्र में अनुवाद करना कार्यक्रम को शब्दार्थ देना है। यदि यूक्लिडियन मशीन एक प्रोग्राम है, और $$$Init_ {ME} \ भूमि \ वर्ग [Next_ {ME}] _ {<...>}$ - उसके गणितीय संकेतन, फिर $$$(Init_E \ land \ square [Next_E] _ {<x, y>}, \ thinspace x \ leftarrow के साथ ..., y \ leftarrow ...)$ हमें दिखाता है कि इसका मतलब है कि "कार्यक्रम यूक्लिडियन एल्गोरिथ्म को लागू करता है।" प्रोग्रामिंग भाषाएं बहुत जटिल हैं, इसलिए गणित भाषा में कार्यक्रम का यह अनुवाद भी जटिल है, इसलिए व्यवहार में हम नहीं करते हैं। बस, प्रोग्रामिंग भाषाओं को उन पर एल्गोरिदम लिखने के लिए डिज़ाइन नहीं किया गया है। , , , : , x y , . , , , .

- : , , , . , . — . . , . , — , . :

. $$$DecrementX$ :

— $$$DecrementY$ :

, :

.

. Rosetta — , . Virtuoso. . TLA+, . , , . , (Eric Verhulst), . , TLA+, : « TLA+ . - C. TLA+ Virtuoso». . . , , , . . TLA+. , .

. Communications of the ACM ] , - Amazon . Amazon Web Services — , Amazon. , — TLA+. . -, , . , , . -, , . , — , , . -, , Amazon , . , 10% TLA+.

— Microsoft. TLA+ 2004 . 2015 TLA+, . . Amazon Web Services. Microsoft , , . : « , ». , Microsoft - . : « ». 2016-17 . TLA+, 150 , Azure ( Microsoft). Azure 2018 , , . : « , . , ». , , . - : , . , , .

, TLA+ . , TLA+, TLA+ Azure, , TLA+. , . , TLA+ , . Microsoft Cosmos DB, , . , . TLA+, , , TLA+.

TLA+ — . . TLA+ . , , . TLA+ , . : TLA+ , .

, . , , . , . Amazon Microsoft , . , .

, . — , . , Hydra 2019, 11-12 2019 -. .