eCommons

 

Practical Coinduction

dc.contributor.authorKozen, Dexter
dc.contributor.authorSilva, Alexandra
dc.date.accessioned2012-11-12T03:29:55Z
dc.date.available2012-11-12T03:29:55Z
dc.date.issued2012-11-11
dc.description.abstractInduction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively-defined datatypes such as finite lists, finite trees, and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.en_US
dc.identifier.urihttps://hdl.handle.net/1813/30510
dc.language.isoen_USen_US
dc.subjectcoinductionen_US
dc.subjectcoalgebraen_US
dc.subjectverificationen_US
dc.titlePractical Coinductionen_US
dc.typetechnical reporten_US

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Structural.pdf
Size:
211.76 KB
Format:
Adobe Portable Document Format
Description:
Main article