Sun Mar 14 23:07:46 CET 2010

About compilation

It really is ultimately about proof that a walk towards an optimum
given by one measure, doesn't change another measure.

I have this neat little bag of symbols here that after a complex
computation (interpretation) gives a result.

What I want to do is to replace that neat little bag with an even
neater little bag (according to some measure) such that the result
after interpretation isn't influenced.

This is a constrained optimization problem.

     CONSTRAINT:     semantics preserving
     OPTIMIZATION:   minimize some other property.

Suppose my neat packet is X, suppose my correct semantics expressed by
the equation S(X) = 0, and suppose my neatness (i.e. code size,
execution speed, power consumption) maps X into an ordered space P : X
-> {O,<} such that we can compare X1 and X2 based on the order
introduced by the property P.

The deal is: in a transformation machine that preserves semantics
S(X), a lot of the internal structure of S is ``ghosted''.

I think the place to look is the peephole optimizer of [1].

[1] http://compcert.inria.fr/doc/index.html