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

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
USA

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
**********************

-------------------------------------------------------------------------
Abstract

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.