# 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?

-