Sciweavers

Share
CSL
2010
Springer

Fibrational Induction Rules for Initial Algebras

9 years 3 months ago
Fibrational Induction Rules for Initial Algebras
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, an 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 particular syntactic forms. We establish the correctness of our generic induction rule by reducing induction to iteration. We show how our rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The former li...
Neil Ghani, Patricia Johann, Clément Fumex
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CSL
Authors Neil Ghani, Patricia Johann, Clément Fumex
Comments (0)
books