一句话：通过语法方法恢复满射配对下类型转换的可判定性，并用 Rocq 机械化验证。
在依赖类型论中，若等式理论为 β-等价，无类型归约的合流性与终止性可直接用于证明类型转换可判定：只需比较输入的 β-正规形是否相等。然而加入满射配对（即对的 η 律）后，βη-归约不再合流，这一经典技术失效。本文采用已有的语法技术解决由满射配对导致的合流性问题，从而恢复基于合流的类型转换可判定性证明。与依赖 Kripke 式逻辑关系等语义工具的已有证明开发不同，该证明模块化地组合了无类型规范化的最小语义证明与可判定性的语法证明，且无需修改最小语义证明。作者已在 Rocq 定理证明器中完全机械化所有结果。
In a dependent type theory with β -equivalence as its equational theory, the confluence of untyped reduction and termination immediately give us a proof of the decidability of type conversion, where the decision procedure for convertibility simply checks the equality of the β -normal forms of its inputs. This technique is not available in the presence of surjective pairing (i.e. the η -law for pairs) because β η -reduction is not confluent. In this work, we show that by adopting established syntactic techniques, we can resolve the issue with confluence caused by surjective pairing, and recover a confluence-based proof of decidability of type conversion. Compared to existing proof developments, which rely on semantic tools such as Kripke-style logical relations, our proof modularly composes a minimal semantic proof of untyped normalization and a syntactic proof of decidability. This modularity enables us to explore algorithmic conversion through syntactic methods without modifying the minimal semantic proof. We have fully mechanized our results using the Rocq theorem prover.
@article{LiuW26,
title = {Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach},
author = {Yiyun Liu and Stephanie Weirich},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776672}
}