GENERIC FIBRATIONAL INDUCTION
GENERIC FIBRATIONAL INDUCTION
复制标题
DOI：
10.2168/lmcs-8(2:12)2012
复制
发表时间：
2012-01-01
影响因子：
0.6
通讯作者：
Fumex, Clement
中科院分区：
文献类型：
--
作者：
Ghani, Neil;Johann, Patricia;Fumex, Clement
本文提供了一个感应规则，该规则可用于证明其类型具有感应性的数据结构的特性，即是函数初始代数的载体。我们的结果本质上是语义上的，受Hermida和Jacobs优雅的多项式数据类型诱导代数表述的启发。我们的贡献是在略有不同的假设下得出一项声音诱导规则，该规则在所有电感类型（无论是多项式）上都是通用的。我们的诱导规则对要证明的属性的种类是一般性的：像Hermida和Jacob一样，我们在一般的纤维化环境中工作，因此可以在电感类型上容纳非常一般的属性概念，而不仅仅是特定句子形式的概念。我们通过减少对迭代的归纳来确定通用归纳规则的健全性。然后，我们展示如何实例化我们的通用归纳规则，以提供玫瑰树，有限的遗传套装和超功能的数据类型的归纳规则。其中的第一个位于Hermida和Jacobs的作品范围之内，因为它不是多项式的，据我们所知，在一般的纤维化框架中，在第二和第三的众所周知，尚无归纳规则。我们对超功能的实例化强调了在一般纤维环境中工作的值，因为该数据类型不能解释为集合。
This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs' elegant algebraic formulation of induction for polynomial data types. Our contribution is to derive, under slightly different assumptions, a sound induction rule that is generic over all inductive types, polynomial or not. Our induction rule is generic over the kinds of properties to be proved as well: like Hermida and Jacobs, we work in a general fibrational setting and so can accommodate very general notions of properties on inductive types rather than just those of a particular syntactic form. We establish the soundness of our generic induction rule by reducing induction to iteration. We then show how our generic induction rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The first of these lies outside the scope of Hermida and Jacobs' work because it is not polynomial, and as far as we are aware, no induction rules have been known to exist for the second and third in a general fibrational framework. Our instantiation for hyperfunctions underscores the value of working in the general fibrational setting since this data type cannot be interpreted as a set.