Positive Supercompilation for a Higher-Order Call-By-Value Language

TL;DR

This paper introduces a supercompilation algorithm for higher-order call-by-value languages that guarantees termination and preserves program behavior, improving upon previous methods that could alter program termination properties.

Contribution

It presents a novel supercompilation algorithm tailored for higher-order call-by-value languages that ensures termination and correctness, leveraging strictness information.

Findings

Algorithm guarantees termination for higher-order call-by-value programs.

Preserves original termination properties of programs.

Outperforms previous call-by-name transformations in effectiveness.

Abstract

Previous deforestation and supercompilation algorithms may introduce accidental termination when applied to call-by-value programs. This hides looping bugs from the programmer, and changes the behavior of a program depending on whether it is optimized or not. We present a supercompilation algorithm for a higher-order call-by-value language and prove that the algorithm both terminates and preserves termination properties. This algorithm utilizes strictness information to decide whether to substitute or not and compares favorably with previous call-by-name transformations.