Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2605.09179 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911667462340608 |
|---|---|
| author | Pizzo, Nicolò Coen, Claudio Sacerdoti |
| author_facet | Pizzo, Nicolò Coen, Claudio Sacerdoti |
| contents | Landauer's embeddings enable the reversibility of computations for non-reversible programming languages, augmenting each intermediate state with enough data to reconstruct the previous state. An interesting research question is therefore to try to reduce the space overhead required. In this work we propose a Landauer's embedding for Plotkin's call-by-value calculus (CbV). In order to control the computational complexity of CbV and turn the number of $β$-steps into a cost model, CbV is typically implemented via reduction machines. We show that one machine, that has not received much attention, exhibits a particularly compact Landauer's embedding, requiring only constant space overhead for each step. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_09179 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Reversible Crumbling Abstract Machine for Plotkin's Call-by-Value Pizzo, Nicolò Coen, Claudio Sacerdoti Logic in Computer Science Landauer's embeddings enable the reversibility of computations for non-reversible programming languages, augmenting each intermediate state with enough data to reconstruct the previous state. An interesting research question is therefore to try to reduce the space overhead required. In this work we propose a Landauer's embedding for Plotkin's call-by-value calculus (CbV). In order to control the computational complexity of CbV and turn the number of $β$-steps into a cost model, CbV is typically implemented via reduction machines. We show that one machine, that has not received much attention, exhibits a particularly compact Landauer's embedding, requiring only constant space overhead for each step. |
| title | A Reversible Crumbling Abstract Machine for Plotkin's Call-by-Value |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.09179 |