Yet Another Strong Normalization Proof...

To: types@uk.ac.gla.dcs
Subject: Yet Another Strong Normalization Proof...
From: alti@uk.ac.ed.dcs
Date: Tue, 26 Jan 93 14:53:13 GMT
Approved: types@dcs.gla.ac.uk


... for the Calculus of Constructions

I would like to make this paper available by anonymous ftp to an
interested audience. It appeared in the proceedings of the
Wintermoetet of the Chalmers Technical University this year.

Here is the abstract:

   In this note we give a strong normalization argument for the pure
   calculus of constructions which is based on a certain model
   construction, i.e.  $\omega$-Sets with PERs. We replace $\omega$ by
   preterms and define an interpretation of the calculus in such a way
   that realizers are always strongly normalizing. After checking that
   every derivation of a term is realized by its subject we can conclude
   strong normalization.

My intention with this construction was to give a strong normalization
argument for the CoC which can be understood as the straightforward
generalization of the standard Girard-Tait-style argument. The idea is
that you can understand SN proofs as a modification of a realizibility
model and that one has just to apply the same trick to the \omega-Set
model of CoC. This may be interesting for anybody who wants to show SN
for a related system.

I should point out that this is certainly related to Ong's and
Hyland's work on categorical SN proofs. However, I believe that my
construction is different and I don't use any category theory :-)
[Actually, I did use category theory when developing the proof but
this is not used in the presentation].

It is available by anonymous ftp from ftp.dcs.ed.ac.uk. The directory
is export/alti and the file is sn-coc.dvi.Z . It is a compressed dvi
file which should be printable on all standard installations. If you
have any trouble in obtaining, uncompressing or printing it, just send
me a mail.