[Prev][Next][Index][Thread]

result announcement: 2nd-order Lambda Calculus Typability Undecidable


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