5 ms·
Not sure what you mean by "equivalent terms look the same". I'm not clear on how e.g. ##(2 1) and #1 look the same. Going by your remark about name collisions
by Sniffnoy 14y ago
Not sure what you mean by "equivalent terms look the same". I'm not clear on how e.g. ##(2 1) and #1 look the same. Going by your remark about name collisions, I must ask if you are thinking of alpha-equivalence? (Which certainly is rendered unnecessary by the notational system.)
And thank you for making/hopefully fixing this!
- notb 14y agoOh I see. Yes I was thinking of alpha-equivalence, sorry. Now I must ask, do you know any good papers/algos on that reduction? And how would you envision animating? It seems a bit like a lambda/var pair just fall off...
- Sniffnoy 14y agoI don't know what I might refer you to. Beta reduction requires recognizing subtrees of the form (#T S) (where T and S are any subtrees), eta reduction just requires recognizing subtrees of the form #(T 1) (where T is any subtree). No idea about animation. It's really not something I'd thought about, I have to say...
- Sniffnoy 14y agoOops -- I forgot about the non-freeness requirement. So not just any subtree. That makes it trickier. But still not hard, I think.