Normalisation in weakly orthogonal rewriting


A rewrite sequence is said to be outermost-fair if every outermost redex occurrence is eventually eliminated. Outermost-fair rewriting is known to be (head-)normalising for almost orthogonal rewrite systems. In this paper we study (head-)normalisation for the larger class of weakly orthogonal rewrite systems. Normalisation is established and a counterexample against head-normalisation is provided. Nevertheless, infinitary normalisation, which is usually obtained as a corollary of head-normalisation, is shown to hold.