2
$\begingroup$

It is widely known that interaction combinators can implement any interaction net. My question is, can they do so efficiently? I.e., is it possible to prove that there is no interaction net system that can't be emulated on interaction combinators with the same number of reductions up to a finite constant?

$\endgroup$
3
$\begingroup$

The answer is yes. It is an immediate consequence of the definition of translation used by Lafont in his paper introducing the interaction combinators.

A Lafont translation $\Phi$ from an interaction net system to another is an arity-preserving map from the symbols (i.e. the atomic agents) of the first system to principal nets of the other. Basically, a principal net of arity $n$ is a "tree" of agents with some leaves connected to each other and with exactly $n$ free leaves. In particular, it has exactly one free principal port and $n$ free auxiliary ports, so it may be seen as a "macro-agent". See Lafont's paper for the exact definition.

A translation $\Phi$ must also satisfy the following simulation property: for all symbols (i.e. agents) $\alpha,\beta$ of the source system,

$$\alpha\bowtie\beta\to\nu\qquad\text{implies}\qquad\Phi(\alpha)\bowtie\Phi(\beta)\to^\ast\Phi(\nu)$$

where the notation $\alpha\bowtie\beta$ stands for an active pair, and $\Phi(\alpha)\bowtie\Phi(\beta)=\Phi(\alpha\bowtie\beta)$ for its translation.

Now, let $M$ be the longest simulating reduction $\Phi(\alpha)\bowtie\Phi(\beta)\to^\ast\Phi(\nu)$ (such $M$ exists because the number of possible active pairs is finite). It is clear that, if $\mu\to^\ast\mu'$ in $n$ steps the source system, then $\Phi(\mu)\to^\ast\Phi(\mu')$ in at most $M\cdot n$ steps in the target system. This is stated as Proposition 4 in Lafont's paper. So the simulation is efficient according to the notion of efficiency given in the question.

The interaction combinators are universal in the sense that every system of interaction nets may be translated in the interaction combinators, in the above sense. Hence the claim.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.