Polynomial Size Analysis of First-Order Shapely Functions

TL;DR

This paper introduces a size-aware type system for first-order shapely functions, enabling precise polynomial size analysis of functions like matrix multiplication, with proven soundness and a practical semi-decidable inference procedure.

Contribution

It presents a novel type system for shapely functions with polynomial size analysis, including a decidable restriction and an implementation for automatic size dependency inference.

Findings

Type system is sound with respect to operational semantics.

Type checking is undecidable in general but decidable under a syntactic restriction.

Implemented procedure combines runtime testing and type-checking for automatic inference.

Abstract

We present a size-aware type system for first-order shapely function definitions. Here, a function definition is called shapely when the size of the result is determined exactly by a polynomial in the sizes of the arguments. Examples of shapely function definitions may be implementations of matrix multiplication and the Cartesian product of two lists. The type system is proved to be sound w.r.t. the operational semantics of the language. The type checking problem is shown to be undecidable in general. We define a natural syntactic restriction such that the type checking becomes decidable, even though size polynomials are not necessarily linear or monotonic. Furthermore, we have shown that the type-inference problem is at least semi-decidable (under this restriction). We have implemented a procedure that combines run-time testing and type-checking to automatically obtain size dependencies. It terminates on total typable function definitions.