# Tagged Questions

143 views

### Interaction-based approximation for HP-complete λ-theory?

We are looking for a proof or counter-examples for the following hypothesis. Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either  \exists ...
We are looking for a proof or counter-examples to the following Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ ... 0answers 149 views ### Is it possible to implement η-reduction in interaction nets? There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the ... 0answers 60 views ### 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 ...
Let us call primitive an interaction system with the signature $\Sigma = \{(\rho, 0), (\xi, n)\}, \quad n \geq 2;$ and the only rule being of the form \$\rho \bowtie \xi[\rho, \xi(a_1, \dots , a_n), ...