可逆模式匹配的范畴语义
计算机科学中的逻辑
2021-12-30 v3 计算与语言
摘要
本文关注可逆计算的范畴结构。具体而言，我们聚焦于一种基于Theseus的带类型函数式可逆语言。我们讨论join逆rig范畴一般而言为何不能刻画模式匹配——Theseus用以强制可逆性的核心构造。随后我们推导出一种需添加于join逆rig范畴之上的范畴结构以刻画模式匹配。我们展示此种结构如何构成可逆模式匹配的恰当模型。
关键词
引用
@article{arxiv.2109.05837,
title = {Categorical Semantics of Reversible Pattern-Matching},
author = {Kostia Chardonnet and Louis Lemonnier and Benoît Valiron},
journal= {arXiv preprint arXiv:2109.05837},
year = {2021}
}
备注
In Proceedings MFPS 2021, arXiv:2112.13746