6 votes
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 ...
user avatar
6 votes
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 ...
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 ...
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 ...
user avatar
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 ...
user avatar
3 votes
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 ...
user avatar
  • 676
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 ...
user avatar
  • 3,045
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 ...
user avatar
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.
user avatar
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 ...
user avatar
  • 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.
user avatar
  • 1,147

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