# Optimal Reduction in Interaction Calculus

We work in interaction calculus.

Let $\Sigma = \{\lambda, \psi, \delta, \epsilon\}$, $\text{Ar}(\lambda) = \text{Ar}(\psi) = \text{Ar}(\delta) = 2$, and $\text{Ar}(\epsilon) = 0$.

For any $\alpha \in \Sigma$, $\beta \in \{\psi, \delta\}$, $\alpha \neq \beta$, and $\text{Ar}(\alpha) = n$, we assume

$\alpha[x_1, \dots, x_n] \bowtie \alpha[x_1, \dots, x_n];$

$\alpha[\delta(x_1, y_1), \dots, \delta(x_n, y_n)] \bowtie \beta[\alpha(x_1, \dots, x_n), \alpha(y_1, \dots, y_n)];$

$\alpha[\epsilon, \dots, \epsilon] \bowtie \epsilon.$

Any $\lambda$-term $M$ can be mapped into a configuration $\Gamma(M, x)$ as follows:

$\Gamma(y, x) = \{x = y\};$

$\Gamma(\lambda y.M, x) = \{x = \lambda(y, z)\} \cup \Gamma(M, z);$

$\Gamma(M\ N, x) = \{y = \lambda(z, x), t_1 = \psi(t'_1, t''_1), \dots, t_n = \psi(t'_n, t''_n)\} \cup \Gamma(M', y) \cup \Gamma(N', z),$

where

$M' = M[t_1 := t'_1]\dots[t_n := t'_n];$

$N' = N[t_1 := t''_1]\dots[t_n := t''_n];$

$\{t_1, \dots, t_n\} = \text{FV}(M) \cap \text{FV}(N).$

Does the resulting interaction system implement optimal reduction?

-
have you found an answer? –  Viclib Aug 13 at 2:32
Not quite yet. But I modified the interaction system to arxiv.org/pdf/1304.2290v8.pdf and successfully tested it using software implementation github.com/euromake/p2pinet . What I know is that the resulting system implements call-by-need strategy and embeds read-back. It might be possible to show operational equivalence to sciencedirect.com/science/article/pii/S1571066106000934 , but the question regarding optimality by Levy is still open. I would suggest that it should have a negative answer by providing a counterexample which unshares a beta-redex during reduction. –  Anton Salikhmetov Aug 13 at 5:56