From pi-Calculus to Higher-Order pi-Calculus - and Back
From pi-Calculus to Higher-Order pi-Calculus - and Back
复制标题
DOI：
10.1007/3-540-56610-4_62
复制
发表时间：
1993-04
期刊：
影响因子：
--
通讯作者：
D. Sangiorgi
中科院分区：
文献类型：
--
作者：
D. Sangiorgi
我们比较了一阶范式和高阶范式在过程代数中迁移率的表示。一阶范式中的典型演算是π演算。通过推广其排序机制，我们得到了ω阶的推广，称为高阶π -微积分。我们给出了它的应用实例，包括λ-微积分的编码。令人惊讶的是，我们证明了这样的扩展并没有增加表达性：高阶过程可以忠实地在一阶表示。我们的结论是，一阶范式具有更简单和更直观的理论，应该作为基本的。然而，λ演算编码的研究表明，高阶演算对于更抽象的推理是非常有用的。
We compare the first-order and the higher-order paradigms for the representation of mobility in process algebras. The prototypical calculus in the first-order paradigm is theπ -calculus. By generalising its sort mechanism we derive an ω-order extension, calledHigher-Order π - calculus. We give examples of its use, including the encoding ofλ-calculus. Surprisingly, we show that such an extension does not add expressiveness: Higher-order processes can be faithfully represented at first order. We conclude that the first-order paradigm, which enjoys a simpler and more intuitive theory, should be taken asbasic. Nevertheless, the study of the λ-calculus encodings shows that a higher-order calculus can be very useful for reasoning at a more abstract level.