[Prev][Next][Index][Thread]
Lower bound on System F typability
Date: Tue, 22 May 90 15:40:36 met
A Lower Bound for Full Polymorphic Type Inference:
Girard-Reynolds Typability is DEXPTIME-hard
Fritz Henglein
(Utrecht University)
Abstract:
The typability problem for the Girard-Reynolds Calculus (also called
Second Order Lambda Calculus or System F) is an old and elusive
problem. Neither nontrivial upper nor lower bounds have been known,
not even whether the problem is decidable or not. In this paper we
present the, as far as we know, first nontrivial lower bound for
Girard-Reynolds typability. Expanding on work by Kanellakis and
Mitchell and, in particular, Mairson on ML typability we prove that GR
typability is DEXPTIME-hard.
Mairson's proof of DEXPTIME-hardness of ML typability relies on an
encoding of Boolean values by type schemes with equality between some
components of the type scheme. This type equality can be forced in ML
due to ML's monomorphic typing rule for lambda-bound variables. Since
this equality cannot be forced in the Girard-Reynolds Calculus,
Mairson's proof cannot naively be transferred to the Girard-Reynolds
typability problem.
We show that a conventional (untyped) lambda-calculus representation
of Boolean values, together with an analogue of Mairson's fan-out
gates, results in a straightforward simulation of a deterministic
Turing Machine ``in the types'' for an exponential number of steps.
This yields yet another proof, principally based on Mairson's, of
DEXPTIME-hardness of ML typability. Since the lambda-expression
representing a Turing Machine computation simulates the Turing Machine
also under beta-reduction it is easy to extend this lower bound proof
to a DEXPTIME-hardness result for Girard-Reynolds typability by
mapping a rejecting computation to a nonnormalizing lambda-expression.
The simulation relies on a class of lambda-expressions that have a
rank-2 typing if they have any typing at all. Since rank-2 typability
is DEXPTIME-decidable, as shown by Kfoury and Tiuryn, our bound is the
best we can achieve using this particular class. It appears possible,
though, to achieve better lower bounds by extending our technique of
double simulation ``in the types'' and ``in the values'' to
expressions with (only) higher-rank typings.
(End of abstract)
This report is available as technical report RUU-CS-90-14 from the
following address (and please don't forget I'm interested in comments,
corrections, etc.):
Department of Computer Science (Secretariat)
Utrecht University
PO Box 80.089
3508 TB Utrecht
The Netherlands
Fritz
(henglein@cs.ruu.nl)
Current address (June-Dec. 1990):
Fritz Henglein
Department of Computer Science
New York University
715 Broadway, 7th floor
New York, N.Y. 10003
Email: henglein@cs.nyu.edu