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 back lambda terms from normalized interaction nets. For example, this net:



Reads back as λλ(1 0), that is, the church-number 1. This net:



Reads back as λλ(1 (1 (1 (1 0)))), the church-number 4. This net:



Reads back as λλ((1 λλ(1 0)) ((1 λλ(1 (1 0))) ((1 λλ(1 (1 (1 0)))) 0))), the church list of the numbres 1, 2 and 3. The readback procedure is trivial, but it uses the tag annotations: λ for a lambda node, @ for an application, R for root, e for garbage, D for fan (duplication). Now, suppose that we erased those tags:





Is it possible, from the configuration of the net alone, to infer the tags and thus readback the same lambda term without them?
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 the same tag (here, I use 0), and you can infer which is the case based on their positions. Each Duplication node, though, requires an unique tag. Note some terms such as (2 2) will reduce to a net which has Duplication nodes with the same tag. That is not an issue; when decoding, just treat anything with a tag different from 0 as a Duplication node.