Encodability and Separation for a Reflective Higher-Order Calculus

TL;DR

This paper addresses the challenges of encoding the $ ho$-calculus, a reflective higher-order calculus with unique features, by correcting previous errors, providing a new encoding, and establishing a separation result from the $ ho$-calculus to the $\pi$-calculus.

Contribution

It corrects prior encoding errors, introduces a new encoding of the $ ho$-calculus, and proves a separation result showing it cannot be encoded into the $\pi$-calculus.

Findings

Corrected previous encoding errors.

Provided a new, correct encoding of the $ ho$-calculus.

Proved that the $ ho$-calculus cannot be encoded into the $\pi$-calculus.

Abstract

The $\rho$-calculus (Reflective Higher-Order Calculus) of Meredith and Radestock is a $\pi$-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 $\pi$-calculus in the $\rho$-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 $\rho$-calculus cannot be encoded in the $\pi$-calculus.