Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version)

TL;DR

This paper presents a method for automatically analyzing the complexity of higher-order functional programs by transforming them into first-order systems and leveraging existing tools, ensuring the analysis accurately reflects the original program's complexity.

Contribution

It introduces a novel approach combining defunctionalization and transformation strategies to enable complexity analysis of higher-order programs using first-order tools.

Findings

Transformations preserve complexity accurately

Method is applicable to a wide range of programs

Experimental results demonstrate viability

Abstract

We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Further, we describe suitable strategies for the application of the studied transformations and provide ample experimental data for assessing the viability of our method.