Timeline for Representing bound variables with a function from uses to binders
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 12, 2018 at 22:11 | answer | added | Rodolphe Lepigre | timeline score: 5 | |
| Sep 12, 2018 at 16:04 | answer | added | PLL | timeline score: 5 | |
| Sep 8, 2018 at 0:23 | answer | added | Noam Zeilberger | timeline score: 12 | |
| Sep 7, 2018 at 21:11 | answer | added | Łukasz Lew | timeline score: 10 | |
| Sep 7, 2018 at 19:03 | answer | added | Andrej Bauer | timeline score: 6 | |
| Sep 7, 2018 at 17:27 | comment | added | Mike Shulman | @DanDoel Ah, interesting. I thought it was so obvious as to not need mentioning that you would drop in a separate copy of the term being substituted at every occurrence of the variable it's being substituted for; otherwise you wouldn't have a syntax tree any more! It didn't occur to me to think of this copying as alpha-renaming, but now that you point it out I can see it. | |
| Sep 7, 2018 at 14:04 | comment | added | Dan Doel | Right, so each binder uses a unique (within the tree) variable name (the pointer to it is one automatically). This is the Barendregt convention. But when you substitute, you must rebuild (in C) the thing you're substituting to continue to have unique names. Otherwise (in general) you're using the same pointers for multiple subtrees, and can get variable capture. The rebuilding is alpha renaming. Presumably something similar happens depending on the specifics of your encoding of trees as sets? | |
| Sep 7, 2018 at 13:33 | comment | added | Mike Shulman |
By "pointer" I meant a pointer in the C sense: the computer representation I envision would have the abstract syntax tree represented by a tree data structure in the usual way, with nodes being structures/objects/etc., and then the $\bullet$ nodes would additionally contain a member binder *node that points to the node object of the corresponding $\lambda$.
|
|
| Sep 7, 2018 at 13:30 | comment | added | Mike Shulman | @DanDoel mathematically, a term involving $\lambda$s and $\bullet$s is represented by an abstract syntax tree. A tree has in particular a set of nodes with labels. There is then a subset of these nodes labeled by $\bullet$ and a subset of these nodes labeled by $\lambda$, and I'm saying we give a (set-theoretic) function from the former subset to the latter. There is no need to decide whether the nodes "really are" numbers or an ordered list or points on a page or whatever, they are simply an abstract set. | |
| Sep 7, 2018 at 12:31 | comment | added | Dan Doel | Also, I've seen proof nets, which I guess suggests (to me) that the distinguishing is spatial location in a drawing, and the 'function' is lines you draw. But then I don't understand how you represent that drawing in, say, a computer without having to solve all the same problems once reduction causes parts of it to start duplicating and changing. | |
| Sep 7, 2018 at 12:22 | comment | added | Dan Doel | Every way I can come up with for interpreting what this actually means seems fairly similar to some existing convention. You must be distinguishing the dots and binders somehow, but how are you doing that? Your mention of pointers implies some kind of unique number, which is (possibly) called the Barendregt convention (which requires alpha). If the answer is instead the order they appear on the page, that's also going to change and require fixing. The HOAS suggestion seems closest, perhaps, except that just saying that you already have a solution provided to you (which is great, but...). | |
| Sep 7, 2018 at 12:00 | history | tweeted | twitter.com/StackCSTheory/status/1038034239596515328 | ||
| Sep 7, 2018 at 11:21 | comment | added | Mike Shulman | @RodolpheLepigre I don't think so. In particular, my understanding is that HOAS is only correct when the metatheory is fairly weak, whereas this approach is correct in an arbitrary metatheory. | |
| Sep 7, 2018 at 9:41 | comment | added | Rodolphe Lepigre | Isn't this approach equivalent to higher-order abstract syntax (i.e., representing binders as functions in the host language)? In a sense, using a function as a binder establishes pointers to binders implicitly, in the representation of closures. | |
| Sep 7, 2018 at 8:44 | comment | added | Damiano Mazza | I don't know about drawbacks. Maybe formalization (e.g. in a proof assistant) is heavier? I'm not sure... What I know is that there's nothing technically wrong: this way of seeing lambda-terms is the one suggested by their representation as proof nets, so proof-net-aware people (like myself) implicitly use it all the time. But proof-net-aware people are very rare :-) So maybe it's really a matter of tradition. PS: I added a couple of loosely related tags to make the question more visible (hopefully). | |
| Sep 7, 2018 at 8:35 | history | edited | Damiano Mazza |
Added more tangs to (hopefully) improve visibility.
|
|
| Sep 6, 2018 at 18:52 | history | asked | Mike Shulman | CC BY-SA 4.0 |