作为进程的热切函数

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