代数数据类型理论的礼貌性
计算机科学中的逻辑
2020-04-15 v3
摘要
代数数据类型，其中包括列表和树，在自动化推理和可满足性模理论（SMT）中引起了大量关注。自其最新稳定版本起，SMT-LIB 标准定义了代数数据类型理论，目前若干主流 SMT 求解器支持该理论。在本文中，我们研究这一特定的数据类型理论，并证明其是强礼貌的，同时展示了如何借助礼貌组合将其与其他任意不相交理论相组合。我们的结果涵盖归纳与有限数据类型，以及它们的并集。该组合方法使用了一种新颖、简单且自然的加性概念，能够从（弱）礼貌性推导出强礼貌性。
引用
@article{arxiv.2004.04854,
title = {Politeness for the Theory of Algebraic Datatypes},
author = {Ying Sheng and Yoni Zohar and Christophe Ringeissen and Jane Lange and Pascal Fontaine and Clark Barrett},
journal= {arXiv preprint arXiv:2004.04854},
year = {2020}
}