Interaction nets are a graphical model of computation devised by French mathematician Yves Lafont in 1990[1] as a generalisation of the proof structures of linear logic.
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[2] and optimal, in Lévy's sense, Lambdascope.
[3] Interactions nets are graph-like structures consisting of agents and edges.
Free ports together form the interface of an interaction net.
All agent types belong to a set
An interaction net that consists solely of edges is called a wiring and usually denoted as
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.
Inductively defined trees correspond to terms
can be redrawn using the previously defined wiring and tree primitives as follows:
which in the interaction calculus corresponds to a configuration
-conversion and substitution naturally defined on configurations.
Any interaction rule can be graphically represented as follows:
on the right-hand side is redrawn using the wiring and tree primitives in order to translate into the interaction calculus as
The interaction calculus defines reduction on configurations in more details than seen from graph rewriting defined on interaction nets.
, indirection can be applied resulting in substitution of the other occurrence of the name
Generally only deadlock-free interaction nets are considered.
Together, interaction and indirection define the reduction relation on configurations.
Its infinite reduction sequence starting from the corresponding configuration in the interaction calculus is as follows:
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
[6] 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.
boolean operation that returns true if any of its arguments is true, independently of the computation taking place in the other arguments.