Extensional and Non-extensional Functions as Processes

TL;DR

This paper explores how to represent functions as processes in the $ ext{I}oldsymbol{ extpi}$ calculus to achieve extensional and non-extensional $oldsymbol{ extlambda}$-theories, connecting process encodings with classical $oldsymbol{ extlambda}$-theories.

Contribution

It introduces a parametric encoding of functions as processes using wires in $ ext{I}oldsymbol{ extpi}$, enabling the derivation of extensional and non-extensional $oldsymbol{ extlambda}$-theories.

Findings

Parallel wires produce an extensional $oldsymbol{ extlambda}$-theory matching B"ohm trees with infinite $oldsymbol{ exteta}$.

Sequential wires yield non-extensional theories aligned with Lévý-Longo and B"ohm trees.

The encoding clarifies the relationship between process representations and classical $oldsymbol{ extlambda}$-theories.

Abstract

Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure $\lambda$-calculus, the process representations yield (at best) non-extensional $\lambda $-theories (i.e., $\beta$ rule holds, whereas $\eta$ does not). In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal $\pi$, $\mathrm{I}\pi$ (a subset of the $\pi$-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 $\lambda$-theory. Exploiting the symmetries and dualities of $\mathrm{I}\pi$, 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 $\lambda$-theory; in fact, it yields an equality that coincides with that of B\"ohm trees with infinite $\eta$. In contrast, the other two classes of wires yield non-extensional $\lambda$-theories whose equalities are those of the L\'evy-Longo and B\"ohm trees.