Non-Deterministic Interaction Nets

Non-Deterministic Interaction Nets


The Interaction Nets (IN) of Lafont are a graphical formalism used to model parallel computation. Their genesis can be traced back to the Proof Nets of Linear Logic. They enjoy several nice theoretical properties, amongst them pure locality of interaction, strong confluence, computational completeness, syntactically-definable deadlock-free fragments, combinatorial completeness (existence of a Universal IN). They also have nice "pragmatic" properties: they are simple and elegant, intuitive, can capture aspects of computation at widely varying levels of abstraction. Compared to term and graph rewriting systems, INs are much simpler (a subset of such systems that imposes several constraints on the rewriting process), but are still computationally complete (can capture the lambda-calculus). INs are a refinement of graph rewriting which keeps only the essential features in the system.

Conventional INs are strongly confluent, and are therefore unsuitable for the modeling of non-deterministic systems such as process calculi and concurrent object-oriented programming. We study four diffrent ways of "breaking" the confluence of INs by introducing various extensions:

  • IN with Multiple (reduction) Rules (INMR) Allow more than one reduction rule per redex.
  • IN with Multiple Principal Ports (INMPP) Allow more than one active port per node.
  • IN with MultiPorts (INMP) Allow more than one connection per port.
  • IN with Multiple Connections (INMC) Allow hyper-edges (in the graph-theoretical sense), i.e. connections between more than two ports.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Expressiveness: sometimes subjective?

It is instructive to see that though INMPP, INMP, and INMC can be expressed via each other, it is subjectively more natural to use a formalism with multiple extensions (e.g., MIN=INMPP+INMP).

Can this be generalized to PL design?

Another observation

...from a join-calculus tutorial mentioned previously:
In theory, adding any of the above constructs—even the imperative variable— to the concurrent lambda calculus of Section 1.1 gives a formalism equivalent to the join calculus in terms of expressiveness. What are, then, the advantages of the join pattern construct?

Read on to find out...

this looks really interesting

this looks really interesting (thanks) - but why not post things like this to the front page?

I considered that

...but then compared it to Links and decided to play it safe.

Ehud, what are the general guidelines for front page material? Who is the target audience there? Is this documented already somewhere?

Editor Privileges

Readers are supposed to be people interested in programming languages ("in all their gory details"). The point of having many editros is that each has his own tastes and skills, and links to things he personally finds interesting (as long as they are PL related, I am good).

Feel free to post things that you think might interest other LtU readers, or people that currently don't read Lambda - but should...

ah ok (i've done the same).

ah ok (i've done the same). i commented because i was really surprised at the (mistaken) idea you weren't an editor.

Am I producing that much content? :-)

i was really surprised [...] you weren't an editor

Am I producing that much content? :-)

You say this like it's a bad

You say this like it's a bad thing ;-)

Is there a chance someone wil

Is there a chance someone will want to discuss the paper itself, rather than the method I used to post it?! ;-)