Reading back inets in a single pass
Interaction Nets are a model of computation. There exist an interaction sysatem that can be used to implement the λ-calculus. In this article I'll discuss a readback algorithm that can be used to read an interaction net into a λ-calculus term.
This article assumes that the reader is somewhat familiar with the symmetric interaction calculus.
Polarity
A very important concept that springs up when talking about readback is polarity. It turns out that the interaction nets that correspond to λ-calculus terms can be polarized. A polarization of an interaction net is a labeling of ports with either + or -, such that all wires connect a + port and a - port. Each agent type has a fixed polarization for its ports.
For the purposes of polarization, CON agents are not always the same CON agent type, but sometimes they represent LAM agents and sometimes they represent APP agents, depending on context. Similarly, DUP agents are either DUP agents or SUP agents, depending on context.
Later on, we will see how the readback algorithm always has enough information to distinguish between DUP/SUP and LAM/APP when reaching a node.
SIC Polarization
For inets representing λ-calculus, +-polarized ports will represent ports that "produce" terms, while --polarized ports will represent ports that "consume" terms.
It's important to concretely define what is meant by "produce" and "consume" here. Does a LAM node "produce" or "consume" its argument? A common interpretation is "well, a LAM node is simply waiting to 'eat' an argument from an APP node, so it definitely consumes an argument". But that's not the definition that's used to define + and -. Polarity does not depend on what will happen to the node; it only depends on what it currently represents in the λ-calculus AST. Thanks to the LAM node, there's a variable that can be used somewhere else. This means that the LAM node produced the variable.
So, for example, a LAM node "produces" an argument and the function, while it "consumes" the body. Given a body term, the LAM node will create an argument and a function that sets the argument and returns the function body. Their polarity is +/+/-.
An APP node is the opposite. It "consumes" the function and an argument, while it "produces" the return value of the function. Given a function and an argument, the APP node can be used to create an application of the function to the argument. Their polarity is -/-/+.
The two CON node variants have opposite polarities. In both of them, the two auxiliary ports have opposite polarities. The fact that they polarity sets are exact opposites of one another means that annihilation between them respects polarity, as shown here.
DUP nodes consume a term from their principal port, and produce two copies of it through their auxiliary port. Their polarity is -/+/+.
SUP nodes consume two terms through their auxiliary ports, and produce their superposition through their principal port. Their polarity is +/-/-
Polarity is what makes terms such as (λx λx (y y)) invalid. x is bound twice and y is used twice.
You can't plug two lambda arguments together. In polarity, this is encoded by the fact that LAM argument ports have positive polarity, and can't be plugged in together.
You also can't plug an application's argument and an application's function. In polarity, this is represented by the application argument and the application function both having negative polarity.
On readback
If a readback algorithm reaches a node through any of its ports, if it knows the polarity of the port it came from, it can deduce the node type variant of the node it reached.
For example, if we reach a CON node through its principal port, coming from a - port, we know the CON node must produce a value through its principal port. This means that the CON node is a LAM node and represents a lambda.
This is because there are no two variants that have the same polarity for any of the nodes. We can use this to write "inference rules" for polarity.
- todo draw inference rules
The algorithm.
We can use this information to write a single-pass algorithm using "inference rules".
We only need two functions: read_neg, which reads from a - port into a + port, and read_pos, which reads from a + port into a - port.
read_pos will take a Tree and a Term, while read_neg will take a Tree and a "term hole" which read_neg will fill.
also read: https://github.com/HigherOrderCO/bend/blob/direct-readback/src/term/readback/linear.rs