Token-Passing Net Implementation of Optimal Reduction

[codedot]

In the book "The Optimal Implementation of Functional Programming Languages" by Andrea Asperti and Stefano Guerrini the initial encoding of a λ-term M into an interaction net is a configuration <x | x = [M]₀> where translation [M]_n is inductively defined by the following rules:



The corresponding interaction rules consist of annihilation:



and propagation:



where i < j.

The problem is that, in case of an arbitrary λK-term, reduction of such an interaction net has to avoid interactions in parts of the net that are disconnected from the interface; otherwise, it may not reach the normal form.

It appears that in order to allow safe reduction without restricting evaluation strategy, it is sufficient to change initial encoding to <x | Eval(x) = [M]₀> and β-reduction to @_i[x, y] >< λ_i[Wait(z, Hold(z, x)), y], introducing additional agent types Eval, Wait, Hold, Call and Decide with the following interaction rules:

Eval[λ_i(x, y)] >< λ_i[x, Eval(y)];
Eval[δ_i(x, y)] >< δ_i[x, y];
Eval[x] >< Wait[Eval(x), Call];
Call >< Hold[x, Eval(x)];
δ_i[Wait(x, Amb(y, Decide(z, v), v)), Wait(w, y)] >< Wait[δ_i(x, w), z];
Call >< Decide[Call, ε];
ε >< Decide[x, x];
@_i[x, Wait(y, Hold(@_i(x, y), Wait(v, w)))] >< Wait[v, w];
α[Wait(x, y)] >< Wait[α(x), y],

where α is a bracket or a croissant, and Amb(x, y, z) is McCarthy's amb, x representing its second principle port.

This token-passing net version of optimal reduction is implemented on the optimal branch of the MLC repository.