On Sun, Jun 21, 2009 at 07:48:30PM +0100, Andrew Coppin wrote: > Andrew Coppin wrote: >> Well anyway, the obvious thing to do is after each reduction, strip off >> all the variable indicies and rerun the labeller to assign new indicies. >> But does this solution work properly in general? > > No. > > Supposing some Lambda expression eventually reduces to, say, > > \x1 -> \x2 -> x1 x2 > > Now strip off all the indicies: > > \x -> \x -> x x > > ...and recompute them... > > \x1 -> \x2 -> x2 x2 > > FAIL. > > To make it worth properly, I would have to (at least) make the renamer > respect any indicies which are already present. It's nontrivial, but > doable. Of course, the £1,643,264 question is... would it work even then?
I reiterate the pointers to reading material that I gave earlier. A lot of really smart people have spent a lot of time thinking about this already; it's likely not worth any more of your time to try figuring it out yourself. (It's definitely worth some initial time struggling with it, so that you can properly appreciate the solutions---but it sounds like you've already done that!) Briefly, the key operation is substitution---*while* doing a substitution you have to somehow check that names aren't clashing, and possibly rename some things if necessary (or if using de Bruijn indices, you may need to shift some indices around while doing substitution). If you wait until *after* doing a substitution to fix up the names, it's too late. But don't take my word for it, go read about it somewhere. =) -Brent _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
