[Prev][Next][Index][Thread]
paper available by ftp
The following paper, a revised version of an older paper, is
available by ftp (see below):
Kripke models and the (in)equational logic of
the second-order lambda-calculus
We define a new class of Kripke structures for the second-order
lambda-calculus, and investigate the soundness and completeness of
some proof systems for proving inequalities (rewrite rules) as well as
equations. The Kripke structures under consideration are equipped
with preorders that correspond to an abstract form of reduction, and
they are not necessarily extensional. A novelty of our approach is
that we define these structures directly as functors A: worlds ->
Preor equipped with certain natural transformations corresponding to
application and abstraction (where worlds is a preorder, the set of
worlds, and Preor is the category of preorders). We make use of an
explicit construction of the exponential of functors in the
Cartesian-closed category Preor^{worlds}, and we also define a kind of
exponential to take care of type abstraction. However, we strive for
simplicity, and we only use very elementary categorical
concepts. Consequently, we believe that the models described in this
paper are more palatable than abstract categorical models which
require much more sophisticated machinery (and are not models of
rewrite rules anyway). We obtain soundness and completeness theorems
that generalize some results of Mitchell and Moggi to the second-order
lambda-calculus, and to sets of inequalities (rewrite rules).
Available by anonymous ftp as
kripke1.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).