[Prev][Next][Index][Thread]

Re: On Weak and Strong Normalizations


[------ 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 lambda-calculi,
>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 (CPS-translation of any lambda term into the fragment
lambda-I 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 e-mail to rambo@diku.dk.
Here is the title and abstract:

Strong Normalization from Weak Normalization by 
A-Translation in Typed lambda-Calculi.

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 ``user-friendly.''  Our technique
is demonstrated to work on some well-known lambda-calculi including
higher-order polymorphic lambda-calculus. It gives hope for a positive
answer to an open problem concerning pure type systems.