Indexed induction and coinduction, fibrationally.

Neil Ghani, Patricia Johann, Clement Fumex

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

9 Citations (Scopus)

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).
LanguageEnglish
Title of host publicationAlgebra and coalgebra in computer science
Subtitle of host publicationProceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011
EditorsAndrea Corradini, Bartek Klin, Corina Cirstea
PublisherSpringer
Pages176-191
Number of pages15
ISBN (Print)9783642229435
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6859
ISSN (Print)0302-9743

Fingerprint

Coinduction
Proof by induction
Fibration
Equality
Quotient
Coalgebra
Functor
Unit
Slice
Indexing
Restriction
Algebra
Polynomial

Keywords

  • automata theory
  • reversible processes
  • duality
  • computational logic
  • coalgebraic semantics
  • coalgebraic logics
  • categories

Cite this

Ghani, N., Johann, P., & Fumex, C. (2011). Indexed induction and coinduction, fibrationally. In A. Corradini, B. Klin, & C. Cirstea (Eds.), Algebra and coalgebra in computer science : Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011 (pp. 176-191). (Lecture Notes in Computer Science; Vol. 6859 ). Springer.
Ghani, Neil ; Johann, Patricia ; Fumex, Clement. / Indexed induction and coinduction, fibrationally. Algebra and coalgebra in computer science : Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. editor / Andrea Corradini ; Bartek Klin ; Corina Cirstea. Springer, 2011. pp. 176-191 (Lecture Notes in Computer Science).
@inproceedings{6ece7ded93a74baca0c1f876b50b0b3a,
title = "Indexed induction and coinduction, fibrationally.",
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).",
keywords = "automata theory, reversible processes , duality, computational logic, coalgebraic semantics , coalgebraic logics , categories",
author = "Neil Ghani and Patricia Johann and Clement Fumex",
year = "2011",
language = "English",
isbn = "9783642229435",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "176--191",
editor = "Andrea Corradini and Bartek Klin and Corina Cirstea",
booktitle = "Algebra and coalgebra in computer science",

}

Ghani, N, Johann, P & Fumex, C 2011, Indexed induction and coinduction, fibrationally. in A Corradini, B Klin & C Cirstea (eds), Algebra and coalgebra in computer science : Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Lecture Notes in Computer Science, vol. 6859 , Springer, pp. 176-191.

Indexed induction and coinduction, fibrationally. / Ghani, Neil; Johann, Patricia; Fumex, Clement.

Algebra and coalgebra in computer science : Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. ed. / Andrea Corradini; Bartek Klin; Corina Cirstea. Springer, 2011. p. 176-191 (Lecture Notes in Computer Science; Vol. 6859 ).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Indexed induction and coinduction, fibrationally.

AU - Ghani, Neil

AU - Johann, Patricia

AU - Fumex, Clement

PY - 2011

Y1 - 2011

N2 - 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).

AB - 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).

KW - automata theory

KW - reversible processes

KW - duality

KW - computational logic

KW - coalgebraic semantics

KW - coalgebraic logics

KW - categories

UR - http://www.springer.com/computer/theoretical+computer+science/book/978-3-642-22943-5

M3 - Conference contribution book

SN - 9783642229435

T3 - Lecture Notes in Computer Science

SP - 176

EP - 191

BT - Algebra and coalgebra in computer science

A2 - Corradini, Andrea

A2 - Klin, Bartek

A2 - Cirstea, Corina

PB - Springer

ER -

Ghani N, Johann P, Fumex C. Indexed induction and coinduction, fibrationally. In Corradini A, Klin B, Cirstea C, editors, Algebra and coalgebra in computer science : Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011. Springer. 2011. p. 176-191. (Lecture Notes in Computer Science).