Lecture by Harry Mairson: Complexity of Type Inference

Date: Tue, 18 Sep 90 17:45:29 EDT
To: theory-seminars

                Massachusetts Institute of Technology
                   Laboratory for Computer Science
                    Theory of Computation Seminar
                  Date: Thursday, September 27, 1990
                     Time: Refreshments at 4:00pm
                            Talk at 4:15pm
                           Place: NE43-512A
                   The Complexity of Type Inference
                for Higher-order Typed Lambda Calculi
                           Harry G. Mairson
                         Brandeis University
                        Waltham, Massachusetts
We analyze the computational complexity of type inference for untyped
lambda-terms in the second-order polymorphic typed lambda-calculus
(F_2) invented by Girard and Reynolds, as well as higher-order
extensions F_3, F_4,..., F_omega proposed by Girard.  We prove that
recognizing the F_{2}-typable terms requires exponential time, and for
F_omega the problem is nonelementary.  We show as well a sequence of
lower bounds on recognizing the F_{k}-typable terms, where the bound
for F_{k+1} is exponentially larger than that for F_k.

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-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

These results are the first nontrivial lower bounds on type inference
for the Girard/Reynolds system as well as its higher-order extensions.
We believe that the analysis provides important combinatorial insights
which will prove useful in the ultimate resolution of the complexity
of the type inference problem.

This work is joint with Fritz Henglein (Utrecht University and Courant
Institute, NYU).

HOST: Professor Albert R. Meyer