[Prev][Next][Index][Thread]
Type reconstruction in F_\omega

To: types@dcs.gla.ac.uk

Subject: Type reconstruction in F_\omega

From: urzy@cs.bu.edu (Pawel Urzyczyn)

Date: Thu, 22 Sep 1994 12:00:47 0400

Approved: types@dcs.gla.ac.uk
A revised full version of my paper
Type reconstruction in F_\omega
is now available by anonymous ftp from:
ftp.mimuw.edu.pl
directory /pub/users/urzy
files fomega.ps.Z fomega.dvi.Z
csftp.bu.edu
directory /urzy
files fomega.ps fomega.dvi
Abstract
We investigate the Girard's calculus F_\omega as a ``Curry style'' type
assignment system for pure lambda terms. First we show an example of a
strongly normalizable term that is untypable in F_\omega. Then we prove
that every partial recursive function is nonuniformly represented in
F_\omega (even if quantification is restricted to constructor variables
of rank 1). It follows that the type reconstruction problem is undecidable
and cannot be recursively separated from normalization.
Pawe{\l} Urzyczyn