[Prev][Next][Index][Thread]
New Paper Available
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The following paper is available by anonymous ftp from the following
sites:
theory/doc/ic.ac.uk in directory theory/papers/Scott
Homepage of P. Dybjer: http://www.cs.chalmers.se/~peterd
Homepage of P.J.Scott: http://www.csi.uottawa.ca/~phil/extra/papers
=======================================================================
Normalization and the Yoneda Embedding
by
Djordje Cubric, Peter Dybjer, and Philip Scott
We show how to solve the word problem for simply typed
\lambda\beta\eta-calculus by using a few well-known facts about
categories of presheaves and the Yoneda embedding. The formal setting
for these results is $\cP$-category theory, a version of ordinary
category theory where each hom-set is equipped with a partial
equivalence relation. The part of $\cP$-category theory we develop
here is constructive and thus permits extraction of programs. It is
this intuitionistic aspect of our work which is fundamental to
obtaining a normalization algorithm.
In a certain sense, our program is dual to J. Lambek's original goal
of categorical proof theory, in which he used cut-elimination to study
categorical coherence problems. Here, we use a method inspired from
categorical coherence proofs to normalize lambda terms (and thus
intuitionistic proofs). It is important to stress that in our method, we
make no use of traditional proof-theoretic or rewriting techniques.