[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