Denotational semantics as a foundation for cost recurrence extraction for functional languages

TL;DR

This paper formalizes a method for extracting and analyzing cost recurrences in higher-order functional programs using denotational semantics, accommodating various notions of size and polymorphism.

Contribution

It provides a formal, model-based framework for cost recurrence extraction in functional languages, extending informal methods with rigorous semantics.

Findings

Different models describe various size notions for inductive types.

The approach handles polymorphic functions by relating size to shared data.

Examples demonstrate the method's applicability to informal cost analyses.

Abstract

A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input, and then to compute a closed-form upper bound on that recurrence. We give a formal account of that method for functional programs in a higher-order language with let-polymorphism. The method consists of two phases. In the first phase, a monadic translation is performed to extract a cost-annotated version of the original program. In the second phase, the extracted program is interpreted in a model. The key feature of this second phase is that different models describe different notions of size. This plays out in several ways. For example, when analyzing functions that take arguments of inductive types, different notions of size may be appropriate depending on the analysis. When analyzing polymorphic functions, our approach shows that one can formally describe the notion of size of an argument in terms of the data that is common to the notions of size for each type instance of the domain type. We give several examples of different models that formally justify various informal cost analyses to show the applicability of our approach.