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 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 presents the algorithm in process calculus style and discusses its mechanized proof of partial correctness, its complexity, and its lightweight experimental evaluation.

翻译：可转换性检查——判断两个λ项在归约意义下是否相等——是证明辅助工具和依赖类型语言的核心组件。实际实现通常采用启发式方法，在不将项归约为正规形的情况下快速判定两项是否可转换。然而，这些启发式方法可能适得其反，引发大量不必要的计算。本文提出一种新颖的可转换性检查算法，其核心依赖于惰性求值与并发机制：惰性用于共享计算过程，并发则用于并行或通过公平交错方式探索多个可转换性子问题。与基于启发式的方法不同，本算法始终能在存在简单解时找到可转换性问题的简易解法。论文以进程演算风格呈现该算法，并讨论其部分正确性的机械化证明、复杂度分析及轻量级实验评估。