Normalization properties of $λμ$-calculus using realizability semantics
Peter Battyanyi, Karim Nour
TL;DR
This paper addresses normalization in the simply typed λμ-calculus with classical logic by introducing a parameterized realizability semantics built on saturated sets. It develops a unifying framework that handles multiple reduction rules simultaneously, enabling strong normalization for βμρθε and weak normalization for βμμ'ρεθ within the same semantic model. The key technical advance is a modular saturation-based construction using a bottom set ⊥⊥ (and ⊥⊥') and a leadsto-based interpretation of function types, which yields adequacy results and pins down the uniqueness of the saturated typable-term set. The work clarifies how the presence or absence of the μ' rule affects normalization, and it points to a general method that could extend to richer type theories, including second-order classical logic, with potential implications for program extraction and proof normalization in classical settings.
Abstract
In this paper, we present a general realizability semantics for the simply typed $λμ$-calculus. Then, based on this semantics, we derive both weak and strong normalization results for two versions of the $λμ$-calculus equipped with specific simplification rules. The novelty in our method, in addition to its more systematic approach, lies in its applicability to a broader set of reduction rules without relying on the usual postponement technique. Our approach is original in that it introduces a parameter into the definition of the model, thus establishing a general result which we can then apply to systems with different sets of reduction rules by adjusting the parameter accordingly. Our saturation conditions also lead to a neat characterization of typable $λμ$-terms.