一句话：提出基于求值规范化的语义方法，为 Fitch 风格模态 λ-演算提供模块化规范化证明，覆盖 K/T/4 公理并机器化验证。
Fitch 风格模态 λ-演算通过引入锁（lock）扩展类型语境，简化了不同模态公理的类型规则表述，但每种变体都需要繁琐且特设的语法引理来证明规范化。本文采用语义方法——基于求值的规范化（NbE），利用 Fitch 风格演算的可能世界语义，构造出对应于模态逻辑 K、T、4 公理的 NbE 模型，从而以模块化方式证明规范化。与已有工作仅处理 β-等价不同，本文的结果还涵盖了 η-等价。关键结果已在证明助手 Agda 中机器化验证。最后展示了规范化在证明 Fitch 风格演算元理论性质以及基于必然模态不同解释的编程语言应用中的若干推论。
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 𝛽-equivalence, our normalization result also considers 𝜂-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.
@article{paperbot1476,
title = {Normalization for fitch-style modal calculi},
author = {Nachiappan Valliappan and Fabian Ruch and Carlos Tomé Cortiñas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {ICFP},
year = {2022},
doi = {10.1145/3547649}
}