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

Two papers on reducibility


The following two papers are available by ftp (see below).
Both are are revised versions of earlier papers.
The first one is to appear in TCS (June-July 95?), and the second
one is more of a tutorial in nature.
Together with my earlier

             ``On the Correspondence Between
                  Proofs and lambda-Terms''

to appear any day in the ``Cahiers du Centre de Logique de Louvain'',
(edited by Philippe de Groote), these papers constitute
a fairly unified view of the reducibility method and its
applications. If not already fluent with the method,
I would suggest starting with the above paper,
or the second of the two listed below.


Happy Holidays
(and don't forget about geometric intuitions!)

-- Kurt W.A.J.H.Y. Reillag
   Hospices de Beaune

================================================================= 
             Proving Properties of Typed lambda-Terms
             Using Realizability, Covers, and Sheaves

The main purpose of this paper is to take apart the reducibility
method in order to understand how its pieces fit together, and in
particular, to recast the conditions on candidates of reducibility as
sheaf conditions.  There has been a feeling among experts on this
subject that it should be possible to present the reducibility method
using more semantic means, and that a deeper understanding would then
be gained.  This paper gives mathematical substance to this feeling,
by presenting a generalization of the reducibility method based on a
semantic notion of realizability which uses the notion of a cover
algebra (as in abstract sheaf theory).  A key technical ingredient is
the introduction 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.  We are
then able to prove a meta-theorem which shows that if a property of
realizers satisfies some simple conditions, then it holds for the
semantic interpretations of all terms.  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. The above approach is applied to the
simply-typed lambda-calculus (with types rightarrow, times, +, and
false), and to the second-order (polymorphic) lambda-calculus (with
types rightarrow and forall^{2}), for which it yields a new theorem.


Available as

psheaf1.dvi.Z, or
psheaf1.ps.Z

========================================================================

            Typing untyped lambda-terms, or
              Reducibility strikes again!


It was observed by Curry that when (untyped) lambda-terms can be
assigned types, for example, simple types, these terms have nice
properties (for example, they are strongly normalizing). Coppo,
Dezani, and Veneri, introduced type systems using conjunctive types,
and showed that several important classes of (untyped) terms can be
characterized according to the shape of the types that can be assigned
to these terms.  For example, the strongly normalizable terms, the
normalizable terms, and the terms having head-normal forms, can be
characterized in some systems D and DO. The proofs use variants of the
method of reducibility. In this paper, we present a uniform approach
for proving several meta-theorems relating properties of lambda-terms
and their typability in the systems D and DO. Our proofs use a new and
more modular version of the reducibility method. As an application of
our metatheorems, we show how the characterizations obtained by Coppo,
Dezani, Veneri, and Pottinger, can be easily rederived.  We also
characterize the terms that have weak head-normal forms, which appears
to be new.  We conclude by stating a number of challenging open
problems regarding possible generalizations of the realizability
method.


Available as

DDOreduc.dvi.Z, or
DDOreduc.ps.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).