Generic fibrational induction

Neil Ghani, Patricia Johann, Clement Fumex

Research output: Contribution to journalArticle

7 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, a sound 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 a particular syntactic form. We establish the soundness of our generic induction rule by reducing induction to iteration. We then show how our generic induction rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The first of these lies outside the scope of Hermida and Jacobs' work because it is not polynomial, and as far as we are aware, no induction rules have been known to exist for the second and third 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
Article number12
JournalLogical Methods in Computer Science
Volume8
Issue number2
DOIs
Publication statusPublished - 19 Jun 2012

Fingerprint

Rule Induction
Proof by induction
Polynomials
Hyperfunctions
Syntactics
Algebra
Data structures
Polynomial
Semantics
Acoustic waves
Soundness
Functor
Data Structures
Iteration
Formulation

Keywords

  • data structures
  • algebras
  • generic induction

Cite this

Ghani, Neil ; Johann, Patricia ; Fumex, Clement. / Generic fibrational induction. In: Logical Methods in Computer Science. 2012 ; Vol. 8, No. 2.
@article{eb783370d60846fdbeb84d03f750c96e,
title = "Generic fibrational induction",
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, a sound 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 a particular syntactic form. We establish the soundness of our generic induction rule by reducing induction to iteration. We then show how our generic induction rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The first of these lies outside the scope of Hermida and Jacobs' work because it is not polynomial, and as far as we are aware, no induction rules have been known to exist for the second and third 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 = "data structures, algebras, generic induction",
author = "Neil Ghani and Patricia Johann and Clement Fumex",
year = "2012",
month = "6",
day = "19",
doi = "10.2168/LMCS-8(2:12)2012",
language = "English",
volume = "8",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
number = "2",

}

Generic fibrational induction. / Ghani, Neil; Johann, Patricia; Fumex, Clement.

In: Logical Methods in Computer Science, Vol. 8, No. 2, 12, 19.06.2012.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Generic fibrational induction

AU - Ghani, Neil

AU - Johann, Patricia

AU - Fumex, Clement

PY - 2012/6/19

Y1 - 2012/6/19

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, a sound 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 a particular syntactic form. We establish the soundness of our generic induction rule by reducing induction to iteration. We then show how our generic induction rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The first of these lies outside the scope of Hermida and Jacobs' work because it is not polynomial, and as far as we are aware, no induction rules have been known to exist for the second and third 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, a sound 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 a particular syntactic form. We establish the soundness of our generic induction rule by reducing induction to iteration. We then show how our generic induction rule can be instantiated to give induction rules for the data types of rose trees, finite hereditary sets, and hyperfunctions. The first of these lies outside the scope of Hermida and Jacobs' work because it is not polynomial, and as far as we are aware, no induction rules have been known to exist for the second and third 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 - data structures

KW - algebras

KW - generic induction

U2 - 10.2168/LMCS-8(2:12)2012

DO - 10.2168/LMCS-8(2:12)2012

M3 - Article

VL - 8

JO - Logical Methods in Computer Science

T2 - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 12

ER -