Interaction nets

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. 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^[2] and optimal, in Lévy's sense, Lambdascope.^[3]

Interactions nets are graph-like structures consisting of agents and edges.

An agent of type α {\displaystyle \alpha } and with arity ar ( α ) = n ≥ 0 {\displaystyle {\text{ar}}(\alpha )=n\geq 0} has one principal port and n {\displaystyle n} auxiliary ports. Any port can be connected to at most one edge. Any edge is connected to exactly two ports. 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 Σ {\displaystyle \Sigma } called signature.

An interaction net that consists solely of edges is called a wiring and usually denoted as ω {\displaystyle \omega } . A tree t {\displaystyle t} with its root x {\displaystyle x} is inductively defined either as an edge x {\displaystyle x} , or as an agent α {\displaystyle \alpha } with its free principal port x {\displaystyle x} and its auxiliary ports x i {\displaystyle x_{i}} connected to the roots of other trees t i {\displaystyle t_{i}} .

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 Σ {\displaystyle \Sigma } (with ar : Σ → N {\displaystyle {\text{ar}}:\Sigma \rightarrow \mathbb {N} } defined on it) along with a set of interaction rules defined for agents α ∈ Σ {\displaystyle \alpha \in \Sigma } together constitute an interaction system.

Textual representation of interaction nets is called the interaction calculus^[4] and can be seen as a programming language.

Inductively defined trees correspond to terms t ::= α ( t 1 , … , t n )   |   x {\displaystyle t::=\alpha (t_{1},\dots ,t_{n})\ |\ x} in the interaction calculus, where x {\displaystyle x} is called a name.

Any interaction net N {\displaystyle N} can be redrawn using the previously defined wiring and tree primitives as follows:

which in the interaction calculus corresponds to a configuration

c ≡ ⟨ t 1 , … , t m   |   v 1 = w 1 , … , v n = w n ⟩ {\displaystyle c\equiv \langle t_{1},\dots ,t_{m}\ |\ v_{1}=w_{1},\dots ,v_{n}=w_{n}\rangle } ,

where t i {\displaystyle t_{i}} , v i {\displaystyle v_{i}} , and w i {\displaystyle w_{i}} are arbitrary terms. The ordered sequence t 1 , . . . , t m {\displaystyle t_{1},...,t_{m}} in the left-hand side is called an interface, while the right-hand side contains an unordered multiset of equations v i = w i {\displaystyle v_{i}=w_{i}} . Wiring ω {\displaystyle \omega } translates to names, and each name has to occur exactly twice in a configuration.

Just like in the λ {\displaystyle \lambda } -calculus, the interaction calculus has the notions of α {\displaystyle \alpha } -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 α {\displaystyle \alpha } -conversion. In turn, substitution t [ x := u ] {\displaystyle t[x:=u]} is the result of replacing the name x {\displaystyle x} in a term t {\displaystyle t} with another term u {\displaystyle u} if x {\displaystyle x} has exactly one occurrence in the term t {\displaystyle t} .

Any interaction rule can be graphically represented as follows:

where α , β ∈ Σ {\displaystyle \alpha ,\beta \in \Sigma } , and the interaction net N {\displaystyle N} on the right-hand side is redrawn using the wiring and tree primitives in order to translate into the interaction calculus as α [ v 1 , … , v m ] ⋈ β [ w 1 , … , w n ] {\displaystyle \alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]} 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 α [ v 1 , … , v m ] ⋈ β [ w 1 , … , w n ] {\displaystyle \alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]} , the following reduction:

⟨ t →   |   α ( t 1 , … , t m ) = β ( u 1 , … , u n ) , Δ ⟩ → ⟨ t →   |   t 1 = v 1 , … , t m = v m , u 1 = w 1 , … , u n = w n , Δ ⟩ {\displaystyle \langle {\vec {t}}\ |\ \alpha (t_{1},\dots ,t_{m})=\beta (u_{1},\dots ,u_{n}),\Delta \rangle \rightarrow \langle {\vec {t}}\ |\ t_{1}=v_{1},\dots ,t_{m}=v_{m},u_{1}=w_{1},\dots ,u_{n}=w_{n},\Delta \rangle }

is called interaction. When one of equations has the form of x = u {\displaystyle x=u} , indirection can be applied resulting in substitution of the other occurrence of the name x {\displaystyle x} in some term t {\displaystyle t} :

⟨ … t …   |   x = u , Δ ⟩ → ⟨ … t [ x := u ] …   |   Δ ⟩ {\displaystyle \langle \dots t\dots \ |\ x=u,\Delta \rangle \rightarrow \langle \dots t[x:=u]\dots \ |\ \Delta \rangle } or ⟨ t →   |   x = u , t = w , Δ ⟩ → ⟨ t →   |   t [ x := u ] = w , Δ ⟩ {\displaystyle \langle {\vec {t}}\ |\ x=u,t=w,\Delta \rangle \rightarrow \langle {\vec {t}}\ |\ t[x:=u]=w,\Delta \rangle } .

An equation x = t {\displaystyle x=t} is called a deadlock if x {\displaystyle x} has occurrence in term t {\displaystyle t} . Generally only deadlock-free interaction nets are considered. Together, interaction and indirection define the reduction relation on configurations. The fact that configuration c {\displaystyle c} reduces to its normal form c ′ {\displaystyle c'} with no equations left is denoted as c ↓ c ′ {\displaystyle c\downarrow c'} .

Interaction nets benefit from the following properties:

• locality (only active pairs can be rewritten);
• linearity (each interaction rule can be applied in constant time);
• strong confluence also known as one-step diamond property (if c → c 1 {\displaystyle c\rightarrow c_{1}} and c → c 2 {\displaystyle c\rightarrow c_{2}} , then c 1 → c ′ {\displaystyle c_{1}\rightarrow c'} and c 2 → c ′ {\displaystyle c_{2}\rightarrow c'} for some c ′ {\displaystyle c'} ).

These properties together allow massive parallelism.

One of the simplest interaction systems that can simulate any other interaction system is that of interaction combinators. Its signature is Σ = { ϵ , δ , γ } {\displaystyle \Sigma =\{\epsilon ,\delta ,\gamma \}} with ar ( ϵ ) = 0 {\displaystyle {\text{ar}}(\epsilon )=0} and ar ( δ ) = ar ( γ ) = 2 {\displaystyle {\text{ar}}(\delta )={\text{ar}}(\gamma )=2} . Agent ϵ {\displaystyle \epsilon } can be seen as an eraser, deleting resources; δ {\displaystyle \delta } as a duplicator; γ {\displaystyle \gamma } as a constructor, taking two resources and returning some third one- it can represent anything from binary operations, as addition and multiplication, up to general function application in the lambda calculus, taking terms f {\displaystyle f} and x {\displaystyle x} to produce f x {\displaystyle f\,x} .^[5] Interaction rules for these agents are:

• ϵ ⋈ α [ ϵ , … , ϵ ] {\displaystyle \epsilon \bowtie \alpha [\epsilon ,\dots ,\epsilon ]} called erasing;
• δ [ α ( x 1 , … , x n ) , α ( y 1 , … , y n ) ] ⋈ α [ δ ( x 1 , y 1 ) , … , δ ( x n , y n ) ] {\displaystyle \delta [\alpha (x_{1},\dots ,x_{n}),\alpha (y_{1},\dots ,y_{n})]\bowtie \alpha [\delta (x_{1},y_{1}),\dots ,\delta (x_{n},y_{n})]} called duplication;
• δ [ x , y ] ⋈ δ [ x , y ] {\displaystyle \delta [x,y]\bowtie \delta [x,y]} and γ [ x , y ] ⋈ γ [ y , x ] {\displaystyle \gamma [x,y]\bowtie \gamma [y,x]} called annihilation.

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:

⟨ ∅   |   δ ( ϵ , x ) = γ ( x , ϵ ) ⟩ → ⟨ ∅   |   ϵ = γ ( x 1 , x 2 ) ,   x = γ ( y 1 , y 2 ) ,   x = δ ( x 1 , y 1 ) ,   ϵ = δ ( x 2 , y 2 ) ⟩ → ∗ ⟨ ∅   |   x 1 = ϵ ,   x 2 = ϵ ,   x = γ ( y 1 , y 2 ) ,   x = δ ( x 1 , y 1 ) ,   x 2 = ϵ ,   y 2 = ϵ ⟩ → ∗ ⟨ ∅   |   δ ( ϵ , x ) = γ ( x , ϵ ) ⟩ → … {\displaystyle {\begin{aligned}&\langle \varnothing \ |\ \delta (\epsilon ,x)=\gamma (x,\epsilon )\rangle \rightarrow \\&\langle \varnothing \ |\ \epsilon =\gamma (x_{1},x_{2}),\ x=\gamma (y_{1},y_{2}),\ x=\delta (x_{1},y_{1}),\ \epsilon =\delta (x_{2},y_{2})\rangle \rightarrow ^{*}\\&\langle \varnothing \ |\ x_{1}=\epsilon ,\ x_{2}=\epsilon ,\ x=\gamma (y_{1},y_{2}),\ x=\delta (x_{1},y_{1}),\ x_{2}=\epsilon ,\ y_{2}=\epsilon \rangle \rightarrow ^{*}\\&\langle \varnothing \ |\ \delta (\epsilon ,x)=\gamma (x,\epsilon )\rangle \rightarrow \dots \end{aligned}}}

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 amb {\displaystyle {\text{amb}}} ^[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. For instance, it allows to define a ParallelOr {\displaystyle {\text{ParallelOr}}} boolean operation that returns true if any of its arguments is true, independently of the computation taking place in the other arguments.

• Geometry of interaction
• Graph rewriting
• Lambda calculus
• Linear graph grammar
• Linear logic
• Proof net

• Asperti, Andrea; Guerrini, Stefano (1998). The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science. Vol. 45. Cambridge University Press. ISBN 9780521621120.
• Fernández, Maribel (2009). "Interaction-Based Models of Computation". Models of Computation: An Introduction to Computability Theory. Springer Science & Business Media. pp. 107–130. ISBN 9781848824348.

• de Falco, Marc. "tikz-inet. A set of tikz-based macros for drawing interaction nets".
• de Falco, Marc. "INL. Interaction Nets Laboratory".
• Vilaça, Miguel. "INblobs. An editor and interpreter for Interaction Nets".
• Asperti, Andrea. "The Bologna Optimal Higher-Order Machine". GitHub.
• Salikhmetov, Anton (22 March 2018). "JavaScript Engine for Interaction Nets".
• Salikhmetov, Anton. "Macro Lambda Calculus".
• Xie, Yuheng. "iNet, a language and interactive playground for exploring interaction nets".