一句话：用带 join 的逆范畴为结构化可逆流程图语言建立范畴语义，并证明其计算可靠、充分且在一定条件下等式完全抽象。
结构化可逆流程图语言是一类可用有限控制流结构进行简单图示表示的命令式可逆编程语言，涵盖无递归的 Janus 以及较新的 R-CORE、R-WHILE 等，但此前缺乏统一的范畴论语义基础。本文基于带 join 的逆范畴（inverse categories with joins）构造此类语言的范畴基础：将限制范畴的外延性（extensivity）概念推广为逆范畴可容纳的形式，并利用由此得到的决策（decisions）给出谓词与断言的可逆表示。由此得到结构化可逆流程图的范畴语义，并证明该语义相对于操作语义是计算可靠且充分的（computationally sound and adequate），在特定条件下还满足等式完全抽象（equational fully abstract）。
Structured reversible flowchart languages is a class of imperative reversible programming languages allowing for a simple diagrammatic representation of control flow built from a limited set of control flow structures. This class includes the reversible programming language Janus (without recursion), as well as more recently developed reversible programming languages such as R-CORE and R-WHILE. In the present paper, we develop a categorical foundation for this class of languages based on inverse categories with joins. We generalize the notion of extensivity of restriction categories to one that may be accommodated by inverse categories, and use the resulting decisions to give a reversible representation of predicates and assertions. This leads to a categorical semantics for structured reversible flowcharts, which we show to be computationally sound and adequate, as well as equationally fully abstract with respect to the operational semantics under certain conditions.
@article{paperbot379,
title = {A categorical foundation for structured reversible flowchart languages: Soundness and adequacy},
author = {Robert Glück and Robin Kaarsgaard},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:16)2018}
}