An encoding of Turing Machines in the pi-calculus

Turing Basic.json

{
  "gravity": false,
  "palette": {
    "H": "#d62728",
    "E": "black",
    "O": "#1f77b4",
    "Z": "#aec7e8",
    "B": "gray"
  }
}

Turing Basic.pi

new lo,lz,lb,ro,rz,rb.(
  H[lo,lz,lb,ro,rz,rb] |
  new o,z,b.E[ro,rz,rb,o,z,b] |
  new o,z,b.E[lo,lz,lb,o,z,b]
)

E[o,z,b,no,nz,nb] := b<no,nz,nb>.new o,z,b.E[no,nz,nb,o,z,b]
O[o,z,b,no,nz,nb] := o<no,nz,nb>
Z[o,z,b,no,nz,nb] := z<no,nz,nb>
B[o,z,b,no,nz,nb] := b<no,nz,nb>

H[lo,lz,lb,ro,rz,rb] :=
  lo(no,nz,nb).(O[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lo(no,nz,nb).(Z[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lo(no,nz,nb).(B[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lz(no,nz,nb).(O[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lz(no,nz,nb).(Z[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lz(no,nz,nb).(B[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lb(no,nz,nb).(O[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lb(no,nz,nb).(Z[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ lb(no,nz,nb).(B[lo,lz,lb,ro,rz,rb] | H[no,nz,nb,lo,lz,lb])
+ ro(no,nz,nb).(O[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ ro(no,nz,nb).(Z[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ ro(no,nz,nb).(B[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ rz(no,nz,nb).(O[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ rz(no,nz,nb).(Z[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ rz(no,nz,nb).(B[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ rb(no,nz,nb).(O[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ rb(no,nz,nb).(Z[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])
+ rb(no,nz,nb).(B[ro,rz,rb,lo,lz,lb] | H[ro,rz,rb,no,nz,nb])

Turing Machine.json

{
  "gravity": false,
  "palette": {
    "TL": "black",
    "TR": "black",
    "M": "#d62728",
    "MR": "#ff8c32",
    "MW": "#ffc186",
    "MM": "#ffa1a0",
    "I": "#1f77b4",
    "O": "#aec7e8",
    "IR": "#1f77b4",
    "OR": "#aec7e8",
    "W": "#c49c94",
    "WI": "#1f77b4",
    "WO": "#aec7e8"
  }
}

Turing Machine.pi

/* * * * * * * * * * * * * * * * * *\
 * The Turing machine encoded here *
 * is the one with a complete      *
 * transition table, meaning that  *
 * at any step any possible action *
 * is possible.                    *
 * This allows you to pick the     *
 * transitions you want to fire    *
 * from the simulator without      *
 * restrictions, so you can        *
 * reproduce traces of any machine.*
\* * * * * * * * * * * * * * * * * */
new h,a,b.(
   M[a,h]   // the head
 | TR[a,b]  // the tape's right end
 | TL[b,a]  // the tape's left end
)

// The tape's left end.
// It expands to a new cell as needed
TL[r,nr] :=
  r(h).new l,nl.( TL[nl,l] | OR[l,r,nl,nr,h] )

// The tape's expandable right end.
TR[l,nl] :=
  l(h).new r,nr.( TR[nr,r] | OR[l,r,nl,nr,h] )
  
// The machine's head, idle state
M[c,h] := c<h>.MR[c,h]

// The machine is reading the cell
MR[c,h] :=
  h<>.MW[c,h] // read zero
+ h().MW[c,h] // read one

// The machine is writing the cell
MW[c,h] := 
  h<>.MM[c,h] // write zero
+ h().MM[c,h] // write one

// The machine is moving the head
MM[c,h] :=
  h(nl,nr).M[nl,h] // moving left
+ h(nl,nr).M[nr,h] // moving right

// An idle cell with value 1
I[l,r,nl,nr] :=
  l(h).IR[l,r,nl,nr,h] // is accessed from the left
+ r(h).IR[l,r,nl,nr,h] // is accessed from the right

// An idle cell with value 0
O[l,r,nl,nr] :=
  l(h).OR[l,r,nl,nr,h] // is accessed from the left
+ r(h).OR[l,r,nl,nr,h] // is accessed from the right

// A cell communicates its value...
IR[l,r,nl,nr,h] := h<>.W[l,r,nl,nr,h]
OR[l,r,nl,nr,h] := h().W[l,r,nl,nr,h]

// ...then allows the head to write a value
W[l,r,nl,nr,h] :=
  h().WO[l,r,nl,nr,h] // writing zero
+ h<>.WI[l,r,nl,nr,h] // writing one

// Before going back to idle,
// a cell communicates its neighbours
// so the head can decide where to move next
WO[l,r,nl,nr,h] :=
  h<nl,nr>.O[l,r,nl,nr]

WI[l,r,nl,nr,h] :=
  h<nl,nr>.I[l,r,nl,nr]