Share Your Experience: Take the 2024 Developer Survey

# Questions tagged [interaction-nets]

The tag has no usage guidance.

17 questions
Filter by
Sorted by
Tagged with
1 vote
191 views

### What is an efficient algorithm to check for equivalence on symmetric interaction combinators?

Symmetric interaction combinators are a graph-rewriting model of deterministic computation derived from Lafont's interaction nets. In the paper "Observational Equivalence and Full Abstraction in ...
• 3,137
190 views

### Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

Consider the 3 symmetric interaction combinator nets below: Despite being different nets, they are equal, in the sense that, if we view white nodes as lambdas and applications, and black nodes as ...
• 3,137
1 vote
51 views

### Bad Cycles in Interaction Nets

Could someone explain to me the following quote from Interaction Nets 1991 paper by Simon Gay. To be specific, what are bad cycles and how connected ports in the same partition eliminates them? The ...
• 131
138 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 ...
• 675
1 vote
103 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 ...
• 3,137
174 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 ...
280 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 ...
• 1,187
101 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 ...
• 1,187
304 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 ...
• 3,137
470 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 ...
• 3,137
1 vote
74 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,137
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))))))))) ...
• 3,137
108 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-...
• 3,137
68 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
198 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 ...
934 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 ...
• 3,137