# result announcement: 2nd-order Lambda Calculus Typability Undecidable

• To: types@dcs.gla.ac.uk
• Subject: result announcement: 2nd-order 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 TYPE-CHECKING
IN THE SECOND-ORDER 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 second-order 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 lower-bound 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 type-checking 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. Semi-unification is reducible to type checking in System F.
Since semi-unification 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 lambda-K and lambda-I calculi.  We call this method

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 e-mail for details

```