[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.