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

Indexed induction and coinduction, fibrationally.

Ghani, Neil and Johann, Patricia and Fumex, Clement (2011) Indexed induction and coinduction, fibrationally. [Proceedings Paper]

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

    Abstract

    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 sound coinduction rule for any data type arising as the final coalgebra of a functor, thus relaxing Hermida and Jacobs’ restriction to polynomial data types. For this we introduce the notion of a quotient category with equality (QCE), which both abstracts the standard notion of a fibration of relations constructed from a given fibration, and plays a role in the theory of coinduction dual to that of a comprehension category with unit (CCU) in the theory of induction. Second, we show that indexed inductive and coinductive types also admit sound induction and coinduction rules. Indexed data types often arise as initial algebras and final coalgebras of functors on slice categories, so our key technical results give sufficent conditions under which we can construct, from a CCU (QCE) U : E -> B, a fibration with base B/I that models indexing by I and is also a CCU (QCE).

    Item type: Proceedings Paper
    ID code: 33722
    Keywords: automata theory, reversible processes , duality, computational logic, coalgebraic semantics , coalgebraic logics , categories
    Subjects: UNSPECIFIED
    Department: Faculty of Science > Computer and Information Sciences
    Related URLs:
    Depositing user: Pure Administrator
    Date Deposited: 08 Nov 2011 17:12
    Last modified: 13 Dec 2013 20:05
    URI: http://strathprints.strath.ac.uk/id/eprint/33722

    Actions (login required)

    View Item

    Fulltext Downloads: