[Prev][Next][Index][Thread]
Re: On Weak and Strong Normalizations

To: types@dcs.gla.ac.uk

Subject: Re: On Weak and Strong Normalizations

From: Morten Heine Srensen <rambo@diku.dk>

Date: Mon, 19 Feb 1996 13:52:17 +0100 (MET)

Approved: types@dcs.gla.ac.uk
[ The Types Forum  http://www.dcs.gla.ac.uk/~types ]
HongWei_Xi@CTPS.TPS.CS.CMU.EDU writes:
>This is to anounce the availability of the paper
>"On Weak and Strong Normalisations"
>by http://www.cs.cmu.edu/afs/cs/user/hwxi/www/papers/WS.ps
>This paper basically shows why there exists no difference between
>weak and strong normalisations in various typed lambdacalculi,
>and hence, there is no need of complicating methods for proving
>strong normalisation since weak normalisation is equally strong.
For the sake of completeness I would like to announce some very
similar work that I did a couple of months ago. After briefly reading
through Xi's paper it would appear that the techniques we use are
identical (CPStranslation of any lambda term into the fragment
lambdaI in which weak and strong normalization are equivalent). The
main difference seems to be that the technicalities in Xi's paper are
less tedious than in my paper, whereas I on the other hand apply the
technique to more systems and use more traditional formulations of the
typed lambda calculi in question.
If you are interested in a copy of my draft, send an email to rambo@diku.dk.
Here is the title and abstract:
Strong Normalization from Weak Normalization by
ATranslation in Typed lambdaCalculi.
Morten Heine S\o rensen
Department of Computer Science, University of Copenhagen, and
Faculty of Mathematics & Informatics, Catholic University of Nijmegen.
Abstract:
We present a technique to reduce the problem of proving strong
normalization for a notion of reduction in a natural deduction logic
or in a typed lambda calculus to the problem of proving weak
normalization for the same notion of reduction in the same system; the
latter problem is easier to solve for some systems. Previous
techniques reduce the strong normalization problem for one notion of
reduction to the weak normalization problem for a more complicated
notion of reduction, and so are less ``userfriendly.'' Our technique
is demonstrated to work on some wellknown lambdacalculi including
higherorder polymorphic lambdacalculus. It gives hope for a positive
answer to an open problem concerning pure type systems.