Extensional and Non-extensional Functions as Processes

Abstract

Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $\hat{I}»$-calculus, the process representations yield (at best) non-extensional $\hat{I}»$-theories (i.e., ${\hat{I}}^2$ rule holds, whereas $\hat{I}\cdot$ does not). In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal $\ddot{I}€$, $\mathrm{I}\ddot{I}€$ (a subset of the $\ddot{I}€$-calculus in which all outputs are bound), we develop a refinement of Milner's original encoding of functions as processes that is parametric on certain abstract components called wires. These are, intuitively, processes whose task is to connect two end-point channels. We show that when a few algebraic properties of wires hold, the encoding yields a $\hat{I}»$-theory. Exploiting the symmetries and dualities of $\mathrm{I}\ddot{I}€$, we isolate three main classes of wires. The first two have a sequential behaviour and are dual of each other; the third has a parallel behaviour and is the dual of itself. We show the adoption of the parallel wires yields an extensional $\hat{I}»$-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite $\hat{I}\cdot$. In contrast, the other two classes of wires yield non-extensional $\hat{I}»$-theories whose equalities are those of the Lévy-Longo and Böhm trees.