Non-deterministic Interaction Nets. Alexiev, V. Ph.D. Thesis, University of Alberta, 1999.
Non-deterministic Interaction Nets [pdf]Paper  Non-deterministic Interaction Nets [pdf]Slides  Non-deterministic Interaction Nets [pdf]Other  abstract   bibtex   2 downloads  
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. We study in considerable detail the relative expressive power of these systems, both by representing various programming examples in them, and by constructing inter-representations that translate nets from one system to another. We study formally a translation from the finite pi-calculus to a system that we call MultiInteraction Nets: MIN=INMP+NMPP. We prove the faithfulness of the translation to the pi-calculus processes that it represents, both structural and operational (completeness and soundness of reduction). We show that unlike the pi-calculus, our translation implements the Prefix operation of the pi-calculus in a distributed and purely local manner, and implements explicitly the distribution and duplication of values to the corresponding occurrences of a variable. We compare our translation to other graphical and combinatory representations of the pi-calculus, such as the pi-nets of Milner, the Interaction Diagrams of Parrow, and the Concurrent Combinators of Honda and Yoshida. The original paper on IN (Lafont, 1990) states that INs were designed to be simple and practical; to be a "programming language that can be used for the design of interactive software". However, to date INs have been used only for theoretical investigations. This thesis is mostly devoted to a hands-on exploration of applications of IN to various "programming problems".

Downloads: 2