(Deep) Induction Rules for GADTs
(Deep) Induction Rules for GADTs
复制标题
GADT 的（深度）归纳规则
DOI：
10.1145/3497775.3503680
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Ghiorzi, Enrico
中科院分区：
文献类型：
--
作者：
Johann, Patricia;Ghiorzi, Enrico
深度数据类型是由其他数据类型（可能包括它们自身）构造的数据类型。在这种情况下，它们被称为真正嵌套的。深度归纳是结构归纳的扩展，它遍历深度数据类型中的所有结构，在整个结构中传播其基本数据上的谓词。深度归纳法可以用来证明嵌套类型（包括真正的嵌套类型）不能通过结构归纳法证明的属性。在本文中，我们展示了如何将深度归纳扩展到不是真正嵌套的gadt。这开辟了将自动生成（深度）归纳规则纳入证明助手的道路。我们还表明，本文开发的技术不足以将深度归纳扩展到真正嵌套的gadt，因此需要更复杂的技术来为它们推导深度归纳规则。
Deep data types are those that are constructed from other data types, including, possibly, themselves. In this case, they are said to be truly nested. Deep induction is an extension of structural induction that traversesallof the structure in a deep data type, propagating predicates on its primitive data throughout the entire structure. Deep induction can be used to prove properties of nested types, including truly nested types, that cannot be proved via structural induction. In this paper we show how to extend deep induction to GADTs that are not truly nested GADTs. This opens the way to incorporating automatic generation of (deep) induction rules for them into proof assistants. We also show that the techniques developed in this paper do not suffice for extending deep induction to truly nested GADTs, so more sophisticated techniques are needed to derive deep induction rules for them.