Questions tagged [interaction-nets]
The interaction-nets tag has no usage guidance.
14
questions
7
votes
1
answer
94
views
Semantic read-back of sharing graphs
A "sharing graph" is a representation of a $\lambda$-term that modifies an abstract syntax tree by adding edges connecting each variable use to the place where that variable is bound. They are used ...
1
vote
1
answer
83
views
Extending EAL with recursion makes it incompatible with the abstract algorithm?
A few years ago, I've asked if Elementary Affine Logic can be used as the core type system of a practical programming language. The accepted answer argues that, yes, although such language would be ...
- 4,501
5
votes
0
answers
158
views
Upward confluence in the interaction calculus
The lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations $c_1$ and $c_2$ such ...
7
votes
1
answer
221
views
Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?
In Multiplicative Linear Logic (MLL), addition of the mix rule eliminates 'connectedness' from Danos-Regnier criterion. I'm investigating how the criterion changes if we do not distinguish between ...
- 4,783
4
votes
1
answer
86
views
Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?
There are various criteria for the correctness of multiplicative proof nets.
In Correctness of Multiplicative Proof Nets is Linear, Stefano Guerrini nicely describes few of them with an efficient ...
- 4,783
5
votes
2
answers
376
views
Is there a "lambda cube" for interaction nets?
The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about ...
- 1,147
7
votes
1
answer
210
views
Is it possible to unambiguously read back λ terms from interaction nets without node types?
A class of lambda terms can be evaluated using Lamping's abstract algorithm - that is, converting them to interaction nets and applying a set of rules. In order to get the result, you have to read ...
CommunityBot
- 1
4
votes
1
answer
242
views
What, in simple terms, are the restrictions imposed by Elementary Affine Logic?
The answer to my last question on the subject made several insightful points on how EAL could be used as the basis of a practical programming language, which, in turn, could be evaluated using the ...
- 4,783
1
vote
0
answers
48
views
Efficient compilation of interaction combinators with infinite cell types to usual interaction combinators?
It is known that interaction combinators can implement any interaction net system efficiently. Now, let us define a modification of interaction combinators, which, instead of two types of fan cells, ...
- 3,045
11
votes
1
answer
1k
views
Are optimal evaluators actually optimal?
The following term (using bruijn-indexes):
BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0)))))))))
...
5
votes
1
answer
87
views
Is it possible to evaluate interaction combinators efficiently using a path-traveling strategy?
Interaction combinators can be evaluated using a path traversing strategy. That is, instead of applying annihilation/commutation rules to active pairs, one simply walks through the graph using a 2-...
- 676
4
votes
0
answers
65
views
Is the question about closed reduction using token-passing nets still open?
The question about possible implementation of closed reduction using token-passing nets is asked on page 17 in Token-passing Nets for Functional Languages by Jose Bacelar Almeida, Jorge Sousa Pinto, ...
1
vote
0
answers
166
views
Optimal reduction using token-passing nets
I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in the spirit of "Token-Passing Nets: Call-by-Need for Free" by François-Régis ...
10
votes
1
answer
807
views
How do you encode Lamping's abstract algorithm using interaction combinators?
Interaction combinators have been proposed as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to optimize interaction-net ...
- 4,783