Programming Languages

Strong Reduction in Lambda Calculus and its Use in Program Optimization

As­signed to Tiemo-Benedikt Schröder.

Pro­gram op­ti­miza­tion by com­pil­ers is im­por­tant - es­pe­cially for func­tional pro­gram­ming lan­guages. Yet at least parts of it re­main a ”black art”, as Simon Pey­ton Jones de­scribes the in­lin­ing tech­nique in [0], full of com­pro­mises and heuris­tics. The prob­lem, known as code bloat, is that op­ti­miza­tion tech­niques might ac­tu­ally make per­for­mance worse by in­lin­ing too much, blow­ing up the code size.

Rather than em­ploy­ing trial-and-er­ror we pro­pose to adopt the Use­ful Shar­ing re­duc­tion tech­nique, orig­i­nally de­vel­oped by Ac­cat­toli & Dal Lago for solv­ing the re­lated size-ex­plo­sion prob­lem in strong λ-cal­cu­lus [1]. This tech­nique pro­vides proven bounds for the re­sult­ing code size. Mak­ing a start at im­ple­ment­ing and test­ing Use­ful Shar­ing for op­ti­miza­tion in Haskell is the goal of this the­sis.

Fur­ther In­for­ma­tion

  • [0] Simon Pey­ton Jones and Simon Mar­low. 2002. Se­crets of the Glas­gow Haskell Com­piler in­liner. J. Funct. Pro­gram. 12, 5 (July 2002), 393-434.

  • [1] Ac­cat­toli, Be­ni­amino & Dal Lago, Ugo. (2016). (Left­most-Out­er­most) Beta Re­duc­tion is In­vari­ant, In­deed. Log­i­cal Meth­ods in Com­puter Sci­ence. 12. . 10.2168/LMCS-12(1:4)2016.

Con­tact

Philipp Schus­ter