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

Inhabitation in F (Loeb's thm.)



The following paper is available from my Web page:

             http://zls.mimuw.edu.pl/~urzy/ftp.html

or by anonymous ftp from 
                machine:    ftp.mimuw.edu.pl
              directory:    /pub/users/urzy
                  files:    loeb.{dvi,ps}.Z


 Title:  Inhabitation in typed lambda-calculi (a syntactic approach).
                   Author:  Pawel Urzyczyn 

                          Abstract

A type is inhabited (non-empty) in a typed calculus iff there is a closed 
term of this type. The inhabitation (emptiness) problem is to determine
if a given type is inhabited. This paper provides direct, purely syntactic 
proofs of the following results: the inhabitation problem is PSPACE-complete 
for simply typed lambda-calculus and undecidable for the polymorphic second-
order and higher-order lambda calculi (systems F and F-omega). 

By Curry-Howard isomorphism, these lambda calculi correspond to propositional 
intuitionistic logics. Thus, two of the above three results are immediate 
consequences of Statman's and Loeb's results about zero-order and second-order
propositional intuitionistic logics.  However, the present proofs (esp. that
of Loeb's theorem) are much simpler than the existing ones. In addition, the 
proof of Loeb's theorem, being entirely syntactic, does not rely on any 
completeness result. 

The motivation for this work was to provide a way to explain these results
in a comprehensible way to a reader familiar with lambda-calculus but not
necessarily with the proof theory and model theory of intuitionistic logic.
The author hopes that the goal was achieved, at least in part.

=============================================================================
Pawel Urzyczyn                                              urzy@mimuw.edu.pl
Institute of Informatics              http://zls.mimuw.edu.pl/~urzy/home.html
University of Warsaw                           direct phone: +48-22-658-43-77
Banacha 2,  room #4280                          main office: +48-22-658-31-65
02-097 Warszawa, Poland                                 fax: +48-22-658-31-64
=============================================================================