Π-कैलकुलस

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

अनौपचारिक परिभाषा

π-कैलकुलस प्रक्रिया गणना के परिवार समवर्ती गणना के गुणों का वर्णन और विश्लेषण करने के लिए गणितीय औपचारिकताओं से संबंधित है। वास्तव में π-कैलकुलस, जैसे λ-कैलकुलस इतना न्यूनतम है कि इसमें आदिम जैसे संख्या, बूलियन, डेटा संरचना, चर, कार्य, या यहां तक ​​​​कि सामान्य नियंत्रण प्रवाह विवरण सम्मिलित नहीं है (जैसे, if-then-else, while).

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

π-कलन का केंद्र नाम की धारणा है। कलन की सरलता दोहरी भूमिका में निहित है जो नाम संचार चैनलों और चर के रूप में निभाते हैं।

कलन में उपलब्ध प्रक्रिया निर्माण निम्नलिखित हैं (निम्न अनुभाग में सटीक परिभाषा दी गई है):

• समवर्ती, लिखित $P\mid Q$, जहाँ $P$ और $Q$ दो प्रक्रियाएं या सूत्र समवर्ती रूप से निष्पादित होते हैं।
• संचार, जहाँ
  • इनपुट उपसर्ग $c\left(x\right).P$ एक संदेश की प्रतीक्षा करने की एक प्रक्रिया है जिसे $c$ नाम के संचार चैनल पर भेजा गया था $P$ के रूप में आगे बढ़ने से पहले प्राप्त नाम x को नाम से बाइंड करना। सामान्य रूप से यह मॉडल या तो नेटवर्क या लेबल से संचार की अपेक्षा करने वाली प्रक्रिया है c a द्वारा केवल एक बार प्रयोग करने योग्य goto c कार्यवाही।
  • आउटपुट उपसर्ग ${\overline {c}}\langle y\rangle .P$ वर्णन करता है कि नाम $y$ चैनल पर प्रसारित किया जाता है $c$ के रूप में आगे बढ़ने से पहले $P$. सामान्य रूप से, यह मॉडल या तो नेटवर्क पर एक संदेश भेज रहा है या a goto c कार्यवाही।
• प्रतिकृति, लिखित $!\,P$, जिसे एक ऐसी प्रक्रिया के रूप में देखा जा सकता है जो सदैव एक नई प्रतिलिपि बना सकती है $P$. सामान्य रूप से, यह या तो नेटवर्क सेवा या लेबल को मॉडल करता है c किसी भी संख्या की प्रतीक्षा कर रहा है goto c संचालन।
• एक नए नाम का निर्माण, लिखा हुआ $\left(\nu x\right)P$, जिसे एक नई स्थिरांक आवंटित करने वाली प्रक्रिया के रूप में देखा जा सकता है x अंदर $P$. के स्थिरांक π-calculus केवल उनके नाम से परिभाषित होते हैं और सदैव संचार चैनल होते हैं। किसी प्रक्रिया में नए नाम के सृजन को प्रतिबंध भी कहा जाता है।
• शून्य प्रक्रिया, लिखित $0$, एक ऐसी प्रक्रिया है जिसका निष्पादन पूरा हो गया है और रुक गया है।

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

एक छोटा सा उदाहरण

नीचे एक प्रक्रिया का एक छोटा उदाहरण है जिसमें तीन समानांतर घटक होते हैं। चैनल का नाम x केवल पहले दो घटकों द्वारा जाना जाता है।

${\begin{aligned}(\nu x)&\;(\;{\overline {x}}\langle z\rangle .\;0\\&\;|\;x(y).\;{\overline {y}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .0\end{aligned}}$

पहले दो घटक चैनल पर संचार करने में सक्षम हैं x, और नाम y के लिए बाध्य हो जाता है z. प्रक्रिया में अगला कदम इसलिए है

${\begin{aligned}(\nu x)&\;(\;0\\&\;|\;{\overline {z}}\langle x\rangle .\;x(y).\;0\;)\\&\;|\;z(v).\;{\overline {v}}\langle v\rangle .\;0\end{aligned}}$

ध्यान रहे कि शेष y प्रभावित नहीं होता है क्योंकि इसे आंतरिक दायरे में परिभाषित किया गया है। दूसरा और तीसरा समानांतर घटक अब चैनल नाम पर संवाद कर सकते हैं z, और नाम v के लिए बाध्य हो जाता है x. प्रक्रिया का अगला चरण अब है

${\begin{aligned}(\nu x)&\;(\;0\\&\;|\;x(y).\;0\\&\;|\;{\overline {x}}\langle x\rangle .\;0\;)\end{aligned}}$

ध्यान दें कि स्थानीय नाम के बाद से x का उत्पादन किया गया है, का क्षेत्र x तीसरे घटक को भी कवर करने के लिए बढ़ाया गया है। अंत में, चैनल x नाम भेजने के लिए इस्तेमाल किया जा सकता है x. उसके बाद सभी समवर्ती क्रियान्वित प्रक्रियाएँ रुक गई हैं

${\begin{aligned}(\nu x)&\;(\;0\\&\;|\;0\\&\;|\;0\;)\end{aligned}}$

औपचारिक परिभाषा

सिंटेक्स

चलो Χ वस्तुओं का एक सेट है जिसे नाम कहा जाता है। के लिए सार वाक्य रचना π-कलकुलस निम्नलिखित बीएनएफ व्याकरण से बनाया गया है (जहाँ x और y Χ से कोई नाम हैं):

${\begin{aligned}P,Q::=&\;x(y).P\,\,\,\,\,&{\text{Receive on channel }}x{\text{, bind the result to }}y{\text{, then run }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,&{\text{Send the value }}y{\text{ over channel }}x{\text{, then run }}P\\&\;|\;P|Q\,\,\,\,\,\,\,\,\,&{\text{Run }}P{\text{ and }}Q{\text{ simultaneously}}\\&\;|\;(\nu x)P\,\,\,&{\text{Create a new channel }}x{\text{ and run }}P\\&\;|\;!P\,\,\,&{\text{Repeatedly spawn copies of }}P\\&\;|\;0&{\text{Terminate the process}}\end{aligned}}$

नीचे दिए गए ठोस सिंटैक्स में, उपसर्ग समानांतर संरचना (|) की तुलना में अधिक कसकर बांधते हैं, और कोष्ठकों को अलग करने के लिए उपयोग किया जाता है।

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

Construct	Free names
$0$	None
${\overline {a}}\langle x\rangle .P$	a; x; all free names of P
$a(x).P$	a; free names of P except for x
$P|Q$	All free names of P and Q
$(\nu x)P$	Free names of P except for x
$!P$	All free names of P

संरचनात्मक सर्वांगसमता

न्यूनीकरण शब्दार्थ और लेबल संक्रमण शब्दार्थ दोनों का केंद्र संरचनात्मक सर्वांगसमता की धारणा है। दो प्रक्रियाएं संरचनात्मक रूप से सर्वांगसम होती हैं, यदि वे संरचना के समान हों। विशेष रूप से, समानांतर रचना विनिमेय और साहचर्य है।

अधिक सटीक रूप से, संरचनात्मक अनुरूपता को कम से कम समानता संबंध के रूप में परिभाषित किया जाता है जो प्रक्रिया के निर्माण और संतोषजनक द्वारा संरक्षित होता है:

अल्फा-रूपांतरण:

• $P\equiv Q$ यदि $Q$ से प्राप्त किया जा सकता है $P$ एक या एक से अधिक बाध्य नामों का नाम बदलकर $P$.

समानांतर रचना के लिए अभिगृहीत:

• $P|Q\equiv Q|P$
• $(P|Q)|R\equiv P|(Q|R)$
• $P|0\equiv P$

प्रतिबंध के लिए अभिगृहीत:

• $(\nu x)(\nu y)P\equiv (\nu y)(\nu x)P$
• $(\nu x)0\equiv 0$

प्रतिकृति के लिए अभिगृहीत:

• $!P\equiv P|!P$

अभिगृहीत संबंधित प्रतिबंध और समानांतर:

• $(\nu x)(P|Q)\equiv (\nu x)P|Q$ यदि x का मुक्त नाम नहीं है $Q$.

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

कमी शब्दार्थ

हम लिखते हैं $P\rightarrow P'$ यदि $P$ एक संगणना चरण कर सकता है, जिसके बाद यह अब है $P'$. यह कमी संबंध $\rightarrow$ कटौती नियमों के एक सेट के तहत कम से कम बंद संबंध के रूप में परिभाषित किया गया है।

चैनलों के माध्यम से संवाद करने के लिए प्रक्रियाओं की क्षमता को पकड़ने वाला मुख्य कमी नियम निम्नलिखित है:

• ${\overline {x}}\langle z\rangle .P|x(y).Q\rightarrow P|Q[z/y]$

जहाँ $Q[z/y]$ प्रक्रिया को दर्शाता है $Q$ जिसमें मुक्त नाम है $z$ की मुक्त घटनाओं के लिए प्रतिस्थापित किया गया है $y$. यदि एक मुक्त घटना $y$ किसी स्थान पर होता है $z$ मुक्त नहीं होगा, अल्फा-रूपांतरण की आवश्यकता हो सकती है।

तीन अतिरिक्त नियम हैं:

• यदि $P\rightarrow Q$ तब भी $P|R\rightarrow Q|R$.

यह नियम कहता है कि समानांतर रचना गणना को बाधित नहीं करती है।

• यदि $P\rightarrow Q$, तब भी $(\nu x)P\rightarrow (\nu x)Q$.

यह नियम सुनिश्चित करता है कि गणना एक प्रतिबंध के तहत आगे बढ़ सकती है।

• यदि $P\equiv P'$ और $P'\rightarrow Q'$ और $Q'\equiv Q$, तब भी $P\rightarrow Q$.

बाद के नियम में कहा गया है कि संरचनात्मक रूप से संगत प्रक्रियाओं में समान कटौती होती है।

उदाहरण पर दोबारा गौर किया गया

प्रक्रिया पर फिर से विचार करें

$(\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0$

कमी के शब्दार्थ की परिभाषा को लागू करते हुए, हम कमी प्राप्त करते हैं

$(\nu x)({\overline {x}}\langle z\rangle .0|x(y).{\overline {y}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0$

ध्यान दें कि कैसे, कमी प्रतिस्थापन स्वयंसिद्ध को लागू करते हुए, की मुक्त घटनाएँ $y$ अब के रूप में लेबल किए गए हैं $z$.

अगला, हम कमी प्राप्त करते हैं

$(\nu x)(0|{\overline {z}}\langle x\rangle .x(y).0)|z(v).{\overline {v}}\langle v\rangle .0\rightarrow (\nu x)(0|x(y).0|{\overline {x}}\langle x\rangle .0)$

ध्यान दें कि स्थानीय नाम के बाद से x का उत्पादन किया गया है, का क्षेत्र x तीसरे घटक को भी कवर करने के लिए बढ़ाया गया है। इसे स्कोप एक्सटेंशन स्वयंसिद्ध का उपयोग करके कैप्चर किया गया था।

अगला, कमी प्रतिस्थापन स्वयंसिद्ध का उपयोग करके, हम प्राप्त करते हैं

$(\nu x)(0|0|0)$

अंत में, समांतर संरचना और प्रतिबंध के लिए सिद्धांतों का उपयोग करके, हम प्राप्त करते हैं

$0$

लेबल किए गए शब्दार्थ

वैकल्पिक रूप से, कोई पीआई-कैलकुलस को एक लेबल ट्रांज़िशन सिमेंटिक्स दे सकता है (संचार प्रणालियों की गणना के कैलकुलस के साथ किया गया है)।
इस शब्दार्थ में एक राज्य से एक संक्रमण $P$ किसी अन्य राज्य के लिए $P'$ एक क्रिया के बाद $\alpha$ के रूप में नोट किया गया है:

• $P\,\xrightarrow {\overset {}{\alpha }} P'$

जहां राज्यों $P$ और $P'$ प्रक्रियाओं का प्रतिनिधित्व करते हैं और $\alpha$ या तो एक इनपुट क्रिया है $a(x)$, एक आउटपुट क्रिया${\overline {a}}\langle x\rangle$, या एक मौन क्रिया τ.

लेबल किए गए शब्दार्थ के बारे में एक मानक परिणाम यह है कि यह संरचनात्मक अनुरूपता तक कमी शब्दार्थ से सहमत है, इस अर्थ में कि

$P\rightarrow P'$ यदि और केवल यदि
$P\,\xrightarrow {\overset {}{\tau }} \equiv P'$ 

एक्सटेंशन और वेरिएंट

ऊपर दिया गया सिंटैक्स न्यूनतम है। जबकि वाक्य रचना को विभिन्न तरीकों से संशोधित किया जा सकता है।

एक गैर-नियतात्मक पसंद ऑपरेटर $P+Q$ सिंटैक्स में जोड़ा जा सकता है।

नाम समानता के लिए एक परीक्षण $[x=y]P$ सिंटैक्स में जोड़ा जा सकता है। यह मैच ऑपरेटर आगे बढ़ सकता है $P$ यदि और केवल यदि x और $y$ एक ही नाम हैं। इसी तरह, कोई 'नाम असमानता' के लिए बेमेल संकारक जोड़ सकता है। प्रैक्टिकल प्रोग्राम जो नाम (यूआरएल या पॉइंटर्स) पास कर सकते हैं, अधिकतर ऐसी कार्यक्षमता का उपयोग करते हैं: कलन के अंदर ऐसी कार्यक्षमता को सीधे मॉडलिंग करने के लिए, यह और संबंधित एक्सटेंशन अधिकतर उपयोगी होते हैं।

अतुल्यकालिक π-कलन बिना किसी प्रत्यय के केवल आउटपुट की अनुमति देता है, अर्थात फॉर्म के आउटपुट परमाणु ${\overline {x}}\langle y\rangle$, एक छोटे कलन की उपज। जबकि, मूल कलन में किसी भी प्रक्रिया को छोटे अतुल्यकालिक द्वारा दर्शाया जा सकता है π-प्राप्त करने की प्रक्रिया से स्पष्ट पावती का अनुकरण करने के लिए एक अतिरिक्त चैनल का उपयोग करके कैलकुलस। चूंकि एक निरंतरता-मुक्त आउटपुट एक संदेश-इन-ट्रांजिट को मॉडल कर सकता है, यह टुकड़ा दिखाता है कि मूल π-कलकुलस, जो सहजता से सिंक्रोनस कम्युनिकेशन पर आधारित है, इसके सिंटैक्स के अंदर एक अभिव्यंजक एसिंक्रोनस कम्युनिकेशन मॉडल है। जबकि, ऊपर परिभाषित गैर-नियतात्मक पसंद ऑपरेटर को इस तरह से व्यक्त नहीं किया जा सकता है, क्योंकि एक गार्ड (कंप्यूटर विज्ञान) पसंद को एक संरक्षित विकल्प में बदल दिया जाएगा; इस तथ्य का उपयोग यह प्रदर्शित करने के लिए किया गया है कि एसिंक्रोनस कैलकुलस सिंक्रोनस (विकल्प ऑपरेटर के साथ) की तुलना में सख्ती से कम अभिव्यंजक है।

बहुविकल्पी π-कलकुलस एक ही क्रिया में एक से अधिक नामों को संप्रेषित करने की अनुमति देता है: ${\overline {x}}\langle z_{1},...,z_{n}\rangle .P$ (पॉलीडिक आउटपुट) और $x(z_{1},...,z_{n}).P$ (पॉलीडिक इनपुट)। यह पॉलीऐडिक विस्तार, जो विशेष रूप से नाम पासिंग प्रक्रियाओं के प्रकारों का अध्ययन करते समय उपयोगी होता है, एक निजी चैनल के नाम को पास करके मोनैडिक कैलकुस में एन्कोड किया जा सकता है जिसके माध्यम से कई तर्क अनुक्रम में पारित किए जाते हैं। एन्कोडिंग को खंडों द्वारा पुनरावर्ती रूप से परिभाषित किया गया है

${\overline {x}}\langle y_{1},\cdots ,y_{n}\rangle .P$ के रूप में एन्कोड किया गया है $(\nu w){\overline {x}}\langle w\rangle .{\overline {w}}\langle y_{1}\rangle .\cdots .{\overline {w}}\langle y_{n}\rangle .[P]$

$x(y_{1},\cdots ,y_{n}).P$ के रूप में एन्कोड किया गया है $x(w).w(y_{1}).\cdots .w(y_{n}).[P]$

अन्य सभी प्रक्रिया निर्माणों को एन्कोडिंग द्वारा अपरिवर्तित छोड़ दिया जाता है।

ऊपरोक्त में, $[P]$ निरंतरता में सभी उपसर्गों के एन्कोडिंग को दर्शाता है $P$ उसी तरह से।

प्रतिकृति की पूरी शक्ति $!P$ आवश्यकता नहीं है। अधिकतर, कोई केवल प्रतिरूपित इनपुट पर विचार करता है $!x(y).P$, जिसकी संरचनात्मक सर्वांगसमता अभिगृहीत है $!x(y).P\equiv x(y).P|!x(y).P$.

प्रतिकृति इनपुट प्रक्रिया जैसे $!x(y).P$ सर्वर के रूप में समझा जा सकता है, चैनल पर प्रतीक्षा कर रहा है x ग्राहकों द्वारा आह्वान किया जाना है। एक सर्वर का आह्वान इसकी एक नई प्रति उत्पन्न करता है प्रक्रिया $P[a/y]$, जहां a क्लाइंट द्वारा दिया गया नाम है सर्वर, बाद के आह्वान के दौरान।

एक उच्च क्रम π-कैलकुलस को परिभाषित किया जा सकता है जहां न केवल नाम बल्कि प्रक्रियाओं को चैनलों के माध्यम से भेजा जाता है। उच्च क्रम के मामले के लिए महत्वपूर्ण कमी नियम है

${\overline {x}}\langle R\rangle .P|x(Y).Q\rightarrow P|Q[R/Y]$

यहाँ, $Y$ एक प्रक्रिया चर को दर्शाता है जिसे एक प्रक्रिया अवधि द्वारा त्वरित किया जा सकता है। सानगिओर्गी स्थापित किया है कि प्रक्रियाओं को पारित करने की क्षमता नहीं है की अभिव्यक्ति में वृद्धि π-कैलकुलस: एक प्रक्रिया को पास करना P हो सकता है इसके बजाय P को इंगित करने वाले नाम को पास करके सिम्युलेटेड।

गुण

=== ट्यूरिंग पूर्णता === {{pi}pi}}-कलन एक ट्यूरिंग पूर्ण है। इसे पहली बार रॉबिन मिलनर ने अपने पेपर फंक्शन्स ऐज़ प्रोसेसेस में देखा था। जिसमें वह लैम्ब्डा-पथरी के दो एनकोडिंग प्रस्तुत करता है π-कलन। एक एन्कोडिंग उत्सुक (कॉल-बाय-वैल्यू) मूल्यांकन रणनीति का अनुकरण करती है, अन्य एन्कोडिंग सामान्य-ऑर्डर (कॉल-बाय-नेम) रणनीति का अनुकरण करती है। इन दोनों में, महत्वपूर्ण अंतर्दृष्टि पर्यावरण बाइंडिंग का मॉडलिंग है - उदाहरण के लिए,x अवधि के लिए बाध्य है ${\textstyle M}$- प्रतिकृति एजेंटों के रूप में जो शब्द के लिए एक कनेक्शन वापस भेजकर अपनी बाइंडिंग के अनुरोधों का जवाब देते हैं $M$.

की विशेषताएं π-कैलकुलस जो इन एनकोडिंग को संभव बनाते हैं वे नाम-पासिंग और प्रतिकृति (या, समतुल्य, पुनरावर्ती रूप से परिभाषित एजेंट) हैं। प्रतिकृति/पुनरावृत्ति के अभाव में, π-कैलकुलस ट्यूरिंग-पूर्ण होना बंद कर देता है। यह इस तथ्य से देखा जा सकता है कि पुनरावर्तन-मुक्त कैलकुलस और यहां तक ​​कि परिमित-नियंत्रण के लिए bisimulation तुल्यता निर्णायक हो जाती है π-कैलकुलस जहां किसी भी प्रक्रिया में समानांतर घटकों की संख्या एक स्थिरांक से बंधी होती है।

में बाईसिमुलेशन π-कलन

See also: Bisimulation

प्रक्रिया गणना के लिए, π-कैलकुलस बाईसिमुलेशन तुल्यता की परिभाषा की अनुमति देता है। में π-कैलकुलस, बाईसिमुलेशन समतुल्यता की परिभाषा (जिसे बाईसिमिलैरिटी के रूप में भी जाना जाता है) या तो कमी शब्दार्थ या लेबल संक्रमण शब्दार्थ पर आधारित हो सकती है।

में लेबल किए गए बाईसिमुलेशन समकक्ष को परिभाषित करने के (कम से कम) तीन अलग-अलग तरीके हैं π-कैलकुलस: अर्ली, लेट और ओपन बाइसिमिलरिटी। यह इस तथ्य से उपजा है कि π-कैलकुलस एक वैल्यू-पासिंग प्रोसेस कैलकुलस है।

इस भाग के शेष भाग में, हम जाने देते हैं $p$ और $q$ प्रक्रियाओं को निरूपित करें और $R$ प्रक्रियाओं पर द्विआधारी संबंधों को निरूपित करें।

प्रारंभिक और देर से समानता

मिलनर, पैरो और वाकर ने प्रारंभिक और बाद की समानता दोनों को अपने मूल पेपर में तैयार किया था π-कलन। एक द्विआधारी संबंध $R$ प्रक्रियाओं की प्रत्येक जोड़ी के लिए प्रक्रियाओं पर एक प्रारंभिक बाईसिमुलेशन है $(p,q)\in R$,

• जब कभी भी $p\,\xrightarrow {a(x)} \,p'$ फिर प्रत्येक नाम के लिए $y$ कुछ उपस्थित है $q'$ ऐसा है कि $q\,\xrightarrow {a(x)} \,q'$ और $(p'[y/x],q'[y/x])\in R$;
• किसी भी गैर-इनपुट कार्रवाई के लिए $\alpha$, यदि ${p\xrightarrow {\overset {}{\alpha }} p'}$ तो कुछ उपस्थित है $q'$ ऐसा है कि $q\xrightarrow {\overset {}{\alpha }} q'$ और $(p',q')\in R$;
• और सममित आवश्यकताओं के साथ $p$ और $q$ अदला-बदली।

प्रक्रियाओं $p$ और $q$ प्रारंभिक बाईसिमिलर, लिखित कहा जाता है $p\sim _{e}q$ यदि जोड़ी $(p,q)\in R$ कुछ शुरुआती बाईसिमुलेशन के लिए $R$.

देर से द्वि-समानता में, संक्रमण मिलान संचरित होने वाले नाम से स्वतंत्र होना चाहिए। एक द्विआधारी संबंध $R$ प्रक्रियाओं की प्रत्येक जोड़ी के लिए ओवर प्रोसेस एक लेट बाईसिमुलेशन है $(p,q)\in R$,

• जब कभी भी $p\xrightarrow {a(x)} p'$ फिर कुछ के लिए $q'$ यह मानता है $q\xrightarrow {a(x)} q'$ और $(p'[y/x],q'[y/x])\in R$ प्रत्येक नाम वाई के लिए;
• किसी भी गैर-इनपुट कार्रवाई के लिए $\alpha$, यदि $p\xrightarrow {\overset {}{\alpha }} p'$ तात्पर्य है कि कुछ उपस्थित है $q'$ ऐसा है कि $q\xrightarrow {\overset {}{\alpha }} q'$और $(p',q')\in R$;
• और सममित आवश्यकताओं के साथ $p$ और $q$ अदला-बदली।

प्रक्रियाओं $p$ और $q$ परवर्ती बाईस्मिलर, लिखित कहे जाते हैं $p\sim _{l}q$ यदि जोड़ी $(p,q)\in R$ कुछ देर के बाईसिमुलेशन के लिए $R$.

दोनों $\sim _{e}$ और $\sim _{l}$ समस्या से ग्रस्त हैं कि वे इस अर्थ में सर्वांगसम संबंध नहीं हैं कि वे सभी प्रक्रिया निर्माणों द्वारा संरक्षित नहीं हैं। अधिक सटीक रूप से, प्रक्रियाएं उपस्थित हैं $p$ और $q$ ऐसा है कि $p\sim _{e}q$ लेकिन $a(x).p\not \sim _{e}a(x).q$. इसमें सम्मिलित अधिकतम सर्वांगसमता संबंधों पर विचार करके कोई भी इस समस्या का समाधान कर सकता है $\sim _{e}$ और $\sim _{l}$, क्रमशः प्रारंभिक सर्वांगसमता और देर से सर्वांगसमता के रूप में जाना जाता है।

मुक्त द्विसमानता

सौभाग्य से, एक तीसरी परिभाषा संभव है, जो इस समस्या से बचती है, अर्थात् सांगियोर्गी के कारण मुक्त द्विसमानता।

एक द्विआधारी संबंध $R$ प्रत्येक जोड़ी तत्वों के लिए ओवर प्रोसेस एक ओपन बाईसिमुलेशन है $(p,q)\in R$ और प्रत्येक नाम प्रतिस्थापन के लिए $\sigma$ और प्रत्येक क्रिया $\alpha$, जब कभी भी $p\sigma \xrightarrow {\overset {}{\alpha }} p'$ तो कुछ उपस्थित है $q'$ ऐसा है कि $q\sigma \xrightarrow {\overset {}{\alpha }} q'$ और $(p',q')\in R$.

प्रक्रियाओं $p$ और $q$ खुले बाईसिमिलर, लिखित कहे जाते हैं $p\sim _{o}q$ यदि जोड़ी $(p,q)\in R$ कुछ खुले बाईसिमुलेशन के लिए $R$.

प्रारंभिक, देर और मुक्त द्विसमानता भिन्न-भिन्न होती है

प्रारंभिक, देर और खुली बाईस्मिलैरिटी अलग-अलग हैं। रोकथाम उचित हैं, इसलिए $\sim _{o}\subsetneq \sim _{l}\subsetneq \sim _{e}$.

कुछ उप-गणनाओं में जैसे कि अतुल्यकालिक पाई-कैलकुलस, देर से, प्रारंभिक और खुली बाईस्मिलैरिटी को मेल खाने के लिए जाना जाता है। जबकि, इस सेटिंग में एक अधिक उपयुक्त धारणा अतुल्यकालिक बाईसिमिलरिटी की है।

साहित्य में, ओपन बाईसिम्यूलेशन शब्द सामान्य रूप से एक अधिक परिष्कृत धारणा को संदर्भित करता है, जहां प्रक्रियाओं और संबंधों को विशिष्ट संबंधों द्वारा अनुक्रमित किया जाता है; विवरण ऊपर उद्धृत सांगियोर्गी के पेपर में हैं।

बारबेड तुल्यता

वैकल्पिक रूप से कोई व्यक्ति सिमेंटिक्स को कम करने से सीधे बाईसिम्यूलेशन समकक्ष को परिभाषित कर सकता है। हम लिखते हैं $p\Downarrow a$ यदि प्रक्रिया $p$ नाम पर तुरंत इनपुट या आउटपुट $a$ की अनुमति देता है एवं

द्विआधारी संबंध $R$ प्रक्रियाओं पर बारबेड बाईसिमुलेशन है यदि यह एक सममित संबंध है जो संतुष्ट करता है कि तत्वों की प्रत्येक जोड़ी के लिए $(p,q)\in R$ हमारे पास वह है

(1) $p\Downarrow a$ यदि और केवल यदि $q\Downarrow a$ प्रत्येक नाम के लिए $a$

और

(2) प्रत्येक कमी के लिए $p\rightarrow p'$ कमी होती है $q\rightarrow q'$

ऐसा है कि $(p',q')\in R$.

हम कहते हैं $p$ और $q$ कंटीले बाईस्मिलर हैं यदि कांटेदार बाईसिमुलेशन उपस्थित है $R$ जहाँ $(p,q)\in R$.

एक संदर्भ को एक के रूप में परिभाषित करना π छेद वाला शब्द [] हम कहते हैं कि दो प्रक्रियाएँ P और Q कांटेदार सर्वांगसम हैं, लिखी गई हैं $P\sim _{b}Q\,\!$, यदि प्रत्येक संदर्भ के लिए $C[]$ हमारे पास वह है $C[P]$ और $C[Q]$ कांटेदार बाईस्मिलर हैं। यह पता चला है कि कांटेदार सर्वांगसमता प्रारंभिक बाईसिमिलरिटी द्वारा प्रेरित सर्वांगसमता के साथ मेल खाती है।

अनुप्रयोग

π-कैलकुलस का उपयोग कई अलग-अलग प्रकार की समवर्ती प्रणालियों का वर्णन करने के लिए किया गया है। वास्तव में कुछ नवीनतम अनुप्रयोग पारंपरिक कंप्यूटर विज्ञान के क्षेत्र से बाप्रत्येक हैं।

सन 1997 में मार्टिन अबादी और एंड्रयू गॉर्डन ने π-कैलकुलस का विस्तार क्रिप्टोग्राफ़िक प्रोटोकॉल के बारे में वर्णन करने और तर्क करने के लिए एक औपचारिक संकेतन के रूप में स्पाइ-कैलकुलस प्रस्तावित किया। स्पाइ-कैलकुलस, π-एन्क्रिप्शन और डिक्रिप्शन के लिए आदिम के साथ कलन का विस्तार होता है। सन 2001 में मार्टिन अबादी और सेड्रिक फोरनेट ने क्रिप्टोग्राफ़िक प्रोटोकॉल के संचालन को लागू करने के लिए π कलन सामान्यीकृत किया। लागू किए गए वेरिएंट के लिए समर्पित काम का एक बड़ा भाग अब π कलन है जिसमें कई प्रयोगात्मक सत्यापन उपकरण सम्मिलित हैं। एक उदाहरण उपकरण ProVerif [2] है जो ब्रूनो ब्लैंचेट के कारण लागू किए गए अनुवाद पर आधारित है। ब्लैंचेट के लॉजिक प्रोग्रामिंग फ्रेमवर्क में π-कैलकुलस एक अन्य उदाहरण क्रिप्टिक [3] है, एंड्रयू गॉर्डन और एलन जेफरी के कारण जो टाइप सिस्टम के आधार के रूप में वू और लैम के पत्राचार अभिकथन की विधि का उपयोग करता है जो क्रिप्टोग्राफ़िक प्रोटोकॉल के प्रमाणीकरण गुणों की जांच कर सकता है।

सन 2002 के आसपास हॉवर्ड स्मिथ और पीटर फ़िंगर की इसमें रुचि हो गई π-कैलकुलस मॉडलिंग व्यवसाय प्रक्रियाओं के लिए एक विवरण उपकरण बन जाएगा। जुलाई 2006 तक समुदाय में चर्चा हो रही है कि यह कितना उपयोगी होगा। हाल ही में π-कैलकुलस ने बिजनेस प्रोसेस मॉडलिंग लैंग्वेज (BPML) और माइक्रोसॉफ्ट के XLANG के सैद्धांतिक आधार का गठन किया है।

π-कैलकुलस ने आणविक जीव विज्ञान में भी रुचि को आकर्षित किया है। सन 1999 में अवीव रेगेव और एहुद शापिरो ने दिखाया कि एक सेलुलर सिग्नलिंग मार्ग (तथाकथित रिसेप्टर टाइरोसिन किनसे / एमएपीके कैस्केड) और विशेष रूप से आणविक "लेगो" का वर्णन कर सकता है जो π-कैलकुलस के विस्तार में संचार के इन कार्यों को लागू करता है। इस मौलिक पत्र के पश्चात अन्य लेखकों ने न्यूनतम सेल के पूरे चयापचय नेटवर्क का वर्णन किया। सन 2009 में एंथनी नैश और सारा कलवाला ने सिग्नल ट्रांसडक्शन को मॉडल करने के लिए एक π-कैलकुलस फ्रेमवर्क का प्रस्ताव दिया जो डिक्टियोस्टेलियम डिस्कोइडम एग्रीगेशन को निर्देशित करता है।

इतिहास

कैलकुलस मूल रूप से सन 1992 में रॉबिन मिलनर जोआचिम पैरो और डेविड वॉकर द्वारा विकसित किया गया था जो उफ्फे एंगबर्ग और मोगेंस नीलसन के विचारों पर आधारित था। इसे प्रोसेस कैलकुलस सीसीएस (संचार प्रणालियों की गणना) पर मिलनर के काम की निरंतरता के रूप में देखा जा सकता है। अपने ट्यूरिंग व्याख्यान में मिल्नर के विकास का वर्णन π-कैलकुलस अभिनेताओं में मूल्यों और प्रक्रियाओं की एकरूपता को पकड़ने के प्रयास के रूप में करता है।

कार्यान्वयन

निम्नलिखित प्रोग्रामिंग भाषाएँ π-कैलकुलस या इसका एक प्रकार कार्यान्वयन करती हैं:

• बिजनेस प्रोसेस मॉडलिंग लैंग्वेज (बीपीएमएल)
• ओकम-π
• चित्र प्रोग्रामिंग भाषा
• जोकैमल (जोड़-पथरी पर आधारित)
• रोलैंग

संदर्भ

• Milner, Robin (1999). Communicating and Mobile Systems: The π-calculus. Cambridge, UK: Cambridge University Press. ISBN 0-521-65869-1.
• Milner, Robin (1993). "The Polyadic π-Calculus: A Tutorial". In F. L. Hamer; W. Brauer; H. Schwichtenberg (eds.). Logic and Algebra of Specification. Springer-Verlag.
• Sangiorgi, Davide; Walker, David (2001). The π-calculus: A Theory of Mobile Processes. Cambridge, UK: Cambridge University Press. ISBN 0-521-78177-9.