ในวิทยาการคอมพิวเตอร์เชิงทฤษฎีแคลคูลัสπ (หรือแคลคูลัสพาย ) เป็นแคลคูลัสกระบวนการแคลคูลัสπ อนุญาตให้สื่อสารชื่อช่องสัญญาณไปตามช่องสัญญาณเหล่านั้นได้ และในแง่นี้ แคลคูลัส π สามารถอธิบายการคำนวณพร้อมกันซึ่งการกำหนดค่าเครือข่ายอาจเปลี่ยนแปลงได้ในระหว่างการคำนวณ

π - calculus มีคำศัพท์น้อยและเป็นภาษาขนาดเล็กแต่แสดงออกได้ดี (ดู§ ไวยากรณ์ ) โปรแกรมเชิงฟังก์ชันสามารถเข้ารหัสลงในπ -calculus ได้ และการเข้ารหัสเน้นลักษณะการสนทนาของการคำนวณ โดยเชื่อมโยงกับความหมายของเกมส่วนขยายของπ -calculus เช่น spi calculus และπ ประยุกต์ ประสบความสำเร็จในการให้เหตุผลเกี่ยวกับโปรโตคอลการเข้ารหัสลับนอกเหนือจากการใช้งานดั้งเดิมในการอธิบายระบบพร้อมกันแล้วπ -calculus ยังถูกนำมาใช้ในการให้เหตุผลผ่านกระบวนการทางธุรกิจ [ ^{1 ] ชีววิทยา}โมเลกุล [ ^{2 ] และ}ตัวแทนอิสระในปัญญาประดิษฐ์

แคลคูลัสπจัดอยู่ในกลุ่มของแคลคูลัสกระบวนการซึ่งเป็นรูปแบบทางคณิตศาสตร์สำหรับอธิบายและวิเคราะห์คุณสมบัติของการคำนวณพร้อมกัน อันที่จริงแคลคูลัสπ เช่นเดียวกับ แคลคูลัส λนั้นเรียบง่ายมากจนไม่มีองค์ประกอบพื้นฐาน เช่น ตัวเลข บูลีน โครงสร้างข้อมูล ตัวแปร ฟังก์ชัน หรือแม้แต่ คำสั่ง ควบคุมการไหลของโปรแกรม ตามปกติ (เช่นif-then-else, while)

หัวใจสำคัญของ แคลคูลัส πคือแนวคิดเรื่องชื่อความเรียบง่ายของแคลคูลัสนี้อยู่ที่บทบาทคู่ของชื่อในฐานะช่อง ทางการสื่อสารและตัวแปร

โครงสร้างกระบวนการที่มีอยู่ในแคลคูลัสมีดังต่อไปนี้^{[ 3 ]} (คำจำกัดความที่แม่นยำมีอยู่ในหัวข้อถัดไป):

• การทำงานพร้อมกัน (concurrency ) เขียนได้ว่า โดยที่และคือสองกระบวนการหรือเธรดที่ทำงานพร้อมกัน${\displaystyle P\mid Q}$${\displaystyle P}$${\displaystyle Q}$
• การสื่อสารที่ไหน
  • การกำหนดคำนำหน้าอินพุต คือกระบวนการที่รอข้อความที่ส่งมาทางช่องทางการสื่อสารที่ระบุชื่อไว้ก่อน จากนั้นจึงดำเนินการต่อไปโดยผูกชื่อที่ได้รับเข้ากับชื่อxโดยทั่วไปแล้ว กระบวนการนี้จะจำลองกระบวนการที่คาดหวังการสื่อสารจากเครือข่าย หรือป้ายกำกับที่ใช้ได้เพียงครั้งเดียวต่อการดำเนินการ${\displaystyle c\left(x\right).P}$${\displaystyle c}$${\displaystyle P}$cgoto c
  • การกำหนดคำนำหน้าเอาต์พุต หมายความว่าชื่อนั้นจะถูกส่งออกไปทางช่องสัญญาณก่อนที่จะดำเนินการต่อไป โดยทั่วไปแล้ว รูปแบบนี้จะใช้ในการส่งข้อความบนเครือข่ายหรือการดำเนินการใด ๆ${\displaystyle {\overline {c}}\langle y\rangle .P}$${\displaystyle y}$${\displaystyle c}$${\displaystyle P}$goto c
• การจำลองแบบ (replication ) สามารถมองได้ว่าเป็นกระบวนการที่สามารถสร้างสำเนาใหม่ของข้อมูล ได้เสมอ โดยทั่วไปแล้ว รูปแบบนี้จะจำลองบริการเครือข่ายหรือป้ายกำกับ ที่รอ การดำเนินการใดๆ ก็ได้${\displaystyle !\,P}$${\displaystyle P}$cgoto c
• การสร้างชื่อใหม่ ซึ่ง เขียนว่าอาจมองได้ว่าเป็นกระบวนการจัดสรรค่าคงที่x ใหม่ ภายใน ค่าคง ที่ในแคลคูลัส πถูกกำหนดโดยชื่อของมันเท่านั้น และเป็นช่องทางการสื่อสารเสมอ การสร้างชื่อใหม่ในกระบวนการนี้เรียกว่า การจำกัด ( restriction )${\displaystyle \left(\nu x\right)P}$${\displaystyle P}$
• กระบวนการที่เป็นค่าว่าง (nil process) หมายถึงกระบวนการที่การทำงานเสร็จสมบูรณ์และหยุดลงแล้ว${\displaystyle 0}$

แม้ว่าความเรียบง่ายของ แคลคูลัส πจะทำให้เราไม่สามารถเขียนโปรแกรมในความหมายปกติได้ แต่ก็สามารถขยายแคลคูลัสได้ง่าย โดยเฉพาะอย่างยิ่ง สามารถกำหนดโครงสร้างควบคุม เช่น การเรียกซ้ำ ลูป และการประกอบลำดับ และชนิดข้อมูล เช่น ฟังก์ชันอันดับหนึ่งค่าความจริงรายการ และจำนวนเต็ม ได้ง่าย นอกจากนี้ ยังมีการเสนอส่วนขยายของแคลคูลัส π ที่คำนึงถึงการเข้ารหัสแบบกระจายหรือแบบกุญแจสาธารณะแคลคูลัสπประยุกต์ของ Abadi และ Fournet [1]ได้วางส่วนขยายต่างๆ เหล่านี้ไว้บนพื้นฐานที่เป็นทางการโดยการขยายแคลคูลัสπด้วยชนิดข้อมูลตามอำเภอใจ

ด้านล่างนี้คือตัวอย่างเล็กๆ ของกระบวนการที่ประกอบด้วยส่วนประกอบคู่ขนานสามส่วน โดยชื่อช่องสัญญาณ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{ชิดกัน}}}$

ส่วนประกอบสองส่วนแรกสามารถสื่อสารกันได้ผ่านช่องทาง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{รับข้อมูลบนช่อง }}x{\text{ ผูกผลลัพธ์เข้ากับ }}y{\text{ จากนั้นเรียกใช้ }}P\\&\;|\;{\overline {x}}\langle y\rangle .P\,\,\,\,\,&{\text{ส่งค่า }}y{\text{ ผ่านช่อง }}x{\text{ จากนั้นเรียกใช้ }}P\\&\;|\;P|Q\,\,\,\,\,\,\,\,\,&{\text{เรียกใช้ }}P{\text{ และ }}Q{\text{ พร้อมกัน}}\\&\;|\;(\nu x)P\,\,\,&{\text{สร้างช่องใหม่ }}x{\text{ และเรียกใช้ }}P\\&\;|\;!P\,\,\,&{\text{สร้างสำเนาของ }}P\\&\;|\;0&{\text{ยุติกระบวนการ}}\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\ลูกศรขวา 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'}$

โดยที่สถานะและแสดงถึงกระบวนการและเป็นการกระทำขาเข้าการกระทำขาออกหรือ การ ^{กระทำ}เงียบτ [ ^{5 ]}${\displaystyle P}$${\displaystyle P'}$${\displaystyle \alpha }$${\displaystyle a(x)}$${\displaystyle {\overline {a}}\langle x\rangle }$

ผลลัพธ์มาตรฐานเกี่ยวกับความหมายที่มีป้ายกำกับคือสอดคล้องกับความหมายการลดทอนจนถึงความสอดคล้องเชิงโครงสร้าง ในแง่ที่ว่า ก็ต่อเมื่อ^{[ 6 ]}${\displaystyle P\rightarrow P'}$${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$

ไวยากรณ์ที่แสดงข้างต้นเป็นไวยากรณ์ขั้นพื้นฐาน แต่สามารถปรับเปลี่ยนไวยากรณ์ได้หลายวิธี

สามารถเพิ่ม ตัวดำเนินการเลือกแบบไม่กำหนดลง ในไวยากรณ์ได้ ${\displaystyle P+Q}$

สามารถเพิ่ม การทดสอบความเท่าเทียมกันของชื่อลง ในไวยากรณ์ได้ตัวดำเนินการจับคู่จะทำงานก็ต่อเมื่อxและเป็นชื่อเดียวกันเท่านั้น ในทำนองเดียวกัน อาจเพิ่มตัวดำเนินการไม่ตรงกันสำหรับความไม่เท่าเทียมกันของชื่อได้โปรแกรมเชิงปฏิบัติที่สามารถส่งผ่านชื่อ (URL หรือตัวชี้) มักใช้ฟังก์ชันดังกล่าว: สำหรับการจำลองฟังก์ชันดังกล่าวโดยตรงภายในแคลคูลัส ส่วนขยายนี้และส่วนขยายที่เกี่ยวข้องมักมีประโยชน์ ${\displaystyle [x=y]P}$${\displaystyle P}$${\displaystyle y}$

แคลคูลัสπแบบอะซิงโครนัส[ ^{7 ] [ 8 ] อนุญาต} ให้ส่งออกได้เฉพาะโดยไม่มีการต่อเนื่อง กล่าวคือ อะตอมเอาต์พุตในรูปแบบซึ่งทำให้ได้แคลคูลัสที่เล็กลง อย่างไรก็ตาม กระบวนการใดๆ ในแคลคูลัสเดิมสามารถแสดงได้ด้วย แคลคูลัส π แบบอะซิงโครนัสที่เล็กลง โดยใช้ช่องทางพิเศษเพื่อจำลองการรับทราบที่ชัดเจนจากกระบวนการรับ เนื่องจากเอาต์พุตที่ไม่มีความต่อเนื่องสามารถจำลองข้อความระหว่างการส่งได้ ส่วนนี้แสดงให้เห็นว่า แคลคูลัส π เดิม ซึ่งโดยสัญชาตญาณแล้วอิงตามการสื่อสารแบบซิงโครนัส มีแบบจำลองการสื่อสารแบบอะซิงโครนัสที่แสดงออกได้ภายในไวยากรณ์ อย่างไรก็ตาม ตัวดำเนินการเลือกแบบไม่กำหนดที่กำหนดไว้ข้างต้นไม่สามารถแสดงในลักษณะนี้ได้ เนื่องจาก ตัวเลือก ที่ไม่มีการป้องกันจะถูกแปลงเป็นตัวเลือกที่มีการป้องกัน ข้อเท็จจริงนี้ถูกนำมาใช้เพื่อแสดงให้เห็นว่าแคลคูลัสแบบอะซิงโครนัสแสดงออกได้น้อยกว่าแคลคูลัสแบบซิงโครนัสอย่างเคร่งครัด (ด้วยตัวดำเนินการเลือก) ^{[ 9 ]}${\displaystyle {\overline {x}}\langle y\rangle }$

แคลคูลัสπแบบพหุแอดิกช่วยให้สามารถสื่อสารชื่อได้มากกว่าหนึ่งชื่อในการกระทำเดียว: (เอาต์พุตแบบพหุแอดิก)และ(อินพุตแบบพหุแอดิก)ส่วนขยายแบบพหุแอดิกนี้ ซึ่งมีประโยชน์โดยเฉพาะอย่างยิ่งเมื่อศึกษาประเภทสำหรับกระบวนการส่งผ่านชื่อ สามารถเข้ารหัสในแคลคูลัสแบบเอกนาดิกได้โดยการส่งชื่อของช่องสัญญาณส่วนตัวซึ่งจะส่งผ่านอาร์กิวเมนต์หลายตัวตามลำดับ การเข้ารหัสถูกกำหนดแบบเรียกซ้ำโดยข้อความ ${\displaystyle {\overline {x}}\langle z_{1},...,z_{n}\rangle .P}$${\displaystyle x(z_{1},...,z_{n}).P}$

${\displaystyle {\overline {x}}\langle y_{1},\cdots ,y_{n}\rangle .P}$ถูกเข้ารหัสเป็น${\displaystyle (\nu w){\overline {x}}\langle w\rangle .{\overline {w}}\langle y_{1}\rangle .\cdots .{\overline {w}}\langle y_{n}\rangle .[P]}$

${\displaystyle x(y_{1},\cdots ,y_{n}).P}$ถูกเข้ารหัสเป็น${\displaystyle x(w).w(y_{1}).\cdots .w(y_{n}).[P]}$

โครงสร้างกระบวนการอื่นๆ ทั้งหมดจะไม่มีการเปลี่ยนแปลงโดยการเข้ารหัส

ในตัวอย่างข้างต้นหมายถึงการเข้ารหัสคำนำหน้าทั้งหมดในส่วนต่อขยายในลักษณะเดียวกัน ${\displaystyle [P]}$${\displaystyle P}$

ไม่จำเป็นต้องใช้พลังทั้งหมดของการจำลองแบบ บ่อยครั้งที่เราพิจารณาเฉพาะ ข้อมูลป้อนเข้าที่จำลองแบบแล้วซึ่งมีหลักการความสอดคล้องเชิงโครงสร้างคือ ${\displaystyle !P}$${\displaystyle !x(y).P}$${\displaystyle !x(y).P\equiv x(y).P|!x(y).P}$

กระบวนการป้อนข้อมูลแบบจำลอง เช่นสามารถเข้าใจได้ว่าเป็นเซิร์ฟเวอร์ที่รอรับการเรียกใช้งานจากไคลเอ็นต์บนช่องทาง xการเรียกใช้งานเซิร์ฟเวอร์จะสร้างสำเนาใหม่ของกระบวนการโดยที่ a คือชื่อที่ไคลเอ็นต์ส่งไปยังเซิร์ฟเวอร์ในระหว่างการเรียกใช้งานเซิร์ฟเวอร์นั้น ${\displaystyle !x(y).P}$${\displaystyle P[a/y]}$

สามารถกำหนด แคลคูลัสπลำดับสูงกว่าได้ โดยที่ไม่เพียงแต่ชื่อเท่านั้น แต่กระบวนการต่างๆ ก็ถูกส่งผ่านช่องทางด้วย กฎการลดรูปที่สำคัญสำหรับกรณีลำดับสูงกว่าคือ

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

ในที่นี้หมายถึงตัวแปรของกระบวนการซึ่งสามารถกำหนดค่าได้ด้วยเทอมของกระบวนการ Sangiorgi ได้พิสูจน์แล้วว่าความสามารถในการส่งผ่านกระบวนการไม่ได้เพิ่มความสามารถในการแสดงออกของ แคลคูลัส π : การส่งผ่านกระบวนการPสามารถจำลองได้โดยการส่งชื่อที่ชี้ไปยังPแทน ${\displaystyle Y}$

π - calculus เป็นแบบจำลองการคำนวณสากลสิ่งนี้ได้รับการสังเกตครั้งแรกโดยMilnerในบทความของเขาเรื่อง "Functions as Processes" ^{[ 10 ]}ซึ่งเขานำเสนอการเข้ารหัสสองแบบของlambda-calculusในπ -calculus การเข้ารหัสแบบหนึ่งจำลองกลยุทธ์การประเมินแบบ eager (call-by-value) ส่วนการเข้ารหัสอีกแบบจำลองกลยุทธ์แบบ normal-order (call-by-name) ในทั้งสองกรณีนี้ ข้อมูลเชิงลึกที่สำคัญคือการสร้างแบบจำลองการผูกสภาพแวดล้อม – ตัวอย่างเช่น " xถูกผูกกับเทอม" – ในฐานะตัวแทนจำลองที่ตอบสนองต่อคำขอสำหรับการผูกโดยการส่งการเชื่อมต่อกลับไปยังเทอม ${\textstyle M}$${\displaystyle M}$

คุณสมบัติของ แคลคูลัส πที่ทำให้การเข้ารหัสเหล่านี้เป็นไปได้คือการส่งต่อชื่อและการจำลอง (หรือเทียบเท่ากับตัวแทนที่กำหนดแบบเรียกซ้ำ) ในกรณีที่ไม่มีการจำลอง/การเรียกซ้ำ แคลคูลัส πจะไม่สมบูรณ์แบบทัวริงอีกต่อไป สามารถเห็นได้จากข้อเท็จจริงที่ว่าความ เท่าเทียมกัน ของการจำลองแบบคู่กลายเป็นสิ่งที่ตัดสินได้สำหรับแคลคูลัสที่ไม่มีการเรียกซ้ำ และแม้แต่สำหรับ แคลคูลัส π ที่มีการควบคุมแบบจำกัด ซึ่งจำนวนส่วนประกอบแบบขนานในกระบวนการใด ๆ จะถูกจำกัดด้วยค่าคงที่^{[ 11 ]}

สำหรับแคลคูลัสเชิงกระบวนการ แคลคูลัส πอนุญาตให้กำหนดนิยามของความสมมูลแบบบิซิมูเลชันได้ ใน แคลคูลัส πนิยามของความสมมูลแบบบิซิมูเลชัน (หรือที่เรียกว่า บิซิมิลาริตี) อาจอิงตามความหมายเชิงการลดทอนหรือความหมายเชิงการเปลี่ยนสถานะที่มีป้ายกำกับก็ได้

ใน แคลคูลัส πมีวิธีการกำหนดความเท่าเทียมกันของการจำลองแบบมีป้าย กำกับอย่างน้อยสามวิธี ได้แก่ การจำลองแบบต้น การจำลองแบบปลาย และการจำลองแบบเปิด ซึ่งเป็นผลมาจากข้อเท็จจริงที่ว่า แคลคูลัส πเป็นแคลคูลัสกระบวนการส่งผ่านค่า

ในส่วนที่เหลือของหัวข้อนี้ เราจะใช้และแทนกระบวนการ และแทนความสัมพันธ์ทวิภาคเหนือกระบวนการ ${\displaystyle p}$${\displaystyle q}$${\displaystyle R}$

ความคล้ายคลึงแบบต้นและแบบปลายได้รับการกำหนดสูตรโดย Milner, Parrow และ Walker ในบทความต้นฉบับของพวกเขาเกี่ยวกับแคลคูลัสπ ^{[ 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}$

กระบวนการเหล่านี้เรียกว่าเป็น bisimilar ในช่วงต้น ซึ่งเขียนแทนด้วยคำว่าbisimilar ในช่วงต้น ${\displaystyle p}$${\displaystyle q}$${\displaystyle p\sim _{e}q}$${\displaystyle (p,q)\in R}$${\displaystyle R}$

ในความคล้ายคลึงแบบล่าช้า (late bisimilarity) การจับคู่การเปลี่ยนผ่านจะต้องเป็นอิสระจากชื่อที่ส่งผ่าน ความสัมพันธ์แบบไบนารีระหว่างกระบวนการต่างๆ จะเป็นความคล้ายคลึงแบบล่าช้าก็ต่อเมื่อสำหรับทุกคู่ของกระบวนการ ${\displaystyle R}$${\displaystyle (p,q)\in R}$

• เมื่อใดก็ตามที่สำหรับบางคนถือว่าเป็นเช่นนั้นและสำหรับทุกชื่อ y ;${\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}$

กระบวนการและกล่าวกันว่าเป็น bisimilar ในช่วงปลาย โดยเขียนว่าถ้าคู่สำหรับ bisimilation ในช่วงปลายบางอย่าง ${\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}}$

โชคดีที่มีคำจำกัดความที่สามที่เป็นไปได้ ซึ่งหลีกเลี่ยงปัญหานี้ นั่นคือความคล้ายคลึงแบบเปิดเนื่องจาก Sangiorgi ^{[ 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}$

กระบวนการและกล่าวกันว่าเป็นคู่ที่คล้ายคลึงกันแบบเปิด (open bisimilar) ซึ่งเขียนว่าถ้า คู่สำหรับการจำลองแบบเปิดบางอย่าง${\displaystyle p}$${\displaystyle q}$${\displaystyle p\sim _{o}q}$${\displaystyle (p,q)\in R}$${\displaystyle R}$

ความคล้ายคลึงแบบต้น แบบปลาย และแบบเปิดนั้นแตกต่างกัน การบรรจุถูกต้องดังนั้น ${\displaystyle \sim _{o}\subsetneq \sim _{l}\subsetneq \sim _{e}}$

ในแคลคูลัสย่อยบางชนิด เช่น แคลคูลัสพายแบบอะซิงโครนัส พบว่าความคล้ายคลึงแบบล่าช้า แบบเร็ว และแบบเปิดนั้นสามารถเกิดขึ้นพร้อมกันได้ อย่างไรก็ตาม ในบริบทนี้ แนวคิดที่เหมาะสมกว่าคือความคล้ายคลึงแบบอะซิง โครนัส ในเอกสารทางวิชาการ คำว่าความคล้ายคลึงแบบเปิดมักหมายถึงแนวคิดที่ซับซ้อนกว่า โดยที่กระบวนการและความสัมพันธ์จะถูกจัดทำดัชนีโดยความสัมพันธ์ที่แตกต่างกัน รายละเอียดอยู่ในบทความของ Sangiorgi ที่อ้างถึงข้างต้น

อีกทางเลือกหนึ่ง เราอาจกำหนดความเท่าเทียมกันของการจำลองแบบคู่โดยตรงจากความหมายของการลดทอน เราเขียนว่าถ้ากระบวนการอนุญาตให้มีการป้อนข้อมูลหรือส่งออกทันทีบนชื่อ. ${\displaystyle p\Downarrow a}$${\displaystyle p}$${\displaystyle a}$

ความสัมพันธ์ทวิภาคเหนือกระบวนการต่างๆ เรียกว่า ไบ ซิมูเลชันแบบมีหนาม (barbed bisimulation)ถ้าเป็นความสัมพันธ์สมมาตรที่สอดคล้องกับเงื่อนไขที่ว่า สำหรับทุกคู่ขององค์ประกอบเราจะได้ว่า ${\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]}$

แคลคูลัส π ถูกนำมาใช้เพื่ออธิบายระบบแบบขนานหลายประเภท ที่จริงแล้ว การประยุกต์ใช้งานล่าสุดบางส่วนอยู่นอกเหนือขอบเขตของวิทยาศาสตร์คอมพิวเตอร์แบบดั้งเดิมด้วย ซ้ำ

ในปี 1997 Martin Abadiและ Andrew Gordon ได้เสนอการขยาย แคลคูลัส πซึ่งก็คือแคลคูลัส Spi เป็นสัญกรณ์อย่างเป็นทางการสำหรับการอธิบายและการให้เหตุผลเกี่ยวกับโปรโตคอลการเข้ารหัส แคลคูลัส Spi ขยาย แคลคูลัส πด้วยพรีมิทีฟสำหรับการเข้ารหัสและการถอดรหัส ในปี 2001 Martin Abadiและ Cedric Fournet ได้วางนัยทั่วไปของการจัดการโปรโตคอลการเข้ารหัสเพื่อสร้าง แคลคูลัส π ประยุกต์ ปัจจุบันมีผลงานจำนวนมากที่อุทิศให้กับ แคลคูลัส π ประยุกต์รูปแบบต่างๆ รวมถึงเครื่องมือตรวจสอบเชิงทดลองจำนวนหนึ่ง ตัวอย่างหนึ่งคือเครื่องมือProVerif [2]ของ Bruno Blanchet ซึ่งอิงจากการแปลแคลคูลัสπ ประยุกต์เป็น กรอบการเขียนโปรแกรมเชิงตรรกะของ Blanchet อีกตัวอย่างหนึ่งคือ Cryptyc [3]ซึ่งพัฒนาโดย Andrew Gordon และ Alan Jeffrey โดยใช้วิธีการยืนยันความสอดคล้องของ Woo และ Lam เป็นพื้นฐานสำหรับระบบประเภทที่สามารถตรวจสอบคุณสมบัติการรับรองความถูกต้องของโปรโตคอลการเข้ารหัสลับได้

ประมาณปี 2002 Howard Smith และ Peter Fingar เริ่มสนใจว่า แคลคูลัส πจะกลายเป็นเครื่องมืออธิบายสำหรับการสร้างแบบจำลองกระบวนการทางธุรกิจ ภายในเดือนกรกฎาคม 2006 มีการพูดคุยกันในชุมชนเกี่ยวกับประโยชน์ของสิ่งนี้ ล่าสุด แคลคูลัส πได้กลายเป็นพื้นฐานทางทฤษฎีของภาษาสร้างแบบจำลองกระบวนการทางธุรกิจ (BPML) และ XLANG ของ Microsoft ^{[ 14 ]}

แคลคูลัสπยังดึงดูดความสนใจในชีววิทยาโมเลกุลด้วย ในปี 1999 Aviv RegevและEhud Shapiroแสดงให้เห็นว่าสามารถอธิบายเส้นทางการส่งสัญญาณของเซลล์ (ที่เรียกว่าRTK / MAPK cascade) และโดยเฉพาะอย่างยิ่ง "เลโก้" โมเลกุลที่ดำเนินการงานการสื่อสารเหล่านี้ในส่วนขยายของแคลคูลัสπ ได้ ^{[ 2 ]}หลังจากบทความสำคัญนี้ ผู้เขียนคนอื่นๆ ได้อธิบายเครือข่ายเมตาบอลิซึมทั้งหมดของเซลล์ขั้นต่ำ^{[ 15 ]}ในปี 2009 Anthony Nash และSara Kalvalaได้เสนอ เฟรมเวิร์กแคลคูลัส πเพื่อจำลองการส่งสัญญาณที่ควบคุมการรวมกลุ่ม ของ Dictyostelium discoideum ^{[ 16 ]}

แคลคูลัสπได้รับการพัฒนาขึ้นครั้งแรกโดยRobin Milner , Joachim Parrow และ David Walker ในปี 1992 โดยอิงจากแนวคิดของ Uffe Engberg และ Mogens Nielsen ^{[ 17 ]}อาจมองได้ว่าเป็นการต่อยอดจากงานของ Milner เกี่ยวกับแคลคูลัสกระบวนการ CCS ( แคลคูลัสของระบบการสื่อสาร ) ในการบรรยาย Turing ของเขา Milner อธิบายถึงการพัฒนา แคลคูลัส πว่าเป็นความพยายามที่จะจับภาพความสม่ำเสมอของค่าและกระบวนการในนักแสดง^{[ 18 ]}

ภาษาโปรแกรมต่อไปนี้ใช้ แคลคูลัส πหรือรูปแบบต่างๆ ของแคลคูลัส π:

• ภาษาสร้างแบบจำลองกระบวนการทางธุรกิจ (BPML)
• อ็อกแคม-π
• พิคท์
• JoCaml (อิงตามJoin-calculus )
• โรลัง