Semantics for a Turing-complete Reversible Programming Language with Inductive Types

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 sai...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-10
Main Authors: Chardonnet, Kostia, Lemonnier, Louis, Valiron, Benoît
Format: Article
Language:English
Subjects:
Pattern matching
Programming languages
Semantics
Turing machines
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422
DOI:10.48550/arxiv.2309.12151