حساب التفاضل والتكامل π

يُعد مفهوم الاسم جوهرياً في حساب باي . وتكمن بساطة هذا الحساب في الدور المزدوج الذي تلعبه الأسماء كقنوات اتصال ومتغيرات .

تتضمن بنى العمليات المتاحة في حساب التفاضل والتكامل ما يلي ^{[ 3 ]} (يرد تعريف دقيق في القسم التالي):

• التزامن ، مكتوب${\displaystyle P\mid Q}$، أين${\displaystyle P}$و${\displaystyle Q}$هما عمليتان أو خيطان يتم تنفيذهما في وقت واحد.
• التواصل ، حيث
  • بادئة الإدخال${\displaystyle c\left(x\right).P}$هي عملية تنتظر رسالة تم إرسالها عبر قناة اتصال تسمى${\displaystyle c}$قبل المتابعة كـ${\displaystyle P}$، وربط الاسم المستلم بالاسم x . عادةً ما يمثل هذا إما عملية تتوقع اتصالاً من الشبكة أو تسمية cقابلة للاستخدام مرة واحدة فقط بواسطة goto cعملية ما.
  • بادئة الإخراج${\displaystyle {\overline {c}}\langle y\rangle .P}$يصف ذلك الاسم${\displaystyle y}$يتم بثها على القناة${\displaystyle c}$قبل المتابعة كـ${\displaystyle P}$عادةً ، يمثل هذا إما إرسال رسالة على الشبكة أو goto cعملية ما.
• النسخ ، مكتوب${\displaystyle$ !\,P} ، والتي يمكن اعتبارها عملية يمكنها دائمًا إنشاء نسخة جديدة من${\displaystyle P}$عادةً ما يقوم هذا النموذج إما بنمذجة خدمة الشبكة أو علامة cتنتظر أي عدد من goto cالعمليات.
• إنشاء اسم جديد ، مكتوب${\displaystyle \left(\nu x\right)P}$، والتي يمكن اعتبارها عملية تخصيص ثابت جديد x داخل${\displaystyle P}$تُعرَّف ثوابت حساب التفاضل والتكامل π بأسمائها فقط، وهي دائمًا قنوات اتصال. ويُطلق على إنشاء اسم جديد في عملية ما اسم التقييد .
• العملية الصفرية، مكتوبة${\displaystyle 0}$، هي عملية اكتمل تنفيذها وتوقفت.

على الرغم من أن بساطة حساب باي (π -calculus) تمنعنا من كتابة البرامج بالمعنى المعتاد، إلا أنه من السهل توسيع هذا الحساب. فعلى وجه الخصوص، يسهل تعريف كل من هياكل التحكم مثل الاستدعاء الذاتي، والحلقات، والتركيب التسلسلي، وأنواع البيانات مثل الدوال من الدرجة الأولى، وقيم الصواب ، والقوائم، والأعداد الصحيحة. علاوة على ذلك، تم اقتراح امتدادات لحساب باي تأخذ في الاعتبار التشفير بالمفتاح العام أو التشفير بالتوزيع . وقد طُبِّق حساب باي على يد عبادي وفورنيه .وضع هذه الامتدادات المختلفة على أساس رسمي من خلال توسيع حساب التفاضل والتكامل π بأنواع بيانات عشوائية.

فيما يلي مثال بسيط لعملية تتكون من ثلاثة مكونات متوازية. اسم القناة x معروف فقط من خلال المكونين الأولين.

${\displaystyle {\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 . وبالتالي، فإن الخطوة التالية في العملية هي

${\displaystyle {\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 . الخطوة التالية في العملية هي الآن

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

لاحظ أنه بما أن الاسم المحلي x قد تم إخراجه، فإن نطاق x يتوسع ليشمل المكون الثالث أيضًا. أخيرًا، يمكن استخدام القناة x لإرسال الاسم x . بعد ذلك، تتوقف جميع العمليات المتزامنة.

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

ليكن Χ مجموعة من الكائنات تسمى أسماء . يتم بناء الصيغة المجردة لحساب π من قواعد BNF التالية (حيث x و y هما أي اسمين من Χ): ^{[ 4 ]}

${\displaystyle {\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}}}$

في التركيب النحوي الملموس أدناه، ترتبط البادئات بشكل أكثر إحكامًا من التركيب المتوازي (|)، ويتم استخدام الأقواس لإزالة الغموض.

تُقيَّد الأسماء ببنية التقييد وبادئة الإدخال. رسميًا، تُعرَّف مجموعة الأسماء الحرة لعملية ما في حساب التفاضل والتكامل π استقرائيًا بالجدول أدناه. أما مجموعة الأسماء المقيدة لعملية ما، فتُعرَّف بأنها أسماء تلك العملية التي لا تندرج ضمن مجموعة الأسماء الحرة.

بناء	أسماء حرة
${\displaystyle x(y).P}$	x ؛ أسماء حرة لـ P باستثناء y
${\displaystyle {\overline {x}}\langle y\rangle .P}$	x ؛ y ؛ جميع الأسماء الحرة لـ P
${\displaystyle P|Q}$	جميع الأسماء المجانية لـ P و Q
${\displaystyle (\nu x)P}$	أسماء حرة لـ P باستثناء x
${\displaystyle !P}$	جميع الأسماء المجانية لـ P
${\displaystyle 0}$	لا أحد

يُعد مفهوم التطابق البنيوي أساسيًا لكلٍ من دلالات الاختزال ودلالات الانتقال الموسومة . وتكون عمليتان متطابقتين بنيويًا إذا كانتا متطابقتين تمامًا من حيث البنية. وعلى وجه الخصوص، فإن التركيب المتوازي تبادلي وتجميعي.

وبشكل أدق، يُعرَّف التوافق الهيكلي بأنه أقل علاقة تكافؤ تحافظ عليها بنى العملية وتفي بما يلي:

التحويل ألفا :

• ${\displaystyle P\equiv Q}$لو${\displaystyle Q}$يمكن الحصول عليها من${\displaystyle P}$عن طريق إعادة تسمية اسم واحد أو أكثر من الأسماء المرتبطة في${\displaystyle P}$.

بديهيات التركيب المتوازي :

• ${\displaystyle P|Q\equiv Q|P}$
• ${\displaystyle (P|Q)|R\equiv P|(Q|R)}$
• ${\displaystyle P|0\equiv P}$

بديهيات التقييد :

• ${\displaystyle (\nu x)(\nu y)P\equiv (\nu y)(\nu x)P}$
• ${\displaystyle (\nu x)0\equiv 0}$

مبدأ التكرار :

• ${\displaystyle !P\equiv P|!P}$

البديهية المتعلقة بالتقييد والتوازي :

• ${\displaystyle (\nu x)(P|Q)\equiv (\nu x)P|Q}$إذا لم يكن x اسمًا حرًا لـ${\displaystyle Q}$.

تُعرف هذه البديهية الأخيرة باسم بديهية "توسيع النطاق". وتُعد هذه البديهية أساسية، لأنها تصف كيف يمكن توسيع نطاق اسم مرتبط x بواسطة عملية إخراج، مما يؤدي إلى توسيع نطاق x . في الحالات التي يكون فيها x اسمًا حرًا${\displaystyle Q}$، يمكن استخدام التحويل ألفا للسماح باستمرار عملية التمديد.

نكتب${\displaystyle P\rightarrow P'}$لو${\displaystyle P}$يمكنه تنفيذ خطوة حسابية، وبعد ذلك يصبح الآن${\displaystyle P'}$علاقة التخفيض هذه${\displaystyle \rightarrow }$يُعرَّف بأنه العلاقة الأقل إغلاقًا في ظل مجموعة من قواعد الاختزال.

تتمثل قاعدة الاختزال الرئيسية التي تُجسد قدرة العمليات على التواصل عبر القنوات فيما يلي:

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

أين${\displaystyle Q[z/y]}$يشير إلى العملية${\displaystyle Q}$الاسم الحر${\displaystyle z}$تم استبدالها بالظهورات الحرة لـ${\displaystyle y}$إذا حدث حدوث حر لـ${\displaystyle y}$يحدث في مكان حيث${\displaystyle z}$لن يكون مجانيًا، وقد يتطلب الأمر تحويلًا ألفا.

هناك ثلاث قواعد إضافية:

• لو${\displaystyle P\rightarrow Q}$ثم أيضًا${\displaystyle P|R\rightarrow Q|R}$.

تنص هذه القاعدة على أن التركيب المتوازي لا يعيق الحساب.

• لو${\displaystyle P\rightarrow Q}$ثم أيضًا${\displaystyle (\nu x)P\rightarrow (\nu x)Q}$.

تضمن هذه القاعدة إمكانية إجراء العمليات الحسابية في ظل وجود قيد.

• لو${\displaystyle P\equiv P'}$و${\displaystyle P'\rightarrow Q'}$و${\displaystyle Q'\equiv Q}$ثم أيضًا${\displaystyle P\rightarrow Q}$.

وتنص القاعدة الأخيرة على أن العمليات المتطابقة هيكلياً لها نفس الاختزالات.

أعد النظر في العملية

${\displaystyle (\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}$

بتطبيق تعريف دلالات الاختزال، نحصل على الاختزال

${\displaystyle (\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}$

لاحظ كيف أنه بتطبيق بديهية الاستبدال بالاختزال، فإن التكرارات الحرة لـ${\displaystyle y}$تُصنف الآن على أنها${\displaystyle z}$.

ثم نحصل على التخفيض

${\displaystyle (\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 قد امتد ليشمل المكون الثالث أيضًا. وقد تم توثيق ذلك باستخدام بديهية توسيع النطاق.

بعد ذلك، باستخدام بديهية الاستبدال بالاختزال، نحصل على

${\displaystyle (\nu x)(0|0|0)}$

وأخيرًا، باستخدام بديهيات التركيب المتوازي والتقييد، نحصل على

${\displaystyle 0}$

بدلاً من ذلك، يمكن إعطاء حساب باي دلالات انتقال مُصنَّفة (كما هو الحال مع حساب الأنظمة المتصلة ). في هذه الدلالات، يكون الانتقال من حالة${\displaystyle P}$إلى ولاية أخرى${\displaystyle P'}$بعد إجراء ما${\displaystyle \alpha }$يُشار إليه على النحو التالي:

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

الولايات${\displaystyle P}$و${\displaystyle P'}$تمثل العمليات و${\displaystyle \alpha }$إما أن يكون إجراء إدخال${\displaystyle a(x)}$، إجراء إخراج${\displaystyle {\overline {a}}\langle x\rangle }$أو فعل صامت τ . ^{[ 5 ]}

تتمثل إحدى النتائج القياسية المتعلقة بالدلالات المصنفة في أنها تتفق مع دلالات الاختزال حتى التطابق البنيوي، بمعنى أن ${\displaystyle P\rightarrow P'}$إذا وفقط إذا${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$^{[ 6 ]}

يُعدّ حساب باي نموذجًا عالميًا للحساب . وقد لاحظ ميلنر ذلك لأول مرة في بحثه "الدوال كعمليات" ^{[ 10 ]} ، حيث قدّم فيه ترميزين لحساب لامدا ضمن حساب باي . يحاكي أحد الترميزين استراتيجية التقييم الفوري (الاستدعاء بالقيمة) ، بينما يحاكي الآخر استراتيجية التقييم بالترتيب العادي (الاستدعاء بالاسم). في كليهما، تكمن الفكرة الأساسية في نمذجة ارتباطات البيئة - على سبيل المثال، " x مرتبط بالمصطلح" .${\textstyle M}$"– كوكلاء نسخ يستجيبون لطلبات روابطهم عن طريق إرسال اتصال بالمصطلح${\displaystyle M}$.

تتمثل خصائص حساب باي التي تجعل هذه الترميزات ممكنة في تمرير الأسماء والتكرار (أو، بشكل مكافئ، العوامل المعرفة بشكل تكراري). في غياب التكرار/التكرار، يتوقف حساب باي عن كونه كاملاً تورينج. ويتضح ذلك من حقيقة أن تكافؤ المحاكاة الثنائية يصبح قابلاً للتقرير بالنسبة لحساب باي الخالي من التكرار، وحتى بالنسبة لحساب باي ذي التحكم المحدود حيث يكون عدد المكونات المتوازية في أي عملية محدودًا بثابت. ^{[ 11 ]}

وقد صاغ كل من ميلنر وبارو ووالكر مفهومي التماثل المبكر والمتأخر في ورقتهم البحثية الأصلية حول حساب التفاضل والتكامل π . ^{[ 12 ]}

علاقة ثنائية${\displaystyle R}$تُعتبر عملية التماثل الثنائي المبكر بين العمليات إذا كان لكل زوج من العمليات${\displaystyle (p,q)\in R}$،

• حينما${\displaystyle p\,{\xrightarrow {a(x)}}\,p'}$ثم لكل اسم${\displaystyle y}$يوجد بعض${\displaystyle q'}$بحيث${\displaystyle q\,{\xrightarrow {a(x)}}\,q'}$و${\displaystyle (p'[y/x],q'[y/x])\in R}$؛
• لأي إجراء غير متعلق بالإدخال${\displaystyle \alpha }$، لو${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$ثم يوجد شيء ما${\displaystyle q'}$بحيث${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$و${\displaystyle (p',q')\in R}$؛
• ومتطلبات متناظرة مع${\displaystyle p}$و${\displaystyle q}$تم التبديل.

العمليات${\displaystyle p}$و${\displaystyle q}$يقال إنها ثنائية التشابه المبكرة، مكتوبة${\displaystyle p\sim _{e}q}$إذا كان الزوج${\displaystyle (p,q)\in R}$لبعض عمليات المحاكاة الثنائية المبكرة${\displaystyle R}$.

في التماثل الثنائي المتأخر، يجب أن يكون تطابق الانتقال مستقلاً عن الاسم الذي يتم نقله. علاقة ثنائية${\displaystyle R}$تُعتبر عملية التماثل الثنائي المتأخرة على العمليات إذا كان لكل زوج من العمليات${\displaystyle (p,q)\in R}$،

• حينما${\displaystyle p{\xrightarrow {a(x)}}p'}$ثم بالنسبة للبعض${\displaystyle q'}$وهذا يعني أن${\displaystyle q{\xrightarrow {a(x)}}q'}$و${\displaystyle (p'[y/x],q'[y/x])\in R}$لكل اسم ص ؛
• لأي إجراء غير متعلق بالإدخال${\displaystyle \alpha }$، لو${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$وهذا يعني وجود شيء ما${\displaystyle q'}$بحيث${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$و${\displaystyle (p',q')\in R}$؛
• ومتطلبات متناظرة مع${\displaystyle p}$و${\displaystyle q}$تم التبديل.

العمليات${\displaystyle p}$و${\displaystyle q}$يقال إنها ثنائية متماثلة متأخرة، مكتوبة${\displaystyle p\sim _{l}q}$إذا كان الزوج${\displaystyle (p,q)\in R}$لبعض المحاكاة الثنائية المتأخرة${\displaystyle R}$.

كلاهما${\displaystyle \sim _{e}}$و${\displaystyle \sim _{l}}$تعاني هذه العمليات من مشكلة أنها ليست علاقات تطابق بمعنى أنها لا تُحفظ بواسطة جميع بنيات العمليات. وبشكل أدق، توجد عمليات${\displaystyle p}$و${\displaystyle q}$بحيث${\displaystyle p\sim _{e}q}$لكن${\displaystyle a(x).p\not \sim _{e}a(x).q}$يمكن معالجة هذه المشكلة من خلال النظر في علاقات التطابق القصوى المضمنة في${\displaystyle \sim _{e}}$و${\displaystyle \sim _{l}}$، والمعروفة باسم التطابق المبكر والتطابق المتأخر ، على التوالي.

لحسن الحظ، هناك تعريف ثالث ممكن يتجنب هذه المشكلة، ألا وهي مشكلة التماثل الثنائي المفتوح ، وذلك بفضل سانجيورجي. ^{[ 13 ]}

علاقة ثنائية${\displaystyle R}$تُعتبر العمليات ثنائية التماثل مفتوحة إذا كان لكل زوج من العناصر${\displaystyle (p,q)\in R}$ولكل استبدال اسم${\displaystyle \sigma }$وكل فعل${\displaystyle \alpha }$، حينما${\displaystyle p\sigma {\xrightarrow {\overset {}{\alpha }}}p'}$ثم يوجد شيء ما${\displaystyle q'}$بحيث${\displaystyle q\sigma {\xrightarrow {\overset {}{\alpha }}}q'}$و${\displaystyle (p',q')\in R}$.

العمليات${\displaystyle p}$و${\displaystyle q}$يقال إنها ثنائية التشابه مفتوحة، مكتوبة${\displaystyle p\sim _{o}q}$إذا كان الزوج${\displaystyle (p,q)\in R}$لبعض المحاكاة الثنائية المفتوحة${\displaystyle R}$.

بدلاً من ذلك، يمكن تعريف تكافؤ المحاكاة الثنائية مباشرةً من دلالات الاختزال. نكتب${\displaystyle p\Downarrow a}$إذا كانت العملية${\displaystyle p}$يسمح على الفور بإدخال أو إخراج بالاسم${\displaystyle a}$.

علاقة ثنائية${\displaystyle R}$تُعتبر العمليات المتراكبة تناظرًا ثنائيًا مسننًا إذا كانت علاقة متناظرة تحقق الشرط التالي: لكل زوج من العناصر${\displaystyle (p,q)\in R}$لدينا ذلك

(1)${\displaystyle p\Downarrow a}$إذا وفقط إذا${\displaystyle q\Downarrow a}$لكل اسم${\displaystyle a}$

و

(2) لكل تخفيض${\displaystyle p\rightarrow p'}$يوجد تخفيض${\displaystyle q\rightarrow q'}$

بحيث${\displaystyle (p',q')\in R}$.

نقول ذلك${\displaystyle p}$و${\displaystyle q}$تكون متماثلة ثنائية مسننة إذا وُجد تماثل ثنائي مسنن.${\displaystyle R}$أين${\displaystyle (p,q)\in R}$.

بتعريف السياق على أنه حد π ذو ثقب []، نقول إن العمليتين P و Q متطابقتان بشكل شائك ، مكتوبتان${\displaystyle P\sim _{b}Q\,\!}$، إذا كان ذلك لكل سياق${\displaystyle C[]}$لدينا ذلك${\displaystyle C[P]}$و${\displaystyle C[Q]}$هي ثنائية التماثل الشائكة. ويتضح أن التطابق الشائك يتزامن مع التطابق الناتج عن ثنائية التماثل المبكرة.