A Fibrational Induction Rule for Inductive Types

Add to your list(s) Download to your calendar using vCal

• Patricia Johann, University of Strathclyde
• Tuesday 04 May 2010, 13:00-14:00
• Venue to be confirmed.

If you have a question about this talk, please contact Paul Levy.

We develop a generic induction rule that can be used to prove properties of inductive data types. 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 over the data types to which the properties refer. 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. The correctness of our generic induction rule is proved by reducing induction to iteration. We show how our rule can be instantiated to give induction rules for non-polynomial data types such as rose trees, finite hereditary sets, and hyperfunctions. Our instantiation for hyperfunctions underscores the value of working in the general fibrational setting since this data type cannot be interpreted as a set.

This is joint work with Neil Ghani and Clement Fumex.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• Venue to be confirmed
• computer sience

Note that ex-directory lists are not shown.