Acyclic Solos and Differential Interaction Nets

TL;DR

This paper introduces a restricted solos calculus with acyclic diagrams that can encode the pi-calculus, providing a new proof of the expressive power of differential interaction nets for modeling concurrent computations.

Contribution

It defines an acyclic solos calculus compatible with differential interaction nets, simplifying the encoding of pi-calculus processes without name equalization.

Findings

Acyclic solo diagrams induce faithful encodings into differential interaction nets.

The calculus can encode pi-calculus without requiring name equalization.

The approach applies to finitary, replication-free systems without sum or match operations.

Abstract

We present a restriction of the solos calculus which is stable under reduction and expressive enough to contain an encoding of the pi-calculus. As a consequence, it is shown that equalizing names that are already equal is not required by the encoding of the pi-calculus. In particular, the induced solo diagrams bear an acyclicity property that induces a faithful encoding into differential interaction nets. This gives a (new) proof that differential interaction nets are expressive enough to contain an encoding of the pi-calculus. All this is worked out in the case of finitary (replication free) systems without sum, match nor mismatch.