I'm confused by this. It seems to be promising a normal form for all expressions in a Turing-complete language—but that's equivalent to guaranteeing termination, isn't it? Moreover, it promises to produce equal results for equivalent programs, which would allow a solution of the halting problem, wouldn't it?
I suspect that I've got some bad conceptual misunderstanding here; but, on the other hand, I also have a hard time believing that, if beta- and eta-reduction alone were sufficient to express such powerful optimisations, it would have taken this long to discover that.
I suspect that I've got some bad conceptual misunderstanding here; but, on the other hand, I also have a hard time believing that, if beta- and eta-reduction alone were sufficient to express such powerful optimisations, it would have taken this long to discover that.