|
J. B. Wells
Typability is undecidable for F+eta
Tech. Rep. 96-022, Comp. Sci. Dept., Boston Univ., March 1996
System F is the well-known polymorphically-typed
lambda-calculus with
universal quantifiers (“for all'').
F+eta is System F extended with the eta rule,
which says that if term M can be given type tau
and M eta-reduces to N, then N can also be
given the type tau.
Adding the eta rule to System F is equivalent to
adding the subsumption rule using the subtyping
(“containment'') relation that Mitchell defined and
axiomatized.
The subsumption rule says that if M can be given
type tau and tau is a subtype of type
sigma, then M can be given type sigma.
Mitchell's subtyping relation involves no extensions
to the syntax of types, i.e., no bounded
polymorphism and no supertype of all types, and is
thus unrelated to the system F<=
(“F-sub'').
Typability for F+eta is the problem of
determining for any term M whether there is any
type tau that can be given to it using the type
inference rules of F+eta.
Typability has been proven undecidable for System
F (without the eta rule), but the decidability of
typability has been an open problem for F+eta.
Mitchell's subtyping relation has recently been
proven undecidable, implying the undecidability of
“type checking'' for F+eta.
This paper reduces the problem of subtyping to the
problem of typability for F+eta, thus proving the
undecidability of typability.
The proof methods are similar in outline to those
used to prove the undecidability of typability for
System F, but the fine details differ greatly.
[ bib |
.ps.gz |
.html ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
