Strathprints logo
Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

Fibrational induction rules for initial algebras

Ghani, Neil and Johann, Patricia and Fumex, Clement (2010) Fibrational induction rules for initial algebras. In: Computer Science Logic. Lecture Notes In Computer Science, 6247 . Springer, pp. 336-350. ISBN 978-3-642-15204-7

[img]
Preview
PDF - Draft Version
Download (286Kb) | Preview

    Abstract

    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 lies outside the scope of Hermida and Jacobs’ work because it is not polynomial; as far as we are aware, no induction rules have been known to exist for the latter two 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.

    Item type: Book Section
    ID code: 33723
    Keywords: fibrational Induction Rules, initial algebras, computer science , Electronic computers. Computer science, Computer Science (miscellaneous)
    Subjects: Science > Mathematics > Electronic computers. Computer science
    Department: Faculty of Science > Computer and Information Sciences
    Related URLs:
    Depositing user: Pure Administrator
    Date Deposited: 10 Nov 2011 12:37
    Last modified: 06 Sep 2014 18:49
    URI: http://strathprints.strath.ac.uk/id/eprint/33723

    Actions (login required)

    View Item

    Fulltext Downloads: