Post by kunjaanHow does Kleene fixed-point theorem help in optimizations?
The Kleene fixed-point theorem guarantees the existence
of solutions to the sets of equations that arise during
most flow analyses. When the domains are finite, as
they usually are, the proof of the Kleene fixed-point
theorem also provides a practical algorithm for solving
those sets of equations.
Consider, for example, the Twobit compiler used by
Larceny. The compute-fixedpoint procedure that is
defined near the end of src/Compiler/pass2p2.sch [1]
uses an algorithm derived from the proof of the Kleene
fixed point theorem. That procedure is used to solve
the sets of equations that arise during two distinct
optimizations: lambda lifting and constant folding.
Twobit implements at least two other optimizations,
common subexpression elimination and representation
inference, that rely on the Kleene fixed point theorem
(or some similar theorem) but solve the flow equations
using a special purpose solver instead of using the
compute-fixedpoint procedure.
Will
[1] https://trac.ccs.neu.edu/trac/larceny/browser/trunk/larceny_src/src/Compiler/pass2p2.sch