论文标题
树木和代数（CO）数据类型的扩展理论
The Extended Theory of Trees and Algebraic (Co)datatypes
论文作者
论文摘要
自八十年代以来，已经研究了有限和无限树的一阶理论，尤其是逻辑编程社区。在Djelloul，Dao和Frühwirth之后，我们考虑了该理论的扩展，并具有额外的谓词树木的谓词，这对于表达有关（不仅是数据类型，而且还）编码的属性很有用。根据他们的工作，我们提出了一个简化的过程，该过程确定是否可以满足任何给定（不一定关闭的）公式，并返回一个简化的公式，该公式可以阅读所有可能的模型。我们的扩展使该算法适用于代数（CO）数据类型，由于限制性假设，这在其原始工作中是不可能的。我们还提供了简化程序的原型实现，并根据SMT-LIB的实例进行评估。
The first-order theory of finite and infinite trees has been studied since the eighties, especially by the logic programming community. Following Djelloul, Dao and Frühwirth, we consider an extension of this theory with an additional predicate for finiteness of trees, which is useful for expressing properties about (not just datatypes but also) codatatypes. Based on their work, we present a simplification procedure that determines whether any given (not necessarily closed) formula is satisfiable, returning a simplified formula which enables one to read off all possible models. Our extension makes the algorithm usable for algebraic (co)datatypes, which was impossible in their original work due to restrictive assumptions. We also provide a prototype implementation of our simplification procedure and evaluate it on instances from the SMT-LIB.
