Binary pi-calculus

Binary pi-calculus is a binary encoding of pi-calculus outlined in October of 2020 by User:RocketRace. It is to pi-calculus as binary lambda calculus is to lambda calculus.

Encoding scheme

Programs are encoded in prefix notation, using the following rules. Here, P & Q represent processes and x & y represent channels (names). _ represents an omitted argument.

• 000: Nil process (0)
• 001P: Repeatedly spawn copies of P (!P)
• 010P: Bind name, then execute P ((v_)P)
• 011PQ: Execute P and Q in parallel (P|Q)
• 100xyP: Send bound or free name y over channel x, then execute P (x<y>.P)
• 101xP: Receive and bind name over channel x, then execute P (x(_).P)
• 110n0 where n is zero or more ones: the n-th bound name, where 1100 is the most recently bound name, 11010 is the second most recent, and so on
• 111n0 where n is zero or more ones: the free name labeled with n

External resources

• Wikipedia article for pi-calculus