Practical coinduction

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 du...

Full description

Saved in:
Bibliographic Details
Published in:Mathematical structures in computer science 2017-10, Vol.27 (7), p.1132-1152
Main Authors: KOZEN, DEXTER, SILVA, ALEXANDRA
Format: Article
Language:English
Subjects:
Computer science
Functions (mathematics)
Lists
Number theory
Proving
Trees
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0960-1295
1469-8072
DOI:10.1017/S0960129515000493