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 ...
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 ...
- 5,273
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 ...
- 5,273
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 ...
- 5,273
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 ...
- 5,273
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 ...
- 686
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 ...
- 3,117
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 ...
- 5,273
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.
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 ...
- 11.7k
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,177
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,177
Only top scored, non community-wiki answers of a minimum length are eligible