Normalization for Fitch-Style Modal Calculi

TL;DR

This paper introduces a semantic normalization method for Fitch-style modal lambda calculi using normalization by evaluation, enabling modular proofs for various modal axioms and applications in programming languages.

Contribution

It develops a semantic NbE approach for Fitch-style modal calculi, handling multiple modal axioms and eta-equivalence, with mechanization in Agda.

Findings

Constructed NbE models for K, T, and 4 modal axioms

Achieved modular normalization proofs for Fitch-style calculi

Enabled applications in programming language semantics

Abstract

Fitch-style modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted by a lock. The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but each variant demands different, tedious and seemingly ad hoc syntactic lemmas to prove normalization. In this work, we take a semantic approach to normalization, called normalization by evaluation (NbE), by leveraging the possible-world semantics of Fitch-style calculi to yield a more modular approach to normalization. We show that NbE models can be constructed for calculi that incorporate the K, T and 4 axioms of modal logic, as suitable instantiations of the possible-world semantics. In addition to existing results that handle beta-equivalence, our normalization result also considers eta-equivalence for these calculi. Our key results have been mechanized in the proof assistant Agda. Finally, we showcase several consequences of normalization for proving meta-theoretic properties of Fitch-style calculi as well as programming-language applications based on different interpretations of the necessity modality.