Yesterday I attended a talk by Olin Shivers about a clever way to representing lambda terms as DAGs.
Olin talking about uplinks. (Yes, I mainly took the picture to test my new camera mobile phone.)
It was a nifty technique Olin presented clever but simple. After the talk you had a feeling that you completely understood the technique, and it seemed useful for a large class of problems. The main drawback is that the data structure is ephemeral (that is, not persistent), which means that when you perform an update you destructively update the term.
I guess the side-effects mean that we can’t use this for HOL. Ah well.
I don’t think that Olin’s current implementation is appropriate for HOL. However, I have a few half-baked ideas for making the data structure persistant, and Olin promissed me if I sent him an email he would send me the code. (I havn’t done that, yet. Bad me.)
Whether or not I succeed in making the data structure persistant you and the other HOL guys will hear more about this, I promise.