<p>So, yes, turns out it is possible, as can be seen on the <code>decode</code> function of my abstract algorithm implementation <a href="https://github.com/MaiaVictor/interaction-combinators/blob/master/lambda-encoding.js" rel="nofollow noreferrer">here</a>. Basically, Lambda and Apply nodes are given the same tag (here, I use <code>0</code>), 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 <code>(2 2)</code> 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 <code>0</code> as a Duplication node.</p>

CC BY-SA 3.0
2017-05-27T02:07:16.900Z
2017-05-27T02:07:16.900Z
MaiaVictor
<p>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:</p>

<p><a href="https://i.sstatic.net/ArE3C.png" rel="noreferrer"><img src="https://i.sstatic.net/ArE3C.png" alt="enter image description here"></a></p>

<p>Reads back as <code>λλ(1 0)</code>, that is, the church-number 1. This net:</p>

<p><a href="https://i.sstatic.net/NFPHb.png" rel="noreferrer"><img src="https://i.sstatic.net/NFPHb.png" alt="enter image description here"></a></p>

<p>Reads back as <code>λλ(1 (1 (1 (1 0))))</code>, the church-number 4. This net:</p>

<p><a href="https://i.sstatic.net/IPw2e.png" rel="noreferrer"><img src="https://i.sstatic.net/IPw2e.png" alt="enter image description here"></a></p>

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

<p><a href="https://i.sstatic.net/Z6scU.png" rel="noreferrer"><img src="https://i.sstatic.net/Z6scU.png" alt="enter image description here"></a>
<a href="https://i.sstatic.net/qwpwA.png" rel="noreferrer"><img src="https://i.sstatic.net/qwpwA.png" alt="enter image description here"></a>
<a href="https://i.sstatic.net/5naLt.png" rel="noreferrer"><img src="https://i.sstatic.net/5naLt.png" alt="enter image description here"></a></p>

<p>Is it possible, from the configuration of the net alone, to infer the tags and thus readback the same lambda term without them?</p>

CC BY-SA 3.0
2015-07-26T09:00:12.360Z
The interaction nets used in Lamping's algorithm (which are called *sharing graphs*) are more complex than what you state: nodes are indexed and there are "reindexing" nodes (traditionally called *brackets* and *croissants* because of the graphical notations originally used by Lamping). Is that why you start your question with "[a] class of lambda terms"? I mean, you are only considering a restricted class of $\lambda$-terms which do not use indices (such as those coming from elementary linear logic proof nets)?
Damiano Mazza
CC BY-SA 3.0
2015-07-26T12:00:39.187Z
@DamianoMazza Yes! I'm only considering EAL-typeable terms. (In fact I have hundreds of λ terms including whole list/trees/etc libraries and I'm yet to find one that isn't.) In particular, I'm trying to figure out what is the most efficient way to compute the abstract algorithm. My implementation uses the tags on the nodes, but I suspect those are redundant. I believe all nodes are the same thing mechanically, not 5 different things. Also, the question on how to collect garbage is very important, but there is no good solution on literature. I need that insight to start reasoning about it.
MaiaVictor
CC BY-SA 3.0
2015-07-26T12:33:14.387Z
(There are only 2 reduction rules going on, annihilation and commute, so why would 5 tags (`e`, `λ`, `@`, `D`, `R`), plus a label for fans, be necessary? (The beta rule `λ-@` is exactly the same as annihilation for paired fans `D-D`, and erasure `e-x` is exactly the same as duplication `D-x`). I find it very likely that I can represent all those without the tags - just one node and a simple rule for pairing them.)
MaiaVictor
CC BY-SA 3.0
2015-07-26T16:35:05.183Z
(In fact I noticed I could replace every node by fans with a starting label of 0 and the reduction is exactly the same... interesting... I wonder if that means I can readback with the label information... and collect paired garbaged nodes together...?)
MaiaVictor
CC BY-SA 3.0
2015-07-27T18:40:52.530Z
I'm afraid I don't understand your comments.  The tags and labels are necessary for reduction, right?  The rules $\lambda$-@ and, say $\lambda$-D are different (the first is an annihilation, the second a commutation), how do you know which one to apply if you erase the tags?  The same holds for the labels of fan (D) nodes: a D-D pair annihilates or commutes depending on whether the labels of the two cells involved are equal or not.
Damiano Mazza
CC BY-SA 3.0
2015-07-27T19:11:30.273Z
I noticed you can skip the "tags" as in, those: `λ @ e D`. All you need is integer labels. `λ @ e` gets the label 0, and each `D` gets a different label. If the labels are equal, annihilate, if they are different, commute. I'm almost getting an answer, I think.
MaiaVictor
<ds.algorithms><lambda-calculus><functional-programming><interaction-nets>
Is it possible to unambiguously read back λ terms from interaction nets without node types?
MaiaVictor
# Is it possible to unambiguously read back λ terms from interaction nets without node types?

(Asked by: username_0 on 2015-07-25)

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:

[![enter image description here](https://i.sstatic.net/ArE3C.png)](https://i.sstatic.net/ArE3C.png)

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

[![enter image description here](https://i.sstatic.net/NFPHb.png)](https://i.sstatic.net/NFPHb.png)

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

[![enter image description here](https://i.sstatic.net/IPw2e.png)](https://i.sstatic.net/IPw2e.png)

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:

[![enter image description here](https://i.sstatic.net/Z6scU.png)](https://i.sstatic.net/Z6scU.png)
[![enter image description here](https://i.sstatic.net/qwpwA.png)](https://i.sstatic.net/qwpwA.png)
[![enter image description here](https://i.sstatic.net/5naLt.png)](https://i.sstatic.net/5naLt.png)

Is it possible, from the configuration of the net alone, to infer the tags and thus readback the same lambda term without them?

**Tags:** ds.algorithms, lambda-calculus, functional-programming, interaction-nets

> **Comments:**
> **username_1**: The interaction nets used in Lamping's algorithm (which are called *sharing graphs*) are more complex than what you state: nodes are indexed and there are "reindexing" nodes (traditionally called *brackets* and *croissants* because of the graphical notations originally used by Lamping). Is that why you start your question with "[a] class of lambda terms"? I mean, you are only considering a restricted class of $\lambda$-terms which do not use indices (such as those coming from elementary linear logic proof nets)?  
> **username_0**: @DamianoMazza Yes! I'm only considering EAL-typeable terms. (In fact I have hundreds of λ terms including whole list/trees/etc libraries and I'm yet to find one that isn't.) In particular, I'm trying to figure out what is the most efficient way to compute the abstract algorithm. My implementation uses the tags on the nodes, but I suspect those are redundant. I believe all nodes are the same thing mechanically, not 5 different things. Also, the question on how to collect garbage is very important, but there is no good solution on literature. I need that insight to start reasoning about it.  
> **username_0**: (There are only 2 reduction rules going on, annihilation and commute, so why would 5 tags (`e`, `λ`, `@`, `D`, `R`), plus a label for fans, be necessary? (The beta rule `λ-@` is exactly the same as annihilation for paired fans `D-D`, and erasure `e-x` is exactly the same as duplication `D-x`). I find it very likely that I can represent all those without the tags - just one node and a simple rule for pairing them.)  
> **username_0**: (In fact I noticed I could replace every node by fans with a starting label of 0 and the reduction is exactly the same... interesting... I wonder if that means I can readback with the label information... and collect paired garbaged nodes together...?)  
> **username_1**: I'm afraid I don't understand your comments.  The tags and labels are necessary for reduction, right?  The rules $\lambda$-@ and, say $\lambda$-D are different (the first is an annihilation, the second a commutation), how do you know which one to apply if you erase the tags?  The same holds for the labels of fan (D) nodes: a D-D pair annihilates or commutes depending on whether the labels of the two cells involved are equal or not.  
> **username_0**: I noticed you can skip the "tags" as in, those: `λ @ e D`. All you need is integer labels. `λ @ e` gets the label 0, and each `D` gets a different label. If the labels are equal, annihilate, if they are different, commute. I'm almost getting an answer, I think.  

---

## 1 answers

### Answer by username_0 on 2017-05-27. Score: 3

So, yes, turns out it is possible, as can be seen on the `decode` function of my abstract algorithm implementation [here](https://github.com/username_0/interaction-combinators/blob/master/lambda-encoding.js). 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.


---

