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.
Photo by Brett Jordan on Unsplash
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.
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:
The following have contributed to this page