[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.