Picture of DNA strand

Pioneering chemical biology & medicinal chemistry through Open Access research...

Strathprints makes available scholarly Open Access content by researchers in the Department of Pure & Applied Chemistry, based within the Faculty of Science.

Research here spans a wide range of topics from analytical chemistry to materials science, and from biological chemistry to theoretical chemistry. The specific work in chemical biology and medicinal chemistry, as an example, encompasses pioneering techniques in synthesis, bioinformatics, nucleic acid chemistry, amino acid chemistry, heterocyclic chemistry, biophysical chemistry and NMR spectroscopy.

Explore the Open Access research of the Department of Pure & Applied Chemistry. Or explore all of Strathclyde's Open Access research...

Fibrational induction meets effects

Atkey, Robert and Ghani, Neil and Jacobs, Bart and Johann, Patricia (2012) Fibrational induction meets effects. In: Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, 7213 . Springer, pp. 42-57.

[img]
Preview
Text (Atkey-etal-LNCS2012-Fibrational-induction-meets-effects)
Atkey_etal_LNCS2012_Fibrational_induction_meets_effects.pdf
Accepted Author Manuscript

Download (249kB) | Preview

Abstract

This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type μ(TF) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that μ(TF) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and Støvring.