论文标题
反射高阶演算的编码和分离
Encodability and Separation for a Reflective Higher-Order Calculus
论文作者
论文摘要
Meredith和RadeStock的$ρ$ -Calculus（反射性的高阶计算）是一种$π$ -Calculus的语言，具有某些不寻常的功能，特别是结构化的名称，免费名称的运行时生成，并且缺乏用于范围范围的操作员。这些功能在证明具有共同性和分离结果的证明方面构成了一些有趣的困难。我们在先前发表的尝试中描述了两个错误，该错误是在Meredith和Radestock的$ρ$ -Calculus中编码$π$ -calculus。然后，我们使用与Gorla提出的一组编码标准一起给出了一个新的编码并证明其正确性，并讨论与结构化名称的运行时生成的微积分所必需的改编。最后，我们证明了一个分离结果，表明$ρ$ -calculus不能在$π$ -calculus中编码。
The $ρ$-calculus (Reflective Higher-Order Calculus) of Meredith and Radestock is a $π$-calculus-like language with some unusual features, notably, structured names, runtime generation of free names, and the lack of an operator for scoping visibility of names. These features pose some interesting difficulties for proofs of encodability and separation results. We describe two errors in a previously published attempt to encode the $π$-calculus in the $ρ$-calculus by Meredith and Radestock. Then we give a new encoding and prove its correctness, using a set of encodability criteria close to those proposed by Gorla, and discuss the adaptations necessary to work with a calculus with runtime generation of structured names. Lastly we prove a separation result, showing that the $ρ$-calculus cannot be encoded in the $π$-calculus.
