Matching in the Pi-Calculus (Technical Report)

TL;DR

This paper investigates whether the match prefix in the pi-calculus can be expressed using other operators and demonstrates, under relaxed criteria, that it cannot be encoded, strengthening previous non-expressibility results.

Contribution

It provides a stronger separation result showing the match prefix's non-expressibility in the pi-calculus under Gorla's relaxed encoding criteria.

Findings

Match prefix cannot be expressed using other operators in the pi-calculus.

Stronger non-expressibility separation under relaxed encoding criteria.

Extends previous results with more general non-encodability proof.

Abstract

We study whether, in the pi-calculus, the match prefix---a conditional operator testing two names for (syntactic) equality---is expressible via the other operators. Previously, Carbone and Maffeis proved that matching is not expressible this way under rather strong requirements (preservation and reflection of observables). Later on, Gorla developed a by now widely-tested set of criteria for encodings that allows much more freedom (e.g. instead of direct translations of observables it allows comparison of calculi with respect to reachability of successful states). In this paper, we offer a considerably stronger separation result on the non-expressibility of matching using only Gorla's relaxed requirements.