[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
=============================================================================