Normalization proofs for the un-typed μμ-calculus

Abstract

A long-standing open problem of Parigot has been solved by David and Nour, namely, they gave a syntactical and arithmetical proof of the strong normalization of the untyped μμ'-reduction. In connection with this, we present in this paper a proof of the weak normalization of the μ and μ'-rules. The algorithm works by induction on the complexity of the term. Our algorithm does not necessarily give a unique normal form: sometimes we may get different normal forms depending on our choice. We also give a simpler proof of the strong normalization of the same reduction. Our proof is based on a notion of a norm defined on the terms.

Keywords

• <i>λμ</i>-calculus
• <i>μμ</i>'-calculus
• strong normalization
• weak normalization
• normalization algorithm