Deep Induction: Induction Rules for (Truly) Nested Types
Deep Induction: Induction Rules for (Truly) Nested Types
复制标题
DOI：
10.1007/978-3-030-45231-5_18
复制
发表时间：
2020-04-17
期刊：
影响因子：
--
通讯作者：
Polonsky A
中科院分区：
文献类型：
--
作者：
Johann P;Polonsky A
本文介绍了深层诱导，并表明它是最适合嵌套类型和其他数据类型的概念，或（其他）类型的类型。标准感应规则仅在数据的顶级结构上诱导，使顶级结构内部的任何数据未经触及。相比之下，所有存在的结构化数据对深度诱导规则诱导。我们给出了语法，生成了强大的嵌套类型类型（以及ADT），并使用其最近定义的语义作为本地可访问类别的可访问函数的固定点来为它们开发深层诱导的基本理论。然后，我们使用理论来得出一些常见的ADT和嵌套类型的深度归纳规则，并展示这些规则如何专门为这些类型提供标准的结构归纳规则。我们还展示了如何专门解决灌木丛和其他真正嵌套类型的原则性和实际有用的结构诱导规则的长期存在的问题。总体而言，深度归纳为制定适合于编程语言和证明助手提供的丰富结构数据类型的归纳原则开辟了道路。我们开发的AGDA实施和示例，包括两个扩展案例研究。
This paper introduces deep induction, and shows that it is the notion of induction most appropriate to nested types and other data types defined over, or mutually recursively with, (other) such types. Standard induction rules induct over only the top-level structure of data, leaving any data internal to the top-level structure untouched. By contrast, deep induction rules induct over all of the structured data present. We give a grammar generating a robust class of nested types (and thus ADTs), and develop a fundamental theory of deep induction for them using their recently defined semantics as fixed points of accessible functors on locally presentable categories. We then use our theory to derive deep induction rules for some common ADTs and nested types, and show how these rules specialize to give the standard structural induction rules for these types. We also show how deep induction specializes to solve the long-standing problem of deriving principled and practically useful structural induction rules for bushes and other truly nested types. Overall, deep induction opens the way to making induction principles appropriate to richly structured data types available in programming languages and proof assistants. Agda implementations of our development and examples, including two extended case studies, are available.
登录
查看更多内容
影响因子：
1.1
作者：
Abbott, M;Altenkirch, T;Ghani, N
通讯作者：
Ghani, N
影响因子：
0.6
作者：
Ghani, Neil;Johann, Patricia;Fumex, Clement
通讯作者：
Fumex, Clement
影响因子：
1.1
作者：
Matthes, Ralph
通讯作者：
Matthes, Ralph
影响因子：
1.1
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
通讯作者：
Morris, Peter
影响因子：
--
作者：
Abel, Andreas
通讯作者：
Abel, Andreas