4 votes
Accepted

Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?

For question 1, if by "deadlock" you mean "non-trivial vicious circle", then the answer is obviously yes, simply because a non-trivial vicious circle cannot be typed: you will have a cut between a ...
Damiano Mazza's user avatar
4 votes
Accepted

What, in simple terms, are the restrictions imposed by Elementary Affine Logic?

The terms "stratification" and "boxes" come from proof nets. Elementary linear logic ($\mathbf{ELL}$) was originally introduced by Girard as a variant of light linear logic ($\mathbf{LLL}$) and its ...
Damiano Mazza's user avatar
4 votes

Is there a "lambda cube" for interaction nets?

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 ...
Damiano Mazza's user avatar
3 votes
Accepted

Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

This does not answer your main question but concerns the following point: I'm looking for an equivalence on interaction nets that implies lambda calculus read-back equivalence, but that also ...
Damiano Mazza's user avatar
3 votes

Is it possible to unambiguously read back λ terms from interaction nets without node types?

So, yes, turns out it is possible, as can be seen on the decode function of my abstract algorithm implementation here. Basically, Lambda and Apply nodes are given ...
MaiaVictor's user avatar
  • 3,147
3 votes
Accepted

Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?

Your observation about cut-elimination being faithfully represented in the unlabelled interaction nets is correct. However, the answer to your question is no. Let us call $\delta$ the unique agent ...
Damiano Mazza's user avatar
2 votes

Semantic read-back of sharing graphs

I do not have a proper answer, but you might want to have a look at this paper by Asperti where there is a study of sharing graphs inspired by category theory.
Beniamino Accattoli's user avatar
1 vote

Bad Cycles in Interaction Nets

Quoting from the paper: It is possible to define rules which lead to non-terminating computations, [...] but further constraints on nets can ensure that when a sequence of reductions terminates, the ...
D.W.'s user avatar
  • 12.1k
1 vote

Extending EAL with recursion makes it incompatible with the abstract algorithm?

The term that you gave does have one duplication, i.e.: ones is used in the body and returned in form of a free variable. The following example illustrates the same ...
Łukasz Lew's user avatar
  • 1,187
1 vote
Accepted

Is there a "lambda cube" for interaction nets?

The Structure of Interaction paper seems to be what you are asking for.
Łukasz Lew's user avatar
  • 1,187

Only top scored, non community-wiki answers of a minimum length are eligible