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.

翻译：本文关注基于Theseus的函数式高阶可逆编程语言的表现力及其指称语义。在该语言中，模式匹配被用于确保函数的可逆性。我们展示了如何将任意可逆图灵机编码至该语言中。随后，我们基于连接逆范畴构建了一个可靠且充分的范畴语义，并附加了捕捉模式匹配的结构。接着，我们推导出一个完全完备性结果，表明任何可计算的、部分单射的函数都是该语言中某个项的解释。