将功能作为过程进行评估
Evaluating functions as processes
摘要：
米尔纳的一个著名的结果是，π演算可以在π演算中模拟出π演算。然而，这种模拟只在进程上保持模强双相似性，即β约简与π演算中的模拟方式之间存在轻微的不匹配。这个想法是，在π演算中计算一个可达项就像运行一个基于环境的抽象机器，而不是应用普通的beta归约。在本文中，我们表明，这样一个抽象的机器评估对应于线性弱头减少，从表示的线性逻辑证明网的EQUIDA条款所产生的战略，这两者之间的关系是紧密的，因为它可以。该研究也顺利改写呼叫的价值的情况下，引入了呼叫的价值类似的线性弱头减少。
英文摘要：
A famous result by Milner is that the lambda-calculus can be simulated inside the pi-calculus. This simulation, however, holds only modulo strong bisimilarity on processes, i.e. there is a slight mismatch between beta-reduction and how it is simulated in the pi-calculus. The idea is that evaluating a lambda-term in the pi-calculus is like running an environment-based abstract machine, rather than applying ordinary beta-reduction. In this paper we show that such an abstract-machine evaluation corresponds to linear weak head reduction, a strategy arising from the representation of lambda-terms as linear logic proof nets, and that the relation between the two is as tight as it can be. The study is also smoothly rephrased in the call-by-value case, introducing a call-by-value analogous of linear weak head reduction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
