language: en

Weak and Strong Beta Normalisations in Typed -Calculi

Hongwei Xi
Department of Mathematical Sciences Carnegie Mellon University
Pittsburgh, PA 15213, USA

Abstract. We present a technique to study relations between weak and strong fi-normalisations in various typed -calculi. We first introduce a translation which translates a -term into a I-term, and show that a -term is strongly fi-normalisable if and only if its translation is weakly fi-normalisable. We then prove that the translation preserves typability of -terms in various typed -calculi. This enables us to establish the equivalence between weak and strong fi-normalisations in these typed -calculi. This translation can deal with Curry typing as well as Church typing, strengthening some recent closely related results. This may bring some insights into answering whether weak and strong fi-normalisations in all pure type systems are equivalent.

1 Introduction