Acyclic Solos and Differential Interaction Nets

摘要

We present a restriction of the solos calculus which is stable underreduction and expressive enough to contain an encoding of the pi-calculus. As aconsequence, it is shown that equalizing names that are already equal is notrequired by the encoding of the pi-calculus. In particular, the induced solodiagrams bear an acyclicity property that induces a faithful encoding intodifferential interaction nets. This gives a (new) proof that differentialinteraction nets are expressive enough to contain an encoding of thepi-calculus. All this is worked out in the case of finitary (replication free) systemswithout sum, match nor mismatch.