[Prev][Next][Index][Thread]
result announcement: 2ndorder Lambda Calculus Typability Undecidable

To: types@dcs.gla.ac.uk

Subject: result announcement: 2ndorder Lambda Calculus Typability Undecidable

From: jbw@cs.bu.edu (Joe Wells)

Date: Tue, 15 Jun 93 21:04:35 0400

Approved: types@dcs.gla.ac.uk
This message is the announcement of a result and a forthcoming paper.
TYPABILITY AND TYPECHECKING
IN THE SECONDORDER LAMBDA CALCULUS
ARE EQUIVALENT AND UNDECIDABLE
by
J. B. Wells
Computer Science Dept
Boston University
We consider the problems of typability[1] and type checking[2] in
the Girard/Reynolds secondorder polymorphic lambda calculus, which
we will call System F, which we use in the "Curry style" where types
are assigned to pure lambda terms. These problems have been
considered and proven to be decidable or undecidable for various
restrictions and extensions of System F and other related systems,
and lowerbound complexity results for System F have been achieved,
but they have remained "embarrassing open problems"[3] for System F
itself.
The typability problem is to decide, given an (untyped) lambda term
M, whether there exists a type t and a type assignment[4] A such
that there exists a valid derivation in system F for the
assertion[5] A  M : t. The closely related typechecking problem
is to decide, given a lambda term M, a type t, and a type assignment
A, whether there is a valid derivation in system F for the assertion
A  M : t.
We prove the following two theorems:
1. Semiunification is reducible to type checking in System F.
Since semiunification is undecidable, type checking in System F
is also. The proof is straightforward.
2. Type checking in System F is reducible to typability in System F.
Since the reverse reduction is already known, this implies that
type checking and typability are equivalent in System F and that
typability is undecidable. The proof uses a novel method of
constructing lambda terms such that in all type derivations,
specific bound variables must always be assigned a specific type.
Using this technique, we can require that specific subterms must
be typable using a specific, fixed type assignment in order for
the entire term to be typable at all. The method allows
simulating any desired type assignment. We develop it for both
the lambdaK and lambdaI calculi. We call this method
"constants for free".
The above results will be included in the author's forthcoming
doctoral thesis, supervised by A. J. Kfoury.
[1] Typability is also called type reconstruction.
[2] Type checking is also called derivation reconstruction.
[3] Robin Milner as quoted by Henk Barendregt.
[4] A type assignment may also be called an environment, a context,
or a basis.
[5] An assertion may also be called a sequent, a type assignment
formula, or a judgement.
Author's comment:
These results exist only on handwritten notes now. I will type them in
as soon as I can and make them available via anonymous FTP, but due to
another commitment (a software consulting contract), I will not have
time until the beginning of July.

Joe Wells <jbw@cs.bu.edu>
Member of the League for Programming Freedom  send email for details