Resource approximation for the $λμ$-calculus
Fuente:
arXiv
Gespeichert in:
| 1. Verfasser: | |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912033336721408 |
|---|---|
| author | Barbarossa, Davide |
| author_facet | Barbarossa, Davide |
| contents | The $λμ$-calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not satisfy Böhm's Theorem and it lacks the corresponding notion of approximation. On the contrary, we show that Ehrhard and Regnier's Taylor expansion can be easily adapted, thus providing a resource conscious approximation theory. This produces a sensible $λμ$-theory with which we prove some advanced properties of the $λμ$-calculus, such as Stability and Perpendicular Lines Property, from which the impossibility of parallel computations follows. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_11587 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Resource approximation for the $λμ$-calculus Barbarossa, Davide Logic in Computer Science The $λμ$-calculus plays a central role in the theory of programming languages as it extends the Curry-Howard correspondence to classical logic. A major drawback is that it does not satisfy Böhm's Theorem and it lacks the corresponding notion of approximation. On the contrary, we show that Ehrhard and Regnier's Taylor expansion can be easily adapted, thus providing a resource conscious approximation theory. This produces a sensible $λμ$-theory with which we prove some advanced properties of the $λμ$-calculus, such as Stability and Perpendicular Lines Property, from which the impossibility of parallel computations follows. |
| title | Resource approximation for the $λμ$-calculus |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2409.11587 |