Supercompilation

Termination combinators forever

Termination combinators forever, Max Bolingbroke, Simon Peyton Jones, and Dimitrios Vytiniotis, Haskell Symposium, Tokyo, Sept 2011.

Abstract

We describe a library-based approach to constructing termination tests suitable for controlling termination of symbolic methods such as partial evaluation, supercompilation and theorem proving. With our combinators, all termination tests are correct by construction. We show how the library can be designed to embody various optimisations of the termination tests, which the user of the library takes advantage of entirely transparently.

Improving supercompilation: tag-bags, rollback, speculation, normalisation, and generalisation

Improving supercompilation: tag-bags, rollback, speculation, normalisation, and generalisation, Max Bolingbroke and Simon Peyton Jones, submitted to ICFP 2011.

Abstract

Supercompilation is a technique due to Turchin Supercompilation is a powerful technique for program optimisation and theorem proving. In this paper we describe and evaluate three improvements to the Cambridge Haskell Supercompiler (CHSC). We reduce supercompiled program size by the use of a weak normaliser and aggressive rollback, and we improve the performance of supercompiled programs by heap speculation and generalisation. Our generalisation method is simpler than those in the literature, and is better at generalising computations involving primitive operations such as those on machine integers. We also provide the first comprehensive account of the tag-bag termination mechanism.

Supercompilation by evaluation, Max Bolingbroke and Simon Peyton Jones

Abstract

Supercompilation is a technique due to Turchin which allows for the construction of program optimisers that are both simple and extremely powerful. Supercompilation is capable of achieving transformations such as deforestation, function specialisation and constructor specialisation. Inspired by Mitchell's promising results (ICFP'10), we show how the call-by-need supercompilation algorithm can be recast to be based explicitly on an evaluator, and in the process extend it to deal with recursive let-expressions.

Simon Peyton Jones, simonpj@microsoft.com