Semantics for a Turing-complete Reversible Programming Language with Inductive Types
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916426408787968 |
|---|---|
| author | Chardonnet, Kostia Lemonnier, Louis Valiron, Benoît |
| author_facet | Chardonnet, Kostia Lemonnier, Louis Valiron, Benoît |
| contents | This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching. We then derive a full completeness result, stating that any computable, partial injective function is the image of a term in the language. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2309_12151 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Semantics for a Turing-complete Reversible Programming Language with Inductive Types Chardonnet, Kostia Lemonnier, Louis Valiron, Benoît Logic in Computer Science This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching. We then derive a full completeness result, stating that any computable, partial injective function is the image of a term in the language. |
| title | Semantics for a Turing-complete Reversible Programming Language with Inductive Types |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2309.12151 |