一句话：给出从半统一到 System F 可类型性的直接归约，简化经典不可判定性证明并在 Coq 中机器验证。
论文重新审视 System F（多态 lambda 演算）的可类型性（typability）与类型检查（type checking）不可判定性。Wells 在 1990 年代证明二者不可判定，其中类型检查可归约自 semi-unification，而可类型性依赖复杂的 invariant type assumptions 演算，整体论证难以概览。本文给出从 semi-unification 到 System F 可类型性的更简单、直接归约：在存在式可类型性设定中，只需考虑特定类型推导，且只需闭类型、无嵌套量化。类型检查不可判定性则通过民间归约从可类型性得到。作者在 Coq 中机器验证该方法的正确性，并集成到现有不可判定性证明库；该库免费提供从图灵机停机到 System F 可类型性与类型检查的构造性多一归约。
The undecidability of both typability and type checking for System F (polymorphic lambda-calculus) was established by Wells in the 1990s. For type checking Wells gave an astonishingly simple reduction from semi-unification (first-order unification combined with first-order matching). For typability Wells developed an intricate calculus to control the shape of type assumptions across type derivations via term structure. This calculus of invariant type assumptions allows for a reduction from type checking to typability. Unfortunately, this approach relies on heavy machinery that complicates surveyability of the overall argument. The present work gives comparatively simple, direct reduction from semi-unification to System F typability. The key observation is as follows: in the existential setting of typability, it suffices to consider some specific (but not all, as for invariant type assumptions) type derivations. Additionally, the particular result requires only to consider closed types without nested quantification. The undecidability of type checking is obtained via a folklore reduction from typability. Profiting from its smaller footprint, correctness of the new approach is witnessed by a mechanization in the Coq proof assistant. The mechanization is incorporated into the existing Coq library of undecidability proofs. For free, the library provides constructive, mechanically verified many-one reductions from Turing machine halting to both System F typability and System F type checking.
DOI 原文 ·
@inproceedings{paperbot6240,
title = {The Undecidability of System F Typability and Type Checking for Reductionists},
author = {Andrej Dudenhefner},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470520}
}