On modular properties of higher order extensional lambda calculi

Abstract

We prove that confluence and strong normalisation are both modular properties for the addition of algebraic term rewriting systems to Girard's Fω equipped with either β-equaiity or βη-equality. The key innovation is the use of ηexpansions over the more traditional jj-contractions. We then discuss the difficulties encountered in generalising these results to type theories with dependent types. Here confluence remains modular, but results concerning strong normalisation await further basic research into the use of ηexpansions in dependent type theory.