Extensional and Non-extensional Functions as Processes
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866914039307698176 |
|---|---|
| author | Sakayori, Ken Sangiorgi, Davide |
| author_facet | Sakayori, Ken Sangiorgi, Davide |
| contents | 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 $π$, $\mathrm{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 $\mathrm{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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_03536 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Extensional and Non-extensional Functions as Processes Sakayori, Ken Sangiorgi, Davide Logic in Computer Science Programming Languages 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 $π$, $\mathrm{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 $\mathrm{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. |
| title | Extensional and Non-extensional Functions as Processes |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2405.03536 |