Abstract
| Original language | English |
|---|---|
| Title of host publication | Algebra and coalgebra in computer science |
| Subtitle of host publication | Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30 - September 2, 2011 |
| Editors | Andrea Corradini, Bartek Klin, Corina Cirstea |
| Publisher | Springer |
| Pages | 176-191 |
| Number of pages | 15 |
| ISBN (Print) | 9783642229435 |
| Publication status | Published - 2011 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 6859 |
| ISSN (Print) | 0302-9743 |
Fingerprint
Keywords
- automata theory
- reversible processes
- duality
- computational logic
- coalgebraic semantics
- coalgebraic logics
- categories
Cite this
}
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 proceeding › Conference 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 -