Complexity Analysis of Tunable Type Inference for Generic Universe Types

Abstract

This work studies the computational complexity of a tunable static type inference problem which was introduced in prior research [1]. The problem was assumed to be inherently difficult, without evidence, and a SAT solver was used to obtain a solution. In this thesis, we analyze the complexity of the inference problem. We prove that it is indeed highly unlikely that the problem can be solved efficiently. We also prove that the problem cannot be approximated efficiently to within a certain factor. We discuss the computational complexity of three restricted but useful versions of the problem, showing that whilst one of them can be solved in polynomial time, the other two are still inherently difficult. We discuss our efforts and the roadblocks we faced while attempting to conduct experiments to gain further insight into the properties which distinguish between hard and easy instances of the problem.

References: [1] W. Dietl, M. D. Ernst and P. Müller, Tunable Static Inference for Generic Universe Types, European Conference on Object-Oriented Programming (ECOOP), July 2011, Best Paper Award.