Interaction nets

Interaction nets are a graphical model of computation devised by Yves Lafont in 1990 as a generalisation of the proof structures of linear logic. An interaction net system is specified by a set of agent types and a set of interaction rules. Interaction nets are an inherently distributed model of computation in the sense that computations can take place simultaneously in many parts of an interaction net, and no synchronisation is needed. The latter is guaranteed by the strong confluence property of reduction in this model of computation. Thus interaction nets provide a natural language for massive parallelism. Interaction nets are at the heart of many implementations of the lambda calculus, such as efficient closed reduction and optimal, in Lévy's sense, Lambdascope.
Definitions.
Interactions nets are graph-like structures consisting of "agents" and "edges".
An agent of type formula_1 and with "arity" formula_2 has one "principal port" and formula_3 "auxiliary ports". Any port can be connected to at most one edge. Ports that are not connected to any edge are called "free ports". Free ports together form the "interface" of an interaction net. All agent types belong to a set formula_4 called "signature".
An interaction net that consists solely of edges is called a "wiring" and usually denoted as formula_5. A "tree" formula_6 with its "root" formula_7 is inductively defined either as an edge formula_7, or as an agent formula_1 with its free principal port formula_7 and its auxiliary ports formula_11 connected to the roots of other trees formula_12.
Graphically, the primitive structures of interaction nets can be represented as follows:
When two agents are connected to each other with their principal ports, they form an "active pair". For
active pairs one can introduce "interaction rules" which describe how the active pair rewrites to another interaction
net. An interaction net with no active pairs is said to be in "normal form". A signature formula_4 (with formula_14 defined on it) along with a set of interaction rules defined for agents formula_15 together constitute an "interaction system".
Interaction calculus.
Textual representation of interaction nets is called the "interaction calculus" and can be seen as a programming language.
Inductively defined trees correspond to "terms" formula_16 in the interaction calculus, where formula_7 is called a "name".
Any interaction net formula_18 can be redrawn using the previously defined wiring and tree primitives as follows:
which in the interaction calculus corresponds to a "configuration"
formula_19,
where formula_12, formula_21, and formula_22 are arbitrary terms. The ordered sequence formula_23 in the left-hand side is called an "interface", while the right-hand side contains an unordered multiset of "equations" formula_24. Wiring formula_5 translates to names, and each name has to occur exactly twice in a configuration.
Just like in the formula_26-calculus, the interaction calculus has the notions of "formula_1-conversion" and "substitution" naturally defined on configurations. Specifically, both occurrences of any name can be replaced with a
new name if the latter does not occur in a given configuration. Configurations are considered equivalent up to formula_1-conversion. In turn, substitution formula_29 is the result of replacing the name formula_7 in a term formula_6 with another term formula_32 if formula_7 has exactly one occurrence in the term formula_6.
Any interaction rule can be graphically represented as follows:
where formula_35, and the interaction net formula_18 on the right-hand side is redrawn using the wiring and tree primitives in order to translate into the interaction calculus as formula_37 using Lafont's notation.
The interaction calculus defines reduction on configurations in more details than seen from graph
rewriting defined on interaction nets. Namely, if formula_38, the following reduction:
formula_39
is called "interaction". When one of equations has the form of formula_40, "indirection" can be applied resulting
in substitution of the other occurrence of the name formula_7 in some term formula_6:
formula_43
or
formula_44.
An equation formula_45 is called a "deadlock" if formula_7 has occurrence in term formula_6. Generally only deadlock-free interaction nets are considered. Together, interaction and indirection define the reduction relation on configurations. The fact that configuration formula_48 reduces to its "normal form" formula_49 with no equations left is denoted as formula_50.
Properties.
Interaction nets benefit from the following properties:
These properties together allow massive parallelism.
Interaction combinators.
One of the simplest interaction systems that can simulate any other interaction system is that of "interaction combinators". Its signature is formula_56 with formula_57 and formula_58. Interaction rules for these agents are:
Graphically, the erasing and duplication rules can be represented as follows:
with an example of a non-terminating interaction net that reduces to itself. Its infinite reduction sequence starting from the corresponding configuration in the interaction calculus is as follows:
formula_63
Non-deterministic extension.
Interaction nets are essentially deterministic and cannot model non-deterministic computations directly. In order to express non-deterministic choice, interaction nets need to be extended. In fact, it is sufficient to introduce just one agent formula_64 with two principal ports and the following interaction rules:
This distinguished agent represents ambiguous choice and can be used to simulate any other agent with arbitrary number of principal ports. For instance, it allows to define a formula_65 boolean operation that returns true if any of its arguments is true, independently of the computation taking place in the other arguments.