The complexity of type inference for higher-order typed lambda calculi

Publisher Website
Google Scholar
Abstract
We analyse the computational complexity of type inference for untyped λ-terms in the second-order polymorphic typed λ-calculus (F2) invented by Girard and Reynolds, as well as higher-order extensionsF3,F4, …,Fωproposed by Girard. We prove that recognising theF2-typable terms requires exponential time, and forFωthe problem is non-elementary. We show as well a sequence of lower bounds on recognising theFk-typable terms, where the bound forFk+1is exponentially larger than that forFk.The lower bounds are based on generic simulation of Turing Machines, where computation is simulated at the expression and type level simultaneously. Non-accepting computations are mapped to non-normalising reduction sequences, and hence non-typable terms. The accepting computations are mapped to typable terms, where higher-order types encode reduction sequences, and first-order types encode the entire computation as a circuit, based on a unification simulation of Boolean logic. A primary technical tool in this reduction is the composition of polymorphic functions having different domains and ranges.These results are the first nontrivial lower bounds on type inference for the Girard/Reynolds system as well as its higher-order extensions. We hope that the analysis provides important combinatorial insights which will prove useful in the ultimate resolution of the complexity of the type inference problem.

This publication has 25 references indexed in Scilit: