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

lmcs:738 - Logical Methods in Computer Science, August 28, 2013, Volume 9, Issue 3
Indexed Induction and Coinduction, Fibrationally

Authors: Ghani, Neil and Johann, Patricia and Fumex, Clement

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.

Source :
DOI : 10.2168/LMCS-9(3:6)2013
Volume: Volume 9, Issue 3
Published on: August 28, 2013
Submitted on: February 25, 2012
Keywords: Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 92 times.
This article's PDF has been downloaded 23 times.