# Binary pi-calculus

Jump to navigation
Jump to search

**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