# Tag Info

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 ...
• 5,483
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 ...
• 5,483

### 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 ...
• 5,483
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 ...
• 5,483

### 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 ...
• 3,147
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 ...
• 5,483

### 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.
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 ...
• 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 ...
• 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.
• 1,187

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