Jump to : Download | Abstract | Keyword | Contact | BibTex reference | EndNote reference |


Fritz Henglein, Harry G. Mairson. The complexity of type inference for higher-order lambda calculi. In POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 119-130, New York, NY, USA, January 1991.


Download paper: (link)

Download paper: Adobe portable document (pdf) pdf

Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


We analyze the computational complexity of type inference for untyped lambda-terms in the second-order polymorphic typed lambda-calculus (F2) invented by Gi- rard and Reynolds, as well as higher-order extensions F3, F4, . . . . Fw proposed by Girard. We prove that recognizing the F2-typable terms requires exponential time, and for Fw the problem is nonelementary. We show as well a sequence of lower bounds on recogniz- ing the Fk-typable terms, where the bound for Fk+1 is exponentially larger than that for Fk. The lower bounds are based on generic simulation of Turing Machines, where computation is simulated at the expression and type level simultaneously. Nonaccepting computations are mapped to non-normalizing 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 analy- sis provides important combinatorial insights which will prove useful in the ultimate resolution of the complexity of the type inference problem


[ Parametricity ]


Fritz Henglein
H.G. Mairson

BibTex Reference

   Author = {Henglein, Fritz and Mairson, Harry G.},
   Title = {The complexity of type inference for higher-order lambda calculi},
   BookTitle = {POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
   Pages = {119--130},
   Publisher = {ACM},
   Address = {New York, NY, USA},
   Month = {January},
   Year = {1991}

EndNote Reference [help]

Get EndNote Reference (.ref)