一种反射式高阶演算的可编码性与分离性

Meredith与Radestock的$\rho$-演算（反射式高阶演算）是一种类$\pi$-演算语言，具有一些不寻常特征，特别是结构化名、自由名的运行时生成，以及缺少限制名可见性的算符。这些特征给可编码性与分离性结果的证明带来了一些有趣的困难。我们描述了Meredith与Radestock此前将$\pi$-演算编码进$\rho$-演算的尝试中的两个错误。随后我们给出一种新的编码并证明其正确性，使用了接近Gorla所提出标准的一组可编码性准则，并讨论了为适用于具有结构化名运行时生成的演算所需的调整。最后我们证明了一个分离结果，表明$\rho$-演算无法编码进$\pi$-演算。