Theory of higher order interpretations and application to Basic Feasible Functions

TL;DR

This paper extends interpretation methods to higher order functional languages, enabling complexity analysis and characterization of Basic Feasible Functions through fixpoint semantics and polynomial bounds.

Contribution

It develops a theory of higher order interpretations using complete lattices and fixpoints, advancing complexity analysis for higher order functions.

Findings

Interpretation domain is a complete lattice.

Program interpretation expressed as a least fixpoint.

Bounding interpretations by higher order polynomials characterizes Basic Feasible Functions.

Abstract

Interpretation methods and their restrictions to polynomials have been deeply used to control the termination and complexity of first-order term rewrite systems. This paper extends interpretation methods to a pure higher order functional language. We develop a theory of higher order functions that is well-suited for the complexity analysis of this programming language. The interpretation domain is a complete lattice and, consequently, we express program interpretation in terms of a least fixpoint. As an application, by bounding interpretations by higher order polynomials, we characterize Basic Feasible Functions at any order.