[Prev][Next][Index][Thread]
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
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 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