Strong Reduction in Lambda Calculus and its Use in Program Optimization
Assigned to Tiemo-Benedikt Schröder.
Program optimization by compilers is important - especially for functional programming languages. Yet at least parts of it remain a ”black art”, as Simon Peyton Jones describes the inlining technique in [0], full of compromises and heuristics. The problem, known as code bloat, is that optimization techniques might actually make performance worse by inlining too much, blowing up the code size.
Rather than employing trial-and-error we propose to adopt the Useful Sharing reduction technique, originally developed by Accattoli & Dal Lago for solving the related size-explosion problem in strong λ-calculus [1]. This technique provides proven bounds for the resulting code size. Making a start at implementing and testing Useful Sharing for optimization in Haskell is the goal of this thesis.
Further Information
-
[0] Simon Peyton Jones and Simon Marlow. 2002. Secrets of the Glasgow Haskell Compiler inliner. J. Funct. Program. 12, 5 (July 2002), 393-434.
-
[1] Accattoli, Beniamino & Dal Lago, Ugo. (2016). (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science. 12. . 10.2168/LMCS-12(1:4)2016.