A hierarchy of expressiveness in concurrent interaction nets

Abstract

We give separation results, in terms of expressiveness, concerning all the concurrent extensions of interaction nets defined so far in the literature: we prove that multirule interaction nets (of which Ehrhard and Regnier's differential interaction nets are a special case) are strictly less expressive than multiwire interaction nets (which include Beffara and Maurel's concurrent nets and Honda and Laurent's version of polarized proof nets); these, in turn, are strictly less expressive than multiport interaction nets (independently introduced by Alexiev and the second author), although in a milder way. These results are achieved by providing a notion of barbed bisimilarity for interaction nets which is general enough to adapt to all systems but is still concrete enough to allow (hopefully) convincing separation results. This is itself a contribution of the paper. © 2013 Springer-Verlag.