Read-Back Embedded into Interaction System

http://arxiv.org/pdf/1304.2290v7.pdf

Interaction system of MLC implements token-passing nets and embeds read-back mechanism.

Specifically, starting from initial configuration that encodes a λ-term

<x | r_[ ](x) = y, Γ(M^•, y)>,

the r(ead) agent will trigger duplication and application:

s[c(x, r_{C[ ]}(y)), x] >< r_{C[ ]}[y];
@[λ(x, r_{C[ ]}(y)), x] >< r_{C[ ]}[y];

and will construct normal form of the encoded λ-term:

a_M >< λ[r_{M [ ]}(x), x];
a_M >< r_C[ ][a_C[M]];
λ[a_y, r_C[λy.[ ]](x)] >< r_C[ ][x], where y ∈ Λ is a new variable.

If normal form N of the λ-term exists, interaction results in configuration

<a_N | ∅>

which consists of only one a(tom) agent in its interface.