Fibrational induction rules for initial algebras

Neil Ghani, Patricia Johann, Clement Fumex

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

12 Citations (Scopus)

Abstract

This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs’ elegant algebraic formulation of induction for polynomial data types. Our contribution is to derive, under slightly different assumptions, an induction rule that is generic over all inductive types, polynomial or not. Our induction rule is generic over the kinds of properties to be proved as well: like Hermida and Jacobs, we work in a general fibrational setting and so can accommodate very general notions of properties on inductive types rather than just those of particular syntactic forms. We establish the correctness of our generic induction rule by reducing induction to iteration. We show how our rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The former lies outside the scope of Hermida and Jacobs’ work because it is not polynomial; as far as we are aware, no induction rules have been known to exist for the latter two in a general fibrational framework. Our instantiation for hyperfunctions underscores the value of working in the general fibrational setting since this data type cannot be interpreted as a set.
LanguageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings
EditorsAnuj Dawar , Helmut Veith
PublisherSpringer
Pages336-350
Number of pages15
Volume6247
ISBN (Print)978-3-642-15204-7
DOIs
Publication statusPublished - 2010

Publication series

NameLecture Notes In Computer Science
PublisherSpringer
Volume6247
ISSN (Print)0302-9743

Fingerprint

Algebra
Polynomials
Syntactics
Data structures
Semantics

Keywords

  • fibrational Induction Rules
  • initial algebras
  • computer science

Cite this

Ghani, N., Johann, P., & Fumex, C. (2010). Fibrational induction rules for initial algebras. In A. Dawar , & H. Veith (Eds.), Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings (Vol. 6247, pp. 336-350). (Lecture Notes In Computer Science; Vol. 6247). Springer. https://doi.org/10.1007/978-3-642-15205-4_27
Ghani, Neil ; Johann, Patricia ; Fumex, Clement. / Fibrational induction rules for initial algebras. Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. editor / Anuj Dawar ; Helmut Veith. Vol. 6247 Springer, 2010. pp. 336-350 (Lecture Notes In Computer Science).
@inproceedings{2d25dadb7e3343188fd06c2f62644e08,
title = "Fibrational induction rules for initial algebras",
abstract = "This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs’ elegant algebraic formulation of induction for polynomial data types. Our contribution is to derive, under slightly different assumptions, an induction rule that is generic over all inductive types, polynomial or not. Our induction rule is generic over the kinds of properties to be proved as well: like Hermida and Jacobs, we work in a general fibrational setting and so can accommodate very general notions of properties on inductive types rather than just those of particular syntactic forms. We establish the correctness of our generic induction rule by reducing induction to iteration. We show how our rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The former lies outside the scope of Hermida and Jacobs’ work because it is not polynomial; as far as we are aware, no induction rules have been known to exist for the latter two in a general fibrational framework. Our instantiation for hyperfunctions underscores the value of working in the general fibrational setting since this data type cannot be interpreted as a set.",
keywords = "fibrational Induction Rules, initial algebras, computer science",
author = "Neil Ghani and Patricia Johann and Clement Fumex",
year = "2010",
doi = "10.1007/978-3-642-15205-4_27",
language = "English",
isbn = "978-3-642-15204-7",
volume = "6247",
series = "Lecture Notes In Computer Science",
publisher = "Springer",
pages = "336--350",
editor = "{Dawar }, Anuj and Helmut Veith",
booktitle = "Computer Science Logic",

}

Ghani, N, Johann, P & Fumex, C 2010, Fibrational induction rules for initial algebras. in A Dawar & H Veith (eds), Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. vol. 6247, Lecture Notes In Computer Science, vol. 6247, Springer, pp. 336-350. https://doi.org/10.1007/978-3-642-15205-4_27

Fibrational induction rules for initial algebras. / Ghani, Neil; Johann, Patricia; Fumex, Clement.

Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. ed. / Anuj Dawar ; Helmut Veith. Vol. 6247 Springer, 2010. p. 336-350 (Lecture Notes In Computer Science; Vol. 6247).

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

TY - GEN

T1 - Fibrational induction rules for initial algebras

AU - Ghani, Neil

AU - Johann, Patricia

AU - Fumex, Clement

PY - 2010

Y1 - 2010

N2 - This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs’ elegant algebraic formulation of induction for polynomial data types. Our contribution is to derive, under slightly different assumptions, an induction rule that is generic over all inductive types, polynomial or not. Our induction rule is generic over the kinds of properties to be proved as well: like Hermida and Jacobs, we work in a general fibrational setting and so can accommodate very general notions of properties on inductive types rather than just those of particular syntactic forms. We establish the correctness of our generic induction rule by reducing induction to iteration. We show how our rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The former lies outside the scope of Hermida and Jacobs’ work because it is not polynomial; as far as we are aware, no induction rules have been known to exist for the latter two in a general fibrational framework. Our instantiation for hyperfunctions underscores the value of working in the general fibrational setting since this data type cannot be interpreted as a set.

AB - This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs’ elegant algebraic formulation of induction for polynomial data types. Our contribution is to derive, under slightly different assumptions, an induction rule that is generic over all inductive types, polynomial or not. Our induction rule is generic over the kinds of properties to be proved as well: like Hermida and Jacobs, we work in a general fibrational setting and so can accommodate very general notions of properties on inductive types rather than just those of particular syntactic forms. We establish the correctness of our generic induction rule by reducing induction to iteration. We show how our rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The former lies outside the scope of Hermida and Jacobs’ work because it is not polynomial; as far as we are aware, no induction rules have been known to exist for the latter two in a general fibrational framework. Our instantiation for hyperfunctions underscores the value of working in the general fibrational setting since this data type cannot be interpreted as a set.

KW - fibrational Induction Rules

KW - initial algebras

KW - computer science

UR - http://mfcsl2010.fi.muni.cz/csl

U2 - 10.1007/978-3-642-15205-4_27

DO - 10.1007/978-3-642-15205-4_27

M3 - Conference contribution book

SN - 978-3-642-15204-7

VL - 6247

T3 - Lecture Notes In Computer Science

SP - 336

EP - 350

BT - Computer Science Logic

A2 - Dawar , Anuj

A2 - Veith, Helmut

PB - Springer

ER -

Ghani N, Johann P, Fumex C. Fibrational induction rules for initial algebras. In Dawar A, Veith H, editors, Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Vol. 6247. Springer. 2010. p. 336-350. (Lecture Notes In Computer Science). https://doi.org/10.1007/978-3-642-15205-4_27