Beluga 对 $\pi$-演算中和谐引理的形式化

“和谐引理”(Harmony Lemma)，由 Sangiorgi & Walker 形式化，建立了标记传递语义与 $\pi$-演算中约化语义之间的等价性。尽管这一结果在标准 $\pi$-演算中广为人知且被接受，但从未进行过严格的形式化证明，无论正式还是非正式。因此，在考虑 $\pi$-演算的扩展时，其有效性可能并不立即显而易见。为迎合 Concurrent Calculi Formalization Benchmark 的第二个挑战——一套针对机制化并发系统主要问题的挑战——我们在 Benchmark 中检讨的 $\pi$-演算片段上 presented了一个该结果的形式化。我们的形式化在 Beluga 中实现，并受到 Honsell 等人流行的 HOAS 形式化 LTS 语义的启发。在此过程中，我们引入了几个处理 telescope 和 lexicographic induction 的有用编码技术。