一句话：提出一种依赖惰性与并发的可转换性检查算法，总能找到存在的简单解，避免启发式带来的冗余计算。
可转换性检查——判定两个 lambda 项是否在归约意义下相等——是证明助手与依赖类型语言的核心组件。实际实现常用启发式快速判定两词项是否可转换，而不将其归约到正规形式，但这类启发式可能适得其反，触发大量无用的计算。本文提出一种全新的可转换性检查算法，其关键在于惰性与并发：惰性用于共享计算，避免重复归约；并发用于并行或公平交错地探索多个可转换性子问题。与基于启发式的方法不同，只要可转换性问题存在简单解，该算法总能找到它。论文以进程演算风格描述算法，讨论其复杂度，并报告了部分正确性的机器化证明与轻量级实验评估。
Convertibility checking — determining whether two lambda-terms are equal up to reductions — is a crucial component of proof assistants and dependently-typed languages. Practical implementations often use heuristics to quickly conclude that two terms are convertible, or are not convertible, without reducing them to normal form. However, these heuristics can backfire, triggering huge amounts of unnecessary computation. This paper presents a novel convertibility-checking algorithm that relies crucially on laziness and concurrency . Laziness is used to share computations, while concurrency is used to explore multiple convertibility subproblems in parallel or via fair interleaving. Unlike heuristics-based approaches, our algorithm always finds an easy solution to the convertibility problem, if one exists. The paper describes the algorithm in process calculus style, discusses its complexity, and reports on its mechanized proof of partial correctness and its lightweight experimental evaluation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{CourantL26,
title = {A Lazy, Concurrent Convertibility Checker},
author = {Nathanaëlle Courant and Xavier Leroy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776695}
}