Lambda the Ultimate

Abstract

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.