Polynomial Size Analysis with Families of Piecewise Polynomials for Functional Programs over Lists? With soundness proof and examples in detail

Abstract. Size analysis can play an important role in optimising mem-ory management and in preventing failure due to memory exhaustion. Static size analysis can be performed using size-aware type systems. In size-aware type systems types express output-on-input size dependencies where sizes of outputs depend on sizes of inputs but they do not depend directly on the actual values. We present a novel type system for a strict functional language. We introduce size annotations that are indexed families of piecewise polyno-mials. Families are defined using indices. They collect possible different size dependencies of a single function. With families compositionality becomes straightforward, even for non-monotonic size dependencies. Lower and upper size bounds can be ex-pressed in a natural way as members of the family. Furthermore, families make it possible to allow non matrix-like structures where inner lists have different lengths. The type system is proven to be sound with respect to a standard opera-tional semantics. Type checking in our type system is not fully decidable. However, we identify two large decidable subclasses. Moreover, the type system admits a semi-automatic inference procedure.