article · 2012

Practical Coinduction

Dexter Kozen Alex, Ra Silva

Cited by 0Abstract and details only

Abstract

Induction 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. 1

Cite this paper

APA 7

Alex, D. K., & Silva, R. (2012). Practical Coinduction.

MLA 9

Alex, Dexter Kozen, and Ra Silva. “Practical Coinduction.” 2012.

Chicago

Alex, Dexter Kozen, and Ra Silva. 2012. “Practical Coinduction.”

Harvard

Alex, D.K. and Silva, R. (2012) ‘Practical Coinduction’.

BibTeX

@article{alex2012practical,
  title = {{Practical Coinduction}},
  author = {Alex, Dexter Kozen and Silva, Ra},
  year = {2012}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.