Denotational cost semantics for functional languages with inductive types

TL;DR

This paper presents a formal method for extracting cost and size recurrences from higher-order functional programs with inductive datatypes, accommodating various size notions and ensuring accurate evaluation cost predictions.

Contribution

It introduces a monadic translation and size abstraction techniques that work across multiple models, providing a sound and flexible framework for complexity analysis of functional programs.

Findings

Recurrences correctly predict evaluation costs.

Supports diverse notions of size, including list length and tree height.

Proven upper bounds for evaluation cost via logical relations.

Abstract

A central method for analyzing the asymptotic complexity of a functional program is to extract and then solve a recurrence that expresses evaluation cost in terms of input size. The relevant notion of input size is often specific to a datatype, with measures including the length of a list, the maximum element in a list, and the height of a tree. In this work, we give a formal account of the extraction of cost and size recurrences from higher-order functional programs over inductive datatypes. Our approach allows a wide range of programmer-specified notions of size, and ensures that the extracted recurrences correctly predict evaluation cost. To extract a recurrence from a program, we first make costs explicit by applying a monadic translation from the source language to a complexity language, and then abstract datatype values as sizes. Size abstraction can be done semantically, working in models of the complexity language, or syntactically, by adding rules to a preorder judgement. We give several different models of the complexity language, which support different notions of size. Additionally, we prove by a logical relations argument that recurrences extracted by this process are upper bounds for evaluation cost; the proof is entirely syntactic and therefore applies to all of the models we consider.