Picture of boy being examining by doctor at a tuberculosis sanatorium

Understanding our future through Open Access research about our past...

Strathprints makes available scholarly Open Access content by researchers in the Centre for the Social History of Health & Healthcare (CSHHH), based within the School of Humanities, and considered Scotland's leading centre for the history of health and medicine.

Research at CSHHH explores the modern world since 1800 in locations as diverse as the UK, Asia, Africa, North America, and Europe. Areas of specialism include contraception and sexuality; family health and medical services; occupational health and medicine; disability; the history of psychiatry; conflict and warfare; and, drugs, pharmaceuticals and intoxicants.

Explore the Open Access research of the Centre for the Social History of Health and Healthcare. Or explore all of Strathclyde's Open Access research...

Image: Heart of England NHS Foundation Trust. Wellcome Collection - CC-BY.

Generic fibrational induction

Ghani, Neil and Johann, Patricia and Fumex, Clement (2012) Generic fibrational induction. Logical Methods in Computer Science, 8 (2). ISSN 1860-5974

Full text not available in this repository. Request a copy from the Strathclyde author

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.