5
$\begingroup$

The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about interaction combinators?

$\endgroup$
  • 1
    $\begingroup$ I doubt it. There is not much research on interaction nets. It should be possible to look at it all. $\endgroup$ – Martin Berger Feb 4 '16 at 11:24
1
$\begingroup$

The Structure of Interaction paper seems to be what you are asking for.

$\endgroup$
  • $\begingroup$ Maybe, but I'm not so sure I make the connection between what is presented on this paper and my understanding of the λ-cube and dependent types. For example, how'd you express dependent types, things like the λ (t : *) -> λ (x : t) -> x term (Morte syntax)? $\endgroup$ – MaiaVictor Sep 22 '17 at 23:58
4
$\begingroup$

Like Martin said, nothing like an equivalent for the $\lambda$-cube has ever been developed for interaction nets or interaction combinators.

The only work that considers types for interaction nets is Lafont's original paper [1]. (My own CONCUR 2005 paper also considers types but adds nothing new to what Lafont did). It is an extremely simple system: only basic types plus a polarity, no type constructors at all. Nevertheless, it is enough to obtain a desirable safety property: a well typed net cannot reduce to a net containing a "clash" (an active pair which does not have a corresponding reduction rule and is therefore "stuck").

Of course, since multiplicative linear logic proof nets are a particular system of interaction nets, it is defintely possible to equip certain systems of interaction nets with more complex types, using non-trivial type constructors. But nothing has ever been studied, mostly because the interest of such an endevour is unclear.

[1] Yves Lafont, Interaction Nets. In Proceedings of POPL, 1990.

$\endgroup$
  • 1
    $\begingroup$ One more thing: this year at POPL, Stéphane Gimenez and Georg Moser had a paper using interaction nets (for studying complexity properties). I missed their talk and haven't yet seen the paper, but it's possible that it contains some new work on types for interaction nets, although I doubt it is anything in the style of the $\lambda$-cube types. $\endgroup$ – Damiano Mazza Feb 4 '16 at 12:17
  • $\begingroup$ So my question is more in the lines - interaction nets aren't as useful for proofs and related as the λ-calculus, I guess? $\endgroup$ – MaiaVictor Feb 4 '16 at 12:26
  • 1
    $\begingroup$ @DamianoMazza Lafont's POPL paper is available electronically here and, if you can access the ACM library, here. $\endgroup$ – Martin Berger Feb 5 '16 at 8:37
  • $\begingroup$ @MartinBerger That's great, thank you! The last time I checked there was no electronic copy freely available, but it was a long time ago, somebody must have scanned it in the meantime! $\endgroup$ – Damiano Mazza Feb 5 '16 at 10:01

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.