Lambda the Ultimate

My intro to partial evaluation treats the same two examples in Scheme, of course without the typechecking which is the whole point of the above paper. They seem to be doing about the same thing, with the abstract code and value types as a way of lifting information out of the opaque code type.

My intro to partial evaluation treats the same two examples in Scheme, They seem to be doing about the same thing ...

One approach to code generation is to make the generator simple, and optimize the generated code later. Your introduction to PE follows this approach: a straight-forward generator based on the FFT recurrence, followed by the _second_ pass that does algebraic simplifications (like 1*a=1) and common-subexpression elimination (CSE). We, on the other hand, generate code in one pass. The result is already optimal and does _not_ need any CSE nor other optimization passes.

Why we are so uneasy about the manipulation of the generated code? Because doing so significantly weakens the equational theory, as Walid proved. Currently, we maintain the invariant that the generated code is _automatically_ strongly typed and does not need to be typechecked. That significantly simplifies the work of code generators (e.g., OCaml-to-C or OCaml-to-Fortan, perhaps other would follow). Post-processing of the generated code makes such invariants significantly harder to maintain.

Let's take an example. The "intro to partial evaluation" describes CSE that works by memoizing code fragments. That implies the comparison of code fragments in equality. How to compare two, usually open, code fragments in equality? The extensional comparison is undecidable; the intensional comparison is either unsound or insufficient. For example, are (+ x1 x2) and (+ x1 x2) the same? First of all, it depends if x1 and x2 refer to the same identifiers in both fragments. If the source language has binding forms with shadowing, the above fact is not given. Then we have to ask, if x1 and x2 _always_ refer to the same _values_? In the language with mutations such an property is far harder to determine. The "intro to partial evaluation" did not seem to include either binding forms or mutations in the source language. Furthermore, are (+ x100 x101) (+ x1002 x1003) are equal pieces of code? That again depends on what '+', x100, etc. mean. Incidentally, just structural comparison of these code fragments would say they are not equal, even if it turns our x1002 and x100 are the same identifier, etc. What about (* a (+ b c)) and (+ (* a b) (* a c)). These two fragments are structurally non-equal -- yet they essentially are common sub-expressions. Compilers therefore apply CSE, algebraic simplification, inlining, copy propagation several times, until a fixpoint is reached. To achieve the good quality of the resulting code, we therefore will have to implement a good part of the optimizing compiler! It is also far harder to assure the correctness of all these transformations.

Our approach is more algorithmic -- it really forces the user to understand the algorithm in order to generate the optimal code. In regards to FFT: if you try to generate FFT code in a straightforward way and then apply various simplifications, such as

• noting that 1*x = x and 0*x =0
• noting that sin(pi/4) and cos(pi/4) are the same and so complex multiplications by the roots of unity of the 8th order can be done simpler. Note, _computed_ sin(pi/4) and cos(pi/4) are _not_ actually identical.
• make all numerical constants positive
• CSE

I should specifically point out the phrase from the paper: ``there are benefits to focusing on writing better generators rather than on fixing the results of simple generators.''"

Regarding the CPS of your evaluator: that is indeed quite a useful technique, which is first described in Anders Bondorf, "Improving Binding Times without Explicit CPS-Conversion", LFP'92

First of all, the paper "Relating FFTW and Split-Radix" ( LtU discussion) shows that it is possible to exactly match FFTW in floating-point operation count using staging with abstract interpretation. Incidentally, this current paper ``A Methodology for Generating Verified Combinatorial Circuits'' is not obsolete as it provides the most detailed explanation and illustration of our abstract interpretation in the staging domain. The ``staging monad'' used in this and ``Relating FFTW...'' papers is explained in detail in a draft Staging Dynamic Programming Algorithms