Affiliations: ULTRA Group (Useful Logics, Types, Rewriting, and their Automation), Heriot-Watt University, School of Mathematical and Computer Sciences, Mountbatten building, Edinburgh EH14 4AS, UK. [email protected]; [email protected]; [email protected]
Note: [] Address for correspondence: ULTRA Group (Useful Logics, Types, Rewriting, and their Automation), Heriot-Watt University, School of Mathematical and Computer Sciences, Mountbatten building, Edinburgh EH14 4AS, UK
Abstract: Reducibility, despite being quite mysterious and inflexible, has been used to prove a number of properties of the λ-calculus and is well known to offer general proofs which can be applied to a number of instantiations. In this paper, we look at two related but different results in λ-calculi with intersection types. 1. We show that one such result (which aims at giving reducibility proofs of Church-Rosser, standardisation and weak normalisation for the untyped λ-calculus) faces serious problems which break the reducibility method. We provide a proposal to partially repair the method. 2. We consider a second result whose purpose is to use reducibility for typed terms in order to show the Church-Rosser of β-developments for the untyped terms (and hence the Church-Rosser of β-reduction). In this second result, strong normalisation is not needed. We extend the second result to encompass both βI- and βη-reduction rather than simply β-reduction.
