On Weak and Strong Normalisations

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

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.

Hongwei Xi

Mathematics Department
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213

Telphone: +1 412 268 1439
Fax:      +1 412 268 6380
E-mail:   hwxi@cs.cmu.edu
URL:      http://www.cs.cmu.edu/afs/cs/user/hwxi/www/hwxi.html


With the help of continuations, we first construct a transformation
T which transforms every lambda-term t into a (lambda I)-term T(t).
Then we apply the conservation theorem in lambda-calculus to show that
t is strongly normalisable if T(t) has a beta-normal form. In this way,
we succeed in establishing the equivalence between weak and strong
normalisation theorems in various typed lambda$-calculi. This not only
enhances the understanding between weak and strong normalisations, but
also presents an elegant approach to proving strong normalisation
theorems via the notion of weak normalisations.