Discussion:
How does Kleene fixed-point theorem help in optimization?
(too old to reply)
kunjaan
2009-05-06 19:48:32 UTC
Permalink
I am sorry I didnt know where to ask this question. Since most of the
people I respect in functional programming world use this group, I
thought i'd post it here.

How does Kleene fixed-point theorem help in optimizations?
William D Clinger
2009-05-06 20:37:48 UTC
Permalink
Post by kunjaan
How 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
Loading...