7
$\begingroup$

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

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

enter image description here

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

enter image description here

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 enter image description here enter image description here

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

Improve this question
$\endgroup$
6
  • 2
    $\begingroup$ 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)? $\endgroup$
    – Damiano Mazza
    Commented Jul 26, 2015 at 9:00
  • $\begingroup$ @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. $\endgroup$
    – MaiaVictor
    Commented Jul 26, 2015 at 12:00
  • $\begingroup$ (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.) $\endgroup$
    – MaiaVictor
    Commented Jul 26, 2015 at 12:33
  • $\begingroup$ (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...?) $\endgroup$
    – MaiaVictor
    Commented Jul 26, 2015 at 16:35
  • 1
    $\begingroup$ 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. $\endgroup$
    – Damiano Mazza
    Commented Jul 27, 2015 at 18:40

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.