Reasoning about codata
Programmers happily use induction to prove properties of recursive programs. To show properties of corecursive programs they employ coinduction, but perhaps less enthusiastically. Coinduction is often considered a rather low-level proof method, in particular, as it departs quite radically from equat...
| Príomhchruthaitheoir: | |
|---|---|
| Formáid: | Journal article |
| Teanga: | English |
| Foilsithe / Cruthaithe: |
2010
|
| _version_ | 1826284925927555072 |
|---|---|
| author | Hinze, R |
| author_facet | Hinze, R |
| author_sort | Hinze, R |
| collection | OXFORD |
| description | Programmers happily use induction to prove properties of recursive programs. To show properties of corecursive programs they employ coinduction, but perhaps less enthusiastically. Coinduction is often considered a rather low-level proof method, in particular, as it departs quite radically from equational reasoning. Corecursive programs are conveniently defined using recursion equations. Suitably restricted, these equations possess unique solutions. Uniqueness gives rise to a simple and attractive proof technique, which essentially brings equational reasoning to the coworld. We illustrate the approach using two major examples: streams and infinite binary trees. Both coinductive types exhibit a rich structure: they are applicative functors or idioms, and they can be seen as memo-tables or tabulations. We show that definitions and calculations benefit immensely from this additional structure. © 2010 Springer-Verlag. |
| first_indexed | 2024-03-07T01:21:10Z |
| format | Journal article |
| id | oxford-uuid:90628842-22b0-4dec-88ed-e58c1c2d4ab8 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T01:21:10Z |
| publishDate | 2010 |
| record_format | dspace |
| spelling | oxford-uuid:90628842-22b0-4dec-88ed-e58c1c2d4ab82022-03-26T23:11:15ZReasoning about codataJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:90628842-22b0-4dec-88ed-e58c1c2d4ab8EnglishSymplectic Elements at Oxford2010Hinze, RProgrammers happily use induction to prove properties of recursive programs. To show properties of corecursive programs they employ coinduction, but perhaps less enthusiastically. Coinduction is often considered a rather low-level proof method, in particular, as it departs quite radically from equational reasoning. Corecursive programs are conveniently defined using recursion equations. Suitably restricted, these equations possess unique solutions. Uniqueness gives rise to a simple and attractive proof technique, which essentially brings equational reasoning to the coworld. We illustrate the approach using two major examples: streams and infinite binary trees. Both coinductive types exhibit a rich structure: they are applicative functors or idioms, and they can be seen as memo-tables or tabulations. We show that definitions and calculations benefit immensely from this additional structure. © 2010 Springer-Verlag. |
| spellingShingle | Hinze, R Reasoning about codata |
| title | Reasoning about codata |
| title_full | Reasoning about codata |
| title_fullStr | Reasoning about codata |
| title_full_unstemmed | Reasoning about codata |
| title_short | Reasoning about codata |
| title_sort | reasoning about codata |
| work_keys_str_mv | AT hinzer reasoningaboutcodata |