0
votes
1answer
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 ...
1
vote
1answer
191 views

Hypothesis: interaction-based model for λKβη

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\ |\ ...
2
votes
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 ...
1
vote
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 ...
1
vote
0answers
106 views

Turing-complete primitive interaction systems

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), ...