[<<][staapl][>>][..]

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

[Reply][About]

[<<][staapl][>>][..]