What is it about?

The type Int of integer numbers is not a primitive type in typical programming languages. What we have are int16, int32, int64, etc. that are finite approximations of increasing dimension of the type of integers. All the programs we are used to, are essentially programs on finite types, parametric with respect to the dimensions of these types: a sorting algorithm takes as input an array of dimension m of elements with fixed dimension n, and returns an array of the same kind. When we enlarge the size of inputs to tackle complexity issues, we are actually enlarging their types, and we can address complexity in terms of the asymptotic behaviour of programs for types of growing dimensions.

Featured Image

Why is it important?

Traditional Computational Complexity is badly compositional. Complexity is expressed in terms of the size of inputs, but the complexity of an algorithm tells us very little about the size of its output. If the output is a finite type, we do not have such a problem. Everything fits perfectly together, allowing a fine grained, compositional investigation of the complexity of programs. Moreover, when the input and output types are finite, we can directly provide interesting upper bounds to the complexity of transformations between them, allowing to derive interesting characterization of basic complexity classes in terms of the hierarchical structure of these types.

Perspectives

FInite Types are pervasive in Computer Science. Think of the advent of Deep Neural Computation. Vectors are a typical example of finite type, and a NN layer is just a function between vectors, that is still another finite type (the space of functions between finite types is finite). Re-founding Complexity Theory in terms of finite types is not only an exciting perspective, but a compelling necessity.

Andrea Asperti
Universita degli Studi di Bologna

Read the Original

This page is a summary of: Computational Complexity Via Finite Types, ACM Transactions on Computational Logic, July 2015, ACM (Association for Computing Machinery), DOI: 10.1145/2764906.
You can read the full text:

Read

Contributors

The following have contributed to this page