Neil Ghani ; Patricia Johann ; Clement Fumex - Indexed Induction and Coinduction, Fibrationally

lmcs:738 - Logical Methods in Computer Science, August 28, 2013, Volume 9, Issue 3 - https://doi.org/10.2168/LMCS-9(3:6)2013
Indexed Induction and Coinduction, FibrationallyArticle

Authors: Neil Ghani ; Patricia Johann ; Clement Fumex

    This paper extends the fibrational approach to induction and coinduction pioneered by Hermida and Jacobs, and developed by the current authors, in two key directions. First, we present a dual to the sound induction rule for inductive types that we developed previously. That is, we present a sound coinduction rule for any data type arising as the carrier of the final coalgebra of a functor, thus relaxing Hermida and Jacobs' restriction to polynomial functors. To achieve this we introduce the notion of a quotient category with equality (QCE) that i) abstracts the standard notion of a fibration of relations constructed from a given fibration; and ii) plays a role in the theory of coinduction dual to that played by a comprehension category with unit (CCU) in the theory of induction. Secondly, we show that inductive and coinductive indexed types also admit sound induction and coinduction rules. Indexed data types often arise as carriers of initial algebras and final coalgebras of functors on slice categories, so we give sufficient conditions under which we can construct, from a CCU (QCE) U:E \rightarrow B, a fibration with base B/I that models indexing by I and is also a CCU (resp., QCE). We finish the paper by considering the more general case of sound induction and coinduction rules for indexed data types when the indexing is itself given by a fibration.


    Volume: Volume 9, Issue 3
    Published on: August 28, 2013
    Imported on: February 25, 2012
    Keywords: Computer Science - Logic in Computer Science

    4 Documents citing this article

    Consultation statistics

    This page has been seen 1126 times.
    This article's PDF has been downloaded 355 times.