# Tag Info

Accepted

### How do you encode Lamping's abstract algorithm using interaction combinators?

I am not aware of any implementation of Lamping's algorithm directly in the interaction combinators. I do know that the presence of integer labels is a necessary feature of Lamping's algorithm, even ...
• 4,823
Accepted

### Are optimal evaluators actually optimal?

Efficiency of optlam I have not studied the details of BADTERM nor of the implementation of optlam evaluator, but I find quite strange that optlam performs a number of ß-interactions drastically ...

### 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 ...
• 4,823
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 ...
• 4,823
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 ...
• 4,823
Accepted

### Is it possible to evaluate interaction combinators efficiently using a path-traveling strategy?

This has been a subject of investigation for the Implicit Computational Complexity (ICC) community recently. It is known that in certain cases, when the graph you want to evaluate is of a specific ...
• 676

### 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,045
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 ...
• 4,823
1 vote

### 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

### 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,147
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,147

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