Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure λ-calculus, the process representations yield (at best) non-extensional λ-theories (i.e., β rule holds, whereas η does not).In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal π, Iπ (a subset of the π-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 λ-theory. Exploiting the symmetries and dualities of 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 λ-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite η. In contrast, the other two classes of wires yield non-extensional λ-theories whose equalities are those of the Lévy-Longo and Böhm trees.
Extensional and Non-extensional Functions as Processes / Sakayori K.; Sangiorgi D.. - STAMPA. - 2023-:(2023), pp. 1-13. (Intervento presentato al convegno 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023 tenutosi a Boston University, usa nel June 26-29, 2023) [10.1109/LICS56636.2023.10175686].
Extensional and Non-extensional Functions as Processes
Sakayori K.;Sangiorgi D.
2023
Abstract
Following Milner's seminal paper, the representation of functions as processes has received considerable attention. For pure λ-calculus, the process representations yield (at best) non-extensional λ-theories (i.e., β rule holds, whereas η does not).In the paper, we study how to obtain extensional representations, and how to move between extensional and non-extensional representations. Using Internal π, Iπ (a subset of the π-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 λ-theory. Exploiting the symmetries and dualities of 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 λ-theory; in fact, it yields an equality that coincides with that of Böhm trees with infinite η. In contrast, the other two classes of wires yield non-extensional λ-theories whose equalities are those of the Lévy-Longo and Böhm trees.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.