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

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

DDOreduc.dvi.Z
realiz1.dvi.Z
realiz2.dvi.Z

The above paper(s) can be retrieved by anonymous ftp using the
instructions below.

% ftp ftp.cis.upenn.edu
Name: anonymous
Password:  <<your e-mail address>>
ftp> cd pub/papers/gallier
ftp> binary
ftp> get  filename.dvi.Z
ftp> quit

Then, use the unix "uncompress" command on this file to
get the dvi file(s).