作为进程的热切函数（长版本）

我们研究 Milner 将 call-by-value $\lambda$-演算编码进 $\pi$-演算的方法。我们表明，通过将编码调谐至 $\pi$-演算的两个子演算（Internal $\pi$ 与 Asynchronous Local $\pi$），该编码在 $\lambda$-项上诱导的等价恰为 Lassen 的热切范式双模拟等价（扩展以处理 $\eta$-等式）。作为 $\pi$-演算中的行为等价，我们考虑上下文等价与带刺同余。我们亦将结果扩展至预序。证明中一个关键的技术成分是近期引入的方程唯一解技术，本文对其作了进一步发展。就此而言，本文亦旨在成为该技术适用性与表达力的一个扩展案例研究。