论文标题
代数数据类型理论的礼貌
Politeness for the Theory of Algebraic Datatypes
论文作者
论文摘要
代数数据类型，其中包括列表和树，对自动推理和满意度模型理论（SMT）引起了很多兴趣。自最新稳定版本以来，SMT-LIB标准定义了代数数据类型的理论，该理论目前由几个主流SMT求解器支持。在本文中，我们研究了这种特殊的数据类型理论，并证明它是有礼貌的，还表明了如何使用礼貌的组合将其与其他任意脱节理论结合在一起。我们的结果涵盖了归纳和有限的数据类型及其结合。组合方法使用了一种新的，简单和自然的添加性概念，从而使（弱）礼貌地推断出强烈的礼貌。
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.
