Encodability and Separation for a Reflective Higher-Order Calculus

Stian Lybech

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.

In Valentina Castiglioni and Claudio A. Mezzina: Proceedings Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics (EXPRESS/SOS 2022), Warsaw, Poland, 12th September 2022, Electronic Proceedings in Theoretical Computer Science 368, pp. 95–112.
Published: 6th September 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.368.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org