Acyclic Solos and Differential Interaction Nets
Logic in Computer Science
2015-07-01 v3 Programming Languages
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.
Keywords
Cite
@article{arxiv.1007.0120,
title = {Acyclic Solos and Differential Interaction Nets},
author = {Thomas Ehrhard and Olivier Laurent},
journal= {arXiv preprint arXiv:1007.0120},
year = {2015}
}