## Static polynomial size analysis for functional programs

Digital Security Group

Institute for Computing and Information Sciences

Radboud Universiteit Nijmegen

Thursday, 14 August 2008, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**Abstract**: Recently we have presented a size-aware type
system for first-order shapely function definitions. A function
definition is called shapely when the size of the result is determined
exactly by a polynomial in the sizes of the arguments.

At present we study generalisation of the method to function
definitions with size dependencies limited by (piecewise) polynomials
from above and below. A simple example of such definition is an
encoding of insertion an element into a list.

The main idea is to annotate an output type not with a single
polynomial, but with a parametrised family of (piecewise) polynomials,
where a parameter(s) varies inside a certain range. Type-checking
amounts to instantiation of the parameter of the type under checking.
It must force equality of two polynomials and belong to the range.

This problem is undecidable in non-linear integer arithmetic, so
one has to involve real arithmetic. We have designed a form of type
annotations which significantly simplifies predicates arising at the
end of type-checking.

Similarly to shapely function definitions, one may involve testing
to infer lower and upper bounds, once these bounds are
polynomials. The condition is that for (almost) any vector of input
sizes there are inputs on which the minimal output size is achieved
and inputs on which the maximal size is achieved.

To extend applicability, we allow higher-order functions, if an
output annotation does not depend on size parameters/dependencies of
the non-zero-order arguments. Thus we cover almost all function
definitions, say, from the Clean lists library. (Joint work with
M. van Eekelen, A. Tamalet.)

Tarmo Uustalu

Last update 23.7.2008