Overview

In this post we will introduce polarized interaction systems. These can be seen as a very simple type system on interaction nets that restricts which nets we can consider valid. We'll then use this notion to more clearly understand the 2-SIC encoding. Then, we'll use polarity to understand how we can read back interaction nets as lambda calculus terms. Finally, we'll see that there is a natural extension of lambda calculus by expanding how we interpret interaction nets as lambda calculus terms.

Readback

Motivation

Previously, we introduced the 2-SIC system as a way to encode and reduce a subset of the lambda calculus. One critical point we glossed over is how we translate normalized interaction nets back into lambda calculus terms. This process is known as read back.

This algorithm is not immediately intuitive because we encode different lambda calculus constructs into the same kind of node. For example, consider the following normalized interaction net:

How do we know what lambda calculus term this net represents? Let's try understanding what lambda calculus term is at the head of this net. That is, is node an abstraction or an application?

Intuition

Ignoring erasures and duplications for a moment, let's recall our 2-SIC translation which maps lambda calculus terms to 2-SIC nets:

From looking at the definition of our translation, can you now tell which lambda calculus term is at the head of the net in Figure 1?

The head of the term in Figure 1 has to be an abstraction: . This is because the term is identified by the principal port of a constructor node. In a constructor node representing an application, the principal port consumes a function. So, this port cannot be used to refer to the head of any lambda calculus term, as there is no notion of an expectation of a term in lambda calculus.

On the other hand, the principal port of a constructor node representing an abstraction produces a lambda calculus term. Thus, this port can be used to refer to the head of a lambda calculus term.

The formalization of ports either producing or consuming terms is polarization.

Polarized Interaction Systems

Polarizing SIC Nodes

A polarized interaction system is a refinement of an interaction system. For each kind of node, we define (possibly multiple) classifications of its ports as either producers or consumers.

In Franchu's post on read back, polarization is described as a labeling of ports as "positive" or "negative", where positive ports are producers and negative ports are consumers. While I will also use this terminology here, I find it very useful to draw polarity using arrows, where the direction goes from positive to negative. That is, the arrow starts at a producer and ends at a consumer.

For each of the three 2-SIC nodes, we will have two possible polarizations:

Note that these labels are just to identify the polarizations, there are still only three kinds of nodes:

Some things to note:

• The rewrite rules are unchanged.
• Each polarization has a dual (e.g. ), where the polarization of each wire is flipped.
• An outgoing arrow can be seen as producing a value.
• An incoming arrow can be seen as consuming a value.

• The Greek letters are intended to refer to the following names in English:

  • : Null
  • : Erasure
  • : Application
  • : Abstraction
  • : Duplication
  • : Superposition

An Example Polarized Term

Let's look at the polarization of the term discussed in the previous post, :

While I've labeled nodes with their polarization symbols ( , , etc.), these labels can be inferred by inspecting the polarization alone, given that the lone free wire is positive. This is the essence of reading 2-SIC nets back as lambda calculus terms.

An Algorithm for Readback

Since we always identify terms through an open wire at the positive end, we can always infer the polarizations of the nodes in the entire net. This is because if we know the polarity of a single port and the kind of 2-SIC node (eraser, constructor, duplication) we are looking at, then we also know the polarization of the entire node. This is precisely due to the fact that each kind of node has two dual polarizations. If there were more polarizations for a given kind of node, we would not necessarily be able to infer the polarization of the entire node knowing only a single port's polarity. Knowing a node's polarization then also lets us know which lambda calculus construct the node corresponds to.

This algorithm for readback is of course specific to 2-SIC, but can also be applied in other contexts where polarity is relevant.

Understanding the 2-SIC Polarizations

Abstraction and Application

Let's go through abstraction and application polarizations first, as I believe these to be the most intuitive. In lambda calculus, the term is an application that consumes two terms, and , and produces one. Thus, we expect two ports with incoming arrows (negative) and one port with an outgoing arrow (positive):

The reason for the principal port of the constructor node to receive the function – as opposed to one of the auxiliary ports – is to create an active pair or reducible expression when is an abstraction. That is, we want the lambda calculus term to be translated into an active pair when a beta-reduction is possible, which is only when is an abstraction.

When encoding an application, we connect the single positive wire to the occurence of the application in the net.

Dually, an abstraction consumes a term but it produces two, and :

While it might be strange to see a variable described as a term, can be placed anywhere a term can, and thus can be seen as one.

Similarly to applications, when encoding an abstraction, we connect the single positive wire to the occurence of the abstraction in the net.

Erasure and Duplication

Erasure and duplication are two more polarizations of nodes that are in the image of our 2-SIC translation . For example, erasers appear when we create abstractions that do not use their variables:

And duplications appear when using a variable more than once:

In terms of producers and consumers, erasure is a consumer. It is – sensibly – not a value. Duplication, however, is both a consumer and a producer. It produces two values, which also makes sense as it consumes its argument to produce two copies of it.

Null

In a type system for the lambda calculus, if a term is well-typed, intermediate terms found during reduction are also well-typed. Ideally, valid polarized nets should also have a similar property: if an initial net is valid, all intermediate nets during reduction should also be valid. At a minimum, this can be used to read back nets during reduction, and not only after it.

The problem here is that the four polarizations we have detailed above (abstraction, application, erasure, and duplication) are not sufficient to obtain this property. For example, when erasing the identity function :

This intermediate term has an eraser node with a negative polarity, but on the other end is also an eraser node, which thus must have a positive polarity. Nets with a positive free port can be seen as values. This positive eraser can be interpreted as a new kind of term that represents a "null" value. It's important to emphasize that this positive eraser does not appear when translating lambda calculus terms, only when reducing them.

Superposition

Duplication nodes have a similar situation. When duplicating the identity function, the commutation rewrite rule necessarily results in two duplication nodes that have opposite polarities:

This intermediate term has two duplication nodes connected via their principal port. They therefore must have different polarizations. When looking at this dual of the duplication node, it consumes two values and produces one, but the consumed values are symmetric. That is, both of the consumed values go into aux ports, unlike in an application where one consumed value goes into an aux port and one into a principal port. Because of the commutation rules, this can be seen as a single term with two values, or a superposition.

Extending Lambda Calculus

Null and Superpositions as Terms

As we saw above, there are two polarizations that are only present in intermediate nets. What if we allowed for these polarizations to appear in the image of ? That would require us to add some new lambda calculus terms that map to null values (positive erasers), and superpositions (dual of duplication).

Null values can be described as a term with an additional beta-reduction rule:

This is very similar to a bottom term as it "infects" or "destroys" the computation.

Superpositions are a new term with the following beta-reduction rule¹:

Superpositions are especially interesting as they are like a pair but with some auto-vectorization properties. Specifically, applying a superposition of functions to an argument reduces to a superposition of applications. Additionally, applying a function to a superposition of arguments is equivalent² to a superposition of applications:

Aside: Unscoped Lambdas

Yet another extension – that doesn't really come out of polarity – is that of unscoped lambdas. I'd like to discuss these more deeply at some point, but in short: interaction nets do not require you to connect the wire of an abstraction's variable to somewhere in its body. You are free to connect them anywhere else in the net, resulting in a sort of "use-once channel" where data can be sent and read. A term like this for example:

where is an unscoped variable that is being referenced outside of this body. Can you figure out what this term normalizes to?³ Try normalizing the interaction net and reading back the result.

Conclusion

We've seen how polarity can be used to read back interaction nets as lambda calculus terms, by uniquely identifying which lambda calculus constructs correspond to which nodes. We've also seen that there are some additional polarizations of nodes that are not present in the image of our 2-SIC translation. These two additional polarizations can be used to extend the lambda calculus with some new interesting terms.

I'd like to eventually extend the discussion on superpositions to how they can be used – along with the beta-optimal properties of interaction nets – to efficiently perform program search.

---