New papers available by ftp
The following three papers are now available by anonymous ftp.
The first paper (Reducibility Strikes Again, I!)
is more a set of notes, since most of
the results are known (Coppo, Dezani, Pottinger).
However, I prove more general results, and I use
a version of reducibility which also has some new twists.
It is an "untyped version" of what I used in my "Cahiers paper", which
really is "Reducibility Strikes Again, II!", but was
named more conservatively (and previously announced on "types").
These notes are very heavily inspired by Krivine's book,
and this should inspire people to read it.
I also characterize the lambda terms that are
weakly head-normalizing in terms of
a system with intersection types.
The next two papers are really just one paper, but since it is quite long,
I thought it would be best to divide into two parts.
I would like to thank Jim Lipton for telling me that
conditions on candidates of reducibility can be viewed
as sheaf conditions, and for other invaluable suggestions
and remarks. Without his contribution, I would not have been able
to write these two papers.
Comments are very welcomed.
-- Jean Gallier
Reducibility Strikes Again, I!
Abstract. In these notes, we prove some general theorems
for establishing properties of untyped lambda-terms, using a variant
of the reducibility method. These theorems apply to
(pure) lambda-terms typable in the systems of
conjunctive types DO and D. As applications, we
give simple proofs of the characterizations of the terms having
head-normal forms, of the normalizable terms, and of the
strongly normalizing terms. We also give a characterization
of the terms having weak head-normal forms.
This last result appears to be new.
Realizability, Covers, and Sheaves.
I. Applications to the Simply-Typed lambda-Calculus
II. Applications to the Second-Order Typed lambda-Calculus
Abstract. We present a general method for proving properties
of typed $\lambda$-terms. This method is obtained by introducing
a semantic notion of realizability which uses the notion of
a cover algebra (as in abstract sheaf theory,
a cover algebra being a Grothendieck topology in the case of a preorder).
For this, we introduce a new class of semantic structures equipped with
preorders, called pre-applicative structures.
These structures need not be extensional. In this framework,
a general realizability theorem can be shown.
Kleene's recursive realizability and
a variant of Kreisel's modified realizability both fit into this framework.
Applying this theorem to the special case of the term model, yields
a general theorem for proving properties of typed lambda-terms,
in particular, strong normalization and confluence.
This approach clarifies the reducibility method by showing
that the closure conditions on candidates of reducibility can be viewed
as sheaf conditions.
Part I of this paper applies the above approach to
the simply-typed lambda-calculus
(with types -->, X, +, and false).
Part II of this paper deals with the second-order
(polymorphic) lambda-calculus (with types --> and forall).
The file names for the above two papers are
The above paper(s) can be retrieved by anonymous ftp using the
% ftp ftp.cis.upenn.edu
Password: <<your e-mail address>>
ftp> cd pub/papers/gallier
ftp> get filename.dvi.Z
Then, use the unix "uncompress" command on this file to
get the dvi file(s).