On weak and strong normalisations

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 ╬▓-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.