Encodability and Separation for a Reflective Higher-Order Calculus

Abstract

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.