5
$\begingroup$

The church-encoding for natural numbers is a natural mean of implementing addition, multiplication and so on on the lambda calculus. Interaction nets are said to be an alternative universal computation system, yet, nothing is published as to how one could encode simple data structures and algorithms on the interaction nets directly. What are the natural encodings of numbers and numeric algorithms on interaction combinators?

$\endgroup$
  • $\begingroup$ I don't think the ds.algorithms tag is appropriate here. It is quite likely that no-one following that tag even knows what interaction combinators are. Also, I do not see the relevance of the turing-machines tag. $\endgroup$ – Damiano Mazza Sep 27 '15 at 21:39
  • $\begingroup$ Mazza, you know you could probably have edited those tags out, I just didn't know what tags apply. A tag for interaction nets and/or reduction strategies would be interesting, but I guess I can't create new tags yet. $\endgroup$ – MaiaVictor Sep 28 '15 at 13:26
8
$\begingroup$

Contrarily to the $\lambda$-calculus, the interaction combinators have no underlying logical system (i.e., there is no Curry-Howard correspondence for them), it is therefore hard to say that a numeral system is more "natural" than another.

(In the $\lambda$-calculus, Church numerals may be claimed to be "natural" because their type is the erasure of the second order definition of natural number, i.e.

$\mathsf{Nat}(x) := \forall X.(X(0)\Rightarrow\forall y.(X(y)\Rightarrow X(Sy))\Rightarrow X(x)).$

If you erase all quantifiers and first-order terms, you get $X\to(X\to X)\to X$, which is exactly the simple type of Church integers, perhaps modulo a permutation, i.e. $(X\to X)\to X\to X$ also works. But even in the $\lambda$-calculus there are lots of other numeral systems which may be preferred to the Church integers in some cases).

Anyhow, there are at least a couple of reasons why no-one bothered to explicitly define a numeral system for the interaction combinators:

  • the interaction combinators are studied more as an abstract model of computation than an actual programming language in which one wants to explicitly code algorithms; more general interaction net systems, in which one defines the agents and the interaction rules arbitrarily, are much more suitable for explicit programming (as shown for instance in Lafont's very first paper on interaction nets, POPL 1990), just like a functional language with a primitive integer type and fixpoint definitions (a la PCF) is better for real-life programming than the bare $\lambda$-calculus.
  • if you really want to, it is fairly straightforward to find numeral systems in the interaction combinators. It is well known (see for instance Barendregt's The Lambda Calculus book, Sect. 6.4) that in a language allowing arbitrary recursive definitions (such as the interaction combinators), Turing-completeness is ensured as soon as one is able to define zero, successor, if-then-else (with test for zero) and predecessor. It doesn't take much to find a numeral system satisfying the above. The quickest solution I came up with in 5 minutes is to mimick Scott numerals (another numeral system in the $\lambda$-calculus). Scott numerals have the advantage of being linear, so they may be encoded in multiplicative proof nets, which in turn are essentially the $\gamma\varepsilon$ fragment of the interaction combinators. This is nice because these numerals will be duplicable without problems (by $\delta$ cells). Here are the definitions:

Scott numerals in the interaction combinators

where $\mathbf M_3$ and $\mathbf M_3^\ast$ are the multiplexor and demultiplexor of rank 3 as defined in Lafont's Interaction Combinators paper (I&C, 1995). They both consist of two $\gamma$ cells and they annihilate with each other generating 3 parallel wires.

$\endgroup$
  • $\begingroup$ Sorry, I'm afraid I switched the $b$ and $c$ wires in the ifz-then-else net. I don't feel like changing the picture now, I'll do it whenever I have some time. Anyway, the net currently given above encodes "ifz a then c else b". $\endgroup$ – Damiano Mazza Sep 27 '15 at 21:57

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.