Re: On Weak and Strong Normalizations
Subject: Re: On Weak and Strong Normalizations
From: Morten Heine S|rensen <firstname.lastname@example.org>
Date: Mon, 19 Feb 1996 13:52:17 +0100 (MET)
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
>This is to anounce the availability of the paper
>"On Weak and Strong Normalisations"
>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 email@example.com.
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.
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.